diff --git a/reviews/iba2_012_localized_moment_20261006/NOTE.md b/reviews/iba2_012_localized_moment_20261006/NOTE.md new file mode 100644 index 000000000..9dd7d583e --- /dev/null +++ b/reviews/iba2_012_localized_moment_20261006/NOTE.md @@ -0,0 +1,178 @@ +# IBA2-012 addendum: localize before taking the count moment + +Object: IBA2-012-LOCALIZED-MOMENT-20261006-v1. +Author: OpenAI / GPT-6 Astra Pro, `iba2-count-weight-transfer-r6-20261006`, +for Dylan Roy — delegated AI work. Source-exposed; organizational credit0; +scientific effect NONE. **Conditional author-side addendum; delta review required.** + +## 1. Parent, scope and provenance reconciliation + +The count-transfer theorem, shrinking-sector negligibility and the all-fixed-order +obstruction to loss-free transfer are ALREADY recorded by merged Math-#319. They +are not new claims of this addendum. Its canonical five-file packet remains +unchanged. This note extracts only a useful input reduction and a fixed-order +sharpness result from the conflicting #324 draft at af85f05fdfcb810e0973e829d838ecb35946390a. +That draft and its review6007975992 remain historical evidence, not a replacement +for #319 and not an independent second discovery of its core theorem. + +Read these exact sources at cut `75ce4eab431e487a163cc4ebb30c5d2386a0e887`: + +| Tag | Path | Full Git blob | Slice | +|---|---|---|---| +| CT | `reviews/iba2_012_count_transfer_20261006/PROOF.md` | `752bc9da5e49af3d0724d80c91cffc0dde35a2d8` | Entire parent; especially first-moment input in sections2–3, scope/denominators and section6 obstruction | +| FR | `reviews/iba2_012_finite_radius_20261005/PROOF.md` | `5ed684c9bb446efc9bef5f3980717c6dc039abfd` | Sections3–5/8, finite-r derivative-weighted event bounds | +| CP | `frontiers/c6_palm_route_20260929/PROOF.md` | `89eb8adf08fe7afc2cab9662d3a9875c05ae5cc5` | Sections1.1–1.3, one fixed-order instance of Theorem Q and all inherited qualifications | +| ERR | `reviews/d5_dimension_lift_erratum_20261005/ERRATUM.md` | `23df87bbe4ffd3b2d786cd695fb9f5448cfa1d05` | Entire additive correction, read with unchanged originals | + +Removing an independently consumed first-moment input at this transfer step does +NOT remove DL from CP's own proof ancestry, resolve an ancestor review gap, or +prove the field count bounds independently. All field applications remain +conditional on the stated source interfaces. No old proof or status is revised. + +## 2. One factorial order is enough after event localization + +Work on one probability space with N a nonnegative integer-valued count, K>=1, +a measurable event E, a small scale rho>0 and 0=0, 0=2. Put theta=1-p/m. Assume only + + E[(N)_m] <= B_m rho, + E[K^t 1_E] <= A_t rho Xi for t=0 and t=a/theta. (L-input) + +Constants are independent of rho and Xi in the stated parameter range. Then + + E[K^a N^p 1_E] + <= [m^m(A_0 C0+B_m)]^(p/m) A_(a/theta)^theta + rho Xi^theta. (L) + +**Proof.** For every integer n>=0, + + n^m <= m^m[1+(n)_m]. (1) + +For n=m each of the m factors n-i is at least +n/m, since n-m+1>=n/m. Thus (n)_m>=(n/m)^m. Apply (1) only on E: + + E[N^m 1_E] <= m^m(P(E)+E[(N)_m]) + <= m^m(A_0 C0+B_m)rho. (2) + +Finite mth factorial moment also excludes N=infinity, or one may start with +truncations. Holder on this same probability measure gives + + E[K^a N^p 1_E] + <= (E[N^m 1_E])^(p/m) + (E[K^(a/theta) 1_E])^theta. (3) + +Insert the two bounds. The exponents of rho add to p/m+theta=1, proving (L). +No independence of N,K,E is used. The indicator belongs in BOTH finite moments. +The term1 in (1) cannot be removed: n=1 annihilates every factorial order m>=2. + +A global first moment is genuinely not forced by L-input. Abstractly, let N=1 +almost surely, K=1 and P(E)=rho Xi with rho Xi<=1. Then all m>=2 factorial moments +are0 and the localized assumptions hold, but E[N]=1 is not O(rho). This is not a +Gaussian-field counterexample. It shows why replacing (2) by an unproved global +O(rho) ordinary moment would impose an unnecessary additional premise. + +## 3. Apply the lemma without changing the parent theorem's meaning + +Use FR and CP on their SAME full-normalizer tilted pin law P_r=Q_r^W. Keep fixed +d>=3,L>0, observation radius R>=1, compact birth heights and strictly positive +compact gap marks, exactly as in CT and FR. Let N be the torus-wide between-pin +count, N_R its local subcount, and K FR's C4 control. For 1<=q<=d-2 set + + S = {h_j<=eta_j for j=2,...,q+1}, + E = {N_R>0} intersect S, + Xi = product_(j=2..q+1)(eta_j+r)^(j+2). + +The h_j are FR's ordered midpoint transverse eigenvalues. For ordered thresholds +0<=eta_2<=...<=eta_(q+1)<=1 and r<=1, Xi<=2^beta, beta=q(q+7)/2. FR-mixed supplies +the two event bounds in L-input with rho=r^3; one chosen instance of CP Theorem Q +supplies the factorial bound. Consequently + + E[K^a N^p 1_E] <= C r^3 Xi^(1-p/m), + E[K^a N_R^p 1_S] <= C r^3 Xi^(1-p/m). (4) + +The second line uses p>0 and N_R^p 1_S=N_R^p 1_E<=N^p 1_E. For p=0 keep the +nonempty event and use FR directly. Remote-only outcomes with N_R=0 are not +controlled by removing E from the first line. No additional normalization is +performed and no K under CP's witness regression is identified with FR's K. + +This obtains the parent's count-transfer CONCLUSION using a narrower list of +explicit inputs at this inference step: one factorial order and two FR moment +orders. It does not require every factorial order or separately insert DL's first +moment. To make the exponent loss arbitrarily small, more fixed orders still need +to be available; constants are not uniform in m and m cannot vary with r here. + +The same arguments include zero thresholds and the all-soft transverse case. +On thresholds eta_j=r^alpha_j ordered with alpha_2>=...>=alpha_(q+1)>0, (4) has +order r^[3+(1-p/m) sum_(j=2..q+1)(j+2)min(alpha_j,1)], hence o(r^3). This is a +restatement of the parent's scaling at the reduced input interface, not a second +sector closure. No new radial lifetime integration or all-mark conclusion follows. + +## 4. The fixed-order exponent is sharp from these inputs + +Fix an integer m>=2 and real 0=1. + +For every eta in [0,1], E={N_R>0,h_2<=eta} is empty if eta=0. Also + + E[(N)_m] <= E[N^m] = (2^m+1)r_n^3. + +At eta=r_n, + + E[N^p;E] = r_n^7 2^(4np) + = r_n^3 r_n^[4(1-p/m)], + Xi = (2r_n)^4. (5) + +The ratio to r_n^3 Xi^(1-p/m) is the nonzero constant16^[-(1-p/m)]. For any +larger Xi exponent, the ratio is unbounded as n increases. This proves sharpness +of 1-p/m from the listed single-order inputs. It is NOT a lower bound for the +actual Gaussian field. The next ordinary moment obeys + + E[N^(m+1)]/r_n^3 = 2^(m+1)+2^(4n), + +so this family does not supply all higher O(r^3) moments. The parent's section6 +already supplies the DIFFERENT all-fixed-orders obstruction to loss-free transfer; +that result is credited and not recopied here. The ordinary-atom constant in the +last display additively corrects its omission in review6007975992's discussion of +the first draft. Divergence and the reviewed sector identity were unaffected. + +## 5. Positional tuple measures: a small consequence, not a convergence theorem + +For a fixed integer s>=1, (N_R)_s<=N_R^s. Let nu_(r,s) be r^-3 times the expected +positive measure of ordered s-tuples of distinct local window points, with any +measurable location or rescaled-location coordinates. Let nu_(r,s)^keep delete +configurations in S. Their difference is a positive measure, and + + ||nu_(r,s)-nu_(r,s)^keep||_variation + = r^-3 E[(N_R)_s 1_S] <= C Xi^(1-s/m), m>s,m>=2. (6) + +These measures are finite at each r by (1) and a fixed CP moment; no uniform global +first moment is needed merely for finiteness. The variation convention is total +mass of a positive measure, not half-L1 for probabilities. Signed tuple functions +bounded by K^a obey the corresponding absolute upper bound from (4). + +This only controls deleted-sector mass. It provides no full point-process limit, +location law, correlation density, elder matching or rate for the remaining +measure. Conditional-on-local-occurrence or factorial Palm normalization still +needs its own positive lower denominator; none is inserted here. + +## 6. Verification, exact preservation and remaining obligations + +The supplied test_count_transfer.py is EXACTLY blob629ba742ee777e7da992cf0a975cb7384ad1763f +from the first draft, not a rewritten suite. The actual xAI/Grok4.7 reader of that +head ran its13methods in both Python3.12.3 modes, all passing; M1–M4 gave intended +assertion failures, no test errors, and unknown labels exited2. Baseline stdout +SHA256 d8a2efa940de518122ee6037ebf15c35f3908fb5264472351d3aa4936f69e425. +That is reviewer's execution, not local author execution. The single-order model +was separately checked algebraically in the same written review. The author's +execution tools remain unavailable before command startup. + +Those tests cover finite algebra, not arbitrary probability spaces or source +validity. A changed-source delta read must check this note against the reviewed +draft sections3,5.1,4.2 and canonical CT. Do not transfer the old whole-text verdict +automatically. All five canonical CT files, FR, CP, ERR and scientific records must +remain byte-identical. General IBA2-012/IBA2-009, loss-free conditional sector +moments, escaping marks, growing R, actual moment-law construction and full formal +alignment remain open outside this additive scope. diff --git a/reviews/iba2_012_localized_moment_20261006/README.md b/reviews/iba2_012_localized_moment_20261006/README.md new file mode 100644 index 000000000..048e560ef --- /dev/null +++ b/reviews/iba2_012_localized_moment_20261006/README.md @@ -0,0 +1,43 @@ +# Localized-moment addendum to the landed IBA2 count-transfer packet + +Read [NOTE.md](NOTE.md) and [SOURCES.json](SOURCES.json). Canonical Math-#319 is +preserved unchanged in `../iba2_012_count_transfer_20261006/`; this is a distinct, +additive path. The initial #324 replacement draft was found to overlap that +landing and was not merged. + +The only retained mathematical additions are the event-localized ordinary-moment +bound from one fixed factorial order and event mass, sharpness of that fixed-order +exponent, and a positive ordered-tuple measure consequence. They do not reclaim +the parent's count-transfer theorem or its all-orders obstruction. Eliminating a +separately consumed first-moment premise at the transfer step does not remove DL +from C6's own ancestry or prove any underlying field theorem independently. + +The exact test script is reused from the first draft, with its real13-method +normal/optimized runs credited to xAI/Grok reviewer6007975992. It is not thirteen +new tests on top of that result. Source changes in NOTE need a new delta read. +The author runtime is unavailable; no new author-local run is claimed. + +```sh +python3 -B -S test_count_transfer.py +python3 -B -O -S test_count_transfer.py +python3 -B -S test_count_transfer.py --mutant M1 +python3 -B -S test_count_transfer.py --mutant M2 +python3 -B -S test_count_transfer.py --mutant M3 +python3 -B -S test_count_transfer.py --mutant M4 +``` + +Baseline: exit0,13methods, JSON empty failures/errors. Mutants must exit1 for the +intended assertions and no errors; repeat optimized. Unknown labels exit2. These +are finite algebra controls, not continuum/Lean verification. Existing general CI +does not automatically execute this standalone packet. + +For offline use, save these four files and their four exact input sources at the +cut in SOURCES.json into a NEW directory. Preserve actual stdout/stderr, versions, +exit codes and source hashes outside the frozen packet. A GitHub publication is +not a laptop installation. Do not overwrite the sealed R5 kit, private cloud +sources, existing worktrees or any local model cache. + +Scientific effect NONE; organizational credit0. General IBA2-012 and IBA2-009, +loss-free conditional-sector moments, local/factorial lower denominators, growing +R, escaping marks, Gaussian field realization and full formal alignment remain +outside this addendum. Current review and integration state lives in the PR. diff --git a/reviews/iba2_012_localized_moment_20261006/SOURCES.json b/reviews/iba2_012_localized_moment_20261006/SOURCES.json new file mode 100644 index 000000000..d744b129d --- /dev/null +++ b/reviews/iba2_012_localized_moment_20261006/SOURCES.json @@ -0,0 +1,44 @@ +{ + "object": "IBA2-012-LOCALIZED-MOMENT-20261006-v1", + "repository": "d6g8k5htny-coder/Math-", + "source_cut": "75ce4eab431e487a163cc4ebb30c5d2386a0e887", + "author": "OpenAI / GPT-6 Astra Pro / iba2-count-weight-transfer-r6-20261006", + "principal": "Dylan Roy — delegated AI work", + "scientific_effect": "NONE", + "organizational_independence_credit": 0, + "scope": "Addendum only: event-localized one-factorial-order input, its sharp exponent, and local-tuple mass deletion. Does not replace the canonical Math-319 theorem or its ancestry.", + "inputs": [ + {"tag":"CT","path":"reviews/iba2_012_count_transfer_20261006/PROOF.md","git_blob":"752bc9da5e49af3d0724d80c91cffc0dde35a2d8","slice":"Entire parent; existing core transfer, first-moment input, lower denominators and all-orders obstruction"}, + {"tag":"FR","path":"reviews/iba2_012_finite_radius_20261005/PROOF.md","git_blob":"5ed684c9bb446efc9bef5f3980717c6dc039abfd","slice":"3–5 and8; finite-r derivative-weighted event estimates"}, + {"tag":"CP","path":"frontiers/c6_palm_route_20260929/PROOF.md","git_blob":"89eb8adf08fe7afc2cab9662d3a9875c05ae5cc5","slice":"1.1–1.3; one fixed Theorem Q order and all inherited qualifications"}, + {"tag":"ERR","path":"reviews/d5_dimension_lift_erratum_20261005/ERRATUM.md","git_blob":"23df87bbe4ffd3b2d786cd695fb9f5448cfa1d05","slice":"Entire additive correction"} + ], + "canonical_parent_preservation": { + "directory":"reviews/iba2_012_count_transfer_20261006/", + "PROOF.md":"752bc9da5e49af3d0724d80c91cffc0dde35a2d8", + "README.md":"7a58357c825d9737b9fa5251b5b55c31cd467fa9", + "SOURCES.json":"a9f8f29cc9e651cd3fff1c86b71823249054d1f6", + "test_transfer.py":"175388b9047abb4e88d98c855b9ffe38cb45aad7", + "transfer_check.py":"b36abff316da46eaa08a20dd5641e9d6d18e3d06" + }, + "payloads":[ + {"path":"NOTE.md","git_blob":"9dd7d583e50336aea6e0625d57dffabc50ed4f3e"}, + {"path":"test_count_transfer.py","git_blob":"629ba742ee777e7da992cf0a975cb7384ad1763f","sha256_from_review":"c81a2ad32f9adb4e904bebd7fb472af55673fd0935c8d8a1220bfa1f246ca6b0"} + ], + "history": { + "superseded_conflicting_draft":"af85f05fdfcb810e0973e829d838ecb35946390a", + "original_review":"Math-324/6007975992", + "collision_notice":"Math-324/6007993806", + "reconciliation":"Math-324/6008009480", + "meaning":"Old draft/review retained in history; no parent replacement and no automatic transfer of a whole-text verdict to this new note." + }, + "test_execution": { + "performer":"xAI Grok 4.7 via Cursor, model grok-4.7-high-fast", + "session":"bc-0ffd9a55-553f-42eb-9559-748fb609584f", + "python":"3.12.3", + "source_blob":"629ba742ee777e7da992cf0a975cb7384ad1763f", + "methods_per_mode":13, + "baseline_stdout_sha256":"d8a2efa940de518122ee6037ebf15c35f3908fb5264472351d3aa4936f69e425", + "note":"Actual reader runs at the previous directory; bytes unchanged and script has no path-relative inputs. New-note delta review remains required. No author local execution or kernel proof is asserted." + } +} diff --git a/reviews/iba2_012_localized_moment_20261006/test_count_transfer.py b/reviews/iba2_012_localized_moment_20261006/test_count_transfer.py new file mode 100644 index 000000000..629ba742e --- /dev/null +++ b/reviews/iba2_012_localized_moment_20261006/test_count_transfer.py @@ -0,0 +1,198 @@ +#!/usr/bin/env python3 +"""Exact finite controls for the conditional IBA2 count-transfer note. + +No network, third-party packages, field simulation or Lean execution. +Exit 0: every finite control passes. Exit 1: assertion rejection only. +Exit 2: invalid arguments or an unexpected test error, not a math rejection. +""" +from __future__ import annotations + +import argparse +from fractions import Fraction as F +from itertools import permutations +import json +from math import factorial +import sys +import unittest + +MUTANT = None + + +def falling(n: int, m: int) -> int: + if n < m: + return 0 + value = 1 + for i in range(m): + value *= n - i + return value + + +def beta(q: int) -> int: + return sum(j + 2 for j in range(2, q + 2)) + + +def theta(p: F, order: int) -> F: + p = F(p) + if p < 0 or order < 2 or order <= p: + raise ValueError("need p >= 0 and integer order >= 2, order > p") + return F(1) if MUTANT == "M2" else 1 - p / order + + +def common_radial_power(p: F, order: int) -> F: + return F(3) * theta(p, order) if MUTANT == "M1" else F(3) + + +def mixed_power(alphas: tuple[F, ...]) -> F: + weights = list(range(4, 4 + len(alphas))) + if MUTANT == "M3": + weights.reverse() + return sum((w * min(F(a), F(1)) for w, a in zip(weights, alphas)), F(0)) + + +def envelope(n: int, order: int) -> int: + return order ** order * (falling(n, order) + (0 if MUTANT == "M4" else 1)) + + +def spike(n: int, q: int = 1) -> tuple[F, F, F, int]: + r = F(1, 2 ** n) + ordinary = r ** 3 + rare = r ** (3 + beta(q)) + return r, ordinary, rare, n + 2 + + +class CountTransferTests(unittest.TestCase): + def test_beta(self): + self.assertEqual([beta(q) for q in range(1, 5)], [4, 9, 15, 22]) + for q in range(1, 12): + self.assertEqual(beta(q), q * (q + 7) // 2) + + def test_factorial_envelope(self): + for order in range(2, 9): + for n in range(0, 41): + with self.subTest(order=order, n=n): + self.assertLessEqual(n ** order, envelope(n, order)) + + def test_holder_exponents(self): + for order in range(2, 9): + for p in range(1, order): + self.assertEqual(theta(F(p), order), F(order - p, order)) + self.assertEqual(F(p, order) + theta(F(p), order), 1) + self.assertEqual(theta(F(3, 2), 4), F(5, 8)) + for p, order in [(2, 2), (3, 2), (-1, 2), (0, 1)]: + with self.assertRaises(ValueError): + theta(F(p), order) + + def test_radial_power(self): + for order in range(2, 9): + for p in range(1, order): + self.assertEqual(common_radial_power(F(p), order), 3) + self.assertEqual(3 * F(p, order) + 3 * F(order - p, order), 3) + + def test_weighted_holder_finite_laws(self): + laws = [ + [(F(1, 2), 0, 1), (F(1, 8), 1, 2), (F(1, 8), 2, 3), + (F(1, 8), 3, 5), (F(1, 8), 7, 7)], + [(F(1, 3), 1, 9), (F(1, 3), 4, 2), (F(1, 3), 9, 1)], + ] + for law in laws: + for cutoff in [1, 2, 5]: + selected = [(w, n, k) for w, n, k in law if n >= cutoff] + for order in range(2, 7): + for p in range(1, order): + lhs = sum((w * k ** (order-p) * n ** p for w,n,k in selected), F(0)) + moment = sum((w * n ** order for w,n,k in selected), F(0)) + weighted = sum((w * k ** order for w,n,k in selected), F(0)) + self.assertLessEqual(lhs ** order, moment ** p * weighted ** (order-p)) + + def test_event_restricted_moment(self): + # A large count outside E does not justify removing the event from K. + law = [(F(1, 2), 0, False), (F(1, 4), 1, True), + (F(1, 8), 5, True), (F(1, 8), 19, False)] + pe = sum((w for w,n,e in law if e), F(0)) + for order in range(2, 8): + lhs = sum((w * n ** order for w,n,e in law if e), F(0)) + fm = sum((w * falling(n, order) for w,n,e in law), F(0)) + self.assertLessEqual(lhs, order ** order * (pe + fm)) + + def test_mixed_diagonal(self): + b = mixed_power((F(1, 2), F(1, 4))) + self.assertEqual(b, F(13, 4)) + self.assertEqual(common_radial_power(F(1), 2) + b * theta(F(1), 2), F(37, 8)) + self.assertEqual(common_radial_power(F(2), 4) + 4 * theta(F(2), 4), 5) + + def test_saturation(self): + self.assertEqual(mixed_power((F(2), F(1))), 9) + self.assertEqual(mixed_power((F(1),)), 4) + self.assertEqual(mixed_power((F(1, 2),)), 2) + for n in range(1, 15): + r = F(1, 2 ** n) + self.assertLessEqual(r ** 2 + r, 2*r) + self.assertGreaterEqual(r ** 2 + r, r) + + def test_spike_event_thresholds(self): + for q in range(1, 5): + for n in range(1, 13): + r, ordinary, rare, count = spike(n, q) + self.assertLess(ordinary + rare, 1) + for eta in [F(0), r/2, r, min(2*r, F(1)), F(1)]: + mass = rare if eta >= r else F(0) + self.assertLessEqual(mass, r ** 3 * (eta+r) ** beta(q)) + + def test_spike_fixed_moments(self): + for order in range(2, 9): + bound = 2 ** order + 6 ** order * factorial(order) + for n in range(1, 65): + r, ordinary, rare, count = spike(n) + moment = ordinary * 2 ** order + rare * count ** order + fm = ordinary * falling(2, order) + rare * falling(count, order) + self.assertLessEqual(fm, moment) + self.assertLessEqual(moment, bound * r ** 3) + self.assertGreaterEqual(ordinary + rare, r ** 3) + + def test_lossfree_obstruction(self): + for p in [1, 2, 3]: + ratios = [] + for n in [2, 8, 32, 128]: + r, ordinary, rare, count = spike(n) + value = rare * count ** p / (r ** 3 * (2*r) ** 4) + self.assertEqual(value, F((n+2) ** p, 16)) + ratios.append(value) + self.assertEqual(ratios, sorted(ratios)) + self.assertGreater(ratios[-1], 1) + # Finite checks only; divergence follows from (n+2)^p/16 -> infinity. + + def test_remote_only_exclusion(self): + global_count, local_count, soft = 7, 0, True + event = local_count > 0 and soft + self.assertFalse(event) + self.assertEqual(local_count ** 2 * int(soft), 0) + self.assertGreater(global_count ** 2 * int(soft), 0) + self.assertEqual(global_count ** 2 * int(event), 0) + + def test_factorial_intensity_mass(self): + for n in range(0, 7): + for degree in range(1, 5): + ordered_tuples = sum(1 for _ in permutations(range(n), degree)) + self.assertEqual(ordered_tuples, falling(n, degree)) + self.assertLessEqual(falling(n, degree), n ** degree) + + +def main() -> int: + global MUTANT + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--mutant", choices=["M1", "M2", "M3", "M4"]) + args = parser.parse_args() + MUTANT = args.mutant + suite = unittest.defaultTestLoader.loadTestsFromTestCase(CountTransferTests) + result = unittest.TextTestRunner(stream=sys.stderr, verbosity=2).run(suite) + report = {"ok": result.wasSuccessful(), "tests": result.testsRun, + "mutant": MUTANT, + "failures": [str(t) for t, _ in result.failures], + "errors": [str(t) for t, _ in result.errors], + "scope": "finite arithmetic only; no continuum or kernel verdict"} + print(json.dumps(report, sort_keys=True, separators=(",", ":"))) + return 2 if result.errors else (0 if result.wasSuccessful() else 1) + + +if __name__ == "__main__": + sys.exit(main())