Audit #4100 BIT.md's local-ring algebra, row stock, depth, recurrence and wrapper: all hold (no new κ)

research/bit-stock-recurrence-audit/README.md

@@ -0,0 +1,106 @@
+# Audit of #4100 BIT.md: local-ring algebra, row stock, depth, recurrence and wrapper
+
+**Audit with a positive scoped result; no new κ.** The selected κ is unchanged.
+
+Pinned #4100 head: `337d04939571a637aeab54a0f58f54fde811663a`
+(`research/unconditional-batched-crt/BIT.md`).
+
+The #4311 coverage map lists BIT.md's "row stock, whole high packets and fixed
+tapes" and "weighted leaves and fast header routes" with no #4100-specific
+audit. This package checks every finite or algebraic statement in BIT.md
+§1–§4. The moments `mu_1`, `mu_(1-c)` and the body word are #4330's and are
+used, not re-certified.
+
+## Results
+
+| Statement in BIT.md | Outcome |
+|---|---|
+| §1: `q = 2^89-1` prime; `2·64^3/q < 10^-16` | Holds. Primality is confirmed by Lucas–Lehmer, independently of #4100's Pratt certificate. The bound is 8.5·10^-22. |
+| §1: `N(P) = [[I-P,PC],[CP,I-CPC]]` gives `N(P)^2 = I`; disjoint commuting projectors add; nested differences multiply; conjugation by `diag(A,I)` keeps these; split rank over `Z/q^w` | Holds when C is an involution, as NORMAL-FORM.md's coordinate reversal is (proof below). Checked exactly on 150 instances over `Z/3`, `Z/27`, `Z/25`, `Z/49` and `Z/961`, with C the reversal or a random involution. The rank of P mod q equals its split rank. |
+| §2: `K(w) = 269241600 N q^(4096(w-1))`, and splitting family, low matrix and high matrix leaves `U = 9475 t K^(D-1)` | Holds exactly, with `269241600 = W·9475` and `N q^(4096(w-1)) = |GL_64(Z/q^w)|`. The order formula is proved below and brute-forced on small rings. Exact big-integer division (N has 364,544 bits) gives U, and every child's stock divides it, for w = 1, 2 and D = 1..3. |
+| §2: D monotone; every child `r floor(n/64)`, r ≤ 42, drops D; two coarse levels halve; `h ≤ 2 log2 e + O(1)` | Holds (proof below). Scanned for n ≤ 3·10^5 (3·10^6 in the development run); `max(D − 2 log2 n) = −11`. |
+| §3: header routes come from the low-digit carry plus an ordered high-field addition; doubling and halving are a two-piece split/interleave | Holds: the identity `xA = (x_lo A_lo mod q) + q(carry + x_lo A_hi + x_hi A)` is checked over `Z/q^w` on 800 cases, and doubling maps `[0,(M+1)/2)` onto the evens and the rest onto the odds. |
+| §3: `F = 32·64^2·ΣH = 118606528512`; the fallback's at most 49,911 children fit `32·64^2` | Holds. |
+| §3: the recurrence gives `T ≤ C/(1-mu_1) n + C/(1-mu_t) n^t w^(1-a)` | The induction is correct (below). The equality recursion stays below the envelope for a ∈ {0, a1}, w ∈ {1, 10, 10^6} and n up to 10^9, and it is monotone, which the `max_(j≤f)` step needs. |
+| §4: `k = O_q(w log(e+1)) = o(e)`; elementary fallback only at finitely many widths | Holds. With the literal constants, `2k < e` and `n ≥ 64` first hold at `e = 2^19` (k ≈ 1.6·10^5) and keep holding up to `2^400`. |
+| §4: stage cost `O(V e^(1-c+c^2-ca))`, `a_next = c(1-c)+ca`, reaching `a2` | Holds exactly. Every cost term (`n`, `n^(1-c) w^(1-a)`, `k`, `w`) is dominated because `a ≤ c`. |
+
+**Minor wording.** §2 says each child's payload has volume `V/(WN)`. The split
+also divides by the high-matrix fibre `q^(4096(w-1))`, so the payload is
+`V/(W N q^(4096(w-1)))`. It is smaller, so the geometric-series step holds a
+fortiori.
+
+## Proofs
+
+**`N(P)` identities.** Let `C^2 = I`.
+- For an idempotent P, the top-left block of `N(P)^2` is
+  `(I-P)^2 + PC·CP = I - P + P = I`. The top-right block is
+  `(I-P)PC + PC(I-CPC) = PC - P^2C = 0`, and the other two blocks are
+  symmetric.
+- For idempotents with `P1 P2 = P2 P1 = 0`, multiplying `N(P1) N(P2)`
+  block by block gives `N(P1+P2)`, because every cross term carries
+  `P1 P2` or `P2 P1`.
+- For `Q = PQ = QP`, the same expansion gives `N(P) N(Q) = N(P-Q)`.
+- Conjugation by `diag(A,I)` is an algebra automorphism, so it keeps all
+  three identities.
+- Over the local ring `Z/q^w`, an idempotent's image is free with rank equal
+  to its rank mod q (idempotents lift uniquely). The characteristic
+  polynomial is `x^(n-r) (x-1)^r`.
+
+The controls in `test_verify.py` show that `N(P)^2 = I` fails for a
+non-involution C, and that additivity fails for overlapping projectors.
+
+**`|GL_n(Z/q^w)|`.** Reduction mod q is surjective onto `GL_n(F_q)`. Its
+kernel is `{I + qM}`, which has `q^(n^2 (w-1))` elements, because every such
+matrix is a unit. So `K(w)/269241600 = |GL_64(Z/q^w)|`, and dividing
+`R = t K^D` by `W·|GL_64(Z/q^w)|` leaves `9475 t K^(D-1)`.
+
+**Depth.** `floor(n/64)` is nondecreasing, so D is nondecreasing. A child
+`r floor(n/64)` with `r ≤ 42` has `D ≤ D(42 floor(n/64)) = D(n)-1`. Two levels
+multiply the width by at most `(42/64)^2 < 1/2`, so
+`D(n) ≤ 2 log2 n + O(1)`.
+
+**Recurrence.** Put `A = C/(1-mu_1)` and `B = C/(1-mu_t)`, where
+`mu_x = (Σ_r H_r (r/64)^x + η F (1/64)^x)/W`. Since `rf ≤ rn/64`, the
+children contribute at most `mu_1 A n + mu_t B n^t w^(1-a)`. The `max_(j≤f)`
+term is bounded by the envelope at f, which is monotone. The local toll
+`C(n + w^(1-a))` is absorbed because `A(1-mu_1) = C` and
+`B(1-mu_t) n^t ≥ C`. Leaves need `B ≥ C`.
+
+**Wrapper exponents.** With `w = e^c` and `n ≈ e^(1-c)`, the term
+`n^(1-c) w^(1-a)` gives `e^(1-c+c^2-ca)`. The other terms have exponents
+`1-c` and `c`, both at most that, because `a ≤ c`. The identity
+`(1-c)^2 + c(1-a) = 1 - a_next` gives `a1 = c(1-c)` and
+`a2 = c(1-c^2)`.
+
+## Not covered
+
+- The PR2809 block construction itself: the encoded continuation stack,
+  stream serialization, capsule copying and restoration.
+- The finite word certificate and owner data, which `evidence/bit-local-ring-current.log` replays.
+- The Schwartz–Zippel density step, which #4227/#4228 audit.
+
+These are prose constructions or are audited elsewhere.
+
+## Validation
+
+```sh
+python3.12 -B research/bit-stock-recurrence-audit/verify.py
+python3.12 -B research/bit-stock-recurrence-audit/test_verify.py
+python3.12 scripts/research_package.py --package research/bit-stock-recurrence-audit
+```
+
+The finite checks support the written proofs; they do not replace them.
+
+## Credit
+
+The construction is by Cinna Davis (#4100). The moment certificate is #4330
+(pinterbanget), and the coverage map is #4311 (Ryanson Jonathan). Prepared for
+Mark (Matarener) with substantial Claude Code assistance. Apache-2.0.
+
+## Open next questions
+
+Does the PR2809 block construction's encoded stack keep the claimed `O_q(V)`
+visited space when the continuation is serialized at every recursive cut, at
+the new c? First step: bound the parked bytes per ancestor level against
+`V/(W N q^(4096(w-1)))^level`. See `TASK.json`.

research/bit-stock-recurrence-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/unconditional-batched-crt/BIT.md",
+      "usage": "input",
+      "git_blob": "2aa2544fa61259ac48b936b8c906ec9d31d813fa",
+      "sha256": "83a0cc082e52219a5f142becc8b5b92019e091cb3ede6c5bccbd8508993fc4da"
+    },
+    {
+      "path": "research/unconditional-batched-crt/NORMAL-FORM.md",
+      "usage": "input",
+      "git_blob": "a0e1d5b370fe34174575f9773bf9981188643fc5",
+      "sha256": "8649127267c0658b699d5bb16a0a5ac3f1bbd7395d2dbd738c1145a0a65ae09c"
+    }
+  ]
+}

research/bit-stock-recurrence-audit/TASK.json

@@ -0,0 +1,74 @@
+{
+  "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": "refined",
+  "actual_scope": "One #4100 obligation group: every finite or algebraic statement of BIT.md sections 1-4 (local-ring N(P) algebra, row-stock split, depth recursion, header-route arithmetic, recurrence induction, wrapper threshold and stage exponents).",
+  "scope_change_reason": "The #4311 coverage map lists BIT.md's row stock and header routes with no #4100-specific audit; #4330 covers only the moments, so this package checks the remaining finite and algebraic claims.",
+  "bottleneck_link": "Side result for the #4100 admission audit: confirms the finite and algebraic layer of the BIT auxiliary theorem; it does not move the selected frontier.",
+  "budget_minutes": 90,
+  "stop_rule": "Stop after the finite and algebraic statements of BIT.md sections 1-4 are checked; do not audit the prose PR2809 block construction or re-certify #4330's moments.",
+  "outcome": "completed",
+  "evidence": "Written proofs in README.md; verify.py binds sources and checks every finite statement; test_verify.py has rejecting controls.",
+  "author": "Mark (Matarener)",
+  "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.",
+  "open_questions": [
+    {
+      "question": "Does the PR2809 block construction's serialized continuation stack keep O_q(V) visited space at the new c when it parks at every recursive cut?",
+      "why_it_matters": "BIT.md's space bound relies on the parked ancestor volumes forming a geometric series including stack encodings.",
+      "first_step": "Bound the parked bytes per ancestor level against V/(W N q^(4096(w-1)))^level and add the encoding overhead per level.",
+      "blocked_by": "none"
+    }
+  ]
+}

research/bit-stock-recurrence-audit/VERIFY.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/unconditional-batched-crt/BIT.md",
+    "research/unconditional-batched-crt/NORMAL-FORM.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Bind BIT.md statements; Lucas-Lehmer for 2^89-1 and the constants; N(P) identities over Z/q^w; exact stock split and child divisibility; depth, halving; header-route carry decomposition and doubling; recurrence envelope; wrapper threshold; stage exponents."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/test_verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Rejecting controls: non-involution C, overlapping projectors, wrong stock factor, one extra rank-1 child, small widths in the wrapper, and an omitted carry all fail."
+    }
+  ]
+}

research/bit-stock-recurrence-audit/test_verify.py

@@ -0,0 +1,66 @@
+#!/usr/bin/env python3
+"""Rejecting controls for verify.py."""
+import random
+import unittest
+
+import verify as v
+
+
+class Controls(unittest.TestCase):
+    def test_non_involution_breaks_square(self):
+        rng = random.Random(5)
+        p, m, n = 5, 25, 5
+        broke = 0
+        for _ in range(20):
+            S, Si = v.unit(n, p, m, rng)
+            P = v.mm(v.mm(S, [[int(i == j and i < 2) for j in range(n)] for i in range(n)], m), Si, m)
+            C, _ = v.unit(n, p, m, rng)
+            if v.mm(C, C, m) == v.eye(n):
+                continue
+            NP = v.N(P, C, m)
+            broke += v.mm(NP, NP, m) != v.eye(2 * n)
+        self.assertGreater(broke, 10)
+
+    def test_overlapping_projectors_do_not_add(self):
+        rng = random.Random(6)
+        p, m, n = 7, 49, 5
+        S, Si = v.unit(n, p, m, rng)
+        proj = lambda idx: v.mm(v.mm(S, [[int(i == j and i in idx) for j in range(n)]
+                                         for i in range(n)], m), Si, m)
+        C = v.reversal(n)
+        P, Q = proj([0, 1]), proj([1, 2])
+        self.assertNotEqual(v.N(v.add(P, Q, m), C, m), v.mm(v.N(P, C, m), v.N(Q, C, m), m))
+
+    def test_wrong_stock_factor_fails(self):
+        Nq = v.gl_order(64, v.q)
+        K = 269241600 * Nq
+        U, r = divmod(K ** 2, v.W * Nq)
+        self.assertEqual(r, 0)
+        self.assertNotEqual(U, 9474 * K)
+
+    def test_moment_with_extra_rank_one_child_fails(self):
+        saved = dict(v.H)
+        try:
+            v.H[1] += 1
+            self.assertGreater(v.mu(1 - float(v.c)), 1.0)  # #4330's sensitivity remark
+        finally:
+            v.H.clear()
+            v.H.update(saved)
+
+    def test_wrapper_fails_for_small_widths(self):
+        e, w, k = v.wrapper_k(10)
+        self.assertFalse(2 * k < e)
+
+    def test_carry_omitted_breaks_route(self):
+        p, m = 5, 125
+        x, A = [7, 99], [[13, 88], [41, 3]]
+        y = [sum(x[i] * A[i][j] for i in range(2)) % m for j in range(2)]
+        xl, xh = [t % p for t in x], [t // p for t in x]
+        Al, Ah = [[t % p for t in r] for r in A], [[t // p for t in r] for r in A]
+        lo = [sum(xl[i] * Al[i][j] for i in range(2)) % p for j in range(2)]
+        hi = [sum(xl[i] * Ah[i][j] + xh[i] * A[i][j] for i in range(2)) % 25 for j in range(2)]
+        self.assertNotEqual(y, [a + p * b for a, b in zip(lo, hi)])
+
+
+if __name__ == "__main__":
+    unittest.main()