From 6aaf48105c2100d0dcf47b5b1ff5a85c37ddef52 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 05:52:09 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20check=20#4451/#4452:=20within-c?= =?UTF-8?q?ell=20halo=20exponents=2011,=2024,=2026,=2026,=206=20under=20de?= =?UTF-8?q?lta=20(no=20new=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- research/delta-halo-exponent-check/README.md | 81 ++++++++++++++ .../delta-halo-exponent-check/SOURCES.json | 30 ++++++ research/delta-halo-exponent-check/TASK.json | 74 +++++++++++++ .../delta-halo-exponent-check/VERIFY.json | 21 ++++ research/delta-halo-exponent-check/verify.py | 102 ++++++++++++++++++ 5 files changed, 308 insertions(+) create mode 100644 research/delta-halo-exponent-check/README.md create mode 100644 research/delta-halo-exponent-check/SOURCES.json create mode 100644 research/delta-halo-exponent-check/TASK.json create mode 100644 research/delta-halo-exponent-check/VERIFY.json create mode 100644 research/delta-halo-exponent-check/verify.py diff --git a/research/delta-halo-exponent-check/README.md b/research/delta-halo-exponent-check/README.md new file mode 100644 index 0000000000..5c0baedae6 --- /dev/null +++ b/research/delta-halo-exponent-check/README.md @@ -0,0 +1,81 @@ +# Independent check of #4451 and #4452: the halo exponents 11, 24, 26, 26 and 6 inside one cell + +**Claim type:** an independent check of conditional exponent arithmetic, by a separate proof route +plus exact rational arithmetic. **No new κ.** It covers jwr404's +[#4451](https://github.com/CrocSwap/integer-mult-bounds/pull/4451) (head `be243a28`) and +[#4452](https://github.com/CrocSwap/integer-mult-bounds/pull/4452) (head `af68f597`). The ideal gaps +`1/(8p²)` stay hypotheses. + +## What is checked + +Notation: `D = 2^{32760p}`, `δ = 4/D`, `g = 1/(8p²)`, `η = 2^{−32768p}`. + +1. **(R) Relative-error repair (#4451).** From `a − 4η < â ≤ a` and `a > 2^{−8p}`, we get + `a/â < 1/(1 − 4η·2^{8p}) = 1/(1 − δ)`. Also `δ < 1/(16p²)`. +2. **(N) Neumann ceiling.** The identity `(1 − δ)/(g − δ) = U = 8p²(D − 4)/(D − 32p²)` is checked + exactly. Also the rounded off-sum `(1 − g)/(1 − δ)` is below 1, so the absolute sums are below 2. +3. **(B) The U chain, for all `p ≥ 2`, by a route different from the PRs'.** From `p < 2^p` we get + `512p⁴ < 2^{4p+9} ≤ D`, so `r = 32p²/D < 1/(16p²)`. With `V = 8p²/(1 − r)`: + + 8p² < U < V < 8p² + 1 ≤ 16p² − 1 < p⁶, V² < (8p² + 1)² < p^{11}. + + The last step is `1089 < 2048` at `p = 2`, and `(8p²+1)² ≤ 81p⁴ ≤ p⁸` for `p ≥ 3`. +4. **(S) Neumann polynomial.** `P − A^{−1} = −Q^L A^{−1}` and `‖Q‖ < 1 − p^{−22}`, so the error is + below `U·e^{−p^{−22}L}`. At `L = p^{24}` that is `U·e^{−p²} < p⁶e^{−p²}`. The bandwidth is + `(2L ± 1)(p − 1) < p^{26}`. +5. **Exact replay.** Every inequality in 1–4 is checked with `Fraction` for each `p` from 2 to 64. +6. **The "fails" column at `p = 2`.** + - `U > 32 = p⁵`, so normalizer 5 and spectral endpoint 10 fail. + - Length `p^{23}` fails on this route, by the certified lower bound `(1−x)^L ≥ e^{−xL−x²L}`. + - The loose radius `2p^{24} + 1` exceeds `p^{25}`. + +| Role | #4452 | Confirmed | +| --- | ---: | --- | +| Spectral endpoint | 11 | yes; 10 fails at `p = 2` | +| Series length | 24 | yes; 23 fails at `p = 2` | +| Bandwidth | 26 | yes; 25 fails (loose count at `p = 2`, sharp count for `p ≥ 3`) | +| Agreement distance | 26 | yes | +| Normalizer | 6 | yes; 5 fails at `p = 2` | + +## Remarks + +- **The sharp count at `p = 2` is below `p^{25}`.** The sharp bandwidth count is `2^{25} − 1`, so + "25 fails" at `p = 2` holds only for the loose count `(2p^{24}+1)W`. For `p ≥ 3`, the sharp count + exceeds `p^{25}`, so the uniform conclusion is unchanged. #4452's text already says this, and the + verifier records it explicitly. +- **#4452 relies on `Ĝ_0 = 1`.** The Neumann step needs the unit diagonal. #4452's lemma states only + `0 ≤ Ĝ ≤ G`, but `Ĝ_0 = 1` is inherited from #4438/#4439. A future write-up should restate it. +- **"Smallest" is relative to this proof route.** The failures are failures of the stated + majorant route, not lower bounds for the actual block. + +## Not covered + +- The ideal gaps `1/(8p²)` for every prime. +- Across-cell entries (#4449, #4442). +- Any new κ. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/delta-halo-exponent-check --check-only +python3.12 -B scripts/research_package.py --package research/delta-halo-exponent-check +``` + +The verifier prints `PASS_DELTA_HALO_EXPONENT_CHECK` in about 20 seconds, using only the standard +library. + +## Open next questions + +1. **Do 11, 24, 26, 26 and 6 survive across a cell?** + - *Why it matters:* this is #4452's own open question, and the global reference still uses + 20, 42, 45, 48 and 100. + - *First step:* #4442's column split with `δ` in place of `1/(16p²)`, using #4449's `0 ≤ H ≤ n`. + +## Credit + +- The lemmas, exponents and proofs are James Reed's (jwr404, #4451 and #4452, building on #4438 and + #4439). +- The downward rounding contract is in the pinned downstream phase-cell report. + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/delta-halo-exponent-check/SOURCES.json b/research/delta-halo-exponent-check/SOURCES.json new file mode 100644 index 0000000000..8396f77595 --- /dev/null +++ b/research/delta-halo-exponent-check/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md", + "usage": "input", + "git_blob": "d72345a0aa748443c4efcddf87aa10d524664841", + "sha256": "3cdf492bcb719db4295658604dc202d6a2c5a008b87de43ec54f0107c64db730" + }, + { + "path": "research/unconditional-batched-crt/HALO.md", + "usage": "input", + "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b", + "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc" + } + ] +} diff --git a/research/delta-halo-exponent-check/TASK.json b/research/delta-halo-exponent-check/TASK.json new file mode 100644 index 0000000000..b448cc4d20 --- /dev/null +++ b/research/delta-halo-exponent-check/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Independently check the within-cell delta exponent arithmetic of #4451 and #4452 (11, 24, 26, 26, 6) by a separate proof route and exact rational replay.", + "scope_change_reason": "Independent audit of two open author-checked precision/conditioning steps.", + "bottleneck_link": "Side result: an independent check of one precision/conditioning step under the #4100 transfer obligations.", + "budget_minutes": 40, + "stop_rule": "Stop at the within-cell arithmetic; across-cell transfer is out of scope.", + "outcome": "completed", + "evidence": "All #4452 inequalities hold for all p>=2 via p<2^p (r=32p^2/D<1/(16p^2)) and exactly for p=2..64; each 'fails' entry confirmed at p=2. Remarks: the sharp bandwidth count at p=2 is 2^25-1 (only the loose count fails there); Ghat_0=1 is inherited from #4438.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "Do 11, 24, 26, 26 and 6 survive across a cell?", + "why_it_matters": "The global reference still uses 20, 42, 45, 48 and 100.", + "first_step": "#4442's column split with delta in place of 1/(16p^2), using #4449's 0<=H<=n.", + "blocked_by": "None." + } + ] +} diff --git a/research/delta-halo-exponent-check/VERIFY.json b/research/delta-halo-exponent-check/VERIFY.json new file mode 100644 index 0000000000..7c7fed46e5 --- /dev/null +++ b/research/delta-halo-exponent-check/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md", + "research/unconditional-batched-crt/HALO.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Independent check of #4451/#4452: delta repair, exact Neumann ceiling identity U, the chain 8p^2=2 (separate route) and exactly for p=2..64, series error at L=p^24, bandwidth 2^-8p, eta = 2^-32768p => a/ahat < 1/(1-delta). + (N) Neumann ceiling (1-delta)/(g-delta) equals U = 8p^2(D-4)/(D-32p^2) (exact identity). + (B) For all p >= 2, p < 2^p gives 512 p^4 < 2^(4p+9) <= D, so r = 32p^2/D < 1/(16p^2), and with + V = 8p^2/(1-r): 8p^2 < U < V < 8p^2 + 1 <= 16p^2 - 1 < p^6, and V^2 < (8p^2+1)^2 < p^11. + (S) Neumann polynomial P = p^-11 sum_{j 2^-8p, ahat -> a - 4 eta + need(4 * eta / floor_a == delta and delta < 1, "R: 4 eta / 2^-8p = delta") + need(delta < F(1, 16 * p * p), "#4451: delta < 1/(16p^2)") + U = F(8 * p * p * (D - 4), D - 32 * p * p) + V = F(8 * p * p * D, D - 32 * p * p) + need((1 - delta) / (g - delta) == U, "N: Neumann ceiling identity") + need((1 - g) / (1 - delta) < 1, "rounded off-sum < 1, absolute sums < 2") + need(8 * p * p < U < V < 8 * p * p + 1 <= 16 * p * p - 1 < p ** 6, "B: U chain") + need(V * V < p ** 11, "B: V^2 < p^11") + need(U * U < p ** 11 and 4 < p ** 11, "spectrum of A*A inside (p^-11, p^11)") + L = p ** 24 + need((2 * L - 1) * (p - 1) < p ** 26 and (2 * L + 1) * (p - 1) < p ** 26, "bandwidth/agreement < p^26") + return U + + +def series_error_ok(p, length_exp): + """certified: U*(1-x)^L < p^6 exp(-p^2) with x = p^-22, L = p^length_exp; uses (1-x)^L <= exp(-xL)""" + xL = F(p ** length_exp, p ** 22) + U_upper = 8 * p * p + 1 + # need log(U_upper) - xL < 6 log p - p^2, i.e. xL - p^2 > log(U_upper / p^6) (negative RHS) + return xL - p * p > math.log(U_upper / p ** 6) + 1e-9 + + +def series_error_fails(p, length_exp): + """certified failure of the bound route: U*(1-x)^L >= p^6 exp(-p^2), using (1-x)^L >= exp(-xL - x^2 L)""" + x = F(1, p ** 22) + L = p ** length_exp + lower_exp = x * L + x * x * L + U_lower = 8 * p * p + return math.log(U_lower / p ** 6) - float(lower_exp) > -p * p + 1e-9 + + +def main(): + pins() + for p in range(2, PMAX + 1): + U = exact(p) + if p == 2: + U2 = U + # general p >= 2 by p < 2^p (B): 512 p^4 < 2^(4p+9) <= 2^(32760p) = D + need(all(p < 2 ** p for p in range(2, 200)), "p < 2^p sample") # induction: 2^(p+1) = 2*2^p > 2p >= p+1 + need(4 * 2 + 9 <= 32760 * 2 and 32760 - 4 > 0, "4p+9 <= 32760p for p >= 2") + # with r < 1/(16p^2): V = 8p^2/(1-r) < 8p^2 (1 + 2r) < 8p^2 + 1; 8p^2 + 1 <= 16p^2 - 1 iff p^2 >= 1/4; + # 16p^2 - 1 < p^6 iff p^4 >= 16; (8p^2+1)^2 < p^11: p = 2 gives 1089 < 2048, p >= 3 gives <= 81 p^4 <= p^8. + need(33 ** 2 < 2 ** 11 and 64 + 16 + 1 <= 81 <= 3 ** 4, "V^2 < p^11 for all p") + # Neumann series error at L = p^24 holds; lengths and endpoints one lower fail on this route at p = 2 + need(all(series_error_ok(p, 24) for p in range(2, PMAX + 1)), "S: error < p^6 exp(-p^2) at L = p^24") + need(series_error_fails(2, 23), "series length 23 fails at p = 2") + need(U2 > 2 ** 5 and U2 * U2 > 2 ** 10, "endpoint 10 and normalizer 5 fail at p = 2") + need((2 * 2 ** 24 + 1) * 1 > 2 ** 25, "loose radius exceeds p^25 at p = 2") + need(all((2 * p ** 24 - 1) * (p - 1) > p ** 25 for p in range(3, PMAX + 1)), "sharp radius exceeds p^25, p >= 3") + need((2 * 2 ** 24 - 1) * 1 < 2 ** 25, "sharp radius stays below p^25 at p = 2 (only the loose count fails)") + print(json.dumps({"status": "PASS_DELTA_HALO_EXPONENT_CHECK", "exact_p_range": [2, PMAX], + "exponents": {"spectral_endpoint": 11, "series_length": 24, "bandwidth": 26, + "agreement_distance": 26, "normalizer": 6}, + "U_at_p2": f"{float(U2):.12f}", "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())