From 5fad1d2e9ae4e1ac269a812b024c9c53024603ec Mon Sep 17 00:00:00 2001 From: Mihir Srivastava Date: Wed, 21 Oct 2026 19:23:25 -0700 Subject: [PATCH] Audit cross-cell rounding and inverse bounds independently --- .../README.md | 281 ++++++++++++++++++ .../RESULT.json | 29 ++ .../REVIEWED.json | 20 ++ .../SOURCES.json | 36 +++ .../TASK.json | 120 ++++++++ .../VERIFY.json | 23 ++ .../reviewed/README.md | 105 +++++++ .../reviewed/verify.py | 101 +++++++ .../verify.py | 232 +++++++++++++++ 9 files changed, 947 insertions(+) create mode 100644 research/delta-cross-cell-independent-audit/README.md create mode 100644 research/delta-cross-cell-independent-audit/RESULT.json create mode 100644 research/delta-cross-cell-independent-audit/REVIEWED.json create mode 100644 research/delta-cross-cell-independent-audit/SOURCES.json create mode 100644 research/delta-cross-cell-independent-audit/TASK.json create mode 100644 research/delta-cross-cell-independent-audit/VERIFY.json create mode 100644 research/delta-cross-cell-independent-audit/reviewed/README.md create mode 100644 research/delta-cross-cell-independent-audit/reviewed/verify.py create mode 100644 research/delta-cross-cell-independent-audit/verify.py diff --git a/research/delta-cross-cell-independent-audit/README.md b/research/delta-cross-cell-independent-audit/README.md new file mode 100644 index 0000000000..3c06827177 --- /dev/null +++ b/research/delta-cross-cell-independent-audit/README.md @@ -0,0 +1,281 @@ +# Independent audit of the cross-cell rounding and inverse bounds in PR #4462 + +**Result: the two conditional lemmas hold.** This answers the explicit request +for a different contributor to check [#4462](https://github.com/CrocSwap/integer-mult-bounds/pull/4462) +at `89548dc186c9c90d459085b6d1be4834977705b9`. It supplies an independent written +derivation of the inverse approximation and locality steps, an explicit combined +within/across-cell rounding budget, and a separately written rational matrix +verifier with six failure controls. **No new kappa or selected-frontier change.** + +The original paper claims, ideal Gaussian gaps and production page generator +remain hypotheses. This is a conditional matrix proof with exact finite checks, +not a formal-kernel proof or an independent human review. It does not certify the +full multiplication theorem or the Schur/tensor extensions. + +## 1. Contract and relation to the caller + +Let integer `p >= 2`, `0 <= W <= p-1`, and let `H` be a finite square complex +matrix with diagonal exactly one and half-bandwidth `W`. Both the absolute row +and column off-sums of an ideal nonnegative matrix `N` are at most `1-g`, where + +``` +g = 1/(8p^2), delta = 2^(2-32760p), eta = 2^(-32768p). +``` + +Within each cell assume `|H_ij| <= N_ij/(1-delta)`. Across cells either use +`0 <= H_ij <= N_ij` (Lemma A), or permit an absolute rounding error `e` from +`N_ij` (the mixed application of Lemma B). These are off-diagonal conditions; +the diagonal stays exactly one, including at cuts. Principal sections inherit +the hypotheses. The locality argument also applies on a cycle using the +inherited graph distance, provided the section really agrees with the full +matrix on all retained entries. + +The three live input notes in [SOURCES.json](SOURCES.json) establish the source +context, not these hypotheses independently: LOG-A specifies downward entries +across cells and a unit diagonal; FINE-PRIME uses rounded entries and states an +eventual row/column perturbation `poly(p) 2^(-(C-o(1))p)`; the downstream report +sets `P=32768p`. The selected #4359 review continues to retain analytic/native +assumptions. The #4100 claim is not the selected theorem. + +Exact snapshots of #4462's README and verifier, including their original credit, +are in `reviewed/`; [REVIEWED.json](REVIEWED.json) records their original commit, +Git blobs and SHA256 hashes. The new verifier authenticates but never imports or +executes them. Its rational matrix implementation was written separately after +reading the audited claim and code; this is not a blind replication. + +## 2. Downward transfer and the mixed rounding ledger + +For any fixed row or column split the ideal off-sum as `T_in + T_out <= 1-g`. +Under Lemma A, + +``` +off(H) <= T_in/(1-delta) + T_out <= (1-g)/(1-delta). +``` + +The second inequality follows by subtracting `T_in+T_out` after multiplying by +`1-delta`: the difference is `-delta*T_out <= 0`. Thus its gap is at least +`(g-delta)/(1-delta)`, giving the same ceiling as #4462: + +``` +U = (1-delta)/(g-delta) = 8p^2 (D-4)/(D-32p^2), D=2^(32760p). +``` + +Here `||H^-1||_1, ||H^-1||_infinity, ||H^-1||_2 <= U`; the bound on `U` need +not be strict when the premises are non-strict. The stronger comparison with +`10p^2` below is strict. + +The per-entry statement needs its reference specified. If **every** entry is +within `e=1/(64p^4)` of `N`, there are at most `2W` errors in each off-sum, so +the excess is at most `2(p-1)e < 1/(32p^3)`. If instead that error bound only +applies **across cells**, the within-cell ratio error must also be charged: + +``` +off(H) <= (1-g) + delta*T_in/(1-delta) + 2W e + <= (1-g) + 2delta + 2(p-1)e. +``` + +The constants still suffice. For every integer `p>=2`, `p<=2^(p-1)` (induction +from `p=1`, since `p+1<=2p`). Consequently + +``` +128p^4 <= 2^(4p+3) < 2^(32760p-2), +delta < 1/(128p^4) < 1/2, +2delta + 2(p-1)e < (2p-1)/(64p^4) < 1/(32p^3). +``` + +This supplies the combined budget that #4462 leaves implicit when moving +between its two readings. It also handles a raw oracle with `|z-N_ij|<2eta`: +`64p^4 <= 2^(4p+2) < 2^(32768p-1)` implies `2eta=2`. +Negative rounded outputs cause no problem: `|z|<=N_ij+|z-N_ij|`. +No source change or actual page-generator implementation is asserted here. + +## 3. Robust inverse and spectral bounds + +Assume directly, as in Lemma B, that **both** absolute row and column off-sums +of `H` are at most `1-g+rho`, with `rho<=1/(32p^3)`. Put + +``` +q = g - 1/(32p^3) = (4p-1)/(32p^3). +``` + +Writing `H=I+E`, both induced norms of `E` are at most `1-q<1`. The Neumann +series gives the two inverse norm bounds `<=1/q`; the inequality +`||A||_2 <= sqrt(||A||_1 ||A||_infinity)` gives the same 2-norm bound. Since + +``` +q >= 7/(64p^2) > 1/(10p^2), +100 < 2^7 <= p^7, 10 < 2^4 <= p^4, +``` + +we obtain `||H^-1||_2<10p^21` from zero to `x`), + +``` +||H^-1-P_L||_2 < (1-p^-22)^(p^24) ||H^-1||_2 + < p^6 exp(-p^2). +``` + +This is an all-p argument, not a numerical evaluation of an enormous matrix +power. Since each `H` or `H*` step changes index by at most `W`, a monomial in +`Q^j H*` has at most `2j+1` such steps. Thus `P_L` has half-bandwidth at most +`(2L-1)W`. A row at distance **greater than** `(2L-1)W` from omitted section +indices has identical restricted and full polynomial rows: every path in the +matrix product stays in the section. This does not assert equality of the +two exact inverse rows. Their difference can subsequently be bounded using +both approximation errors. + +The predecessor's more conservative agreement distance `(2L+1)W` also fits +under `p^26`. Indeed + +``` +p^26 - (2p^24+1)(p-1) = p^24((p-1)^2+1) - p + 1 > 0 +``` + +for `p>=2`, since `p^24>=p` and the bracket is at least two. This verifies +length 24 and both bandwidth/agreement exponents 26. It does not transfer +them to a Schur complement or certify a core/halo geometry. + +## 5. Discriminating exact fixtures + +The new standard-library verifier uses rational Gauss-Jordan elimination and +matrix multiplication, not the predecessor's scalar-only replay. It checks: + +- scalar identities and conservative bounds at every integer `p=2..512`, with + the universal justification in sections 2-4; +- 24 four-by-four mixed-cell matrices: every contiguous partition and three + signed cross-cell error patterns, including nonnormal cases, using the + deliberately larger delta envelope `1/(128p^4)` at `p=3`; +- all 16 sign vectors per mixed matrix, both exact inverse identities, and + both induced inverse norms; +- exact nonnormal polynomial residuals at lengths 1-4, an interior row + agreement fixture, and failure of that agreement near a cut; +- six controls: omit row control, omit column control, increase excess beyond + the spectral tolerance, omit the unit diagonal, reverse the residual order, + or claim near-face polynomial agreement. + +The one-sided controls are substantive. At `p=2`, let `r=249/256` and take the +six-by-six unit-diagonal matrix with `H[0,1]=-r` and `H[i,i-1]=-r` for +`i=1..5`. It has bandwidth one and every row off-sum equals the allowed `r`, +but one column off-sum is `2r`. Its inverse on `e_0` is + +``` +x_i = r^i/(1-r^2), i=0..5, +||x||_2^2 = 6342978758591946527831281/3517374640846117273600 > 1600. +``` + +Therefore `||H^-1||_2>40=10p^2`: the row hypothesis alone is insufficient. +Transposition gives the column-only counterexample. These are generic contract +controls, not examples satisfying the ideal Gaussian hypotheses of Lemma A. + +The reported `p=2` threshold is also corroborated. A symmetric two-by-two +matrix with diagonal one and off-diagonal `-(31/32+rho)` has the eigenvector +`(1,1)` with eigenvalue `1/32-rho`. For `0<=rho<1/32`, spectral endpoint 11 +holds exactly when + +``` +rho < 1/32 - 2^(-11/2). +``` + +Exact rational squaring puts this threshold strictly between `91/10000` and +`92/10000`. The budget `1/256` is safely below it. This demonstrates sharpness +of the generic off-sum implication, not an optimum for Gaussian matrices or +for the sufficient ceiling `10p^2`. + +## Reproduce and evidence + +```sh +python3.12 -B scripts/research_package.py --package research/delta-cross-cell-independent-audit --check-only +python3.12 -B scripts/research_package.py --package research/delta-cross-cell-independent-audit +python3.12 -O -I -B research/delta-cross-cell-independent-audit/verify.py +``` + +The direct verifier also runs from a committed package export with the three +declared input files and no Git or third-party libraries. It prints +`PASS_DELTA_CROSS_CELL_INDEPENDENT_AUDIT`. Checks use explicit exceptions and +remain active under `-O`. [RESULT.json](RESULT.json) records the finite receipt; +passing checks support, but do not formally prove, the written universal steps. + +Environment: Windows, CPython 3.12.0. Linux execution and a formal proof-kernel +replay were not run. The generic source-binding baseline was attempted but +stopped at the sparse omission `research/kappa-0023-productive-jobs`; this audit +does not report it or the selected cold replay as passed. The exact selected +record, review, source manifest and certificate were read. + +Local validation passed: registered metadata and replay, direct optimized +replay, committed-byte preflight (12 package/input files), export integrity, +and optimized replay of that export with an identical RESULT.json. The optional +full source-history preflight was not run in this shallow clone. All replay +inputs are either on the base commit or retained inside this package; the +unmerged predecessor commit is not needed to run the standalone verifier. + +## Coordination, coverage and limits + +Base: canonical main `2a13eb1827784206202db90e5dc8327cf8a250db`, priority +revision 7, selected conditional kappa `23/10000`. +[Discussion #4498](https://github.com/CrocSwap/integer-mult-bounds/discussions/4498) +is the canonical investigation, answering [the #1166 handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19111508). + +The initial overlap refresh covered 351 open PRs (including drafts) and 3,375 +discussion records with complete pagination. Local notes were sparse: 5,730 +of 5,731 tracked note paths were initially absent. No novelty claim follows. +Live search and the relevant package inspection identified #4462 (audited), +#4473 (its independent-check request), #4472 (rounding-contract audit), and +#4481 (distinct Schur follow-up). The card was retrieved explicitly after the +handoff selection, not rerolled. Final freshness is recorded in TASK.json. + +No ideal Gaussian row/column gap, analytic truncation estimate, raw exponential +oracle implementation, physical page generator, Schur transfer, tensor/core +error, native/stock budget or integer multiplication theorem is verified here. +FINE-PRIME's stated exponentially small perturbation eventually meets the +budget for a fixed positive C, but no effective threshold is computed and no +uniformity of hidden constants is supplied by this audit. + +## Open next questions + +Does the actual page generator meet the **combined** within/across-cell error +ledger for both rows and columns? This matters because the matrix implication +alone does not supply its caller hypotheses. Pin one emitted reference block +and reconstruct all diagonals, band entries and certified perturbations. An +all-size conclusion still needs a certified ideal gap and a uniform generator +argument; small matrices alone cannot provide them. #4481's Schur follow-up is +already separate work and is not proposed here as a new assignment. + +## Credit + +Ryanson Jonathan / pinterbanget supplied #4462's conditional transfer and +robustness lemmas and requested another contributor's check; its snapshots +retain his Claude Code / Claude Opus 5.5 disclosure. James Reed / jwr404 supplied +the column split and exponent chain (#4442, #4451, #4452). The #4449 across-cell +rounding contract is credited to mihir-s-05 with OpenAI assistance; this audit +does not independently reprove that predecessor. Cinna Davis and the retained +LOG-A, FINE-PRIME and rad20 authors retain their source attribution. + +Prepared by mihir-s-05 with substantial OpenAI Codex assistance. The matrix +Neumann series, norm inequalities and finite geometric-series identity are +classical; no priority claim is made. New work and retained snapshots are +Apache-2.0. No independent human or formal-kernel verification is claimed. diff --git a/research/delta-cross-cell-independent-audit/RESULT.json b/research/delta-cross-cell-independent-audit/RESULT.json new file mode 100644 index 0000000000..fdb0461879 --- /dev/null +++ b/research/delta-cross-cell-independent-audit/RESULT.json @@ -0,0 +1,29 @@ +{ + "status": "PASS_DELTA_CROSS_CELL_INDEPENDENT_AUDIT", + "authenticated_files": 5, + "scalar_p_cases": 511, + "mixed_matrix_cases": 24, + "polynomial_checks": { + "residual_lengths": [ + 1, + 2, + 3, + 4 + ], + "locality_fixture_order": 9 + }, + "boundary_controls": { + "row_only_inverse_column_squared_norm": "6342978758591946527831281/3517374640846117273600", + "claimed_ceiling_squared": 1600, + "controls": [ + "row-only", + "column-only", + "excess-0.0092", + "missing-unit-diagonal", + "nonnormal-wrong-residual-side", + "near-face-agreement" + ] + }, + "new_kappa_claimed": false, + "scope": "Exact finite checks support the separate all-p conditional proof; no Gaussian gap, generator, Schur or full theorem verification." +} diff --git a/research/delta-cross-cell-independent-audit/REVIEWED.json b/research/delta-cross-cell-independent-audit/REVIEWED.json new file mode 100644 index 0000000000..bf12ed5ed8 --- /dev/null +++ b/research/delta-cross-cell-independent-audit/REVIEWED.json @@ -0,0 +1,20 @@ +{ + "repository": "https://github.com/pinterbanget/integer-mult-bounds", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/4462", + "commit": "89548dc186c9c90d459085b6d1be4834977705b9", + "files": [ + { + "path": "reviewed/README.md", + "source_path": "research/delta-cross-cell-transfer/README.md", + "git_blob": "95c8244b537e1d3ee047683308997a0662b99800", + "sha256": "97d4e9fb2cadc24ca39a236f1b01d0c0007530da407a4d049e8a24dd0962160d" + }, + { + "path": "reviewed/verify.py", + "source_path": "research/delta-cross-cell-transfer/verify.py", + "git_blob": "11ed76d670b58cc7365646e0492e631cf6ba7240", + "sha256": "b773dccb85d1dd35bb517bd7b45777de1db426edcadcf176c9af5ffba8c1b520" + } + ], + "credit": "Ryanson Jonathan; substantial Claude Code (Claude Opus 5.5) assistance; Apache-2.0. These exact snapshots are evidence only, never imported or executed by this audit." +} diff --git a/research/delta-cross-cell-independent-audit/SOURCES.json b/research/delta-cross-cell-independent-audit/SOURCES.json new file mode 100644 index 0000000000..96847e7720 --- /dev/null +++ b/research/delta-cross-cell-independent-audit/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/capped-fusion-t74-k554/vendor/pr1786/FINE-PRIME-PADDING.md", + "usage": "input", + "git_blob": "bf9899ee21be4058e4aac0b64bfa67d01ee8ddd3", + "sha256": "47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce" + }, + { + "path": "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md", + "usage": "input", + "git_blob": "3bcf490a8c164d44aff5b7e2ec2e0f4bf07d7a73", + "sha256": "e05d6b8596c80b6e8676569a0ff464a29fa704c3304143f58914f47cdf38b272" + } + ] +} diff --git a/research/delta-cross-cell-independent-audit/TASK.json b/research/delta-cross-cell-independent-audit/TASK.json new file mode 100644 index 0000000000..d5d0c03815 --- /dev/null +++ b/research/delta-cross-cell-independent-audit/TASK.json @@ -0,0 +1,120 @@ +{ + "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": "Independent conditional audit of PR4462 Lemmas A/B, including combined within/across error, Neumann inverse approximation, locality and sharp failure controls.", + "scope_change_reason": "Accept the explicit different-contributor check requested in #1166 comment 19111508 and #4473. Stop before #4481 Schur propagation.", + "bottleneck_link": "Checks one retained precision/conditioning implication at the banded Gaussian reference; leaves the ideal gaps, generator and full multiplication theorem as premises.", + "budget_minutes": 60, + "stop_rule": "Stop at a proved conditional banded-reference implication or precise counterexample. No full supplier replay, Schur/tensor extension or new kappa.", + "outcome": "completed", + "evidence": "All-p conditional proof of both PR4462 lemmas, combined within/across error ledger, exact inverse approximation/locality derivation. Independent rational checks: 511 p cases, 24 mixed matrices, 384 sign-vector responses, six failure controls. No new kappa.", + "author": "mihir-s-05 with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance; separate implementation, not an independent human or formal proof-kernel review.", + "open_questions": [ + { + "question": "Does the actual page generator meet the simultaneous row/column error ledger, including its within-cell ratios and across-cell rounding?", + "why_it_matters": "This audit proves a conditional matrix implication and does not instantiate its hypotheses on the production generator.", + "first_step": "Pin one emitted reference block and reconstruct every diagonal, band entry and row/column perturbation with exact interval certificates.", + "blocked_by": "A source-bound production page generator and certified ideal gap; finite samples alone do not establish the all-size contract." + } + ], + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4498", + "predecessor_head": "89548dc186c9c90d459085b6d1be4834977705b9", + "upstream_refresh": { + "commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "priority_revision": 7, + "checked_utc": "2026-10-22T02:22:07.5917417+00:00" + }, + "baseline_check": "Attempted python -B scripts/research_baseline.py; blocked by sparse omission research/kappa-0023-productive-jobs. Selected record, review, source manifest and certificate were read; no selected replay PASS claimed.", + "overlap_refresh": { + "open_prs": { + "fetched_at": "2026-10-22T02:22:04.965281+00:00", + "complete_pagination": true, + "records": 352 + }, + "discussions": { + "fetched_at": "2026-10-22T02:23:20.147518+00:00", + "complete_pagination": true, + "records": 3378 + }, + "local_note_limitation": "Sparse checkout; initial scan omitted 5730/5731 tracked note paths. Final scan omitted 5729/5733. Relevant sources and PR head were read directly. No novelty inference.", + "relevant_prs": [ + 4462, + 4473, + 4472, + 4481 + ], + "decision": "Continue the explicitly requested independent audit; no competing check of this exact scope found in the covered records." + }, + "validation": { + "environment": "Windows, CPython 3.12.0, standard library only", + "passed": [ + "registered metadata/pins", + "registered replay", + "optimized isolated direct replay", + "committed-byte preflight: 12 files", + "committed export integrity", + "optimized export replay equal to RESULT.json" + ], + "unrun": [ + "Linux execution", + "formal proof-kernel verification", + "selected cold replay", + "optional full source-history preflight (shallow clone)" + ], + "scientific_boundary": "Written all-p conditional matrix proof plus exact finite evidence; all ideal-gap, generator, Schur/tensor and native/outer assumptions remain." + } +} diff --git a/research/delta-cross-cell-independent-audit/VERIFY.json b/research/delta-cross-cell-independent-audit/VERIFY.json new file mode 100644 index 0000000000..6f56099db7 --- /dev/null +++ b/research/delta-cross-cell-independent-audit/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md", + "research/capped-fusion-t74-k554/vendor/pr1786/FINE-PRIME-PADDING.md", + "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticated sources; exact scalar budgets; rational matrix inverse and polynomial identities; signed mixed rounding; row-only, column-only, diagonal, excess, residual-side and boundary controls. Universal implications are proved in README.md." + } + ] +} diff --git a/research/delta-cross-cell-independent-audit/reviewed/README.md b/research/delta-cross-cell-independent-audit/reviewed/README.md new file mode 100644 index 0000000000..95c8244b53 --- /dev/null +++ b/research/delta-cross-cell-independent-audit/reviewed/README.md @@ -0,0 +1,105 @@ +# The δ halo exponents 11, 24, 26, 26 and 6 transfer across cells, and survive the "rounded" reading + +**Claim type:** a conditional transfer lemma plus a robustness lemma, with exact rational checks. +**No new κ.** It answers the open question of jwr404's +[#4452](https://github.com/CrocSwap/integer-mult-bounds/pull/4452) and of my #4460: do the within-cell +δ exponents survive on the banded reference across cells? The ideal gaps `1/(8p²)` stay hypotheses. + +## Setting + +The banded reference `H` has diagonal exactly one and bandwidth `W ≤ p − 1`. The ideal Gaussian matrix +`N` has row and column off-sums `T ≤ 1 − g`, where `g = 1/(8p²)`. Within cells, `|H| ≤ N/(1 − δ)` with +`δ = 2^{2−32760p}`, as in #4451 and #4452. + +## Lemma A: the downward reading + +LOG-A says "across cells, use the retained downward Gaussian entries", and #4449 proves the matching +contract `0 ≤ H ≤ n`. Split each off-sum as `T = T_in + T_out`. Then + + off(H) ≤ T_in/(1−δ) + T_out ≤ T/(1−δ) ≤ (1−g)/(1−δ), + +because `(1−δ)[T_in/(1−δ) + T_out] − T = −δ·T_out ≤ 0`. This is #4442's column split with δ in place +of `1/(16p²)`. The global Neumann ceiling is therefore exactly #4452's +`U = 8p²(D−4)/(D−32p²)`, so all five exponents transfer verbatim. + +## Lemma B: any reading with a small excess + +Suppose every row and column off-sum of `|H|` is at most `(1 − g) + ρ`, with `ρ ≤ 1/(32p³)`. Then +`1 − off ≥ (4p−1)/(32p³) ≥ 7/(64p²) > 1/(10p²)`. Hence: + +- `‖H^{−1}‖₂ < 10p²`, so `100p⁴ < p^{11}` gives spectral endpoint 11; +- `10p² < p⁶` gives normalizer 6; +- the series error `< 10p²·e^{−p²} < p⁶e^{−p²}` at length `p^{24}`; +- bandwidth and agreement distance stay below `p^{26}`. + +Per entry, an absolute error `e ≤ 1/(64p⁴)` on the at most `2W` band entries of a row or column is +enough. The downward reading has `ρ ≤ 2δ`, far inside this budget. + +**Why this matters.** #4442 noted that FINE-PRIME says "rounded Gaussian entries" where LOG-A says +"downward". Under the coarser ceiling `16p² − 1`, an overshoot of one part in 64 already broke the +argument at `p = 2`. Under δ, the exponents no longer depend on the direction of rounding. Any rounding +with absolute error at most `1/(64p⁴)` per entry works. In particular FINE-PRIME's own +`poly(p)·2^{−(C−o(1))p}` row and column perturbation works eventually, which matches the eventual +status of the ideal gaps. + +**#4449's repair is not needed for these exponents.** The raw negative-exponential oracle output `z`, +with `|z − n| < 2η` and `η = 2^{−32768p}`, has a per-row excess of at most `2(p−1)·2η`. That is far +below `1/(32p³)`, and the verifier checks it for every `p` from 2 to 64. Downward repair (#4449) is still +what gives the exact ceiling `U` of Lemma A. + +**Near-tightness at `p = 2`.** On this route the excess tolerance at `p = 2` lies in +`(0.0091, 0.0092)`. The budget `1/(32p³) = 1/256` sits inside it. + +## Checks + +`verify.py` checks: + +- the pinned LOG-A, FINE-PRIME and downstream phrases; +- the split identity, as a polynomial identity of degree at most 2 per variable, on a 3×3×3 grid + (which proves it identically); +- Lemma A's ceiling and exponents, exactly for `p` in 2..64, at several within/across shares; +- Lemma B's gap, `B`, endpoint, normalizer, per-entry budget and bandwidth, exactly for `p` in 2..64, + together with the all-`p` inequalities `70 > 64`, `100 < p⁷` and `10 < p⁴`; +- the `p = 2` tolerance interval. + +| | value | +| --- | --- | +| global ceiling, downward reading, `p = 2` | `U = 32.000…` (just above 32) | +| robust excess budget | `1/(32p³)` per row or column | +| per-entry budget | `1/(64p⁴)` | +| `p = 2` tolerance | in `(0.0091, 0.0092)` | + +## Not covered + +- The ideal gaps `1/(8p²)`. +- Whether an existing page generator implements either rounding. +- The Schur complement and the core exponent 400. +- The #4100 notes, which keep 20, 42, 45, 48 and 100. +- Any new κ. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/delta-cross-cell-transfer --check-only +python3.12 -B scripts/research_package.py --package research/delta-cross-cell-transfer +``` + +The verifier prints `PASS_DELTA_CROSS_CELL_TRANSFER` in about 45 seconds, using only the standard +library. + +## Open next questions + +1. **Do the smaller exponents propagate through the Schur complement?** + - *Why it matters:* the core exponent 400 still dominates the agreement distance 26. + - *First step:* restate the interior elimination's row-dominance gap with `B < 10p²` in place of + `16p² − 1`. + +## Credit + +- The column split, the exponent route and the question are James Reed's (jwr404: #4442, #4451, + #4452). +- The across-cell rounding contract is mihir-s-05's (#4449). +- The source sentences come from LOG-A, FINE-PRIME and the 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-cross-cell-independent-audit/reviewed/verify.py b/research/delta-cross-cell-independent-audit/reviewed/verify.py new file mode 100644 index 0000000000..11ed76d670 --- /dev/null +++ b/research/delta-cross-cell-independent-audit/reviewed/verify.py @@ -0,0 +1,101 @@ +#!/usr/bin/env python3 +"""Across-cell transfer of the delta halo exponents 11, 24, 26, 26, 6 (#4452), and robustness to the rounded reading. + +Setting (#4442/#4452): banded reference H, diagonal exactly one, bandwidth W <= p-1, ideal Gaussian matrix N with +row and column off-sums T <= 1 - g, g = 1/(8p^2). Within-cell entries obey |H| <= N/(1-delta), delta = 2^(2-32760p). + (A) Downward reading (LOG-A, #4449: 0 <= H <= n across cells). Split T = T_in + T_out: + off(H) <= T_in/(1-delta) + T_out <= T/(1-delta) <= (1-g)/(1-delta), + because (1-delta)[T_in/(1-delta) + T_out] - T = -delta T_out. So the global Neumann ceiling is #4452's + U = 8p^2(D-4)/(D-32p^2) and the five exponents transfer verbatim. + (B) Any reading with excess rho: if every row and column off-sum of |H| is at most (1-g) + rho with + rho <= 1/(32p^3), then 1 - off >= (4p-1)/(32p^3) >= 7/(64p^2) > 1/(10p^2), so ||H^-1||_2 < 10p^2 with 100p^4 < p^11 + and B < p^6: endpoint 11, length 24, bandwidth/agreement 26 and normalizer 6 hold. Per entry, an absolute + error e <= 1/(64p^4) on the <= 2W band entries suffices. The downward reading has rho <= 2 delta. +Exact rational checks for p = 2..64; the split identity is a polynomial identity of degree <= 2 per variable, checked +on a 3x3x3 grid (hence identically). The tolerance is near-tight at p = 2 on this route. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as F +import hashlib +import itertools +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PMAX = 64 + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def pins(): + for row in json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["files"]: + need(hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], row["path"]) + loga = (ROOT / "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md").read_text(encoding="utf-8") + fine = (ROOT / "research/capped-fusion-t74-k554/vendor/pr1786/FINE-PRIME-PADDING.md").read_text(encoding="utf-8") + down = (ROOT / "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md").read_text(encoding="utf-8") + need("across cells, use the retained downward Gaussian entries; set H_jj=1." in loga, "LOG-A downward phrase") + need("across cells use rounded\nGaussian entries, with diagonal exactly one." in fine, "FINE-PRIME rounded phrase") + need("poly(p) 2^(-(C-o(1))p)` in row and column norm" in fine, "FINE-PRIME perturbation phrase") + need("Set P=32768p and eta=2^(-P)." in down, "downstream precision") + + +def split_identity(): + # (1-d)[a/(1-d) + (t-a)] - t + d(t-a) == 0 as a polynomial in (a, t, d), degree <= 2 in each variable + vals = [F(1, 7), F(2, 5), F(3, 4)] + for a, t, d in itertools.product(vals, repeat=3): + need((1 - d) * (a / (1 - d) + (t - a)) - t + d * (t - a) == 0, "split identity") + + +def downward(p): + D = 2 ** (32760 * p) + delta, g = F(4, D), F(1, 8 * p * p) + U = F(8 * p * p * (D - 4), D - 32 * p * p) + for t_in_share in (F(0), F(1, 3), F(1)): + T = 1 - g + off = t_in_share * T / (1 - delta) + (1 - t_in_share) * T + need(off <= T / (1 - delta) and 1 / (1 - off) <= U, "A: global ceiling is U") + need(U * U < p ** 11 and U < p ** 6 and T / (1 - delta) < 1, "A: exponents 11 and 6") + need(T / (1 - delta) - T <= 2 * delta <= F(1, 32 * p ** 3), "downward excess within the robust budget") + return U + + +def robust(p): + g, rho = F(1, 8 * p * p), F(1, 32 * p ** 3) + off = 1 - g + rho + need(off < 1 and 1 - off == F(4 * p - 1, 32 * p ** 3) >= F(7, 64 * p * p) > F(1, 10 * p * p), "B: gap") + B = 1 / (1 - off) + need(B * B < p ** 11 and B < p ** 6 and B < 10 * p * p and 100 * p ** 4 < p ** 11 and 10 * p * p < p ** 6, "B: endpoint 11, normalizer 6") + need(2 * (p - 1) * F(1, 64 * p ** 4) <= rho, "B: per-entry error 1/(64p^4)") + # the raw exponential oracle (|z - n| < 2 eta, eta = 2^-32768p, no downward repair) on <= 2W = 2(p-1) entries + need(2 * (p - 1) * 2 * F(1, 2 ** (32768 * p)) <= rho, "B: raw oracle output fits the budget") + L = p ** 24 + need((2 * L - 1) * (p - 1) < p ** 26 and (2 * L + 1) * (p - 1) < p ** 26, "bandwidth/agreement 26") + + +def main(): + pins() + split_identity() + for p in range(2, PMAX + 1): + U = downward(p) + robust(p) + if p == 2: + U2 = U + # all p >= 2: (4p-1)/p >= 7/2; 70 > 64; 100 < p^7 and 10 < p^4 for p >= 2 + need(2 * (4 * 2 - 1) >= 7 * 2 and 70 > 64 and 100 < 2 ** 7 and 10 < 2 ** 4, "B for all p >= 2") + # near-tightness at p = 2: the exponent-11 route needs (1 - off)^2 * 2^11 > 1 with off = 31/32 + rho + ok = lambda rho: (1 - (F(31, 32) + rho)) ** 2 * 2 ** 11 > 1 + need(ok(F(91, 10000)) and not ok(F(92, 10000)), "p = 2 tolerance lies in (0.0091, 0.0092)") + need(F(1, 256) < F(91, 10000), "the budget 1/(32p^3) = 1/256 at p = 2 is within it") + print(json.dumps({"status": "PASS_DELTA_CROSS_CELL_TRANSFER", "exact_p_range": [2, PMAX], + "downward_global_ceiling_U_p2": f"{float(U2):.12f}", "robust_excess_budget": "1/(32p^3)", + "per_entry_budget": "1/(64p^4)", "p2_tolerance_interval": [0.0091, 0.0092], + "exponents": [11, 24, 26, 26, 6], "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/research/delta-cross-cell-independent-audit/verify.py b/research/delta-cross-cell-independent-audit/verify.py new file mode 100644 index 0000000000..61a8f36b79 --- /dev/null +++ b/research/delta-cross-cell-independent-audit/verify.py @@ -0,0 +1,232 @@ +#!/usr/bin/env python3 +"""Independent exact checks of PR4462's conditional matrix implications. + +mihir-s-05 with substantial OpenAI Codex assistance. Apache-2.0. +The reviewed author's verifier is authenticated as evidence, never executed. +Universal arguments, including spectral and exponential steps, are in README.md. +""" +from fractions import Fraction as F +from hashlib import sha256, sha1 +from pathlib import Path +import itertools +import json + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(): + rows = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8'))['files'] + count = 0 + for row in rows: + if row['usage'] == 'input': + data = (ROOT / row['path']).read_bytes() + require(sha256(data).hexdigest() == row['sha256'], 'source drift: ' + row['path']) + count += 1 + review = json.loads((HERE / 'REVIEWED.json').read_text(encoding='utf-8')) + for row in review['files']: + data = (HERE / row['path']).read_bytes() + require(sha256(data).hexdigest() == row['sha256'], 'review snapshot drift') + require(sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() == row['git_blob'], + 'review Git blob mismatch') + count += 1 + return count + + +def eye(n): + return [[F(i == j) for j in range(n)] for i in range(n)] + + +def transpose(a): + return [list(row) for row in zip(*a)] + + +def add(a, b, sign=1): + return [[x + sign*y for x, y in zip(ar, br)] for ar, br in zip(a, b)] + + +def scale(a, c): + return [[c*x for x in row] for row in a] + + +def mul(a, b): + return [[sum((x*y for x, y in zip(row, col)), F(0)) for col in transpose(b)] for row in a] + + +def inverse(a): + n = len(a) + aug = [row[:] + unit for row, unit in zip(a, eye(n))] + for j in range(n): + pivot = next((i for i in range(j, n) if aug[i][j]), None) + require(pivot is not None, 'singular matrix') + aug[j], aug[pivot] = aug[pivot], aug[j] + d = aug[j][j] + aug[j] = [x/d for x in aug[j]] + for i in range(n): + if i != j: + d = aug[i][j] + aug[i] = [x-d*y for x, y in zip(aug[i], aug[j])] + return [row[n:] for row in aug] + + +def norm_inf(a): + return max(sum(map(abs, row)) for row in a) + + +def off_bounds(a): + b = [[abs(x) if i != j else F(0) for j, x in enumerate(row)] for i, row in enumerate(a)] + return norm_inf(b), norm_inf(transpose(b)) + + +def polynomial(a, c, length): + unit = eye(len(a)) + q = add(unit, scale(mul(transpose(a), a), c), -1) + power, total = unit, scale(unit, F(0)) + for _ in range(length): + total = add(total, power) + power = mul(power, q) + return scale(mul(total, transpose(a)), c), power + + +def scalar_checks(): + # README proves this small rational delta envelope for every p >= 2; + # do not reproduce the predecessor's million-bit D arithmetic in a loop. + for p in range(2, 513): + gap, budget, e = F(1, 8*p*p), F(1, 32*p**3), F(1, 64*p**4) + envelope = F(1, 128*p**4) + require(32760*p-2 > 4*p+3, 'delta exponent envelope') + require(32768*p-1 > 4*p+2, 'raw oracle exponent envelope') + require(2*envelope + 2*(p-1)*e < budget, 'combined within/across budget') + q = gap-budget + require(q == F(4*p-1, 32*p**3) and q >= F(7, 64*p*p), 'robust gap') + require(q > F(1, 10*p*p) and q*q*p**11 > 1 and 1/q < p**6, 'inverse endpoints') + require(100 < p**7 and 10 < p**4, 'monotone endpoint inequalities') + length = p**24 + require((2*length-1)*(p-1) < p**26, 'polynomial bandwidth') + require((2*length+1)*(p-1) < p**26, 'conservative agreement radius') + margin = p**24*((p-1)**2+1) - p + 1 + require(p**26-(2*p**24+1)*(p-1) == margin and margin > 0, 'radius margin') + for share in (F(0), F(1, 5), F(1, 2), F(1)): + inside, outside = (1-gap)*share, (1-gap)*(1-share) + off = inside/(1-envelope) + outside + ceiling = (1-envelope)/(gap-envelope) + require(1/(1-off) <= ceiling < 1/q, 'split inverse envelope') + require((1-envelope)*off-(inside+outside) == -envelope*outside, 'split algebra') + p = 2 + d = 1 << (32760*p) + delta, gap = F(4, d), F(1, 8*p*p) + require((1-delta)/(gap-delta) == F(8*p*p*(d-4), d-32*p*p), 'U identity') + for rho, expected in [(F(91, 10000), True), (F(92, 10000), False)]: + q = F(1, 32)-rho + require(q > 0 and (q*q*2**11 > 1) == expected, 'p2 sharp endpoint') + return 511 + + +def mixed_matrices(): + count = 0 + p, n = 3, 4 + gap, budget = F(1, 8*p*p), F(1, 32*p**3) + e, delta_envelope = F(1, 64*p**4), F(1, 128*p**4) + edges = [(0, 1), (0, 2), (1, 3), (2, 3)] + ideal = eye(n) + for i, j in edges: + ideal[i][j] = ideal[j][i] = (1-gap)/2 + for cuts in itertools.product((0, 1), repeat=n-1): + cells = [0] + for cut in cuts: + cells.append(cells[-1]+cut) + for mode in (-1, 0, 1): + h = eye(n) + for i, j in edges: + if cells[i] == cells[j]: + h[i][j] = ideal[i][j]/(1-delta_envelope) + h[j][i] = ideal[j][i]/(1-delta_envelope) + else: + h[i][j] = ideal[i][j] + mode*e + h[j][i] = ideal[j][i] - mode*e + require(max(off_bounds(h)) <= 1-gap+budget, 'mixed matrix budget') + inv = inverse(h) + require(mul(h, inv) == eye(n) == mul(inv, h), 'inverse identity') + bound = 1/(gap-budget) + require(norm_inf(inv) <= bound and norm_inf(transpose(inv)) <= bound, 'two inverse norms') + for signs in itertools.product((-1, 1), repeat=n): + out = mul(inv, [[F(x)] for x in signs]) + require(sum(row[0]**2 for row in out) <= bound**2*n, 'inverse response bound') + count += 1 + return count + + +def polynomial_checks(): + h = [[F(1), F(1, 3), F(0)], [F(-1, 5), F(1), F(1, 7)], [F(0), F(1, 11), F(1)]] + inv, c = inverse(h), F(1, 2**11) + wrong_side_rejected = False + for length in range(1, 5): + approx, power = polynomial(h, c, length) + residual = add(inv, approx, -1) + require(residual == mul(power, inv), 'left normal-equation residual') + wrong_side_rejected |= residual != mul(inv, power) + require(wrong_side_rejected, 'nonnormal wrong-side control did not reject') + full = eye(9) + for i in range(8): + full[i][i+1], full[i+1][i] = F(1, 16), F(-1, 32) + section = [row[1:8] for row in full[1:8]] + pf, _ = polynomial(full, c, 2) + ps, _ = polynomial(section, c, 2) + require(pf[4][1:8] == ps[3], 'interior polynomial row') + require(pf[1][1:8] != ps[0], 'near-face locality control did not reject') + for i, row in enumerate(pf): + require(all(x == 0 for j, x in enumerate(row) if abs(i-j) > 3), 'length-two bandwidth') + return {'residual_lengths': [1, 2, 3, 4], 'locality_fixture_order': 9} + + +def boundary_controls(): + p, r = 2, F(249, 256) + h = eye(6) + h[0][1] = -r + for i in range(1, 6): + h[i][i-1] = -r + rows, cols = off_bounds(h) + require(rows == r and cols == 2*r, 'one-sided fixture') + inv = inverse(h) + expected = [r**i/(1-r*r) for i in range(6)] + require([row[0] for row in inv] == expected, 'one-sided inverse column') + energy = sum(x*x for x in expected) + require(energy > (10*p*p)**2, 'row-only fails claimed 2-norm ceiling') + inv_t = inverse(transpose(h)) + require(inv_t == transpose(inv) and sum(x*x for x in inv_t[0]) == energy, + 'column-only transpose control') + for rho, succeeds in [(F(91, 10000), True), (F(92, 10000), False)]: + t = F(31, 32)+rho + a = [[F(1), -t], [-t, F(1)]] + require(mul(a, [[F(1)], [F(1)]]) == [[1-t], [1-t]], 'exact threshold eigenvector') + require(((1-t)**2 > F(1, 2**11)) == succeeds, 'excess threshold control') + singular = [[F(0), F(0)], [F(0), F(0)]] + require(off_bounds(singular) == (0, 0), 'zero off-sums') + try: + inverse(singular) + except ValueError: + pass + else: + raise ValueError('diagonal-one omission control did not reject') + return {'row_only_inverse_column_squared_norm': str(energy), + 'claimed_ceiling_squared': 1600, + 'controls': ['row-only', 'column-only', 'excess-0.0092', 'missing-unit-diagonal', + 'nonnormal-wrong-residual-side', 'near-face-agreement']} + + +def main(): + report = {'status': 'PASS_DELTA_CROSS_CELL_INDEPENDENT_AUDIT', + 'authenticated_files': authenticate(), 'scalar_p_cases': scalar_checks(), + 'mixed_matrix_cases': mixed_matrices(), 'polynomial_checks': polynomial_checks(), + 'boundary_controls': boundary_controls(), 'new_kappa_claimed': False, + 'scope': 'Exact finite checks support the separate all-p conditional proof; no Gaussian gap, generator, Schur or full theorem verification.'} + print(json.dumps(report, indent=2)) + + +if __name__ == '__main__': + main()