Rebuild #4416's p7 invoice from its literal controller word: exact Laurent replay gives T and P exactly (no new κ)

research/pr4416-invoice-rebuild/README.md

@@ -0,0 +1,95 @@
+# #4416's p7 invoice, rebuilt from its literal controller word
+
+**Claim type: an independent exact replay and assembly. No new κ.** It
+answers the open question of my
+[#4420](https://github.com/CrocSwap/integer-mult-bounds/pull/4420) for the
+part of #4416's invoice that is new.
+
+## Object
+
+#4420 certified #4416's strictification inequalities at κ = 0.00268647, but
+took its invoices from #4416's inventory. There `α` clears its requirement by
+only `5.6·10⁻⁹`, while one extra rank-one paid call would move `α` by about
+`7.6·10⁻⁶`. So the invoice itself is the weak link:
+
+```text
+T = {5:420, 6:270, 7:840, 8:1395, 9:3195, 25:448, 41:448, 57:448, 121:224},
+P = {1:37305, 2:10695, 3:3360, 4:1530, 5:300, 8:1464, 16:448, 32:448, 48:448}.
+```
+
+## Result
+
+**The invoice is rebuilt exactly** from `P7-FACTOR.json`'s literal word, the
+112 port recipes on main, and the supplier receipt.
+
+1. **Laurent identity.**
+   - **The replay.** All 70 physical events are replayed as an exact
+     Laurent matrix `M` over `Q, D0..D14`, under #4416's stated native
+     contract (`F_s = D_s S_y(Q⁻¹)`, `B_s = D_s S_x(−Q)`).
+   - **The scalar programs.** The left and right programs replay to the
+     stored matrices.
+   - **The identity.** `left · M · right` equals the stated diagonal of 14
+     monomials exactly, and every replayed coefficient matrix equals the
+     stored one.
+2. **Main targets.**
+   - Each role's rank is `1 + 8·(number of D exponents)`, over the 112 ports,
+     giving `{25:448, 41:448, 57:448, 121:224}`.
+   - The exponent alphabet is `Q^±1` with `D_s ∈ {0,1}`.
+3. **Paid idles.**
+   - The 12 retained windows are exactly the literal `IDLE` events, and the
+     keep mask 232127 selects exactly those windows.
+   - Each window pays rank `8·|stages|` on both roles of its pair at every
+     port, giving `{8:1344, 16:448, 32:448, 48:448}`.
+4. **Supplier.** Over the 15 native calls:
+   - the THREE-base helper widths `{5:28, 6:18, 7:56, 8:93, 9:213}` give the
+     helper targets;
+   - its unsplit paid profile `{1:2487, 2:713, 3:224, 4:102, 5:20, 8:8}`
+     (forward equal to backward) gives the rest of the paid calls.
+5. **Total.** `T` and `P` equal #4416's invoice. The rank-one masses are
+   131,723 and 131,115.
+
+**Control.** Flipping one reversed native call breaks the Laurent identity.
+
+## Method and independence
+
+- **No #4416 code.** Nothing is imported or run from #4416. The Laurent
+  polynomials, scalar programs and assembly are my own code. The native call
+  contract is #4416's stated input, replayed and not derived.
+- **Inputs.** `P7-FACTOR.json` and the supplier receipt are the files whose
+  SHA256 values #4416's own RESULT.json records. All three are vendored
+  byte-identically. The port recipes are `adaptive-kernel-demotion`'s
+  `DATA-PHASES.json` on main, with the same SHA256.
+
+## Not covered
+
+- **The supplier's numbers.** Its helper widths and paid profile are taken
+  from its receipt, part of #4359's lineage. Its native replay is not redone
+  here.
+- **The physical premises.** The native local contract itself, and the
+  121-axis physical admission of contacts, endpoints and phases.
+- **Downstream.** The tensor, completion and outer arguments.
+
+## Reproduce
+
+```sh
+python3.12 -B research/pr4416-invoice-rebuild/verify.py
+```
+
+It prints `PASS_PR4416_INVOICE_REBUILD` in under a second, using only the
+standard library.
+
+## Open next questions
+
+1. **Replay the THREE-base supplier's paid profile from its native
+   certificate.**
+   - *Why it matters:* it contributes `15 · 2487` rank-one calls, so a
+     difference of one call per invocation moves `α` well past its margin.
+   - *First step:* census
+     `THREE-base-FULL-IDENTITY-NATIVE.json.gz` with separate code.
+   - *Blocked by:* nothing.
+
+## Credit
+
+The controller, word and invoice are 1337isnot1337's (#4416, with OpenAI
+Codex assistance), building on zxv's #4359. Prepared by Ryanson Jonathan with
+substantial Claude Code (Claude Opus 5.5) assistance. Apache-2.0.

research/pr4416-invoice-rebuild/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/adaptive-kernel-demotion/inputs/DATA-PHASES.json",
+      "usage": "input",
+      "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70",
+      "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa"
+    }
+  ]
+}

research/pr4416-invoice-rebuild/TASK.json

@@ -0,0 +1,100 @@
+{
+  "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": "Rebuild #4416's target and paid invoice from its literal p7 controller word (exact Laurent replay, main targets, paid idles) plus its supplier receipt, answering the open question of #4420.",
+  "scope_change_reason": "#4420 certified #4416's inequalities on its recorded invoice; alpha's 5.6e-9 margin makes the invoice the weak link.",
+  "bottleneck_link": "#4416's kappa = 0.00268647 rests on this invoice; a one-call change would break alpha's margin.",
+  "budget_minutes": 40,
+  "stop_rule": "Stop once the invoice is rebuilt or a discrepancy is found.",
+  "outcome": "completed",
+  "evidence": "verify.py: exact Laurent replay of all 70 events gives left*M*right equal to the stated 14 diagonal monomials and the stored coefficient matrices; main targets {25:448,41:448,57:448,121:224} over 112 ports; 12 retained windows equal the literal IDLE events and give paid idles {8:1344,16:448,32:448,48:448}; THREE-base helper widths and paid profile over 15 calls; T and P equal #4416's invoice; a flipped local orientation fails.",
+  "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": [
+    {
+      "question": "Replay the THREE-base supplier's paid profile from its native certificate with separate code.",
+      "why_it_matters": "It contributes 15*2487 rank-one calls; one call per invocation moves alpha past its margin.",
+      "first_step": "Census THREE-base-FULL-IDENTITY-NATIVE.json.gz independently.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/pr4416-invoice-rebuild/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/adaptive-kernel-demotion/inputs/DATA-PHASES.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Vendored P7-FACTOR.json, RESULT.json and supplier receipt hashes (matching #4416's own records); port recipes on main; scalar programs; exact Laurent identity and stored coefficients; main-target, paid-idle and keep-mask derivation; supplier assembly over 15 calls; invoice equality; flipped-orientation control."
+    }
+  ]
+}

research/pr4416-invoice-rebuild/vendor/NOTICE.md

@@ -0,0 +1,14 @@
+# Vendored files
+
+Byte-identical copies from [PR #4416](https://github.com/CrocSwap/integer-mult-bounds/pull/4416)
+at head `e9058860b5c850760fdf970e796a96aefcdb1d98`, checked by SHA256 in `verify.py`. They are
+copied because that head is not reachable from canonical main.
+
+| Vendored file | Source path in #4416 | Git blob |
+| --- | --- | --- |
+| `P7-FACTOR.json` | `research/pr4359-p7-padding/P7-FACTOR.json` | `04c7ef620e760cc8f1764bbf0ccd7f32c6a5bd86` |
+| `RESULT.json` | `research/pr4359-p7-padding/RESULT.json` | `ebb30a9b3b94fb159a316350f7da57bde4a30c25` |
+| `SUPPLIER-RESULT.json` | `research/pr4359-p7-padding/source/research/kappa-rebuild/complex/full-identity-certificates/RESULT.json` | `c6edcbdc43bf36bb11201235027d0ec170d07fc8` |
+
+The controller and package are 1337isnot1337's (with OpenAI Codex assistance); the supplier
+receipt is from zxv's #4359 lineage. Apache-2.0, as those packages state.