Certify the exact grid of the complete #5413 caller: body ceil(9 lambda/2)+6, controller 74 bits (attained) (no new kappa)

research/selected-caller-exact-grid/README.md

@@ -0,0 +1,113 @@
+# Exact grid of the complete selected #5413 caller
+
+**Positive scoped result; no new κ.** One controller level of the selected caller needs **74 extra fractional
+bits** at every cut the verifier observes (listed below); 74 is attained, so it is also necessary. The body needs
+`ceil(9 lambda/2) + 6`, also attained. An earlier version of this package claimed exactly 73; the review of this
+PR found a Gaussian-climb cut it did not observe, which needs 74. This continues the merged
+[selected-word-exact-grid](../selected-word-exact-grid/README.md), which covers the eight-relation word alone, from
+the word to the complete caller of [PR #5413](https://github.com/CrocSwap/integer-mult-bounds/pull/5413). The
+caller's own precision record (`FRESH-PRECISION.json`) has only crude heights: about 19,452 bits per local body
+and 377,688 for the global word. This is target 7 of [PR #5428](https://github.com/CrocSwap/integer-mult-bounds/pull/5428).
+
+## Body
+
+Only backward bodies run: 18 calls, with no forward macro calls. [verify.py](verify.py) executes the literal
+`NEUTRAL-BACKWARD-v16c` body, with `PROVIDER_5402` expanded by its schedule:
+
+- wrappers;
+- mode scalars;
+- the 834-instruction input and output basis programs;
+- the 21,473-event provider word, with a cut after every scalar, warp and Gaussian climb (a climb changes the
+  row's chart, so its output is observed on its own);
+- cache SWAP and CLEAR. Each of the eight SWAPs moves its transformed 56-term cache row to the mode owner; the
+  verifier checks that the cache slot ends zero and the owner nonzero.
+
+Monomials, Gaussians and warps stay symbols, so terms through different operator paths never merge; adjacent
+inverse warps cancel. The 240-map monomial block consists of maps, ADDs and the exact inverse maps. Each y-field
+pair therefore composes to the identity and is omitted. The verifier checks this directly.
+
+| Check | Result |
+|---|---|
+| Odd denominators | none, including the `ZW = 14 I` provider |
+| Owned fields at exit | all 17 zero |
+| Maximum `v2` | 6, attained by a single-occurrence rank-9 helper term (coefficient `-1/64`) |
+| Main-data / helper maxima | `v2 <= 4` / `v2 <= 6` with local rank `<= 9` |
+| Final X rows | `x_p - y_p` on all 112 ports |
+
+## Controller
+
+For each port, `A_x` is the `backward_input_X` wrapper followed by `Delta_{I_x}^-1`; `A_y` is defined likewise.
+Let `Q_p = A_y` followed by `A_x^-1`. On every port `Q_p` has Fourier rank 1 and `Q_p^2` rank 0. Since the final
+rows are `x_p - y_p`, the body computes `X = Phi (x - Q_p y)`, so `Q_p` is the controller's Q.
+
+The verifier replays the controller in the exact Laurent ring of `check_wholecaller_v1`. It has 32 banks with
+integer coefficients and reproduces the diagonal endpoint. The global data live on 145 axes: the central axis plus
+eight private axes per stage. A component `Q^q prod_{t in T} D_t` therefore carries private Fourier rank `8|T|`.
+
+| Region | Exact maximum |
+|---|---|
+| Calls before the last (`|T| <= 16`) | `4 + ceil((128+9)/2) = 73`; helpers `<= 11` |
+| Last call, in-word cuts (after every scalar, warp and climb) | **74** |
+| Last call, t-field after the paid C8 job | 73 |
+| Last call, cache cuts | 73 |
+| 224 rank-145 targets | 73 (necessary) |
+
+In the last call (stage 32, pair 15), original bank 31 enters x as `Q^2 D_T` and y as `Q D_T`, with `|T| = 17`.
+Where both paths reach a cut, they meet on `Phi_x Q^2` with coefficient `c_x + c_y`. Each such term is evaluated
+with exact nine-plane ranks, with warps taken from the native table and admitted as in kappa-round3-warp-20261022.
+
+Not every cut has both paths. The climb of provider event 11204 (zero based: `climb warp_retimed`, row 63, new
+frame 254) leaves row 63 holding input `y70` once, with coefficient `1/4`, no warp word and no `x70` term to merge
+with. Bank 31 reaches it as `Q D_T` with 17 private stages; the nine-plane operator has rank 7 (exact zero-column
+entry `(-1+i)/16`). With the 136 private Fourier axes, a basis input on bank 31, port 70 gives `(-1+i)/2^74` at
+this cut: `2 + ceil((136+7)/2) = 74` bits are necessary. No other observed cut needs more. **The guard of one
+controller level over the observed cuts is therefore 74.** The body's `2^-6` adds nothing on top of it.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/selected-caller-exact-grid
+python3.12 -I -B research/selected-caller-exact-grid/verify.py
+python3.12 -I -B research/selected-caller-exact-grid/test_verify.py
+```
+
+The verifier uses the standard library and the pinned repository Clifford compiler. It takes under a minute and
+prints `PASS_SELECTED_CALLER_BODY_6_CONTROLLER_74`. The controls reject eight mutations:
+
+- a drifted input;
+- an odd division;
+- a block map that is not inverted;
+- a missing controller `Q_POWER`;
+- a missing owned CLEAR;
+- a cache SWAP that drops the cache row instead of moving it (the earlier version's error);
+- climbs that change the chart without entering the census (the earlier version's error; the result falls to 73);
+- a tampered RESULT.json.
+
+## Scope
+
+Several premises are inherited and not re-proved here:
+
+- native operator correctness;
+- the canonical-chart, wrapper and warp conventions;
+- the identification of the controller's Q with the body's Q through `X = Phi (x - Q y)`.
+
+The last of these is the body's specified endpoint and is checked through its final rows. The observed cuts are
+the in-word cuts of the provider word, the t-field cut after the paid C8 job, the cache cuts, the calls before the
+last and the final targets; body operations outside the provider word are not separately cut, so 74 is proved
+necessary and shown sufficient only at these cuts. The symbolic replay keeps the moved cache rows but does not
+prove their algebraic endpoint (the mode outputs `C8 z` of the neutral completion); that is a separate obligation,
+raised in the review of #5442. The result is an
+exact-grid statement, not a rounded execution, a recursive price or a supplier admission. The selected record is
+unchanged.
+
+## Open next questions
+
+- What does the attained 74-bit controller guard cost in the recursive invoice? First compare it with the retained
+  precision_tape packing. #5419 shows that a uniform paid-precision factor above about 1.0046 removes the 0.0033 margin.
+
+## Credit
+
+Clear1nsight (#5413), dillona (#5402), Ali Romman (#5383, #5398) and Cao Yifan (#4610) supplied the caller, provider
+and word. Ross Richardson supplied the Clifford denominator lemma. The coded-native-caller normalizers and the
+kappa-round3-warp native table supplied the wrappers and warps. Prepared by Mark (Matarener) with substantial
+Claude Code assistance. New work is Apache-2.0.

research/selected-caller-exact-grid/RESULT.json

@@ -0,0 +1,60 @@
+{
+ "body": {
+  "class_max_v2": {
+   "helper": 6,
+   "main": 4
+  },
+  "final_X_rows": "x_p - y_p on all 112 ports",
+  "guard": "ceil(9 lambda/2) + 6 (attained)",
+  "helper_witness": [
+   "('word', 19465)",
+   532,
+   470,
+   "-1/64"
+  ],
+  "identity_monomial_pairs": 224,
+  "max_v2": 6,
+  "mode_owner_terms": [
+   56,
+   56,
+   56,
+   56,
+   56,
+   56,
+   56,
+   56
+  ],
+  "odd_denominators": 0
+ },
+ "controller": {
+  "early_calls_bound": 73,
+  "guard": 74,
+  "last_call": {
+   "bank31": {
+    "x": [
+     2,
+     17
+    ],
+    "y": [
+     1,
+     17
+    ]
+   },
+   "cache_cut_max": 73,
+   "in_word_max": 74,
+   "in_word_witness": [
+    "1/4",
+    143,
+    31,
+    70,
+    254,
+    []
+   ],
+   "pair": 15,
+   "stage": 32,
+   "t_cut_max": 73
+  },
+  "rank145_targets": 224,
+  "target_requirement": 73
+ }
+}

research/selected-caller-exact-grid/SOURCES.json

@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-BACKWARD-v16c.json",
+      "usage": "input",
+      "git_blob": "04c6c7f36cb1b9fcf0b464bad3d3d83aaae7c864",
+      "sha256": "cc297ee54c2743615dfe857838d5f40424ccd33fdb08ecfafbc41b1710416d91"
+    },
+    {
+      "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-CALLER-v16c.json",
+      "usage": "input",
+      "git_blob": "975714d0c15714070b2303ca48d31871f2095210",
+      "sha256": "1f17fda221bc781ca0b2a120916ed500ba84c305a916a65436a5d6c72d116bcf"
+    },
+    {
+      "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/agents/budget/inputs/NORMALIZERS.json",
+      "usage": "input",
+      "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f",
+      "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da"
+    },
+    {
+      "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/PROVIDER.json",
+      "usage": "input",
+      "git_blob": "0afd30ed01202eb6ce62462dcf8bc9164f3b0455",
+      "sha256": "676de7551d3364598f4a7e29ae97cae0e4364348786bbe70435b84294ba7dd65"
+    },
+    {
+      "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "f3111b47e89496da8ca0ee45b2e4b258c0634d8e",
+      "sha256": "7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc"
+    },
+    {
+      "path": "research/eight-owned-relations/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "c62fcb59643f87919208100517a2fbc4b57cb7d7",
+      "sha256": "6412632c28e265597fb088087048091d81c19500fb28a0c9c9d2a48f61b8665b"
+    },
+    {
+      "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py",
+      "usage": "input",
+      "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2",
+      "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962"
+    }
+  ]
+}

research/selected-caller-exact-grid/TASK.json

@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "What exact uniform grid does the complete selected #5413 caller need: the runtime backward body with the #5402 provider expanded, and one 145-axis controller level with its 18 body calls?",
+  "scope_change_reason": "research/selected-word-exact-grid (merged) certifies the eight-relation body word only. The selected result runs that word inside the #5413 body and controller, whose own precision record (FRESH-PRECISION.json) has only crude heights. This package supplies the exact statement for the complete caller, continuing target 7 of PR #5428.",
+  "bottleneck_link": "Side result; no new kappa. It replaces the crude precision heights of the selected caller by an exact, attained grid, a precondition for any precision-weighted invoice of the selected construction.",
+  "budget_minutes": 300,
+  "stop_rule": "Stop at the exact attained guard of one controller level; the recursive price of the guard is a separate question.",
+  "outcome": "completed",
+  "evidence": "verify.py expands the #5402 provider inside the #5413 backward body (no odd division, owned fields zero, max v2 = 6 attained: body guard ceil(9 lambda/2)+6), derives the per-port Q from the port wrappers (rank 1, square rank 0, final rows x_p - y_p), replays the controller in its exact Laurent ring and evaluates the cuts of the last call (after every scalar, warp and climb of the provider word, the t-field cut after the paid C8 job and the cache cuts) with exact nine-plane ranks: the maximum is 74, attained by a Gaussian-climb cut where bank 31 reaches y70 alone (review of #5438), one bit above the 73 of the 224 rank-145 targets, so one controller level needs 74 extra bits at these cuts. test_verify.py rejects eight mutations.",
+  "author": "Mark (Matarener)",
+  "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.",
+  "open_questions": [
+    {
+      "question": "What does the attained 74-bit controller guard cost in the recursive invoice?",
+      "why_it_matters": "PR #5419 shows that a uniform paid-precision factor above about 1.0046 removes the 0.0033 margin; the guard is now exact, so its price can be computed.",
+      "first_step": "Express 74 bits per controller level as storage per packed word at the recursion's word width and compare with the retained precision_tape prescription.",
+      "blocked_by": "The retained packing and tape prescription have to be read from the compiler sources."
+    }
+  ]
+}

research/selected-caller-exact-grid/VERIFY.json

@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-BACKWARD-v16c.json",
+    "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-CALLER-v16c.json",
+    "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/agents/budget/inputs/NORMALIZERS.json",
+    "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/PROVIDER.json",
+    "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/WORD.json.gz",
+    "research/eight-owned-relations/WORD.json.gz",
+    "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Pinned inputs; controller binds the body; Q_p rank 1 / Q_p^2 rank 0 on all ports; the 240-map block is maps, ADDs, inverse maps; body with the #5402 provider expanded: no odd denominator, owned fields zero, each cache SWAP moves the 56-term cache row to its owner, max v2 = 6 with a rank-9 helper witness, main v2 <= 4, final X rows x_p - y_p; Laurent replay reproduces the diagonal; calls before the last need <= 73; last call (bank 31 as Q^2 / Q, 17 stages): in-word cuts including every warp and climb need <= 74, attained by the climb cut of event 11204 (bank 31, port 70, frame 254), t-field and cache cuts <= 73; 224 rank-145 targets need 73; guard 74 over the observed cuts; stored RESULT.json equals the rebuild."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/test_verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Rejecting controls: drifted input hash, an odd division in a body ADD, a block map that is not inverted, a missing controller Q_POWER, a missing owned CLEAR, a cache SWAP that drops the cache row, an unobserved climb cut, tampered RESULT.json."
+    }
+  ]
+}