From b82b416e0e19ec9658061ebae011b903b035a012 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 18:39:27 -0700 Subject: [PATCH] IBA2-012: count-weighted finite-radius multi-soft transfer and no-loss inference obstruction Author OpenAI / GPT-6 Astra Pro, iba2-count-weight-transfer-r6-20261006, Dylan Roy delegated work. Five additive files only, under main259 pickup6007422896. Same-law Holder transfer preserves r^3 with an explicit fixed-moment soft-exponent loss; positive-count intensity and factorial denominator limits retained. Abstract spike is not a Gaussian counterexample. Twelve exact finite test methods passed in both modes; source review and hosted evidence remain distinct. Scientific effect NONE; no theorem/status/formal-register promotion. --- .../iba2_012_count_transfer_20261006/PROOF.md | 193 ++++++++++++++++++ .../README.md | 37 ++++ .../SOURCES.json | 78 +++++++ .../test_transfer.py | 118 +++++++++++ .../transfer_check.py | 149 ++++++++++++++ 5 files changed, 575 insertions(+) create mode 100644 reviews/iba2_012_count_transfer_20261006/PROOF.md create mode 100644 reviews/iba2_012_count_transfer_20261006/README.md create mode 100644 reviews/iba2_012_count_transfer_20261006/SOURCES.json create mode 100644 reviews/iba2_012_count_transfer_20261006/test_transfer.py create mode 100644 reviews/iba2_012_count_transfer_20261006/transfer_check.py diff --git a/reviews/iba2_012_count_transfer_20261006/PROOF.md b/reviews/iba2_012_count_transfer_20261006/PROOF.md new file mode 100644 index 000000000..752bc9da5 --- /dev/null +++ b/reviews/iba2_012_count_transfer_20261006/PROOF.md @@ -0,0 +1,193 @@ +# IBA2-012: count-weighted transfer for finite-radius multi-soft sectors + +Object: IBA2-012-COUNT-TRANSFER-20261006-v1. +Author: OpenAI / GPT-6 Astra Pro, session `iba2-count-weight-transfer-r6-20261006`, Dylan Roy — delegated AI work. +Disposition: AUTHOR-SIDE MATHEMATICAL CANDIDATE; nonauthor source review required. +Scientific effect NONE. No prior proof, review, status, catalog, formal manifest or prize changes. +The author wrote the FR precursor and is exposed to prior reviews; organizational-independence credit0. + +## 1. The precise gap addressed + +The landed finite-radius packet FR, Math-#306, §5 explicitly says that inserting a factor N_R^j needs a separate count-moment argument. Its §8 proves an unequal-soft-threshold occurrence estimate, not a count-weighted estimate. This note supplies that missing transfer, conditional on the sharp C6 fixed-order count moments and the matching first moment. It does not re-prove P §7, FR's eigenvalue integration, or C6's witness/collision proof. + +The result preserves the rare r^3 scale, proves negligibility for every fixed polynomial count weight on these sectors, and explains why loss-free preservation of the full soft exponent does NOT follow from these inputs. The last assertion is an abstract countermodel to an inference, not a Gaussian-field counterexample. + +## 2. Exact source bindings and interface alignment + +Repository `d6g8k5htny-coder/Math-`; source cut `2f8b6f372be383d752e9dd30d38234faa977243c`. + +| Tag | Path | Full Git blob | Consumed interface | +|---|---|---|---| +| FR | `reviews/iba2_012_finite_radius_20261005/PROOF.md` | `5ed684c9bb446efc9bef5f3980717c6dc039abfd` | §§3,5,8: finite-r event bound with every fixed derivative-norm power and mixed thresholds | +| C6 | `frontiers/c6_palm_route_20260929/PROOF.md` | `89eb8adf08fe7afc2cab9662d3a9875c05ae5cc5` | §1.1 same tilted law and all-index torus window count; §1.2 Theorem Q; Corollary Theta only for optional normalized consequences | +| DL | `frontiers/d5_dimension_lift_20260929/PROOF.md` | `9d82c707fdb17d3072a8930f26dabedf59e456fc` | §1.2 Theorem G_d (1.7), summed over d+1 indices | +| DE | `reviews/d5_dimension_lift_erratum_20261005/ERRATUM.md` | `23df87bbe4ffd3b2d786cd695fb9f5448cfa1d05` | Original DL and C6 are read with the additive Lipschitz-factor/citation correction; their consumed final estimates are unchanged | +| P | `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` | `dfed3b8d318a3ab1950957f393307733a4bef3f2` | Same field/pins/full normalizer; §5 (5.5) only for the optional unnormalized numerator statement | +| SC | `frontiers/spectral_cluster_closure_20260929/PROOF.md` | `16c56821b52fd76b0be791622b9c3809eafde75a` | FR's deterministic-exclusion ancestry; no new quantitative premise or re-review here | + +FR's scoped nonauthor review is Math-#306/6005379068; its landing is f4c33a98a982d50aa490e49ce9327c755682527c. C6 and DL retain the source-exposed review/ancestor limitations recorded in their own introductions and §2. This note neither creates another vote for those ancestors nor erases inherited obligations. Every conclusion here is conditional on the quoted interfaces at these exact bytes. A defect in an imported estimate blocks the corresponding inference. + +Fix d>=3, L>0, a compact birth interval, a gap-mark interval [k_-,k_+] with k_->0, all orthonormal frames, and a fixed observation radius R>=1. Use the variance-one normalized periodized Gaussian field, pins M=-(r/2)u and S=(r/2)u, heights b and b-kr^3, and zero endpoint gradients. In all sources, + + Q_r = original Gaussian pin law, + W_r = F_d(H_M) F_(d-1)(H_S), + Z_r = E_Q[W_r], P_r = Q_r^W = (W_r/Z_r) Q_r. + +There is ONE tilted law and ONE full normalizer, not a separately normalized soft-sector law. Restrict r to the minimum of the finitely many source cutoffs needed for a chosen moment order. Constants may depend on that order, d,L,R and the fixed mark compacts. + +Let N be C6's all-index count on the whole torus, pins removed, with heights strictly in (b-kr^3,b). Let N_R be FR's count in the physical ball of radius Rr. Thus 0<=N_R<=N pathwise. Write K>=1 for FR's fixed multiple of 1+||f||_(C^4). C6 also uses the letter K for a C^6 control; that variable is NOT identified with ours and is not inserted into its moment theorem. + +Put m=d-1. For 1<=q<=m-1, choose deterministic 0<=eta_2<=...<=eta_(q+1)<=1/2, and take r<=1/2. Let h_j be the ordered eigenvalues of the negative midpoint transverse Hessian, exactly as in FR. They need not be positive at finite r. Define + + E_r = {N_R>0, h_j<=eta_j for 2<=j<=q+1}, + Pi_r = product_(j=2)^(q+1) (eta_j+r)^(j+2), + beta_q = sum_(j=2)^(q+1)(j+2) = q(q+7)/2. + +Here 00 is essential: nothing here controls {N>0,h_j<=eta_j} when no local witness occurs. + +FR supplies, for every fixed t>=0, + + E_(P_r)[K^t ; E_r] <= A_t r^3 Pi_r. (F) + +DL and C6 supply + + E_(P_r)[N] <= B_1 r^3, + E_(P_r)[(N)_j] <= B_j r^3 for every fixed integer j>=2. (C) + +## 3. The count-weighted transfer theorem + +**Theorem CT.** Fix a>=0, s>0, and an integer p>s. Put theta=1-s/p in (0,1). Under the exact interfaces above, + + E_(P_r)[K^a N^s ; E_r] <= C_(a,s,p) r^3 Pi_r^theta. (CT) + +The same upper bound holds with N_R^s or (N_R)_j, s=j, in place of N^s. In particular, for every fixed delta in (0,1), choosing one fixed integer p>=s/delta and p>s gives + + E_(P_r)[K^a N^s ; E_r] <= C_(a,s,delta) r^3 Pi_r^(1-delta). (CT-delta) + +No constant is asserted uniform in p, delta->0, R->infinity, k->0, L or d. + +*Proof.* The Stirling identity for nonnegative integers is + + N^p = sum_(j=1)^p S(p,j) (N)_j, + +with nonnegative Stirling numbers S(p,j). It has no constant term. Applying (C), including the first-moment term j=1, gives + + E[N^p] <= M_p r^3, M_p=sum_(j=1)^p S(p,j) B_j. (1) + +This also shows N=1-delta and Pi_r<=1 imply CT-delta. This chooses p ONCE for a specified delta; p is not a function of r. QED. + +**Unnormalized numerator.** If needed, P(5.5)'s upper bound Z_r<=z^*r^2 gives + + E_Q[W_r K^a N^s ; E_r] <= C r^5 Pi_r^theta. + +This multiplies by the one existing Z_r. It does not divide by Z_r again or change the probability law. + +## 4. Scaling and a useful positive-count measure consequence + +For equal eta_j=r^alpha, alpha>0, + + CT = O(r^[3+theta beta_q min(alpha,1)]). (2) + +For eta_j=r^alpha_j with alpha_2>=...>=alpha_(q+1)>0, + + CT = O(r^[3+theta sum_(j=2)^(q+1)(j+2)min(alpha_j,1)]). (3) + +The ordering is reversed for alpha because 0=q+2. With q=2, eta_2=r^(1/2), eta_3=r^(1/4), s=1,p=4, the exponent is 87/16. These are upper bounds with fixed-order constants, not sharp asymptotics or lower bounds. + +For any deterministic shrinking thresholds eta_j(r)->0, Pi_r->0. Therefore every fixed polynomial-count/norm weighted contribution in CT is o(r^3). It is enough to let one factor of Pi_r tend to zero; requiring all thresholds to shrink is a simple sufficient condition. + +Here is a measure statement that does not presume convergence of the cluster law. Let Y=N or Y=N_R and define positive-count intensities + + mu_r(n) = r^-3 P_r(Y=n), n>=1. + +Delete the exceptional outcomes by Y'=Y 1_(E_r^c), and let mu'_r be its positive-count intensity. Since Y>=1 on E_r, + + sum_(n>=1) n^s |mu_r(n)-mu'_r(n)| + = r^-3 E[Y^s ; E_r] <= C Pi_r^theta. (4) + +The analogous nonnegative measure with K^a inserted obeys the same identity and CT. For s=0, use FR directly and obtain C Pi_r without a loss. The norm in (4) is on POSITIVE counts: including the transferred mass at zero would add another term. This does not assert that either family mu_r converges, give its coefficients, or control locations/elder labels. It shows that deleting THESE sectors cannot change any existing weighted-l1 limit or subsequential limit in a fixed polynomial norm. + +## 5. Normalized consequences and a denominator boundary + +C6 Corollary Theta and DL give + + P_r(N>=1) >= P_r(N>=2) >= c r^3, + E[N] >= 2P_r(N>=2) >= c r^3, + E[(N)_2] >= c r^3. + +Only in this paragraph do we consume those lower statements. Divide CT by these explicit denominators. It follows that the E_r contribution tends to zero in polynomial moments under global nonempty conditioning, and its probability tends to zero under the first and second factorial size-biased laws. For example, for j=1,2 and p>j, + + E[(N)_j 1_E]/E[(N)_j] <= C Pi_r^(1-j/p). (5) + +Additional K^a or polynomial weights are treated by CT at the corresponding larger s. + +For factorial order j>=3, (5) is CONDITIONAL on a separately supplied lower denominator c_j r^3. C6 supplies only upper bounds at those orders. The distribution P(N=2)=r^3, P(N=0)=1-r^3 has all fixed upper moment bounds and E[(N)_2]=2r^3, but E[(N)_3]=0. No third factorial Palm law exists for that example. Likewise no lower bound on P(N_R>0) is imported for arbitrary R; global nonempty conditioning is not silently changed to local nonempty conditioning. + +## 6. Why the loss-free soft exponent is not implied + +**Proposition NL (abstract obstruction).** The interfaces F and C, even with K=1 and every finite count moment, do not imply E[N^s;E_r]=O(r^3 Pi_r) for any fixed s>0. + +It suffices to give a family along r_n=2^-n, n>=1, in the q=1 case beta=4. On a three-atom probability space, set + + P(N=0)=1-r_n^3-r_n^7, + P(N=2)=r_n^3, + P(N=n+3)=r_n^7. + +Let E_n be the last atom, take K=1, N_R=N, and set h_2=r_n there and h_2=2 on the other atoms. For any threshold 0<=eta<=1/2, the event {N_R>0,h_2<=eta} is empty if eta=1, + + E[N^p] = r_n^3 [2^p+(n+3)^p 2^-4n] <= C_p r_n^3, + +because a polynomial times a decreasing exponential is bounded. Hence all fixed factorial upper bounds hold. Also P(N>=2)>=r_n^3 and E[(N)_2]>=2r_n^3, so the first/second lower-scale consequences hold as well. + +Yet at eta=r_n, Pi_r=(2r_n)^4, + + E[N^s;E_n]/(r_n^3 Pi_r) = (n+3)^s/16 -> infinity. (6) + +Thus no loss-free estimate follows from these abstract premises. No Gaussian covariance, Hessian geometry, analytic sample path, or actual field realization is asserted for this countermodel. It blocks an inference from the quoted estimates, not a possible sharper theorem for the real Gaussian model. + +In particular, taking p->infinity in CT is invalid without control of M_p and A_(a/theta). A sufficient additional lemma for loss-free transfer would be a uniform conditional sector bound E[K^a N^s | E_r]<=C whenever P(E_r)>0, combined with F at t=0; or a direct source-bound spectral/witness estimate with the count insertion. Neither is supplied here. The smallest remaining question for that stronger goal is the joint count/soft-sector estimate, not another proof of the cap layer or of the unweighted event. + +## 7. Sector ledger and scientific boundaries + +| Sector/interface | Disposition at the exact bindings of §2 | +|---|---| +| Finite-radius occurrence with extra soft eigenvalues, including unequal scales and norm tails | Covered by FR §§3,8; inherited scoped result, not this author's new PASS | +| Fixed polynomial/factorial count insertion on the SAME event/law | New CT proof candidate, conditional on FR + C6 + DL/DE; source-bound nonauthor review required | +| Same full soft power with no count/exponent loss | AMEND_EXTRAPOLATION: does not follow from these inputs, by the explicit NL family | +| First/second factorial normalization and global nonempty conditioning | CT plus explicit r^3 denominator lower bounds only | +| Higher factorial or arbitrary local-nonempty normalization | Lower denominator missing; not asserted | +| Small k, escaping marks, R->infinity, hard-Hessian higher-jet degeneracy, remote-only soft events, full cluster-law convergence, elder matching | Not controlled here; general IBA2-012 and IBA2-009 remain OPEN | + +There is no spatial radial integration in CT: r is the fixed pin separation and the height window is kr^3. In particular an o(r^3) probability/count statement on compact marks is not an all-mark lifetime-density expansion. The codimension/determinant/Vandermonde powers remain those already derived in FR; Holder transfers their integrated bound and is not a new spectral power count. + +## 8. Reproduction and review + +Run `python -B -S test_transfer.py`, its `-O` equivalent, and `python -B -S transfer_check.py`. The tests check finite exact Holder inequalities, the Stirling/factorial identity, the exponent ledger, positive-count histogram deletion, the rare-spike formula and the missing higher denominator. Five named mutants exercise incorrect exponents, omitted first moments, a loss-free inference and a fabricated third-order lower bound. Unknown labels exit2. No unhandled crash is an intended mathematical rejection. + +These finite tests do NOT prove the arbitrary-law Holder theorem, the asymptotic countermodel, FR, C6, or Gaussian-field facts; the ordinary proofs above provide the new argument. No local Lean execution or new formal target is claimed. Existing repository checks do not automatically run these standalone tests. + +The smallest useful nonauthor review is §2 law/count alignment; the two factors and r^3 cancellation in CT; weighted-intensity and denominator conventions; and NL's simultaneous all-fixed-moment/threshold premises. No repeat review of unchanged ancestor proofs is requested. Consensus Primary returned quota exhaustion; no external paper was retrieved or used as a new premise. No claim of literature novelty is made. diff --git a/reviews/iba2_012_count_transfer_20261006/README.md b/reviews/iba2_012_count_transfer_20261006/README.md new file mode 100644 index 000000000..7a58357c8 --- /dev/null +++ b/reviews/iba2_012_count_transfer_20261006/README.md @@ -0,0 +1,37 @@ +# Finite-radius count-weighted multi-soft transfer + +Author-side mathematical candidate for Dylan Roy's IBA2-012 work. The author +OpenAI / GPT-6 Astra Pro (`iba2-count-weight-transfer-r6-20261006`) wrote the +FR precursor. Scientific effect NONE; organizational independence credit0. + +`PROOF.md` fills the count-insertion gap explicitly left by the landed #306 +finite-radius event estimate. For the same tilted pin law, compact positive +marks and fixed d,L,R, it derives + + E[K^a N^s; E_r] <= C r^3 Pi_r^(1-s/p), p>s fixed integer, + Pi_r = product (eta_j+r)^(j+2). + +Every fixed polynomial-count contribution is o(r^3) on the specified shrinking +sectors. Positive-count intensities inherit weighted-l1 deletion control. +An explicit abstract rare-spike family proves that no-loss preservation of +Pi_r does not follow merely from all fixed moment bounds. This is NOT a +Gaussian counterexample, full cluster-law rate, all-mark theorem, or scientific +acceptance. First/second factorial normalization uses explicit lower bounds; +third and higher orders require a separate denominator lemma. + +Sources are pinned at Math- commit +`2f8b6f372be383d752e9dd30d38234faa977243c`; read original DL/C6 with the additive +erratum. Source and payload hashes are in `SOURCES.json`. + +``` +python -B -S test_transfer.py +python -B -O -S test_transfer.py +python -B -S transfer_check.py +python -B -O -S transfer_check.py +python -B -S transfer_check.py --mutant M1 # exit1, named failed check; M1-M5 +``` + +Twelve tests and the deterministic checker are exact finite controls, not a +continuum or Lean proof. No source files, workflow, formal manifest, status or +review record outside this additive packet are modified. Nonauthor source +review and all applicable integration checks remain separate obligations. diff --git a/reviews/iba2_012_count_transfer_20261006/SOURCES.json b/reviews/iba2_012_count_transfer_20261006/SOURCES.json new file mode 100644 index 000000000..a9f8f29cc --- /dev/null +++ b/reviews/iba2_012_count_transfer_20261006/SOURCES.json @@ -0,0 +1,78 @@ +{ + "object": "IBA2-012-COUNT-TRANSFER-20261006-v1", + "scientific_effect": "NONE", + "disposition": "author-side candidate; nonauthor review required", + "source_commit": "2f8b6f372be383d752e9dd30d38234faa977243c", + "repository": "d6g8k5htny-coder/Math-", + "sources": [ + { + "path": "reviews/iba2_012_finite_radius_20261005/PROOF.md", + "bytes": 17362, + "git_blob": "5ed684c9bb446efc9bef5f3980717c6dc039abfd", + "sha256": "cad7fa81a70dc218286d7ec62f7a86daf337677d65398ff906c455157067f93f", + "consumed": "FR \u00a7\u00a73,5,8" + }, + { + "path": "frontiers/c6_palm_route_20260929/PROOF.md", + "bytes": 53364, + "git_blob": "89eb8adf08fe7afc2cab9662d3a9875c05ae5cc5", + "sha256": "aa37f16040ab9e05bb2e4e3f1d678367497e8dc2cf43eef197a4d6592c2f129b", + "consumed": "C6 \u00a71.1-1.3, Theorem Q; optional lower corollaries" + }, + { + "path": "frontiers/d5_dimension_lift_20260929/PROOF.md", + "bytes": 53727, + "git_blob": "9d82c707fdb17d3072a8930f26dabedf59e456fc", + "sha256": "6fb94b247e8e45bca9dc02f46670ac6029fb54e0ef906001efe48fe908549b80", + "consumed": "DL \u00a71.2 G_d (1.7), summed over indices" + }, + { + "path": "reviews/d5_dimension_lift_erratum_20261005/ERRATUM.md", + "bytes": 6160, + "git_blob": "23df87bbe4ffd3b2d786cd695fb9f5448cfa1d05", + "sha256": "2d239478285a9741ed68334f52d16405ee440aa8ff445ddbb4947b7f60066238", + "consumed": "DL/C6 additive correction, entire file" + }, + { + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "bytes": 40261, + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "consumed": "P law/normalizer \u00a75 (5.5), optional numerator" + }, + { + "path": "frontiers/spectral_cluster_closure_20260929/PROOF.md", + "bytes": 25006, + "git_blob": "16c56821b52fd76b0be791622b9c3809eafde75a", + "sha256": "e971b2cbe50a8a06b47c1219191201e0d1037c9adac23e5e3b7d2051bb70c2eb", + "consumed": "SC ancestor of FR; no new quantitative premise" + } + ], + "payloads": [ + { + "path": "PROOF.md", + "bytes": 14855, + "git_blob": "752bc9da5e49af3d0724d80c91cffc0dde35a2d8", + "sha256": "63eb5fd131d440d918c86269b1b613b3d62b897b1349135405ada04d2a611061" + }, + { + "path": "README.md", + "bytes": 1784, + "git_blob": "7a58357c825d9737b9fa5251b5b55c31cd467fa9", + "sha256": "4b6fd24e670d44d63bff2c2b70e352aa1aad0781337414136807b612ad3a1069" + }, + { + "path": "test_transfer.py", + "bytes": 5020, + "git_blob": "175388b9047abb4e88d98c855b9ffe38cb45aad7", + "sha256": "d3bb0a8ae352707b809ffa79aee805ee7945fb5db4e62da396631336104a5382" + }, + { + "path": "transfer_check.py", + "bytes": 5941, + "git_blob": "b36abff316da46eaa08a20dd5641e9d6d18e3d06", + "sha256": "e73868774cbf7a865621330e27fdda3987986508a20e006f2f4fe274bc9b0952" + } + ], + "self_hash": "This manifest is bound by the external Git blob/delivery manifest, not by a circular self-hash." +} diff --git a/reviews/iba2_012_count_transfer_20261006/test_transfer.py b/reviews/iba2_012_count_transfer_20261006/test_transfer.py new file mode 100644 index 000000000..175388b90 --- /dev/null +++ b/reviews/iba2_012_count_transfer_20261006/test_transfer.py @@ -0,0 +1,118 @@ +"""Exact finite controls for PROOF.md; not a Gaussian-field or Lean replay.""" +from __future__ import annotations +import importlib.util +import json +import subprocess +import sys +import unittest +from fractions import Fraction as F +from pathlib import Path + +ROOT = Path(__file__).resolve().parent + +class TransferTests(unittest.TestCase): + def load(self): + path = ROOT / 'transfer_check.py' + self.assertTrue(path.is_file(), 'implementation file is absent') + spec = importlib.util.spec_from_file_location('transfer_check', path) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + def test_beta_and_codimension(self): + m=self.load() + for q in range(1,8): + self.assertEqual(m.beta(q), q*(q+7)//2) + self.assertEqual(m.beta(q),sum(j+2 for j in range(2,q+2))) + with self.assertRaises(ValueError): m.beta(0) + + def test_mixed_cutoffs_saturate(self): + m=self.load() + self.assertEqual(m.radial_exponent([F(1,2),F(1,4)],1,4),F(87,16)) + self.assertEqual(m.radial_exponent([F(2)],1,4),F(6)) + self.assertEqual(m.radial_exponent([F(1)],1,2),F(5)) + with self.assertRaises(ValueError):m.radial_exponent([F(1,4),F(1,2)],1,4) + + def test_holder_domain(self): + m=self.load() + self.assertEqual(m.theta(1,2),F(1,2)) + for s,p in [(2,2),(3,2),(0,2),(-1,3)]: + with self.assertRaises(ValueError):m.theta(s,p) + + def test_stirling_factorial_identity(self): + m=self.load() + for p in range(1,10): + for n in range(21): + self.assertEqual(n**p,sum(m.stirling(p,j)*m.falling(n,j) for j in range(1,p+1))) + + def test_exact_holder_finite_laws(self): + m=self.load() + cases=0 + for atoms in m.fixtures(): + for p in range(2,7): + for s in range(1,p): + for t in [0,1]: + lhs,rhs=m.holder_sides(atoms,s,p,t) + self.assertLessEqual(lhs,rhs) + cases+=1 + self.assertEqual(cases,360) + + def test_empty_event(self): + m=self.load() + self.assertEqual(m.holder_sides([(F(1),2,3,False)],1,3,1),(0,0)) + + def test_positive_count_intensity_deletion(self): + m=self.load() + atoms=[(F(1,2),0,1,False),(F(1,4),2,1,False),(F(1,4),5,2,True)] + for s in range(4): + self.assertEqual(m.positive_mass_removed(atoms,s),F(5**s,4)) + + def test_rare_spike_probability_and_moments(self): + m=self.load() + for n in range(1,21): + atoms=m.spike(n,4) + self.assertEqual(sum(row[0] for row in atoms),1) + self.assertTrue(all(row[0]>=0 for row in atoms)) + r=F(1,2**n) + for p in range(1,7): + self.assertEqual(m.expect(atoms,p), r**3*(2**p+(n+3)**p*r**4)) + + def test_no_loss_countermodel(self): + m=self.load() + for s in [1,2,3]: + vals=[] + for n in [1,2,4,8,16,32]: + atoms=m.spike(n,4);r=F(1,2**n) + ratio=m.positive_mass_removed(atoms,s)/(r**3*(2*r)**4) + self.assertEqual(ratio,F((n+3)**s,16));vals.append(ratio) + self.assertEqual(vals,sorted(vals)) + self.assertGreater(vals[-1],vals[0]) + + def test_no_third_factorial_lower_bound(self): + m=self.load() + for n in range(1,8): + r=F(1,2**n) + atoms=[(1-r**3,0,1,False),(r**3,2,1,False)] + self.assertEqual(sum(w*m.falling(x,2) for w,x,_,_ in atoms),2*r**3) + self.assertEqual(sum(w*m.falling(x,3) for w,x,_,_ in atoms),0) + + def test_cli_baseline_and_determinism(self): + self.load(); outputs=[] + for flags in [[],['-O']]: + p=subprocess.run([sys.executable,'-B','-S',*flags,str(ROOT/'transfer_check.py')],capture_output=True,text=True,timeout=15) + self.assertEqual(p.returncode,0,p.stderr);self.assertEqual(p.stderr,'') + out=json.loads(p.stdout);self.assertIs(out['ok'],True) + self.assertFalse(out['scientific_acceptance']);outputs.append(p.stdout) + self.assertEqual(*outputs) + + def test_named_wrong_formulas_and_unknown_label(self): + self.load() + for label,failed in [('M1','mixed_scale'),('M2','rare_radial_scale'),('M3','stirling'),('M4','no_loss'),('M5','third_factorial')]: + p=subprocess.run([sys.executable,'-B','-S',str(ROOT/'transfer_check.py'),'--mutant',label],capture_output=True,text=True,timeout=15) + self.assertEqual(p.returncode,1,p.stderr);self.assertEqual(p.stderr,'') + self.assertEqual(json.loads(p.stdout)['failed'],[failed]) + p=subprocess.run([sys.executable,'-B','-S',str(ROOT/'transfer_check.py'),'--mutant','M9'],capture_output=True,text=True,timeout=15) + self.assertEqual(p.returncode,2);self.assertEqual(p.stdout,'unknown mutant\n');self.assertEqual(p.stderr,'') + +if __name__=='__main__': + unittest.main(verbosity=2) diff --git a/reviews/iba2_012_count_transfer_20261006/transfer_check.py b/reviews/iba2_012_count_transfer_20261006/transfer_check.py new file mode 100644 index 000000000..b36abff31 --- /dev/null +++ b/reviews/iba2_012_count_transfer_20261006/transfer_check.py @@ -0,0 +1,149 @@ +"""Exact finite controls; continuum claims and source acceptance are in PROOF.md. + +No external dependencies, network, floating arithmetic, or source execution. +Wrong-formula modes exercise named non-implications, not process crashes. +""" +from __future__ import annotations +import argparse +import json +from fractions import Fraction as F + + +def beta(q: int) -> int: + if type(q) is not int or q < 1: + raise ValueError('q must be a positive integer') + return q*(q+7)//2 + + +def theta(s: int | F, p: int) -> F: + s=F(s) + if type(p) is not int or not 0 < s < p: + raise ValueError('require integer p > s > 0') + return 1-s/p + + +def radial_exponent(alphas: list[F], s: int | F, p: int) -> F: + if not alphas or any(F(x)<=0 for x in alphas): + raise ValueError('positive ordered radial exponents are required') + if any(F(alphas[i]) < F(alphas[i+1]) for i in range(len(alphas)-1)): + raise ValueError('eta is increasing, so alpha must be nonincreasing') + return 3+theta(s,p)*sum((j+2)*min(F(x),1) for j,x in enumerate(alphas,2)) + + +def falling(n: int, j: int) -> int: + if type(n) is not int or type(j) is not int or min(n,j)<0: + raise ValueError('falling factorial inputs must be nonnegative integers') + out=1 + for i in range(j):out*=n-i + return out + + +def stirling(p: int, j: int) -> int: + if type(p) is not int or type(j) is not int or min(p,j)<0: + raise ValueError('Stirling indices must be nonnegative integers') + row=[1]+[0]*p + for _ in range(p):row=[0]+[k*row[k]+row[k-1] for k in range(1,p+1)] + return row[j] if j<=p else 0 + + +def validate(atoms: list[tuple]) -> None: + if not atoms or sum(F(row[0]) for row in atoms)!=1: + raise ValueError('probabilities must sum to one') + for w,n,k,event in atoms: + if F(w)<0 or type(n) is not int or n<0 or type(k) is not int or k<1 or type(event) is not bool: + raise ValueError('invalid probability/count/norm/event atom') + + +def expect(atoms: list[tuple], p: int) -> F: + validate(atoms) + if type(p) is not int or p<1:raise ValueError('positive integer moment required') + return sum((F(w)*n**p for w,n,_,_ in atoms),F(0)) + + +def fixtures() -> list[list[tuple]]: + ans=[] + for j in range(12): + counts=[0,1+j%3,2+j%4,5+j%3] + weights=[1+j%2,2+j%3,3,4] + total=sum(weights) + ans.append([(F(w,total),n,1+(i+j)%4,(i+j)%3!=0 and n>0) + for i,(w,n) in enumerate(zip(weights,counts))]) + return ans + + +def holder_sides(atoms: list[tuple], s: int, p: int, t: int) -> tuple[F,F]: + validate(atoms);theta(s,p) + if type(s) is not int or type(t) is not int or t<0:raise ValueError('integer s,t required for exact power controls') + a=t*(p-s) + left=sum((F(w)*k**a*n**s for w,n,k,e in atoms if e),F(0))**p + rare=sum((F(w)*k**(t*p) for w,n,k,e in atoms if e),F(0)) + return left,rare**(p-s)*expect(atoms,p)**s + + +def positive_mass_removed(atoms: list[tuple], s: int) -> F: + validate(atoms) + if type(s) is not int or s<0:raise ValueError('nonnegative integer weight required') + original={};retained={} + for w,n,_,e in atoms: + if n>0: + original[n]=original.get(n,F(0))+F(w) + if not e:retained[n]=retained.get(n,F(0))+F(w) + return sum((n**s*abs(w-retained.get(n,F(0))) for n,w in original.items()),F(0)) + + +def spike(n: int, b: int=4) -> list[tuple]: + if type(n) is not int or n<1 or type(b) is not int or b<1:raise ValueError('n,b must be positive integers') + r=F(1,2**n);rare=r**(3+b) + return [(1-r**3-rare,0,1,False),(r**3,2,1,False),(rare,n+3,1,True)] + + +def run_checks(mutant: str | None=None) -> dict: + checks={} + # Controls retain the exact mixed exponents and perturbation-scale cap. + mixed=radial_exponent([F(1,2),F(1,4)],1,4) + if mutant=='M1':mixed=3+theta(1,4)*(3*F(1,2)+4*F(1,4)) + checks['mixed_scale']=mixed==F(87,16) + base=3 + if mutant=='M2':base=3*theta(1,4) + checks['rare_radial_scale']=base+4*theta(1,4)==6 + count=0;identities=True + for p in range(1,10): + for n in range(21): + low=2 if mutant=='M3' else 1 + identities &= n**p==sum(stirling(p,j)*falling(n,j) for j in range(low,p+1)) + count+=1 + checks['stirling']=bool(identities) + holder_count=0;holder=True + for atoms in fixtures(): + for p in range(2,7): + for s in range(1,p): + for t in [0,1]: + left,right=holder_sides(atoms,s,p,t);holder &= left<=right;holder_count+=1 + checks['holder']=bool(holder) + no_loss=True;spike_count=0 + for n in [1,2,4,8,16,32]: + r=F(1,2**n);atoms=spike(n) + ratio=positive_mass_removed(atoms,1)/(r**3*(2*r)**4) + no_loss &= ratio<=1 if mutant=='M4' else ratio==F(n+3,16) + spike_count+=1 + checks['no_loss']=bool(no_loss) + atoms=[(F(7,8),0,1,False),(F(1,8),2,1,False)] + third=sum(w*falling(n,3) for w,n,_,_ in atoms) + checks['third_factorial']=third>=F(1,8) if mutant=='M5' else third==0 + removed=positive_mass_removed([(F(1,2),0,1,False),(F(1,4),2,1,False),(F(1,4),5,2,True)],2) + checks['positive_intensity']=removed==F(25,4) + checks['sub_r_saturation']=radial_exponent([F(2)],1,4)==radial_exponent([F(1)],1,4) + failed=[k for k,v in checks.items() if not v] + return {'ok':not failed,'checks':checks,'failed':failed,'mutant':mutant, + 'stirling_cases':count,'holder_cases':holder_count,'spike_cases':spike_count, + 'scientific_acceptance':False,'continuum_proof_by_tests':False} + + +def main() -> int: + parser=argparse.ArgumentParser(description=__doc__);parser.add_argument('--mutant');args=parser.parse_args() + if args.mutant not in [None,'M1','M2','M3','M4','M5']: + print('unknown mutant');return 2 + out=run_checks(args.mutant);print(json.dumps(out,sort_keys=True,separators=(',',':'))) + return 0 if out['ok'] else 1 + +if __name__=='__main__':raise SystemExit(main())