Independently check #4338's ordinary B2 bootstrap arithmetic: every link holds; 1-mu_(576/577) = 1.06e-6 against the 1e-6 the 10^6 coefficient needs (no new κ)

research/pr4338-b2-chain-check/README.md

@@ -0,0 +1,86 @@
+# Independent check of #4338's ordinary B2 bootstrap arithmetic
+
+**Claim type: an independent exact check of a written arithmetic chain,
+including a certified moment enclosure. No new κ.** This does not accept
+#4338, and it checks none of its source-relative physical contracts.
+
+## Object
+
+[PR #4338](https://github.com/CrocSwap/integer-mult-bounds/pull/4338) (Ross
+Richardson, head `0ac8192b…`) splits the optional ordinary B2 stage out of
+#4270. With BIT coupling `c = 1/577`, it claims:
+
+- the ordinary saving `a2 = 57697923247/33292900000000 ≈ 0.00173304`;
+- the bound `T_B2 ≤ 4283584·A·V·e^(1−a2)`;
+- that `a2` exceeds the pooled complex endpoint `C`.
+
+Its own checker runs a frozen interval engine and an integer-power bisection.
+No outside check existed.
+
+## Results
+
+Every link of PROOF.md §1, §3 and §4 holds, recomputed with exact rationals.
+The inputs are read from main: `H` is the selected BIT supplier's
+`nine.profile`, `a1` is PR2899's `ordinary_saving`, and `C` is
+`staged-fourth-mixture-ceiling`'s root.
+
+| Link | Result |
+| --- | --- |
+| `a2 = c(1−c) + c·a1` | exactly the stated rational; `a2 − C` is exactly the stated `2.06·10⁻⁶` |
+| §1: bootstrap at the complex rate | `a_next` and the outer-loss value match to 28 digits. The shortfall below `0.001727989140903569` is `5.84263·10⁻⁸` |
+| `F = 32·64²·ΣH` | `118606528512` |
+| `μ_1` | exactly `2874298095721977/2890625000000000 < 199/200` |
+| `μ_(576/577)` | enclosure width `< 10⁻³³`, inside the stated `10⁻³⁰` interval. `1 − μ = 1.0614·10⁻⁶`, so the `10⁶` coefficient holds, and the old `9999/10000` cap is false |
+| Fit comparisons | `17^128 > 32·16^128`; `32780·(17/16)·20 = 696575 < 2^20`; `2^(20/577) < 17/16` |
+| Exponent algebra | `(1−c) + c(c−a1) = 1 − a2`; `2^(c−a1) < 17/16`; `a2 < c`; `1 − a2 − c > 1/2` |
+| Coefficient | `801 + 4000000·17/16 + 32780 + 3 = 4283584` |
+| Gap table | all four exact. `1 − a2 − c(1−a1) = (1−c)²`, and the minimum gap is `c − a2 = 6.24·10⁻⁸` |
+
+**Control.** Dropping the fallback weight `εF` moves `μ_(576/577)` below the
+stated interval. The interval does include the fallback, as #4338 says.
+
+**Two tight spots.**
+
+- `1 − μ_(576/577)` exceeds the `10⁻⁶` that the `10⁶` coefficient needs by
+  only 6%.
+- The minimum gap `c − a2` is `6.2·10⁻⁸`.
+
+**Orientation.** `a2` lies below the selected BIT saving
+`0.0017334270…` by `3.9·10⁻⁷`. That is expected, since `a2 < c = 1/577` and the
+BIT constructor needs `c` below its moment root. #4338 does not compare them.
+
+## Not covered
+
+- The source-relative contracts:
+  - the B1/C1/B2 factory composition and restoration;
+  - the 1,123-chart registry;
+  - the retained stock-depth bound (coupling-independent; see below);
+  - the fit predicates beyond the stated comparisons.
+- The production B2 factory and any complex caller.
+- The legacy target `0.001727989140903569`. It is quoted from #4338; its
+  source is not on main.
+
+## Reproduce
+
+```sh
+python3.12 -B research/pr4338-b2-chain-check/verify.py
+```
+
+It prints `PASS_PR4338_B2_CHAIN_CHECK` in under a second, using only the
+standard library. `vendor/B2-PROOF.md` is #4338's PROOF.md, byte-identical and
+SHA256-checked, with 28 phrase checks.
+
+## Open next questions
+
+None from this check. The stock bound `k ≤ 16390 e^c log2 e` does not depend
+on the coupling: `retuned-ordinary-coupling` derives it from `D(e) ≤ 2 log2 e`,
+`|GL64(F_q)| < q^4096` and `w ≤ 2e^c`, all of which hold at `c = 1/577`. The
+remaining obligations are #4338's own physical premises.
+
+## Credit
+
+The B2 construction and its arithmetic are #4338's (Ross Richardson with
+OpenAI Codex assistance), composing Jose Manuel's ordinary and fast-primitive
+sources, Rohan Arun's PR185/387 argument and the PR589 BIT profile. Prepared
+by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5)
+assistance. Apache-2.0.

research/pr4338-b2-chain-check/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "input",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json",
+      "usage": "input",
+      "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13",
+      "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4"
+    },
+    {
+      "path": "research/selected-bit-recursive-closure/RESULT.json",
+      "usage": "input",
+      "git_blob": "e7f281a85797dc91ad24e5e5ee6500966e9905b9",
+      "sha256": "85cdaa514113b9e49a578c6856057d2503307e6ba02510ef800d3ace67713e74"
+    },
+    {
+      "path": "research/staged-fourth-mixture-ceiling/RESULT.json",
+      "usage": "input",
+      "git_blob": "2803d5c42b5d49ea72bd9bb006ffb4a9eec6a316",
+      "sha256": "53849028b12f7d9b726ac7576eeb64dc9a1a51bb2890edbb15aa83d1e39fae5f"
+    }
+  ]
+}

research/pr4338-b2-chain-check/TASK.json

@@ -0,0 +1,94 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/staged544-mixed-fourth-entry/README.md",
+      "research/staged-fourth-mixture-ceiling/README.md",
+      "research/r437-two-window-carrier/README.md"
+    ],
+    "methods": [
+      "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+      "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+    ],
+    "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+    "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
+    "allowed_variations": [
+      "Reconstruct either a source ledger or a numeric enclosure with a different method."
+    ],
+    "scope_change_triggers": [
+      "Importing the primary function and calling its output independent verification.",
+      "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering",
+      "4088",
+      "4091",
+      "4067",
+      "staged544-mixed-fourth-entry",
+      "staged-fourth-mixture-ceiling",
+      "r437-two-window-carrier"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Independently recompute #4338's B2 arithmetic chain: a2, the section 1 shortfall, mu_1 and the certified mu_(576/577) enclosure, the fit comparisons, the 4283584 coefficient and the gap table, with H, a1 and C bound to main.",
+  "scope_change_reason": "The card asks for independent coverage of a new paid-profile or moment claim; #4338 is new and had no outside check.",
+  "bottleneck_link": "#4338 removes an ordinary-rate obstruction for the pooled complex route; its arithmetic must hold before its physical contracts are worth review.",
+  "budget_minutes": 25,
+  "stop_rule": "Stop once every stated arithmetic link is certified or fails.",
+  "outcome": "completed",
+  "evidence": "verify.py: a2 and a2-C exact; section 1 digits and 5.84263e-8 shortfall; F = 118606528512; mu_1 exact < 199/200; mu_(576/577) inside the stated 1e-30 interval with width < 1e-33, 1-mu = 1.0614e-6; fit comparisons; coefficient 4283584; gap table exact, minimum c-a2 = 6.24e-8; dropping the fallback leaves the interval.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance in reading, verifier implementation and writing; no independent human or proof-kernel review.",
+  "open_questions": [],
+  "no_open_questions_reason": "Every arithmetic link holds; the stock-depth bound is coupling-independent, and the remaining obligations are #4338's physical premises."
+}

research/pr4338-b2-chain-check/VERIFY.json

@@ -0,0 +1,23 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "research/e8-bit-p111-tuned/tune/EXPECTED.json",
+    "research/selected-bit-recursive-closure/RESULT.json",
+    "research/staged-fourth-mixture-ceiling/RESULT.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Vendored PROOF.md hash and 28 phrases; H, a1, C bound to pinned main files; a2 and a2-C; section 1 outer-loss shortfall; F and mu_1 exact; certified mu_(576/577) enclosure in the stated interval; induction coefficients; fit comparisons; exponent algebra; 4283584 coefficient; gap table; fallback-omission control."
+    }
+  ]
+}