Audit #4359 BIT row stock and its #4470 atom change (no new κ)

research/bit-row-stock-atom-audit/README.md

@@ -0,0 +1,119 @@
+# Audit of the #4359 BIT row stock and its #4470 atom change
+
+**Audit with a positive scoped result; no new κ.** The selected κ is unchanged.
+
+Base: `f626db5c3` (main after the #4470 review). This package independently
+checks the BIT row-stock formulas that #4359 introduced, and the way the
+#4440 → #4470 chain reuses them after raising the atom power from `0.003` to
+`0.004`. The intake review of #4359 (`docs/research/pr-intake-evidence/pr4359/PROOF-REVIEW.md` §4)
+argued the outer reserve in prose; no numerical or finite check of these
+formulas existed.
+
+## Statements checked
+
+| Statement | Source | Outcome |
+|---|---|---|
+| `a_BIT = (1-δ)C1 + δ a_old` with `δ > a_BIT` (linear adapter paid), `δ < 1-a_BIT` (stock lower order) and the middle-exponent identity | DELAYED-COVER-BRIDGE §8; `query-thinned-controllers/verify.py` | Holds exactly: `0.0027418653797` (#4359, δ=.003) and `0.0034363538396` (#4470, δ=.004). With δ=.003 the #4470 adapter would fail, as its verifier says. |
+| Cover prime `q > (256/d) N^5` gives fallback moment `(1+d/4)/(1+d/2) < 1` | DELAYED-COVER-BRIDGE §7 | Holds for `25,600,000` (#4359) and `2^26` (#4470). |
+| Reserve `W(w)^D S_old`, `W(w) = B|GL_N(F_q)| q^(N^2(w-1))`, `D = floor(log_N ceil(e/w))` | DELAYED-COVER-BRIDGE §8 | Holds. `|GL_N(Z/q^w)| = |GL_N(F_q)| q^(N^2(w-1))` is brute-forced on small rings. The reserve divides exactly through D levels, and floor recursion has depth `floor(log_N n)`. The high-matrix factor is present, unlike the #4100 wording noted in #4432. |
+| Borrowed digits `k = O(w log e) = o(e)` | DELAYED-COVER-BRIDGE §8 | Holds. With `log2 N = 6552928412` (#4359) or `25986965159937` (#4470 BIT), `2k < e` from `log2 e ≈ 2 log2 N/(1-δ)`: `1.3145·10^10` and `5.2183·10^13`. It keeps holding afterwards. |
+| BIT-call width `≤ C h (log p)^2` | OUTER-TRANSFER-AUDIT §5, from SUPPLIER-SUPPORT-AUDIT | Holds with an explicit `C`. The exposed support is `2hK` and the three reservoirs add `9kG` with `k = 2hK`. With `K = 128G` and `G = 4⌈log2 p⌉+6`, the width is at most `2hK(1+9G) ≤ 232960 h L^2` for every `L ≥ 1`. |
+| Its stock `O(h^δ (log p)^(1+2δ))`, nesting `log h`, plus complex `O(log h)`, giving `q0 ≤ C(log2 h + h^δ L^3 + 1)` | OUTER-TRANSFER-AUDIT §5 | Holds for both δ, because `2+2δ ≤ 3`. The comparison `e^δ log e ≤ C_w^δ(log2 C_w+3) h^δ L^(1+2δ)` is proved below and checked on a grid. |
+| Threshold `H(p) = [1024 C L^3]^(1/(1-δ))`, `q0+O(1) ≤ h/64`, `R(h) ≤ 3h/128 + q0 + O(1) ≤ h/16` | OUTER-TRANSFER-AUDIT §5 | Holds. For `C ≥ 1` the displayed threshold already suffices; no extra multiple is needed. The phase sum is at most `1.067` times the first phase. |
+| Old ordinary interchanges (`a_old`) act only on atom-width fields, so `S_old` is lower order | `notes/three-stage-cover-bit.tex` (weighted leaves; routing) | Holds. Its role split `W(w) = W_0 q^(m^2(w-1))` agrees with DELAYED-COVER-BRIDGE. |
+| Delayed cover audit: cover size, routing bijection, projector matching, affine high-row carry | `delayed_cover_bridge.py` | Re-implemented independently for `GL_2(Z/9)` (3,888 rows) and `GL_3(Z/4)` (86,016 rows), with true inverses mod `p^w` and the carry for general `w`. Locally I also checked `GL_2(Z/27)` (314,928 rows) and `GL_2(Z/25)` (300,000 rows). All pass. |
+
+## Corrections (wording only; no exponent changes)
+
+1. **The written outer reserve is not updated for #4470.** OUTER-TRANSFER-AUDIT
+   §5 writes `q0(h,p) ≤ C(log2 h + h^0.003 (log2 p)^3 + 1)` and the threshold
+   `[1024 C (log2 p)^3]^(1/(1-0.003))`. The #4440/#4470 chain only says that
+   the new constants are substituted, and it adds the check `β(1-0.004) > 0`.
+   With atom `0.004` the literal display is false for large `h`, since it
+   would need `h^0.001 ≤ C L^0.992`. The argument does not depend on δ. The
+   correct statement for any atom `δ ≤ 1/2` is
+
+   ```
+   q0(h,p) <= C*(log2 h + h^δ*(log2 p)^3 + 1),
+   H(p) = [1024*C*(log2 p)^3]^(1/(1-δ)),
+   ```
+
+   with `δ = 3/1000` for #4359 and `δ = 4/1000` for #4440/#4470. Every
+   conclusion (`R(h) ≤ h/16`, polylog threshold, fit in `p^β`) is unchanged.
+   The pinned file is source-bound by hash in the #4359 receipts, so it is
+   left untouched; this package records the corrected display.
+2. **`β(1-atom) > 0` is weaker than its name.** It is equivalent to `atom < 1`.
+   It accepts, for example, atom `0.99999`, where `δ < 1-a_BIT` fails. The
+   real condition `atom < 1-ordinary` is checked separately in
+   `query-thinned-controllers/verify.py` and `joint-helper-lattice/verify.py`.
+   No gap results.
+3. **Three checks in `delayed_cover_bridge.py` cannot fail.** The projector
+   matching `g P g^-1 = (gS) Q (gS)^-1` is equivalent to `P S = S Q`. Once
+   `P = S Q S^-1` it holds for every `g`, so the 7,776 checks test arithmetic.
+   The weight equality follows from projector equality. The 6,561-address
+   scalar-gauge check builds `before` and `after` from the same expression.
+   The cover size, routing bijection, carry formula and the two negative
+   controls are genuine checks. The companion note's conjugacy argument, not
+   the finite run, carries the claim, as the note itself says.
+
+## Proofs
+
+*Exponents.* The root costs are `e^(1-δ)`, `e^((1-δ)(1-C1)+δ(1-a_old))` and
+`e^δ log e`. The middle exponent equals `1-a_BIT` by expansion. The first is
+at most `1-a_BIT` iff `δ ≥ a_BIT`. The third is lower order iff `δ < 1-a_BIT`.
+
+*Reserve split.* A level's rows are indexed by (role, low class in
+`GL_N(F_q)`, high matrix in `(Z/q^(w-1))^(N^2)`, rest). This is a mixed-radix
+digit of size `W(w)`. Ancestors own distinct digits, so `W^D S_old` rows give
+every simultaneously live level its own digit and leave `S_old` at the leaves.
+
+*Borrowed digits.* `|GL_N(F_q)| < q^(N^2)` gives
+`k ≤ D(N^2 w + log_q B + 1) + log_q S_old + 1`, with `D ≤ log2 e/log2 N`.
+Hence `k/(w log2 e) ≤ (N^2 + o(1))/log2 N`.
+
+*Outer stock.* Let `e = C_w h L^2` with `1 ≤ h ≤ p` and `L = log2 p`. Then
+`log2 e ≤ log2 C_w + 3L` and
+`e^δ log2 e ≤ C_w^δ (log2 C_w + 3) h^δ L^(1+2δ)`. The `log h ≤ L` nesting
+factor and the complex `O(log h)` give `L^(2+2δ) ≤ L^3`.
+
+*Threshold.* If `h^(1-δ) ≥ 1024 C L^3`, then `C h^δ L^3 ≤ h/1024`, and
+`C(log2 h + 2) ≤ h/1024` there as well. The derivative of `h/64 - q0` is
+positive above `H`. So `q0 + O(1) ≤ h/64` and
+`R ≤ 3h/128 + h/64 = 5h/128 ≤ h/16`.
+
+## Scope
+
+Conditional, like #4359 and #4470. Inherited and not re-proved here: the
+outer analytic decomposition and fixed-tape model; that the finite compiler
+really gives each live child distinct physical roles (DELAYED-COVER-BRIDGE
+open question 1); the size of the fixed constant `C`. Thresholds in the
+table use `log2 C ≈ 2 log2 N + 64` only for illustration. The astronomically
+large templates are not materialized.
+
+## Reproduce
+
+```sh
+python3 -B research/bit-row-stock-atom-audit/verify.py       # about 50 s
+python3 -B research/bit-row-stock-atom-audit/test_verify.py  # 7 rejecting controls
+```
+
+The controls cover: the old atom with #4470's `C1`; the literal `h^0.003`
+display at atom `.004`; a broken atom that passes `β(1-atom) > 0`; omitting
+the high-matrix lift; a max instead of a product of stocks; an omitted carry;
+and widths below the borrowed-digit threshold.
+
+## Open next questions
+
+1. Bind the constant `C` of the outer reserve to the actual #4470 template
+   (`N`, `B`, `q`, centers). This would turn the illustrative thresholds into
+   bound ones.
+2. Audit DELAYED-COVER-BRIDGE open question 1. Does the lockstep compiler give
+   each simultaneously live child role a distinct physical array? The
+   row-digit argument above assumes that it does.
+
+## Credit
+
+zxv for #4359 and the delayed-cover bridge; Cinna Davis and zxv for the
+#4440/#4470 controller chain; the capped-phase-fusion support-router and
+three-stage-cover authors credited in those sources. Audit by Mark
+(Matarener), prepared with substantial Claude Code assistance.

research/bit-row-stock-atom-audit/SOURCES.json

@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "notes/three-stage-cover-bit.tex",
+      "usage": "input",
+      "git_blob": "f05225d21f92cf8cef21b6e12601d5b4d61991f0",
+      "sha256": "47123a756f823c83a0d48cca2bf5add6472cd88410b13aed345e70c8834fb511"
+    },
+    {
+      "path": "research/capped-phase-fusion/SUPPLIER-SUPPORT-AUDIT.md",
+      "usage": "input",
+      "git_blob": "ae676a6504cc7987863da1827551c18e7ec20ce1",
+      "sha256": "c41a2571b9c4c1d7920633f10c3ed2c74da39ca3bc8d6a910e6ffed380327413"
+    },
+    {
+      "path": "research/joint-helper-lattice/verify.py",
+      "usage": "input",
+      "git_blob": "0006dd15ca5597edfa506559124d2cdf3c493ae4",
+      "sha256": "8eb13f77a94315f811612cb557a17edeecb6b9d9a75dfa238b112dd6520c336f"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md",
+      "usage": "input",
+      "git_blob": "a58774e237c9362869a60a22bda35be09fb85872",
+      "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/delayed_cover_bridge.py",
+      "usage": "input",
+      "git_blob": "c541a7ea45a5dac49b62078e3aa15585565ad665",
+      "sha256": "96ea0f49a6fc07687e2f932859e5ce18e2b3f42d6e826fdc555c48069560a2ec"
+    },
+    {
+      "path": "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md",
+      "usage": "input",
+      "git_blob": "e8b7ef8956ece5bd493cbf52113916e5dc288535",
+      "sha256": "67569961d068633c6ff3ac9dfde47a0c17f0da6d20432799dcc920cff92b5779"
+    },
+    {
+      "path": "research/query-thinned-controllers/verify.py",
+      "usage": "input",
+      "git_blob": "f1114036fff66f57014e5c1256141fb78ff4c4a9",
+      "sha256": "07dea601d6bbaa4d90e576f20c8607c37fb01e8778c798d919fa9df435049950"
+    }
+  ]
+}

research/bit-row-stock-atom-audit/TASK.json

@@ -0,0 +1,88 @@
+{
+  "schema_version": 1,
+  "task_id": "selected-stock-envelope",
+  "priority_revision": 7,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "original_card": {
+    "id": "selected-stock-envelope",
+    "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?",
+    "starting_points": [
+      "research/selected-bootstrap-stock-audit/README.md",
+      "research/bootstrap-cutoff-time-space-split/README.md",
+      "certificates/selected-result.json",
+      "docs/research/community-efficient1000-review.md",
+      "research/stock-margin-chain/README.md"
+    ],
+    "methods": [
+      "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.",
+      "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope."
+    ],
+    "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read #2972 stock-margin chain and the selected stock audit. The new source archive reports the remaining cutoff comparisons, but leaves every actual stock coefficient unresolved; it is not an independently validated reserve envelope.",
+      "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission."
+    },
+    "first_experiment": "Choose one actual selected producer/stage and derive its parent reserve and depth coefficient from source. Check whether newer handoffs already cover that exact obligation. Stop with the missing implementation lemma if it cannot be bounded; do not rerun #2972 cutoff/headroom arithmetic as a new contribution.",
+    "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.",
+    "allowed_variations": [
+      "One stage or one explicit reserve/depth implication.",
+      "An independently checked same-domain proof repair, retaining all remaining assumptions."
+    ],
+    "scope_change_triggers": [
+      "Importing the historical 57604 or 252 allowance without a selected-producer binding.",
+      "Calling a conditional fit lemma a full outer-proof adoption.",
+      "Replacing an actual selected stock coefficient with cutoff comparisons or a conditional fit inequality."
+    ],
+    "overlap_terms": [
+      "selected stock",
+      "stock envelope",
+      "bootstrap cutoff",
+      "1956",
+      "1965",
+      "1990",
+      "2972",
+      "stock-margin-chain",
+      "actual_stock_coefficient"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Retained stock audit identifies missing actual selected-stage coefficients; later cutoff-chain arithmetic does not supply them.",
+        "evidence": "docs/research/research-family-status.md#revision-6-handoffs-source-archives-awaiting-independent-validation",
+        "remaining": "Derive one actual reserve/depth coefficient from the selected producer.",
+        "status": "reviewed",
+        "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "The BIT row-stock formulas of the selected #4359 producer (DELAYED-COVER-BRIDGE sections 7-8, OUTER-TRANSFER-AUDIT section 5) and their reuse with atom 0.004 in the #4440/#4470 chain.",
+  "scope_change_reason": "The selected producer changed with #4359; its new BIT reserve and outer row stock had only a prose intake check, and #4470 changed the atom power without restating the reserve.",
+  "bottleneck_link": "Side result for the selected-result audit: confirms the stock layer of the conditional kappa line and corrects one display; it does not move the frontier.",
+  "budget_minutes": 120,
+  "stop_rule": "Stop after the stock, depth, borrowed-digit, outer-reserve and delayed-cover finite statements are checked; do not audit the outer analytic decomposition or materialize templates.",
+  "outcome": "completed",
+  "evidence": "README.md proofs; verify.py binds the source statements and checks them exactly or on stated grids; test_verify.py has seven rejecting controls.",
+  "author": "Mark (Matarener)",
+  "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.",
+  "open_questions": [
+    {
+      "question": "What is the actual constant C of the outer reserve for the #4470 template?",
+      "why_it_matters": "It fixes the eventual thresholds; the package uses log2 C ~ 2 log2 N + 64 only for illustration.",
+      "first_step": "Sum the BIT digit count D(N^2 w + log_q B + 1) with the complex ceil(log2 W) D and the router constants for the #4470 N, B, q.",
+      "blocked_by": "none"
+    },
+    {
+      "question": "Does the lockstep compiler give every simultaneously live child role a distinct physical array?",
+      "why_it_matters": "The row-digit reserve argument assumes it (DELAYED-COVER-BRIDGE open question 1).",
+      "first_step": "Replay the finite compiler's role assignment on the materialized rank-50 BIT example and check digit ownership along every root-leaf path.",
+      "blocked_by": "none"
+    }
+  ]
+}

research/bit-row-stock-atom-audit/VERIFY.json

@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "notes/three-stage-cover-bit.tex",
+    "research/capped-phase-fusion/SUPPLIER-SUPPORT-AUDIT.md",
+    "research/joint-helper-lattice/verify.py",
+    "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md",
+    "research/kappa-rebuild/bit/delayed_cover_bridge.py",
+    "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md",
+    "research/query-thinned-controllers/verify.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Bind source statements; exact ordinary BIT conversion and cover prime for #4359 and #4470; GL lift, reserve split and depth; borrowed-digit threshold; outer reserve width, stock, threshold and h/16; independent delayed-cover audit on GL_2(Z/9) and GL_3(Z/4); tautological gauge check."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/test_verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Rejecting controls: old atom at #4470, literal h^0.003 at atom .004, broken atom passing beta*(1-atom), missing high-matrix lift, max instead of product, omitted carry, widths below threshold."
+    }
+  ]
+}

research/bit-row-stock-atom-audit/test_verify.py

@@ -0,0 +1,62 @@
+#!/usr/bin/env python3
+"""Rejecting controls for verify.py."""
+import math
+import unittest
+from fractions import Fraction as Q
+
+import verify as v
+
+
+class Controls(unittest.TestCase):
+    def test_old_atom_fails_adapter_for_4470(self):
+        c = v.CASES["pr4470"]
+        a = v.ordinary_saving(c["C1"], Q(3, 1000))
+        self.assertLessEqual(Q(3, 1000), a)
+
+    def test_literal_h0003_bound_false_at_atom_0004(self):
+        # h^.004 L^2.008 <= C h^.003 L^3 fails once h^.001 > C L^.992
+        logC, L = 2 * v.CASES["pr4470"]["log2N"] + 64, 10.0 ** 18
+        logh = 0.99 * L
+        lhs = 0.004 * logh + 2.008 * math.log2(L)
+        rhs = logC + 0.003 * logh + 3 * math.log2(L)
+        self.assertGreater(lhs, rhs)
+
+    def test_beta_predicate_passes_broken_atom(self):
+        atom = Q(99999, 100000)
+        a = v.ordinary_saving(v.CASES["pr4470"]["C1"], atom)
+        self.assertGreater(v.CASES["pr4470"]["beta"] * (1 - atom), 0)
+        self.assertFalse(atom < 1 - a)
+
+    def test_omitting_high_matrix_lift_underreserves(self):
+        N, q, w, B, S, D = 2, 3, 2, 5, 7, 3
+        full = B * v.gl_order(N, q) * q ** (N * N * (w - 1))
+        wrong = B * v.gl_order(N, q)
+        R = wrong ** D * S
+        levels = 0
+        while R % full == 0 and R >= full:
+            R //= full
+            levels += 1
+        self.assertLess(levels, D)
+
+    def test_max_instead_of_product_underreserves(self):
+        bit, cx = 12 ** 3, 48 ** 2
+        self.assertLess(max(bit, cx), bit * cx)
+
+    def test_omitted_carry_breaks_high_row(self):
+        p, m = 3, 9
+        g, S = ((2, 7), (4, 5)), ((1, 1), (1, 0))
+        h = v.mat_mul(g, S, m)
+        g0 = [[x % p for x in r] for r in g]
+        G1 = [[(x - y) // p for x, y in zip(r, s)] for r, s in zip(g, g0)]
+        no_carry = tuple(tuple(sum(G1[i][k] * S[k][j] for k in range(2)) % p for j in range(2)) for i in range(2))
+        self.assertNotEqual(tuple(tuple(x // p for x in r) for r in h), no_carry)
+
+    def test_stock_threshold_fails_below(self):
+        c = v.CASES["pr4359"]
+        Le = 1.5 * c["log2N"]
+        k = v.log2_k(Le, float(c["delta"]), float(c["log2N"]))
+        self.assertTrue(k is None or k + 1 >= Le)
+
+
+if __name__ == "__main__":
+    unittest.main()