Independently check PR4100's good-packet normal form on small rings (no new κ)

research/normal-form-exhaustive-audit/README.md

@@ -0,0 +1,93 @@
+# Independent check of PR4100's good-packet normal form
+
+**No new κ. Finite certificate plus a written re-derivation of one algebraic
+identity.** This is not an all-size multiplication theorem, and it does not
+review any other part of PR4100.
+
+## Proposition checked
+
+[NORMAL-FORM.md](../unconditional-batched-crt/NORMAL-FORM.md) in Cinna Davis's
+PR4100 package states the following. Let R be a commutative ring, C the
+m-coordinate reversal, and P an idempotent with a free rank-r image. Suppose
+unit-pivot northeast elimination gives unit lower triangular L and R0 with
+`T = L P C R0 = E D C`. Put `U = L P L^-1`, `S0 = R0^-1 C L^-1`,
+`J = C D^-1 E`, `X = S0 E - J U` and `Q = [[I,0],[X,I]] diag(L,R0^-1)`. Then
+
+    Q N(P) Q^-1 = [[I-E, T], [J, I-JT]],   N(P) = [[I-P, PC], [CP, I-CPC]],
+
+which is one weighted reversed r-coordinate child. The note also states that the
+retained `controlled_normalizer.py` builds exactly this X. PR4100's AUDIT.md
+uses the identity for the BIT good branch (row "Local-ring split ranks").
+
+## Result
+
+**Written re-derivation.** Given `T = E D C`, each step follows over any
+commutative ring: `TS0=U`, `TJ=E` (E and D commute), `ET=T`, `UT=T`
+(P idempotent), `EU=U` (im U = im T lies in the first r coordinates),
+`UE=E` (U projects onto that summand) and `TX = E-U`. Conjugating
+`diag(L,R0^-1) N(P) diag(L^-1,R0) = [[I-U,T],[S0U,I-S0T]]` by `[[I,0],[X,I]]`
+gives `I-U-TX = I-E`, lower right `I+XT-S0T = I-JT`, and lower left
+`S0E - XE = J` because `JE = J`. I found no gap. The only hypothesis is
+`T = E D C`, which needs the Schur block to vanish over R. The note's split-rank
+argument covers that, and the verifier checks it on every instance.
+
+**Finite certificate** (`verify.py`, about 7 s, standard library):
+
+| Domain | Mode | Rank-r idempotents | Good packets |
+|---|---|---:|---:|
+| Z/3, Z/5, Z/7, Z/9, Z/25, Z/27 at m=2; Z/3 at m=3 | every m×m matrix | 2,162 | 1,332 |
+| Z/9 m=3; Z/27 m=4; Z/25 m=4; Z/9 m=5 | seeded charts, every axis set | 4,080 | 1,763 |
+
+- Every idempotent census equals the closed form `|GL_m(R)|/(|GL_r(R)| |GL_(m-r)(R)|)`,
+  so the exhaustive rows miss no idempotent.
+- On each good packet, the elimination factors are unit lower triangular, the
+  Schur block is zero over R, every written equality holds, and the conjugation
+  equals the weighted reversed child with weights `delta_k`, `delta_k^-1`.
+- In the exhaustive domains, the good fraction over Z/q^w equals the fraction
+  over Z/q (63/108 = 567/972 = 7/12 for q=3), as expected if the pivot
+  itinerary depends only on the residue class.
+- **Vendor agreement**, 2,177 cases: the retained `prepare` gives the same
+  pivots and a `cross` matrix equal to the written X. On every basis address,
+  `execute_addresses` with random head unit weights A equals `B N(P) B^-1`, where
+  `B = diag(A, I)`. On every bad chart in this comparison, the vendor rejects with
+  "nongeneric low class".
+- **Mutation controls**: `X = S0E - J`, the cancellation the note warns
+  about, fails in 3,325 of 3,509 checked instances. `X = S0E - UJ` fails in all 3,509.
+
+## Limitations
+
+The table rows are finite. The all-ring claim rests on the written
+re-derivation above, which has no formal proof-kernel check. The vendor
+comparison uses `f = 1` atom columns. Larger f is covered only by the note's
+fiber argument, which I did not execute. This does not check FALLBACK.md, BIT.md
+costs, the Schwartz–Zippel bad-packet rate or any downstream caller.
+
+## Reproduce
+
+From the repository root:
+
+```sh
+python3.12 -B research/normal-form-exhaustive-audit/verify.py
+python3.12 -B scripts/research_package.py --package research/normal-form-exhaustive-audit
+```
+
+The expected last line is `PASS_NORMAL_FORM_EXHAUSTIVE_AUDIT`. Exact pins are in
+[SOURCES.json](SOURCES.json).
+
+## Open next questions
+
+1. BIT.md bounds the bad low-class fraction by `2*64^3/q` using Schwartz–Zippel
+   and charges bad packets at `eta = 1e-16` per request. Is that rate a count over
+   a complete header enumeration or a probability over random headers? If headers
+   are adversarial, every request could be bad. First step: trace how BIT.md
+   generates request headers.
+2. FALLBACK.md's 49,911-child bound charges three children per swap.
+   Opposite-orientation swaps use one child under `paid_children`, so the bound
+   is not sharp. This cannot move κ at `eta = 1e-16`, but a sharp count would
+   tighten F.
+
+## Credit
+
+Proposition and retained source: Cinna Davis (PR4100), building on source527,
+commdata2338 (PR2160) and Jose Manuel (`controlled_normalizer.py`). This check
+produced by Nick Petalas. Apache-2.0.

research/normal-form-exhaustive-audit/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/selected-bit-recursive-closure/vendor/controlled_normalizer.py",
+      "usage": "input",
+      "git_blob": "3e8a72e7ce705c51ff24e9015ccf6463204ff193",
+      "sha256": "401605930f674bd3c27337687fe7425f0d8776703c83bfd42d4c0e10cae6fb77"
+    },
+    {
+      "path": "research/unconditional-batched-crt/NORMAL-FORM.md",
+      "usage": "input",
+      "git_blob": "a0e1d5b370fe34174575f9773bf9981188643fc5",
+      "sha256": "8649127267c0658b699d5bb16a0a5ac3f1bbd7395d2dbd738c1145a0a65ae09c"
+    }
+  ]
+}

research/normal-form-exhaustive-audit/TASK.json

@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "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": "changed",
+  "actual_scope": "One proposition of PR4100: NORMAL-FORM.md's good-packet conjugation identity Q N(P) Q^-1=[[I-E,T],[J,I-JT]] over Z/q^w, its intermediate equalities, and its stated agreement with the retained controlled_normalizer.py coefficients and executed weighted address map.",
+  "scope_change_reason": "The card prioritizes CRT.md total repair and COMPLEX.md free-algebra lift, which open PRs already audit. NORMAL-FORM.md is the BIT good-branch premise in PR4100's AUDIT table and had no independent check. Its quantified statement is an all-ring algebraic identity, so it is checked by a written re-derivation plus an exhaustive small-ring certificate, not substituted by a smoke test.",
+  "bottleneck_link": "Side result for PR4100 acceptance: it settles one premise of the BIT good branch (AUDIT.md row 'Local-ring split ranks'). It changes no supplier, exponent or selected record.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first failed written equality or vendor disagreement and report it; otherwise stop after the bounded domains below.",
+  "outcome": "completed",
+  "evidence": "verify.py: 2,162 rank-r idempotents (1<=r<m) in seven exhaustive (ring, m) domains, with the census matched to the closed form |GL_m|/(|GL_r||GL_(m-r)|); 1,332 good packets among them; 1,763 good packets among 4,080 sampled chart projectors up to m=5; 3,509 good instances checked in total, including vendor-comparison charts; 2,177 vendor agreements on cross and the executed weighted map; both mutation controls rejected.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does the Schwartz-Zippel bad-packet bound 2*64^3/q in BIT.md hold per request for the actual header distribution, rather than for uniformly random low classes?",
+      "why_it_matters": "The recurrence charges bad packets at rate eta=1e-16; a worst-case header stream could make every request bad.",
+      "first_step": "Identify in BIT.md how request headers are generated and whether the bad fraction is a count over a complete packet enumeration or a probability.",
+      "blocked_by": "none"
+    },
+    {
+      "question": "Is FALLBACK.md's 49,911-child bound sharp for the retained paid_children rule?",
+      "why_it_matters": "Opposite-orientation swaps cost one child, not three; a sharper count tightens F but cannot change kappa materially at eta=1e-16.",
+      "first_step": "Count same- and opposite-orientation swaps in compile_program for m=64 at the worst pivot itinerary.",
+      "blocked_by": "none"
+    }
+  ]
+}

research/normal-form-exhaustive-audit/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/selected-bit-recursive-closure/vendor/controlled_normalizer.py",
+    "research/unconditional-batched-crt/NORMAL-FORM.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Exhaustive small-ring census and NORMAL-FORM identity, sampled charts to m=5, vendor cross/executed-map agreement, two mutation controls"
+    }
+  ]
+}