From 2331c101f76b2575e538972a3af10df3e14c8893 Mon Sep 17 00:00:00 2001 From: CubeJerry <80299683+CubeJerry@users.noreply.github.com> Date: Wed, 28 Oct 2026 23:00:05 +0800 Subject: [PATCH] Prove sharp Walsh error with one interleaved integer shear Prepared for @CubeJerry with substantial OpenAI Codex assistance. No new kappa; credits and scope are in the research package. --- research/walsh-interleaved-shear/PROOF.md | 180 ++++++++++ research/walsh-interleaved-shear/README.md | 173 ++++++++++ research/walsh-interleaved-shear/RESULT.json | 32 ++ research/walsh-interleaved-shear/SOURCES.json | 40 +++ research/walsh-interleaved-shear/TASK.json | 182 ++++++++++ research/walsh-interleaved-shear/VERIFY.json | 47 +++ .../walsh-interleaved-shear/WITNESSES.json | 30 ++ .../check_artifacts.py | 89 +++++ .../context/pr6129-PROOF.md | 178 ++++++++++ .../context/pr6140-README.md | 112 ++++++ research/walsh-interleaved-shear/verify.py | 321 ++++++++++++++++++ 11 files changed, 1384 insertions(+) create mode 100644 research/walsh-interleaved-shear/PROOF.md create mode 100644 research/walsh-interleaved-shear/README.md create mode 100644 research/walsh-interleaved-shear/RESULT.json create mode 100644 research/walsh-interleaved-shear/SOURCES.json create mode 100644 research/walsh-interleaved-shear/TASK.json create mode 100644 research/walsh-interleaved-shear/VERIFY.json create mode 100644 research/walsh-interleaved-shear/WITNESSES.json create mode 100644 research/walsh-interleaved-shear/check_artifacts.py create mode 100644 research/walsh-interleaved-shear/context/pr6129-PROOF.md create mode 100644 research/walsh-interleaved-shear/context/pr6140-README.md create mode 100644 research/walsh-interleaved-shear/verify.py diff --git a/research/walsh-interleaved-shear/PROOF.md b/research/walsh-interleaved-shear/PROOF.md new file mode 100644 index 0000000000..c2b60aceb0 --- /dev/null +++ b/research/walsh-interleaved-shear/PROOF.md @@ -0,0 +1,180 @@ +# A sharp error bound for one interleaved integer shear + +Jerry Chen (@CubeJerry), with substantial OpenAI Codex assistance. Apache-2.0. + +## Exact statement and conventions + +Let h > 0, m be any integer, and t,s be distinct elements of {0,1,2,3}. +Let R round a real number to its nearest integer, with ties to the even integer, +and apply it componentwise. Coordinates are numbered by their binary indices. +Define the two **normalized** real Walsh factors + +``` +A = (1/2) [[1, 1, 0, 0], B = (1/2) [[1, 0, 1, 0], + [1,-1, 0, 0], [0, 1, 0, 1], + [0, 0, 1, 1], [1, 0,-1, 0], + [0, 0, 1,-1]] [0, 1, 0,-1]]. +``` + +Let S = I + m e_t e_s^T. In grid units the literal program is + +``` +y = R(Ax); z = S y; F_m(x) = R(Bz), x in Z^4. +``` + +The shear is exact on this integer grid. Rounding after it would be the +identity. Both values in each butterfly are read before either is written. +The **exact comparison operator includes the same shear**: T_m = B S A. +Then, for each of the twelve ordered pairs (t,s), + +``` +sup_(x in Z^4) ||F_m(x) - T_m x||_infinity = (|m|+3)/4. (1) +``` + +For inputs on h Z, multiply the right side by h. Reversing the two axes +preserves (1), by conjugating all coordinates and the shear by the permutation +(1 2). Independent spectator fibers preserve the bound when the shear is +within a fiber. Cross-fiber shears are not asserted here. + +For m=0, (1) recovers Nick Petalas's PR6129 value a_2=3/4. For every nonzero +integer m, that unsheared value is exceeded. This answers the two-stage, +integer-shear instance of Josie Elliston's explicit PR6140 open question. +Neither predecessor claimed that its theorem covered interleaved gates. + +## Upper bound for all inputs and all integer coefficients + +Scale h to one. Put delta = y - Ax. Every component of Ax is a half integer, +so each delta_i belongs to {-1/2,0,1/2}. A crucial implication is + +``` +delta_i != 0 => y_i is even. (2) +``` + +This is the nearest-even tie rule. Let eta = R(B S y) - B S y. +Every component of S y is an integer, so eta_i is again 0 or +/-1/2. +The error is exactly + +``` +F_m(x) - T_m x = B S delta + eta. (3) +``` + +An unaffected output combines the first errors of one second-stage pair +with signs and a factor 1/2. If eta_i=0, its absolute error is at most 1/2. +If eta_i!=0, the two stored inputs have odd sum/difference. They cannot both +be even, so (2) implies that at least one of their first errors is zero. +The error is then at most 1/4+1/2=3/4. + +For an affected output let p=t xor 2 be t's partner in B. Its propagated +first error has the form + +``` +(alpha delta_t + beta delta_p + alpha m delta_s)/2, +alpha,beta in {+1,-1}. +``` + +The two signs are the actual row signs of B; no independence of delta terms +is assumed. The source may equal p, in which case terms refer to the same +error and the triangle inequality remains valid. + +First suppose |m|>=1. If eta_i=0, the absolute total error is at most +(|m|+2)/4, which is smaller than (1). If eta_i!=0, at least one of +**delta_t, delta_p, delta_s is zero**. Otherwise (2) would make all of + y_t, y_p, y_s even; y_t+m y_s and y_p would be even, forcing eta_i=0. +Removing any one of these three terms decreases the triangle bound by at +least 1/2 before the outer division: its weight is either 1 or |m|>=1. +Therefore + +``` +|error_i| <= (|m|+1)/4 + 1/2 = (|m|+3)/4. +``` + +If the same variable appears twice, its vanishing removes both terms and +only strengthens this estimate. For m=0 there are just two relevant terms; +the unaffected-output argument gives 3/4. This proves the upper bound +without a bounded search, residue assumption or inherited Walsh recurrence. + +## Attainment by fixed small inputs + +[WITNESSES.json](WITNESSES.json) has two rows per (t,s), one for each +c in {-1,+1}. A row records (t,s,c,j,x0,x1,x2,x3), with x in {-1,0,1}^4. +Each row satisfies three exact identities: + +``` +(R(Ax))_s = 0, +4(F_0(x)_j - (T_0 x)_j) = 3, +4((T_0 - T_1)x)_j = c. (4) +``` + +Because the stored shear source is zero, **F_m(x)=F_0(x) for every m**. +The exact operator is affine in m. Hence (4) proves the identity + +``` +4(F_m(x)_j - (T_m x)_j) = 3 + c m (all integer m). +``` + +For nonzero m choose c=sign(m); either sign works for m=0. This attains (1). +The 24 finite identities in (4), combined with this algebraic argument, +prove attainment for the unbounded coefficient domain. They are checked +using explicit dense matrices and exact Fraction rounding, independently of +the loop-based integer butterfly interpreter. The certificate is not a claim +that a finite coefficient sweep alone proves (1). + +For example, take t=0, s=1, m=-1 and x=(0,-1,-1,-1). The first stored vector +is (0,0,-1,0), so the shear leaves it unchanged and F_m(x)=(0,0,0,0). +The exact output is (-1,1/4,0,1/4), giving error exactly 1. Removing the +shear yields exact output (-3/4,1/4,1/4,1/4) and error 3/4. +At h=1/4 the input is (0,-1/4,-1/4,-1/4), and the two sharp errors are +1/4 and 3/16 respectively. This is a changed four-coordinate program; +it is not a defect in CubeJerry's unchanged PR6119 surrogate. + +## Why the finite corroboration is complete in its stated domain + +Two elementary reductions make the secondary census meaningful: + +1. **Input period eight.** Replace x by x+8v with arbitrary integer v. + The first exact displacement 8Av has coordinates divisible by four. + Since R(u+2k)=R(u)+2k, the stored displacement is exactly 8Av. + The integer shear preserves divisibility by four. After B the displacement + has even coordinates, so the second rounding also commutes with it. + Thus F_m(x+8v)-T_m(x+8v)=F_m(x)-T_m x for every integer m. +2. **Coefficient residues modulo four.** At fixed x, replace m=r by r+4q. + The pre-final-round displacement is 4q B e_t y_s, whose components are + even integers. The rounded output shifts by this exact displacement. + Consequently four-times the error in output j changes by 4q c_j, where + c_j = 4 B[j,t] delta_s is in {-1,0,1}. Thus it is an affine function + c_j m + a_j within each coefficient residue class. + +The verifier compares **both complete output vectors and the first stored +vector** between its two engines for all 8^4 inputs, all twelve directed +shears and r=0,1,2,3: 196,608 cases, 786,432 final coordinates. For each +pair/residue and slope -1,0,+1, the intercept minimum and maximum are -3,+3. +This independently corroborates the formula under the two proved reductions. +It does not replace the universal upper-bound argument above. + +Large signed period/coefficient tests and the reverse-axis checks are finite +controls. The unrestricted h and spectator statements follow by scaling and +fiberwise application, not numerical testing of every grid or dimension. + +## Scope, inherited obligations and credit + +The theorem assumes real arithmetic, grid inputs, exactly two distinct axes, +one integral off-diagonal shear, exact pre-rounding arithmetic, and sufficient +range. It supplies no finite-width implementation, overflow bound, bit/tape +cost, reversible history, clean-scratch service or accelerated recursive child. +More stages, nonintegral shears, complex Gaussian mixing, multiple interleaved +gates and cross-fiber shears need their own analysis. + +This is a source-context-bound mathematical side result. It does not discharge +the selected PR6030 assumptions native_all_columns, owned_erasure, compiler, +precision_tape or analytic_recovery, and gives **No new κ**. No selected cold +replay, Lean kernel proof or independent human review is claimed. + +The pure-stage sharp bound and its proof are Nick Petalas's PR6129. The +independent audit and interleaved-shear question are Josie Elliston's PR6140. +The two-phase numerical surrogate is CubeJerry's PR6119; the deferred-row/H0 +context is Vlado Vojdanovski's PR1673, with the retained native/BIT/analytic +lineage credited by those packages. The exact-history result PR5912 and +Sricharan Vagvala's PR1631 shear-equivariance obstruction address different +contracts: neither is a two-stage Walsh error classification. No predecessor +code is imported or modified. The verbatim context documents retain their +notices and exact source pins in SOURCES.json. diff --git a/research/walsh-interleaved-shear/README.md b/research/walsh-interleaved-shear/README.md new file mode 100644 index 0000000000..1677295b8d --- /dev/null +++ b/research/walsh-interleaved-shear/README.md @@ -0,0 +1,173 @@ +# Sharp rounding error with one interleaved integer shear + +**Scoped theorem and independent verification. No new κ.** + +Inserting an exact grid-preserving addition between two rounded Walsh stages +can invalidate the error guarantee for pure Walsh stages. For every integer +coefficient `m` and all twelve directed off-diagonal shears on four coordinates, +the exact worst-case sup-norm error is + +``` +h * (|m| + 3) / 4. +``` + +Here `h` is the grid spacing. Each stage is one distinct **normalized** real +Walsh factor `H0=(1/2)[[1,1],[1,-1]]`, rounded to nearest with ties to even. +The intervening operation is `y[target] += m*y[source]`. The exact comparison +map contains **the same shear**. This is not an error comparison against a +different, shear-free transform. + +The unsheared case is `3h/4`; even a unit shear increases the sharp error to +`h`. For `m=-1`, target 0, source 1 and grid-unit input `(0,-1,-1,-1)`, the +rounded output is zero while the exact output is `(-1,1/4,0,1/4)`. + +[PROOF.md](PROOF.md) gives the universal upper bound using nearest-even parity, +then proves sharpness for all integer coefficients from 24 fixed small inputs +in [WITNESSES.json](WITNESSES.json). The certificate rows are finite exact +identities; their affine dependence on `m` proves attainment for the unbounded +coefficient domain. No finite search is presented as a full theorem proof. + +## What is new + +Nick Petalas's [PR6129](https://github.com/CrocSwap/integer-mult-bounds/pull/6129) +proves the sharp law for distinct pure Walsh stages and explicitly excludes +intervening gates. Josie Elliston's +[PR6140](https://github.com/CrocSwap/integer-mult-bounds/pull/6140) independently +audits that law and asks whether it survives an intervening grid shear. This +package answers the complete **two-stage, one-integer-shear** instance, using +new implementations and a proof that does not assume the pure-stage recurrence. +It finds no defect in either predecessor or in CubeJerry's unchanged PR6119 +surrogate. + +The existing nearest-even shear-history and shear-equivariance obstructions +concern different contracts. This contribution is a precision side result, +not a new paid supplier or a selected-caller proof. The assigned track is +independent verification/formalization, OS random integer **83**. The original +catalogue card is retained in [TASK.json](TASK.json), with the scope change to +a written theorem explicitly disclosed. No proof-assistant formalization is +claimed. + +## Reproduce + +From the repository root, with Python 3.12 and no third-party dependencies: + +```sh +python3.12 -I -W error -B research/walsh-interleaved-shear/verify.py +``` + +Expected: JSON with `status: PASS_WALSH_INTERLEAVED_SHEAR`, +`complete_residue_inputs: 196608`, `witnesses: 24`, sixteen rejected controls +and `no_new_kappa: true`, exactly matching [RESULT.json](RESULT.json). +The direct command also works from a relocated copy of this package without +Git or the rest of the repository. Context files are checked against their +recorded SHA256 and Git blob IDs; they are not executable dependencies. + +The registered runner checks the historical task/source bindings and runs the +same complete replay in ordinary and optimized Python, then the portable CLI +and damaged-artifact controls: + +```sh +python3.12 -B scripts/research_package.py --package research/walsh-interleaved-shear +``` + +Expected final marker: `PASS_REGISTERED_RESEARCH_PACKAGE`, outcome `completed`. +Full repository history is needed for those provenance checks. `VERIFY.json` +declares no external live inputs; both context documents are included locally. + +`verify.py --emit-witnesses` deterministically reconstructs the certificate, +searching `{-1,0,1}^4` in lexicographic order and stopping at the first witness +for each of the 24 pair/sign keys. `verify.py --emit-result` performs the full +replay and prints the receipt without comparing it to the committed receipt. +Both options print to stdout and never overwrite a frozen file. + +## Evidence and failure coverage + +The integer engine uses signed floor quotients for nearest-even rounding and +literal butterfly loops. Its independent oracle uses explicit dense matrices +and `Fraction` rounding; neither imports predecessor code. They compare every +rounded output, every exact output and the first stored vector, not merely a +common maximum. + +| Check | Completed coverage | +| --- | --- | +| Residue census | `8^4 * 12 * 4 = 196608` inputs; 786432 output coordinates | +| Fixed-source affine witnesses | 24 rows; both coefficient signs, including signed 201-bit coefficients | +| Signed half-integer rounding | 2051 cases against exact rational rounding | +| Period/coefficient controls | 768 reproducible large signed cases, seed 83 | +| Reversed stage order | 2916 cases plus the written coordinate-conjugacy argument | +| Semantic mutations | Floor ties, missing shear, reversed shear, repeated axis, wrong difference sign, missing exact-comparator shear, and single-final-round all detected | +| Certificate/domain controls | Missing, duplicate, zeroed, wrong-slope and Boolean witnesses; off-grid input, fractional coefficient and aliased ports all rejected | +| Overextended predecessor bound | Explicit unit-shear input defeats `3h/4`; removing the shear restores `3h/4` | + +The written input-period-eight and coefficient-residue lemmas explain why the +census covers its stated domain. The all-input upper proof is independent of +that census. All verifier checks use explicit exceptions and remain active +under `-O`. The transcript SHA256 in RESULT.json binds the ordered complete +computed vectors; it is an integrity check, not a substitute for mathematics. + +`check_artifacts.py` additionally runs the actual optimized CLI in a relocated +temporary package with an empty PATH and no Git. It checks that every file and +mode remains unchanged, then rejects four private-copy corruptions: changed +context bytes, missing context, a missing witness and a Boolean receipt field +replaced by integer one. The last control catches the `True == 1` ambiguity of +untyped Python dictionary comparison. These four controls are separate from +the sixteen mathematical/domain controls in RESULT.json. + +Local validation used CPython 3.12.14 on Linux x86_64. Normal and optimized +registered scientific checks passed in 30.827 seconds combined; this is a +descriptive replay duration, not a performance improvement claim. The portable +CLI and all four artifact controls also passed. Witness regeneration matches +the committed certificate byte for byte. Full environment and checkpoint +details are in TASK.json. Hosted CI is not claimed. + +## Pins and limitations + +Base: `721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8. +The accepted selected record at that base is PR6030, κ = `0.003125804`. +The actual construction, source manifest and review are recorded in TASK.json; +historical task-card numbers are not treated as current frontiers. + +[SOURCES.json](SOURCES.json) pins the historical selected record and catalogue, +plus the exact predecessor context documents: + +- PR6129 head `f496734450c346468c66818c1c35521165b0cdda`, PROOF.md. +- PR6140 head `1c97110e1f25e8345f8ee63c570b88e172d75be9`, README.md. + +The two small verbatim context documents preserve the excluded scope and open +question for review; their original notices remain intact. No pending PR's +code is imported and no pending commit is required in publication ancestry. +The mathematical statement is self-contained in this package. + +Assumptions: real grid inputs, exactly two distinct axes, one integral +off-diagonal shear, exact arithmetic before each specified rounding, and +sufficient range. Scaling gives arbitrary `h>0`; conjugacy gives the reversed +axis order. Independent spectator fibers are covered only for shears within +each fiber. No complex mixing, cross-fiber shear, nonintegral coefficient, +multiple shear, more-stage, finite-width or overflow theorem is asserted. + +No bit/tape cost, reversible restoration, clean-scratch service or accelerated +recursive child is supplied. All selected assumptions—`native_all_columns`, +`owned_erasure`, `compiler`, `precision_tape`, `analytic_recovery`—remain open +here. No selected cold replay, Lean kernel proof, hosted CI result or independent +human review is claimed. **No new κ; the selected frontier is unchanged.** + +## Open next questions + +Can this exact normalization and rounding contract be bound to an actual +selected `precision_tape` caller? First extract one complete rounded trace and +compare its grid, gates and exact comparison map against the unit-shear witness. +That binding is needed before changing any precision allocation; contracts +with more stages or nonintegral/complex gates need separate analysis. This +question and its blocker are structured in TASK.json. + +## Credit + +Prepared for Jerry Chen (@CubeJerry) with substantial OpenAI Codex assistance +in derivation, implementation, verification and writing. New work is Apache-2.0. +Nick Petalas retains credit for PR6129's pure-stage theorem and PR5912's history +analysis; Josie Elliston for PR6140's audit and explicit open question; +CubeJerry for PR6119's surrogate; Vlado Vojdanovski for PR1673's deferred-row +context; Sricharan Vagvala for PR1631's distinct equivariance obstruction. +The retained source documents credit their underlying native/BIT/analytic +lineage. Douglas Colkitt's package scaffold and the repository's source/export +verification tools are reused without modification. diff --git a/research/walsh-interleaved-shear/RESULT.json b/research/walsh-interleaved-shear/RESULT.json new file mode 100644 index 0000000000..51772eca65 --- /dev/null +++ b/research/walsh-interleaved-shear/RESULT.json @@ -0,0 +1,32 @@ +{ + "complete_output_comparisons": 786432, + "complete_residue_inputs": 196608, + "context_documents": 2, + "exact_error_in_grid_units": "(|m|+3)/4", + "full_output_transcript_sha256": "13b65e9e6657d8740b5819405299d80128fd2fa84e733ae11e051f11fd6f8b8b", + "large_signed_period_and_coefficient_cases": 768, + "no_new_kappa": true, + "rejected_controls": [ + "floor-ties", + "omit-shear", + "reverse-shear", + "repeat-axis", + "wrong-difference", + "omit-exact-shear", + "single-final-round", + "missing-witness", + "duplicate-witness", + "zeroed-witness", + "wrong-slope", + "boolean-certificate", + "off-grid", + "fractional-shear", + "aliased-shear", + "unchanged-three-quarter-bound" + ], + "reverse_axis_cases": 2916, + "rounding_cases": 2051, + "scope": "two distinct normalized real Walsh axes, one integer shear", + "status": "PASS_WALSH_INTERLEAVED_SHEAR", + "witnesses": 24 +} diff --git a/research/walsh-interleaved-shear/SOURCES.json b/research/walsh-interleaved-shear/SOURCES.json new file mode 100644 index 0000000000..24df6d4563 --- /dev/null +++ b/research/walsh-interleaved-shear/SOURCES.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ], + "context_documents": [ + { + "local_path": "context/pr6129-PROOF.md", + "repository": "petalas/integer-mult-bounds", + "commit": "f496734450c346468c66818c1c35521165b0cdda", + "source_path": "research/nearest-even-walsh-error/PROOF.md", + "git_blob": "6173c71bc7a93059def02b7e7529dd12b2c506d0", + "sha256": "5bea753bf996648235e5a8e4f639265d91ebf179ad65dd3bd426cab1ac5b91fe", + "usage": "self-contained verbatim context; no code imported", + "license": "Apache-2.0" + }, + { + "local_path": "context/pr6140-README.md", + "repository": "JosieElliston/integer-mult-bounds", + "commit": "1c97110e1f25e8345f8ee63c570b88e172d75be9", + "source_path": "research/nearest-even-walsh-error-audit/README.md", + "git_blob": "7d5fbd0b62b8505055eb17a6b2c44c3f142760e8", + "sha256": "92f09cd0b7c41e36b93b24291a5809b84c33039c8eeafcb815aee24c7e115edd", + "usage": "self-contained verbatim context; no code imported", + "license": "Apache-2.0" + } + ] +} diff --git a/research/walsh-interleaved-shear/TASK.json b/research/walsh-interleaved-shear/TASK.json new file mode 100644 index 0000000000..311318a57f --- /dev/null +++ b/research/walsh-interleaved-shear/TASK.json @@ -0,0 +1,182 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove and independently verify the sharp sup-norm rounding error for two distinct normalized real Walsh axes with one intervening integer grid shear on four coordinates, for every directed shear and every integer coefficient.", + "scope_change_reason": "The donor assigned seed 83 to independent verification/formalization. Among three narrow candidates, seed 83 modulo 3 selected the explicit unclaimed interleaved-shear question in PR6140. This is a written scoped theorem and independent exact implementation, not a proof-assistant formalization or a completed selected-caller interface proof. The original card is retained verbatim for provenance.", + "bottleneck_link": "Precision side result: establishes when a pure-Walsh rounding guarantee cannot be carried across an exact grid-preserving gate. It may inform a later precision_tape caller audit, but does not discharge that assumption or improve a paid supplier profile.", + "budget_minutes": 120, + "stop_rule": "One experiment only: all 12 distinct ordered coordinate pairs, two distinct Walsh axes, one integer coefficient. Stop after a universal upper proof, fixed-source affine witnesses for both coefficient signs, complete mod-8 input and mod-4 coefficient census, and independent negative controls. Do not expand to more stages or multiple shears.", + "outcome": "completed", + "evidence": "PROOF.md proves sharp error h*(abs(m)+3)/4 for every integer m; WITNESSES.json supplies 24 fixed inputs. RESULT.json records independent complete-vector comparisons on 196608 residue cases, 768 large signed cases, 2916 reverse-axis cases, and 16 rejected controls. This is a scoped mathematical proof with finite corroboration, not formal verification of the multiplication theorem.", + "author": "Jerry Chen (@CubeJerry)", + "ai_assistance": "Prepared for Jerry Chen (@CubeJerry) with substantial OpenAI Codex assistance in task selection, mathematical derivation, implementation, proof review, testing and packaging. No independent human review or proof-assistant kernel check claimed.", + "open_questions": [ + { + "question": "Does an actual selected precision_tape caller contain an interleaved shear with the exact normalization, rounding points and coordinate contract proved here?", + "why_it_matters": "Only an exact caller binding could turn this local error classification into a relevant precision obligation; the theorem alone does not change the multiplication result.", + "first_step": "Extract one complete rounded caller trace, identify its actual grid and exact comparison map, and test the unit-shear witness before proposing a new precision allocation.", + "blocked_by": "No such caller binding is supplied here. Nonintegral coefficients, more stages, complex mixing and range/overflow require separate proofs." + } + ], + "selection": { + "track": "Independent verification or formalization", + "os_random_method": "secrets.randbelow(100)", + "os_random_integer": 83, + "catalogue_task": "formal-interface-lemma", + "picker_seed": "00000000000000000000000000000053", + "scope_key": "636f26dec98e26b296e8", + "three_candidates": [ + "PR6106: independently check affine phase composition against native operation semantics.", + "PR6110: check one stopped-recursion source binding; existing source-binding work made this less distinct.", + "PR6140: answer the explicitly open integer-shear interleaving question for the PR6129 Walsh rounding law." + ], + "diversification": "83 modulo 3 selected the third candidate; odd parity selected initial coefficient -1. Random(83) fixes the later signed stress cases. Novelty comes from the excluded interleaving mechanism, not the random seed." + }, + "coordination": { + "claim_utc": "2026-10-28T14:22:00Z", + "expected_finish_utc": "2026-10-28T16:16:00Z", + "claim_location": "Local claim recorded before the experiment; no public reservation issue.", + "reason_local": "Connected GitHub tools have no Discussions write method, the inspected GitHub browser is signed out, and shell gh is absent. Donor explicitly permits a local claim when posting is unavailable.", + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19243168", + "overlap": "Read Discussions1163/1166, latest 60 PRs, targeted all-state PR searches (Walsh/shear, nearest-even, intervening/round), central review ledger and nearby negative results before selection. No same-scope successor found in that coverage; not a novelty certificate.", + "local_helper": "find_overlap.py offline at 2026-10-28T14:25:25Z: complete HEAD README/TASK inventory (8348 files), no usable remote cache. Live plugin/browser inspection supplies the limited remote coverage separately.", + "nearby_distinct_work": [ + "PR5912 nearest-even-shear-history: information/history contract, not two-stage forward error.", + "PR1631 shear-equivariant-rounding: a global equivariance obstruction, not this error classification.", + "equivariant-grid-frame-classification: frame contract, not this two-stage program." + ] + }, + "checkpoints": [ + { + "utc": "2026-10-28T14:17:00Z", + "canonical_main": "721c03822c421b7f7fcbb2598993b947c4d88419", + "priority_revision": 8, + "decision": "Read current entry instructions, selected certificate and actual source/review; continue with the explicitly open side question." + }, + { + "utc": "2026-10-28T14:24:00Z", + "canonical_main": "721c03822c421b7f7fcbb2598993b947c4d88419", + "priority_revision": 8, + "decision": "Refreshed canonical main before creating the isolated branch; unchanged guidance and selected frontier. Frozen research inputs retained." + }, + { + "utc": "2026-10-28T14:49:49Z", + "canonical_main": "721c03822c421b7f7fcbb2598993b947c4d88419", + "priority_revision": 8, + "decision": "Fetched canonical main during verification; no guidance/catalogue/selected/review-ledger/bottleneck changes. Live PR6129/6140 heads unchanged. Latest 30 open PRs and first 30 of 100 all-state search hits inspected for related scope; Discussion1166 re-read, no successor claim seen. Continue the same package with frozen inputs." + } + ], + "selected_baseline": { + "certificate": "certificates/selected-result.json", + "selected_pr": 6030, + "kappa": "781451/250000000 = 0.003125804", + "construction": "research/p104-helper470-twin-rung-removal", + "review": "docs/research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md", + "source_manifest": "certificates/frontier6030-source.json", + "claim": "certificates/frontier6030/CLAIM.json", + "orientation_check": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; no selected cold replay claimed.", + "remaining_assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "new_kappa": false + }, + "coverage": { + "universal_claim": "h>0, every integer m, all x in (h Z)^4, all 12 off-diagonal shears, exactly two distinct normalized real Walsh axes; reversed axes by conjugacy.", + "finite_census": "All x in {0,...,7}^4, all 12 directed pairs and coefficient residues 0,...,3: 196608 complete-vector comparisons. Written period and affine-residue lemmas explain the domain.", + "witness_search": "Lexicographic x in {-1,0,1}^4, then output 0,...,3; stop at first valid witness for each pair and sign. Completed all 24 keys. No unsuccessful search is used as an impossibility claim.", + "unresolved": "No finite-width/range guard, complex/multiple-shear/more-stage theorem, reversible restoration, bit or tape costs, recursive supplier, selected-caller binding, Lean proof, or independent human review." + }, + "validation": { + "environment": "CPython 3.12.14; Linux 6.18.55 x86_64; Git 2.51.1; standard library only.", + "executed": [ + "Normal and optimized full scientific replay through the registered runner: PASS; combined elapsed 30.827 s (descriptive check time, not a speed claim).", + "Relocated Git-free optimized CLI with empty PATH: PASS, all bytes and modes unchanged.", + "Actual CLI rejects four private-copy corruptions: changed context bytes, missing context, missing witness, Boolean receipt replaced by integer one.", + "Witness regeneration byte-identical to WITNESSES.json." + ], + "not_claimed": [ + "Hosted CI", + "selected frontier cold replay", + "independent human review", + "formal proof-kernel acceptance" + ] + } +} diff --git a/research/walsh-interleaved-shear/VERIFY.json b/research/walsh-interleaved-shear/VERIFY.json new file mode 100644 index 0000000000..84417a6c7a --- /dev/null +++ b/research/walsh-interleaved-shear/VERIFY.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent integer and Fraction/dense-matrix engines compare every output on all 196608 input/coefficient residue cases; authenticate pinned context; verify 24 affine witnesses, signed rounding, period and axis controls, 16 mathematical/domain/certificate rejection controls, and exact typed RESULT.json receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the same complete mathematical and failure-detection coverage under optimized Python; all guards use explicit exceptions, not disabled assertions." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/check_artifacts.py" + ], + "timeout_seconds": 180, + "checks": "Relocated Git-free optimized CLI replay with empty PATH preserves every package byte/mode; damaged/missing context, truncated witness certificate and Boolean-as-integer result receipt fail through the actual CLI with targeted errors." + } + ] +} diff --git a/research/walsh-interleaved-shear/WITNESSES.json b/research/walsh-interleaved-shear/WITNESSES.json new file mode 100644 index 0000000000..c2d74bde1b --- /dev/null +++ b/research/walsh-interleaved-shear/WITNESSES.json @@ -0,0 +1,30 @@ +{ + "schema": "walsh-integer-shear-witnesses/v1", + "columns": ["target", "source", "slope", "output", "x0", "x1", "x2", "x3"], + "rows": [ + [0, 1, -1, 0, 0, -1, -1, -1], + [0, 1, 1, 0, -1, 0, -1, -1], + [0, 2, -1, 2, -1, -1, 0, 1], + [0, 2, 1, 0, -1, -1, -1, 0], + [0, 3, -1, 0, -1, -1, 0, -1], + [0, 3, 1, 0, -1, -1, -1, 0], + [1, 0, -1, 1, 0, 1, -1, 1], + [1, 0, 1, 1, -1, 0, -1, 1], + [1, 2, -1, 1, -1, 1, 0, 1], + [1, 2, 1, 1, -1, 1, -1, 0], + [1, 3, -1, 3, -1, 1, 0, -1], + [1, 3, 1, 1, -1, 1, -1, 0], + [2, 0, -1, 2, -1, 0, 1, 1], + [2, 0, 1, 0, -1, 0, -1, -1], + [2, 1, -1, 2, -1, 0, 1, 1], + [2, 1, 1, 0, -1, 0, -1, -1], + [2, 3, -1, 0, -1, -1, 0, -1], + [2, 3, 1, 0, -1, -1, -1, 0], + [3, 0, -1, 3, -1, 0, 1, -1], + [3, 0, 1, 1, -1, 0, -1, 1], + [3, 1, -1, 3, -1, 0, 1, -1], + [3, 1, 1, 1, -1, 0, -1, 1], + [3, 2, -1, 3, -1, 1, 0, -1], + [3, 2, 1, 1, -1, 1, -1, 0] + ] +} diff --git a/research/walsh-interleaved-shear/check_artifacts.py b/research/walsh-interleaved-shear/check_artifacts.py new file mode 100644 index 0000000000..1e4e5ffddd --- /dev/null +++ b/research/walsh-interleaved-shear/check_artifacts.py @@ -0,0 +1,89 @@ +#!/usr/bin/env python3 +"""Portable CLI and damaged-artifact controls; Jerry Chen/Codex, Apache-2.0.""" +from hashlib import sha256 +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def snapshot(root): + return {str(p.relative_to(root)): (sha256(p.read_bytes()).hexdigest(), + p.stat().st_mode & 0o777) + for p in root.rglob('*') if p.is_file()} + + +def main(): + with tempfile.TemporaryDirectory(prefix='walsh-shear-') as directory: + root = Path(directory) + package = root / 'relocated-package' + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns('__pycache__')) + before = snapshot(package) + environment = os.environ.copy() + environment['PATH'] = '' + environment.pop('PYTHONPATH', None) + environment.pop('PYTHONOPTIMIZE', None) + argv = [sys.executable, '-I', '-O', '-W', 'error', '-B', + str(package / 'verify.py')] + + def replay(): + return subprocess.run(argv, cwd=root, env=environment, text=True, + capture_output=True, timeout=120, check=False) + + good = replay() + require(good.returncode == 0, 'Git-free portable replay: ' + good.stderr) + require(json.loads(good.stdout)['status'] == 'PASS_WALSH_INTERLEAVED_SHEAR', + 'portable success marker') + require(snapshot(package) == before, 'portable replay changed files or modes') + + receipt = json.loads((package / 'RESULT.json').read_text()) + receipt['no_new_kappa'] = 1 # True == 1 in Python; the receipt must be typed. + certificate = json.loads((package / 'WITNESSES.json').read_text()) + certificate['rows'] = certificate['rows'][:-1] + cases = ( + ('context-bit-flip', 'context/pr6129-PROOF.md', b'corrupted\n', + 'context source hash'), + ('missing-context', 'context/pr6140-README.md', None, + 'FileNotFoundError'), + ('missing-witness-cli', 'WITNESSES.json', json.dumps(certificate).encode(), + 'witness count'), + ('boolean-as-integer-receipt', 'RESULT.json', json.dumps(receipt).encode(), + 'committed result differs from computed result'), + ) + rejected = [] + for name, path, replacement, reason in cases: + file = package / path + original = file.read_bytes() + mode = file.stat().st_mode & 0o777 + if replacement is None: + file.unlink() + else: + file.write_bytes(replacement) + try: + bad = replay() + require(bad.returncode != 0 and reason in bad.stderr, + 'wrong failure for ' + name + ': ' + bad.stderr) + require('PASS_WALSH_INTERLEAVED_SHEAR' not in bad.stdout, + 'damaged artifact printed success: ' + name) + rejected.append(name) + finally: + file.write_bytes(original) + file.chmod(mode) + require(snapshot(package) == before, 'private controls did not restore bytes/modes') + print(json.dumps({'status': 'PASS_WALSH_SHEAR_ARTIFACT_CONTROLS', + 'git_free_optimized_replay': True, 'unchanged_bytes_and_modes': True, + 'rejected': rejected}, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/walsh-interleaved-shear/context/pr6129-PROOF.md b/research/walsh-interleaved-shear/context/pr6129-PROOF.md new file mode 100644 index 0000000000..6173c71bc7 --- /dev/null +++ b/research/walsh-interleaved-shear/context/pr6129-PROOF.md @@ -0,0 +1,178 @@ +# Sharp deterministic error for normalized Walsh stages + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement + +Fix a grid spacing h>0 and an integer J>=0. On an array with J selected +binary axes and any spectator axes, apply the J distinct factors + + H0 = (1/2) [[1,1],[1,-1]], + +one axis at a time, in any fixed order. After every factor, round each +coordinate to the nearest multiple of h, with ties to the even grid integer. +The input is any array in h Z, without a magnitude restriction in the +mathematical model. Every sum and difference before rounding is exact; +overflow and other arithmetic defects are excluded. + +Let T be the exact normalized Walsh operator and F its rounded version. +Then the sharp uniform coordinate bound is + + sup_(x in (h Z)^(2^J)) ||F(x)-T x||_infinity = h a_J, + a_J = J/3 + (1-(-1/2)^J)/9. (1) + +Spectator fibers are independent, so the same bound holds for any number +of spectators. Exact final recovery to the raw Walsh operator multiplies +the error by 2^J. In particular its sharp bound is h 2^J a_J. + +The more precise statement for one output coordinate is as follows. If +its stored output divided by h is even, the sharp absolute error is h a_J. +If it is odd and J>=1, the sharp absolute error is h a_(J-1). +At J=0 both errors are zero. + +The theorem concerns this deterministic quantizer. It is not a theorem for +arbitrary bounded faults, non-grid initial data, repeated axes, intervening +non-Walsh gates or the actual accelerated recursive supplier. + +## Reduction to a binary averaging tree + +Scale by h and work with integer grid values. Write R(s) for nearest-even +rounding of a real number to an integer. It is odd, and + + R(s+2k) = R(s)+2k (2) + +for every integer k. Translation by an odd integer need not commute with R. + +Fix an output of the J-stage butterfly network. Its dependencies form a +complete binary tree of depth J, with disjoint original inputs at its +leaves. Each internal node is R((u+v)/2) or R((u-v)/2). +Oddness lets us absorb every minus sign into the leaves and intermediate +subtrees. Thus it suffices to analyze a complete tree of rounded averages. +Its exact value is the average of its 2^J signed leaves. This reduction +uses distinct axes; repeated use of an axis need not give disjoint leaves. + +## Parity-sensitive bounds + +Let a_j and b_j be the maximal absolute error at depth j conditioned on +an even or odd integer output. Start with a_0=b_0=0. We prove inductively +that the finite maxima exist and satisfy + + b_j = a_(j-1), + a_j = 1/2 + (a_(j-1)+b_(j-1))/2. (3) + +Consider child outputs u,v. If u+v is even, the root division is exact. +The child parities agree, and averaging their errors costs at most +max(a_(j-1),b_(j-1))=a_(j-1). + +If u+v is odd, its half lies exactly between consecutive integers. The +stored root is even, its local error has magnitude 1/2, and the child +parities differ. The total error is therefore at most the second line +of (3). An odd root can occur only in the exact-division case, proving +the first line's upper bound. + +For completeness the second line dominates the exact-division bound. +Put d_j=a_j-a_(j-1). The recurrences give d_1=1/2 and + + d_j = (1-d_(j-1))/2, j>=2. + +Induction gives 1/4<=d_j<=1/2 for every j>=1. Hence a_j is increasing and +b_j<=a_j. This proves the comparisons used in the induction, without +assuming a closed form in advance. + +## Attaining inputs + +Construct integer leaf lists E_j,O_j with rounded outputs 0 and 1. +Their signed errors, stored output minus exact average, will be a_j,b_j. +Use concatenation, and let adding an integer to a list mean entrywise +addition. Define + + E_0=[0], O_0=[1], + E_j = E_(j-1) concatenated with (O_(j-1)-2), + O_j = E_(j-1) concatenated with (E_(j-1)+2). (4) + +By (2), the children of E_j have stored outputs 0,-1 and errors +a_(j-1),b_(j-1). Their root rounds -1/2 to 0, so its error is the second +line of (3). The children of O_j have outputs 0,2 and both have error +a_(j-1). Their root is exactly 1, proving the first line of (3). +Negating a leaf list attains the negative extremum. Even translations +give every other prescribed output of the same parity. + +The E_j entries lie in [-j,0]. In the ordinary low-bit-first Walsh +schedule, concatenate the lists along the last processed axis. Then its +zero-frequency output is exactly the averaging tree above. This proves +attainment in the actual butterfly network, rather than in a relaxed +independent-error model. Other fixed axis orders use the matching input +axis permutation. Therefore the coordinate upper bound and the sup norm +maximum in (1) are both sharp. + +Substituting b_j=a_(j-1) in (3), with a_0=0 and a_1=1/2, gives + + a_j = 1/2 + (a_(j-1)+a_(j-2))/2, j>=2. + +The expression (1) satisfies these initial conditions and recurrence, +which proves the formula. The usual stagewise bound is J h/2. Equation +(1) is strictly smaller for every J>=2, and its ratio to J h/2 tends to 2/3. +These are exact algebraic comparisons, not measured speedups. + +## Complete residue domains + +For depth J the error is periodic in each integer input coordinate with +period 2^(J+1). Indeed, add 2^(J+1) times an arbitrary integer array to +the input. After k stages its exact displacement has coordinates +divisible by 2^(J+1-k), which are even integers for all k<=J. Equation +(2) therefore propagates precisely that displacement through every +rounded stage. The final displacement equals the exact Walsh displacement, +so their error arrays coincide. This also holds in the presence of signs. + +Consequently the verifier's 4^2 one-stage inputs and 8^4 two-stage inputs +are complete residue-domain checks for those depths. Larger depths are +corroborated by witnesses and a parity-state enumeration; the all-J +conclusion rests on the proof above. + +## Application to PR #6119's numerical surrogate + +CubeJerry's PR #6119, head bdfe5a10d488b5f774e906d8d4588dc8da25e7ba, +defines an eight-input surrogate with exposure, four temporary coordinates, +the echo m=1/2,a=4, two distinct H0 axes and projection of the temporaries. +It rounds after its six nominated noisy maps to the same h grid. +Its arbitrary-defect theorem and its finite ternary-cube observation are +credited prior results and context; neither is re-audited here. + +For every grid retained coordinate x=h k, its initially zero echo temporary +becomes h R(k/2). The upper addition and its inverse are integer-grid +operations and cancel exactly. The lower inverse leaves, before rounding, + + h [R(k/2)-k/2], + +which is 0 or +/-h/2, and hence rounds to zero. Thus for every grid input +the entire rounded echo is the identity on retained data and returns the +temporary row to zero. The remaining retained computation is precisely +two rounded Walsh axes. Exposure and its inverse are exact permutations. +Its sharp normalized error is therefore 3h/4, for all eight grid inputs. + +At the predecessor's h=1/4 this is 3/16; exact raw recovery multiplies it +by four, giving 3/4. One attaining original-coordinate input is + + (0,0,-1/4,0,-1/2,0,0,0). + +The four entries of the first spectator fiber are E_2/4. This supplies an +all-grid theorem and explicit witness beyond the predecessor's finite +6,561-point cube. It is still a numerical surrogate, not a materialized +PR6030 child or a physical disposal implementation. + +## Limits and credit + +CubeJerry supplies the explicit open distinction between independent +defect boxes and deterministic quantizer errors, and the two-phase surrogate. +Vlado Vojdanovski's PR1673 supplies the normalized H0/deferred-row context; +the selected construction retains its original authors and five assumptions. +JoyboyBrian's `native-rounded-butterfly-contract` supplies related pair-first +nearest-even arithmetic and parity constraints for different complex Gaussian +letters. The present averaging-tree parity recurrence and attaining all-J +Walsh bound are the new result. + +No full selected replay, native admission, proof-kernel check or independent +human review is claimed. The theorem assumes exact pre-rounding arithmetic, +unbounded integer range and the specified grid ABI. Bit costs, intermediate +range guards, tape movement, reversible history and an accelerated supplier +remain separate obligations. Source files and the selected frontier are unchanged. diff --git a/research/walsh-interleaved-shear/context/pr6140-README.md b/research/walsh-interleaved-shear/context/pr6140-README.md new file mode 100644 index 0000000000..7d5fbd0b62 --- /dev/null +++ b/research/walsh-interleaved-shear/context/pr6140-README.md @@ -0,0 +1,112 @@ +# Independent audit of #6129's nearest-even Walsh-stage bound + +**Audit of an open PR; no new κ, no selected-frontier change.** + +[PR #6129](https://github.com/CrocSwap/integer-mult-bounds/pull/6129) +(Nick Petalas, head `f496734450c346468c66818c1c35521165b0cdda`) claims that J +distinct normalized Walsh factors `H0=(1/2)[[1,1],[1,-1]]`, each followed by +nearest-even rounding to a common grid h, have sharp sup-norm error + + h a_J, a_J = J/3 + (1-(-1/2)^J)/9, + +with sharp error `h a_(J-1)` on outputs whose stored value over h is odd. It +also claims that CubeJerry's +[PR #6119](https://github.com/CrocSwap/integer-mult-bounds/pull/6119) surrogate +(head `bdfe5a10d488b5f774e906d8d4588dc8da25e7ba`) has exact global +normalized error `3h/4`, which is 3/16 at h=1/4. + +**Verdict: no error found.** I checked PROOF.md step by step and reproduced +every stated number with engines that share no code with #6129 or #6119. + +## Proof review (PR #6129 PROOF.md) + +| Step | Status | +| --- | --- | +| R is odd and `R(s+2k)=R(s)+2k`; signs absorbed into leaves | correct. Nearest-even is symmetric at ties. Negating a subtree's leaves negates every stored value in it. Distinct axes give disjoint leaves. | +| Upper bound (3): even `u+v` is exact with equal child parities; odd `u+v` gives an even root, local error 1/2 and mixed parities | correct. `b_j <= max(a,b)` needs `b_(j-1) <= a_(j-1)`. The `d_j` induction supplies it without circularity. | +| `d_j=(1-d_(j-1))/2`, `1/4<=d_j<=1/2` | correct. The second line of (3) dominates the exact branch because `d_(j-1)<=1`. | +| Witnesses (4): E_j children are (0, a), (-1, b), and the root `R(-1/2)=0` adds +1/2. O_j children are (0, a), (2, a), and the root 1 is exact | correct; all signed errors are positive. | +| Closed form and `a_J=2, ratio → 2/3 | correct | +| Period `2^(J+1)` per input | correct. After k<=J stages the exact displacement is divisible by `2^(J+1-k)`, which is even. | +| #6119 application | correct. `a=4` is an integer, so upper and inverse are exact on the grid. The lower inverse leaves `h(R(k/2)-k/2)` in {0, ±h/2}, and that rounds to 0 under ties-to-even. | + +Two clarifications for readers. They are not errors. + +1. The Walsh law depends on parity tie-breaking, not on ties-to-even itself. + Ties-to-odd gives the same a_J (engine D). The #6119 application does need + ties-to-even: under ties-to-odd, the echo temporary is left at ±h for every + odd k, so the echo would not be the identity. +2. Nearest rounding alone does not give the saving. Floor rounding attains + the stagewise bound J/2 at every J<=5. Ties-away-from-zero already reaches + J/2=1 at J=2. Every rule here obeys `R(s+2t)=R(s)+2t` except ties-away. + +The same integer sequence, `2^J a_J = ((3J+1)2^J-(-1)^J)/9` (0, 1, 3, 9, 23, +57, ...), is the sharp dyadic rotation switch tariff in +`research/dyadic-rotation-switch-tariff` (also Nick Petalas). Both proofs +reduce to the slope recurrence `d_j=(1-d_(j-1))/2`. This is a structural +remark only. Neither result is used here. + +## Independent engines (`verify.py`, stdlib, about 50 s) + +- **A. Residue-tracking tree sets.** For one output tree with sign pattern + σ, I enumerate every leaf residue mod `2^(J+1)`. After each stage I keep + the complete set of (stored value mod `2^(J+1-k)`, exact signed error). By + `R(s+2t)=R(s)+2t`, the root residue mod M/2 is determined by the child + residues mod M when M>=4. This needs only the period lemma, not #6129's + "children can be shifted by any even amount" step. The engine covers every + sign pattern for J<=4, the all-plus pattern for J<=7, and both output + parities. The even-output maximum equals a_J and the odd-output maximum + equals a_(J-1) for every J<=7 (for example, 313/128 at J=7). For J<=4, the + (parity, |error|) set is identical across all 2^J sign patterns. +- **B. Literal network.** This is an exhaustive check of the 8-point network + (J=3) on `[-3,0]^8` (65,536 inputs) in three stage orders, over every + output coordinate. The maximum is exactly 9/8, and no input exceeds it. +- **C. #6119 surrogate.** I rebuilt the 12-wire surrogate (exposure, pad, + echo m=1/2 and a=4, active H0, unpad, restore, tail H0, six rounded maps) in + integer units of h/8. I checked it exhaustively over each spectator fiber + modulo 8h (8,192 inputs), plus 300 random period-8h shifts. The sup is + exactly 3h/4. #6129's original-coordinate witness (0,0,-1/4,0,-1/2,0,0,0) + attains it. *Local-only cross-check, not in the verifier:* on 3,000 random + grid inputs, my rebuild agrees exactly with #6119's own `program()`/`forward(rounding=True)` + at the head above. +- **D. Controls.** Ties-to-odd gives the same law. Floor gives exactly J/2. + Ties-away-from-zero reaches 1 at J=2. Under ties-to-odd, the echo is dirty + on odd residues. + +Engine A uses the period lemma. Its proof is short and is given above and in +#6129. The verifier only samples it, on 400 random literal J=3 networks. So +engine A is a complete check *given* that lemma, not a proof-free +exhaustion. Engine B is literal for J=3 on a box only. All-J correctness rests +on the written proof, which I found correct. + +## Reproduce + +```sh +python3 scripts/research_package.py --package research/nearest-even-walsh-error-audit --check-only +python3.12 scripts/research_package.py --package research/nearest-even-walsh-error-audit +``` + +## Not covered + +This audit makes no claim about #6119's arbitrary-defect theorem or its +mutation checks. It also does not cover bit costs, range guards, reversible +history or any PR6030 child or supplier. These remain separate obligations +of #6129 and #6119. + +## Open next questions + +- Whether a rounded echo is clean depends on the tie rule (engine D). Which + native rounded compilers on main rely on a ties-to-even cancellation like + #6119's lower inverse? A first step is to grep the retained rounded + shear/echo packages and look for `m=1/2` half-tie cancellations. +- Does the sharp law survive when a non-Walsh gate sits between two rounded + stages (for example a grid shear)? #6129 excludes this case. A first step + is to put one intervening shear into engine A and enumerate it. + +## Credit + +The theorem, proof and witnesses are Nick Petalas's (#6129). The surrogate and +the deferred-row context are CubeJerry's (#6119, with OpenAI Codex assistance) +and Vlado Vojdanovski's (PR1673), with the lineage credited in #6129. This +audit and its engines were prepared by Josie Elliston with Claude Opus 5.5 +(Anthropic) assistance. Apache-2.0. diff --git a/research/walsh-interleaved-shear/verify.py b/research/walsh-interleaved-shear/verify.py new file mode 100644 index 0000000000..efcf34b37c --- /dev/null +++ b/research/walsh-interleaved-shear/verify.py @@ -0,0 +1,321 @@ +#!/usr/bin/env python3 +"""Exact two-stage Walsh/shear check; Jerry Chen, OpenAI Codex; Apache-2.0. + +No predecessor implementation is imported. The integer butterfly interpreter +and Fraction/dense-matrix oracle below are separately represented. The universal +claim rests on PROOF.md plus the fixed-source witness certificate, not sampling. +""" +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import random +import sys + +HERE = Path(__file__).resolve().parent +PAIRS = tuple((t, s) for t in range(4) for s in range(4) if t != s) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def half_even(n): + """Nearest-even n/2, with floor quotient valid for both signs.""" + q, r = divmod(n, 2) + return q + (r & (q & 1)) + + +def butterfly_numerators(x, axis): + out = list(x) + for i in range(4): + if not i & (1 << axis): + j = i ^ (1 << axis) + out[i], out[j] = x[i] + x[j], x[i] - x[j] + return out + + +def literal(x, t, s, m, *, axis=0, fault=None): + """Return rounded output, four-times exact output, first stored values.""" + require(len(x) == 4 and all(type(v) is int for v in x), 'integer-grid input') + require(type(m) is int, 'integer shear coefficient') + require((t, s) in PAIRS and axis in (0, 1), 'distinct valid ports/axes') + first = butterfly_numerators(x, axis) + quantize = (lambda n: n // 2) if fault == 'floor-ties' else half_even + stored = [quantize(n) for n in first] + changed = stored.copy() + if fault != 'omit-shear': + if fault == 'reverse-shear': + changed[s] += m * stored[t] + else: + changed[t] += m * stored[s] + second_axis = axis if fault == 'repeat-axis' else 1 - axis + numerators = butterfly_numerators(changed, second_axis) + if fault == 'wrong-difference': + numerators[1 << second_axis] *= -1 + out = [quantize(n) for n in numerators] + exact_first = first.copy() + exact_first[t] += m * first[s] + exact4 = butterfly_numerators(exact_first, 1 - axis) + if fault == 'omit-exact-shear': + exact4 = butterfly_numerators(first, 1 - axis) + if fault == 'single-final-round': + out = [round(Q(v, 4)) for v in exact4] + return tuple(out), tuple(exact4), tuple(stored) + + +# Independent representation: literal dense matrices, exact rational rounding. +M0 = ((1, 1, 0, 0), (1, -1, 0, 0), (0, 0, 1, 1), (0, 0, 1, -1)) +M1 = ((1, 0, 1, 0), (0, 1, 0, 1), (1, 0, -1, 0), (0, 1, 0, -1)) + + +def mv(matrix, vector): + return tuple(sum(a * b for a, b in zip(row, vector)) for row in matrix) + + +def mm(a, b): + columns = tuple(zip(*b)) + return tuple(tuple(sum(x * y for x, y in zip(row, col)) for col in columns) + for row in a) + + +def dense_data(t, s, m, axis=0): + shear = [[int(i == j) for j in range(4)] for i in range(4)] + shear[t][s] = m + first, second = (M0, M1) if axis == 0 else (M1, M0) + return first, shear, second, mm(second, mm(shear, first)) + + +def oracle(x, data): + first, shear, second, exact4 = data + a = tuple(round(Q(v, 2)) for v in mv(first, x)) + b = mv(shear, a) + out = tuple(round(Q(v, 2)) for v in mv(second, b)) + return out, mv(exact4, x), a + + +def authenticate_context(): + source = json.loads((HERE / 'SOURCES.json').read_text()) + for row in source['context_documents']: + data = (HERE / row['local_path']).read_bytes() + require(sha256(data).hexdigest() == row['sha256'], 'context source hash') + header = b'blob ' + str(len(data)).encode() + b'\0' + from hashlib import sha1 + require(sha1(header + data).hexdigest() == row['git_blob'], 'context Git blob') + return len(source['context_documents']) + + +def check_witnesses(rows): + require(type(rows) is list and len(rows) == 24, 'witness count') + seen = set() + for row in rows: + require(type(row) is list and len(row) == 8 + and all(type(v) is int for v in row), 'witness row type') + t, s, c, j, *x = row + require((t, s) in PAIRS and c in (-1, 1) and 0 <= j < 4, 'witness key') + require(all(v in (-1, 0, 1) for v in x), 'small witness input') + require((t, s, c) not in seen, 'duplicate witness') + seen.add((t, s, c)) + zero = oracle(x, dense_data(t, s, 0)) + one = oracle(x, dense_data(t, s, 1)) + require(zero[2][s] == 0, 'rounded shear source must vanish') + require(4 * zero[0][j] - zero[1][j] == 3, 'witness intercept') + require(zero[1][j] - one[1][j] == c, 'witness slope') + # With rounded source zero, the rounded trajectory is independent of m; + # the exact matrix is affine in m. These two identities suffice for all m. + for m in (0, c, c * 83, c * (2**200 + 1)): + got = literal(x, t, s, m) + other = oracle(x, dense_data(t, s, m)) + require(got == other, 'witness engines disagree') + require(4 * got[0][j] - got[1][j] == 3 + c * m, 'witness line') + require(seen == {(t, s, c) for t, s in PAIRS for c in (-1, 1)}, 'witness coverage') + + +def census(): + """Complete input residues and coefficient residues; compare EVERY output.""" + counts = 0 + transcript = sha256() + for t, s in PAIRS: + for r in range(4): + data = dense_data(t, s, r) + # For m=r+4q, four-times error is slope*m+intercept. + maxima = {-1: -10**9, 0: -10**9, 1: -10**9} + minima = {-1: 10**9, 0: 10**9, 1: 10**9} + for x in product(range(8), repeat=4): + got = literal(x, t, s, r) + other = oracle(x, data) + require(got == other, 'residue engines disagree') + out, exact4, stored = got + first = butterfly_numerators(x, 0) + d = [0] * 4 + d[t] = 2 * stored[s] - first[s] + slopes = butterfly_numerators(d, 1) + for j, c in enumerate(slopes): + require(c in (-1, 0, 1), 'coefficient slope') + a = 4 * out[j] - exact4[j] - c * r + maxima[c] = max(maxima[c], a) + minima[c] = min(minima[c], a) + transcript.update(json.dumps(got, separators=(',', ':')).encode() + b'\n') + counts += 1 + require(maxima == {-1: 3, 0: 3, 1: 3}, 'upper affine envelope') + require(minima == {-1: -3, 0: -3, 1: -3}, 'lower affine envelope') + return counts, transcript.hexdigest() + + +def shifted_controls(): + rng = random.Random(83) + count = 0 + for _ in range(768): + t, s = rng.choice(PAIRS) + m = rng.choice((-83, -9, -4, -1, 0, 1, 4, 9, 83, 2**90 + 1)) + x = tuple(rng.randrange(-20, 21) for _ in range(4)) + z = tuple(rng.randrange(-2**40, 2**40) for _ in range(4)) + shifted = tuple(a + 8 * b for a, b in zip(x, z)) + base = literal(x, t, s, m) + moved = literal(shifted, t, s, m) + require(moved == oracle(shifted, dense_data(t, s, m)), 'large signed oracle') + e = tuple(4 * a - b for a, b in zip(*base[:2])) + e_shift = tuple(4 * a - b for a, b in zip(*moved[:2])) + require(e == e_shift, 'period-eight error') + next4 = literal(x, t, s, m + 4) + d = [0] * 4 + d[t] = 2 * base[2][s] - butterfly_numerators(x, 0)[s] + slopes = butterfly_numerators(d, 1) + require(tuple(4 * a - b - old for a, b, old in zip(next4[0], next4[1], e)) + == tuple(4 * c for c in slopes), 'coefficient-period slope') + require(max(map(abs, e)) <= abs(m) + 3, 'sharp upper bound') + count += 1 + # Reversing the two distinct axes is a coordinate permutation (1 <-> 2). + swapped = 0 + perm = (0, 2, 1, 3) + for t, s in PAIRS: + for m in (-1, 0, 1): + data = dense_data(t, s, m, axis=1) + for x in product((-1, 0, 1), repeat=4): + got = literal(x, t, s, m, axis=1) + require(got == oracle(x, data), 'reverse-axis oracle') + standard = literal(tuple(x[i] for i in perm), perm[t], perm[s], m) + require(got == tuple(tuple(v[i] for i in perm) for v in standard), + 'axis conjugacy') + swapped += 1 + return count, swapped + + +def rejection_controls(rows): + rejected = [] + faults = ('floor-ties', 'omit-shear', 'reverse-shear', 'repeat-axis', + 'wrong-difference', 'omit-exact-shear', 'single-final-round') + for fault in faults: + detected = False + for t, s in PAIRS: + for m in (-1, 1): + data = dense_data(t, s, m) + for x in product((-1, 0, 1), repeat=4): + if literal(x, t, s, m, fault=fault) != oracle(x, data): + detected = True + break + if detected: + break + if detected: + break + require(detected, 'undetected semantic fault: ' + fault) + rejected.append(fault) + for name, altered in ( + ('missing-witness', rows[:-1]), + ('duplicate-witness', rows[:-1] + rows[:1]), + ('zeroed-witness', [rows[0][:4] + [0] * 4] + rows[1:]), + ('wrong-slope', [rows[0][:2] + [-rows[0][2]] + rows[0][3:]] + rows[1:]), + ('boolean-certificate', [[True] + rows[0][1:]] + rows[1:]), + ): + try: + check_witnesses(altered) + except ValueError: + rejected.append(name) + else: + raise ValueError('accepted malformed certificate: ' + name) + for name, args in ( + ('off-grid', ((Q(1, 2), 0, 0, 0), 0, 1, 1)), + ('fractional-shear', ((0, 0, 0, 0), 0, 1, Q(1, 2))), + ('aliased-shear', ((0, 0, 0, 0), 0, 0, 1)), + ): + try: + literal(*args) + except ValueError: + rejected.append(name) + else: + raise ValueError('accepted outside-domain input: ' + name) + # A unit shear defeats the unsheared 3/4 bound, while removing it restores 3/4. + x, t, s, m = (0, -1, -1, -1), 0, 1, -1 + out, exact4, _ = literal(x, t, s, m) + require(out == (0, 0, 0, 0) and exact4 == (-4, 1, 0, 1), 'unit-shear witness') + plain = literal(x, t, s, 0) + require(max(abs(4*a-b) for a,b in zip(*plain[:2])) == 3, 'unsheared control') + rejected.append('unchanged-three-quarter-bound') + return rejected + + +def generate_witnesses(): + rows = [] + for t, s in PAIRS: + for c in (-1, 1): + found = None + for x in product((-1, 0, 1), repeat=4): + zero = oracle(x, dense_data(t, s, 0)) + one = oracle(x, dense_data(t, s, 1)) + if zero[2][s]: + continue + for j in range(4): + if (4 * zero[0][j] - zero[1][j] == 3 + and zero[1][j] - one[1][j] == c): + found = [t, s, c, j, *x] + break + if found is not None: + break + require(found is not None, 'witness search exhausted') + rows.append(found) + return rows + + +def main(): + require(sys.argv[1:] in ([], ['--emit-result'], ['--emit-witnesses']), 'unknown option') + if sys.argv[1:] == ['--emit-witnesses']: + rows = generate_witnesses() + print('{\n "schema": "walsh-integer-shear-witnesses/v1",\n' + ' "columns": ["target", "source", "slope", "output", "x0", "x1", "x2", "x3"],\n' + ' "rows": [\n' + ',\n'.join(' ' + json.dumps(r) for r in rows) + '\n ]\n}') + return + sources = authenticate_context() + certificate = json.loads((HERE / 'WITNESSES.json').read_text()) + require(set(certificate) == {'schema', 'columns', 'rows'}, 'certificate fields') + require(certificate['schema'] == 'walsh-integer-shear-witnesses/v1', 'certificate schema') + require(certificate['columns'] == ['target', 'source', 'slope', 'output', + 'x0', 'x1', 'x2', 'x3'], 'certificate columns') + rows = certificate['rows'] + for n in range(-1025, 1026): + require(half_even(n) == round(Q(n, 2)), 'signed half rounding') + check_witnesses(rows) + cases, digest = census() + periods, axes = shifted_controls() + rejected = rejection_controls(rows) + result = { + 'status': 'PASS_WALSH_INTERLEAVED_SHEAR', + 'exact_error_in_grid_units': '(|m|+3)/4', + 'scope': 'two distinct normalized real Walsh axes, one integer shear', + 'context_documents': sources, 'rounding_cases': 2051, 'witnesses': len(rows), + 'complete_residue_inputs': cases, 'complete_output_comparisons': 4 * cases, + 'full_output_transcript_sha256': digest, + 'large_signed_period_and_coefficient_cases': periods, + 'reverse_axis_cases': axes, 'rejected_controls': rejected, + 'no_new_kappa': True, + } + if sys.argv[1:] != ['--emit-result']: + expected = json.loads((HERE / 'RESULT.json').read_text()) + require(json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), + 'committed result differs from computed result') + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main()