Audit #6129's nearest-even Walsh-stage bound: no error; independent engines reproduce a_J, the odd-output split and #6119's 3h/4 (no new κ)

research/nearest-even-walsh-error-audit/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<J/2` for 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.

research/nearest-even-walsh-error-audit/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "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"
+    }
+  ]
+}

research/nearest-even-walsh-error-audit/TASK.json

@@ -0,0 +1,89 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "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_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "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": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Independent adversarial audit of open PR #6129 (head f496734450c346468c66818c1c35521165b0cdda): sharp nearest-even normalized Walsh-stage error h(J/3+(1-(-1/2)^J)/9), its odd-output refinement, and its all-grid 3h/4 application to PR #6119 (head bdfe5a10d488b5f774e906d8d4588dc8da25e7ba).",
+  "scope_change_reason": "The card asks for a proof of an inherited assumption; #6129 claims one precision implication under this card, and a fresh, unreviewed proof is most useful checked independently before anyone relies on it.",
+  "bottleneck_link": "Side result for precision obligations: confirms (or would refute) a deterministic rounding budget that a deferred-row/Walsh supplier could cite. No supplier, invoice or kappa changes.",
+  "budget_minutes": 40,
+  "stop_rule": "Stop after a step-by-step proof review plus independent exact engines reproduce or refute each stated number; report any gap found rather than repairing #6129.",
+  "outcome": "completed",
+  "evidence": "PROOF.md reviewed step by step: no error. verify.py: residue-tracking tree sets J<=7 (all 2^J sign patterns for J<=4) give even/odd maxima a_J/a_(J-1); literal 8-point network exhaustive on [-3,0]^8 in three orders gives 9/8; rebuilt #6119 surrogate exhaustive per fiber mod 8h gives 3h/4 with #6129's witness; controls: ties-to-odd same law, floor and ties-away reach J/2, ties-to-odd leaves #6119's echo dirty. Local-only: rebuild agrees with #6119 forward() on 3000 random grid inputs.",
+  "author": "Josie Elliston with Claude Opus 5.5 (Anthropic) assistance",
+  "ai_assistance": "Claude Opus 5.5 (Anthropic) wrote the review and verifier under Josie Elliston's donated session; no code from #6129 or #6119 is imported.",
+  "open_questions": [
+    {
+      "question": "Which retained rounded compilers rely on a ties-to-even half-tie cancellation like #6119's m=1/2 lower inverse?",
+      "why_it_matters": "Engine D shows the cancellation fails under ties-to-odd although the Walsh law does not; a tie-rule change would silently dirty such echoes.",
+      "first_step": "Search retained rounded shear/echo packages for m=1/2 cancellations and test each under ties-to-odd.",
+      "blocked_by": "none"
+    },
+    {
+      "question": "Does the sharp a_J law survive one intervening grid shear between rounded Walsh stages?",
+      "why_it_matters": "#6129 excludes intervening gates; real suppliers interleave them.",
+      "first_step": "Add one integer shear stage to engine A's residue-tracking enumeration.",
+      "blocked_by": "none"
+    }
+  ]
+}

research/nearest-even-walsh-error-audit/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Engines A-D: residue-tracking tree sets J<=7 (all sign patterns J<=4), literal J=3 box exhaustion in three stage orders, #6119 surrogate fiber exhaustion mod 8h with period samples, rounding-rule controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "The same exact checks with assertions disabled (the verifier uses explicit raises)."
+    }
+  ]
+}