Certify the exact grid of the selected complex word (ceil(9 lambda/2)+6, attained) and bracket the #5413 controller at 73..77 bits (no new kappa)

docs/ci-verification.md

@@ -1,8 +1,40 @@
 # CI verification
 
-## Current selected-family replay: #4610 with #5241
+## Current selected-family replay: #5413 with #5407 and #5414
 
 The [selected record](../certificates/selected-result.json) binds conditional
+κ = 0.003027288235, the [promotion and scope](research/pr-intake-evidence/pr5413-promotion/PROMOTION.md),
+[explicit source closure](../certificates/frontier5413-source.json),
+[review validation](research/pr-intake-evidence/pr5413-promotion/VALIDATION.json), and
+[integration receipt](research/pr-intake-evidence/pr5413-promotion/INTEGRATION.json).
+
+`make frontier5413-verify` authenticates the selected source manifest, derives
+the certificate from frozen numerical evidence, and exports the complete
+three-package execution closure. It replays #5407's five-stage provider audit,
+#5413's eight-stage admission, and #5414's independent companion screen serially.
+The exported inputs are checked again afterward. Source-bound #4610/#5241 and
+earlier BIT/native/compiler/tape/analytic foundation coverage is explicitly
+reused; its historical suites are not rerun.
+
+Each package runs under an external sampled 1 GiB aggregate descendant-memory
+guard, with timeouts of 660 seconds for the provider and primary packages and
+120 seconds for the companion. On macOS the replay uses the reviewed RLIMIT_AS
+adapter; on Linux it invokes the unmodified package wrappers. The recorded
+successful local macOS replay does not establish a hosted Linux pass.
+
+The [frontier5413 workflow](../.github/workflows/frontier5413.yml) is manual-only,
+uses Python 3.12 on Ubuntu, materializes the declared source closure, and uploads
+receipts and logs. Its status is separate from local validation and recorded in
+the integration receipt. Routine donor PRs do not launch this selected replay.
+
+`make selected-record-check` verifies metadata and source/proof hashes. It does
+not execute the operators or prove the five inherited framework assumptions.
+The finite checks do not establish the full integer multiplication theorem,
+and the uniform word remains unmaterialized.
+
+## Historical selected-family replay: #4610 with #5241
+
+The historical [selected record](../certificates/checkpoints/frontier4610.json) binds conditional
 κ = 0.0030217758, the [review](research/pr-intake-evidence/pr4610/PROOF-REVIEW.md),
 [explicit source closure](../certificates/frontier4610-source.json),
 [review validation](research/pr-intake-evidence/pr4610/VALIDATION.json), and

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

@@ -0,0 +1,84 @@
+# Exact internal grid of the selected complex word
+
+**Positive scoped result; no new κ.** The selected chain runs the eight-relation body of
+[PR #5383](https://github.com/CrocSwap/integer-mult-bounds/pull/5383) (Ali Romman), on Cao Yifan's #4610 word,
+through #5392, #5398 and #5413. Public physical inputs, including dirty helpers and owned entries, are arbitrary
+arrays on `2^-f Z[i]`. At payload tensor depth `lambda`, every atomic cut of this body is exact with
+
+```text
+backward program: ceil(9 lambda / 2) + 6 extra fractional bits      (11, 15, 20, 24 at lambda = 1..4)
+forward program:  ceil(9 lambda / 2) + 5 extra fractional bits
+stored component magnitude < H * 457 * 2^(9 lambda / 2)
+```
+
+Both guards are **attained**, so they are the exact minimum for one uniform grid. The #4610 source word gives the
+same numbers. Until now the repository checked only that formal prefix norms and denominators of this word stay
+below `2^192` ([eight-owned-relations/native.py](../eight-owned-relations/native.py)). For comparison, the P104
+words have the sharp guard `ceil(9 lambda/2) + 2` ([p104-retimed-internal-grid](../p104-retimed-internal-grid/README.md)).
+This is step 1 of target 7 in [PR #5428](https://github.com/CrocSwap/integer-mult-bounds/pull/5428).
+
+## Model and proof
+
+The model is the one of PR2772, PR2813 and [p104-joint-prefix-grid](../p104-joint-prefix-grid/README.md).
+At an atomic cut a field standing in frame `F` holds
+
+```text
+sum_s c_s U_s^(tensor lambda) V_s(0),
+```
+
+with exact rational coefficients `c_s`, one per input `s` and native warp word. For a term without a warp word,
+`U_s = Delta_F Delta_{I_s}^-1`. All charts and native maps are exact dyadic Gaussian Cliffords on nine binary
+coordinates. This is inherited from the exact Clifford admission in
+[kappa-round3-warp-20261022](../kappa-round3-warp-20261022/README.md). A Clifford column of Fourier rank `r` has
+`2^r` nonzero entries, each a Gaussian unit times `2^(-r/2)`, so its reduced denominator is exactly
+`2^ceil(r/2)` (Ross Richardson's lemma, as retained in p104-retimed-internal-grid). Under the payload lift the
+rank becomes `r lambda`.
+
+[verify.py](verify.py) replays both programs exactly over Q and records three things:
+
+- **Dyadic coefficients.** Every scalar coefficient is dyadic; there is no odd division anywhere.
+- **Fourier ranks.** For each term it computes the rank of `Delta_F Delta_{I_s}^-1` with the repository's
+  Clifford compiler. As a check, that rank equals the paid rank on every one of the 3,282 to 3,290 climbs per
+  program. Warp-word and owned-entry terms get the universal rank 9.
+- **Pareto front.** The front of `(v2(den c_s), r)` over all terms of all cuts is `{(6, 9)}` backward and
+  `{(5, 9)}` forward, so the guard is the maximum of `v2 + ceil(r lambda/2)`.
+
+**Attainment.** Backward event 19537 adds `L321/4` into `L532`. Input `L470` occurs exactly once in the resulting
+row, with coefficient `-1/64` and rank 9. Inputs are independent, so no other term cancels it: for `lambda = 1` an
+input basis vector produces a component with denominator exactly `2^(6+5)`. The forward witness is event 19466,
+with coefficient `-1/32` and rank 9. The largest coefficient sum `sum_s |c_s|` is 457. Since each row of a
+`2^(9 lambda)`-dimensional unitary has l1 norm at most `2^(9 lambda/2)`, this gives the magnitude bound.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/selected-word-exact-grid
+python3.12 -I -B research/selected-word-exact-grid/verify.py
+python3.12 -I -B research/selected-word-exact-grid/test_verify.py
+```
+
+The verifier uses only the standard library and the pinned repository Clifford compiler. It takes about a minute
+and prints `PASS_SELECTED_WORD_EXACT_GRID_CEIL_9L_2_PLUS_6`. The controls reject a drifted input, an odd division,
+a corrupted climb rank, a smaller guard claim and a tampered RESULT.json.
+
+## Scope
+
+This covers the eight-relation body and its #4610 source, in both programs. It does not cover the #5413 caller
+packet (normalizers, the #5402 coupled provider with `ZW = 14 I`, owned fields). Native operator correctness, the
+canonical-chart convention and the tensor-lift convention stay inherited premises. It is an exact-grid statement,
+not a rounded execution, a paid recursive implementation or a supplier admission. The selected record is unchanged.
+
+## Open next questions
+
+- **Caller packet.** What exact grid does the complete #5413 caller packet need? First replay its literal packets
+  with the same census. An odd division there would rule out a fixed dyadic grid for the selected result.
+- **Recursive price.** What does the attained guard cost in the recursive invoice? #5419 shows that a uniform
+  paid-precision factor above about 1.0046 removes the 0.0033 margin. First compare the guard with the retained
+  precision_tape packing.
+
+## Credit
+
+Cao Yifan (#4610) supplied the word. Ali Romman (#5377, #5383) and the eight-owned-relations package supplied the
+relation body. Ross Richardson supplied the Clifford denominator lemma. The P104 grid packages (PR2674, PR2772,
+PR2813) supplied the model. zxv's #5428 named precision composition as a target. Prepared by Mark (Matarener)
+with substantial Claude Code assistance. New work is Apache-2.0.

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

@@ -0,0 +1,126 @@
+{
+ "eight_relation_body/backward": {
+  "climbs_checked": 3282,
+  "front": [
+   [
+    6,
+    9
+   ]
+  ],
+  "guard": {
+   "1": 11,
+   "2": 15,
+   "3": 20,
+   "4": 24
+  },
+  "guard_formula": "ceil(9 lambda/2) + 6",
+  "max_l1": "163",
+  "witness": {
+   "[6, 9]": [
+    19537,
+    [
+     "L",
+     532
+    ],
+    [
+     "L",
+     470
+    ],
+    "-1/64"
+   ]
+  }
+ },
+ "eight_relation_body/forward": {
+  "climbs_checked": 3290,
+  "front": [
+   [
+    5,
+    9
+   ]
+  ],
+  "guard": {
+   "1": 10,
+   "2": 14,
+   "3": 19,
+   "4": 23
+  },
+  "guard_formula": "ceil(9 lambda/2) + 5",
+  "max_l1": "457",
+  "witness": {
+   "[5, 9]": [
+    19466,
+    [
+     "L",
+     324
+    ],
+    [
+     "L",
+     359
+    ],
+    "-1/32"
+   ]
+  }
+ },
+ "source_4610/backward": {
+  "climbs_checked": 3290,
+  "front": [
+   [
+    6,
+    9
+   ]
+  ],
+  "guard": {
+   "1": 11,
+   "2": 15,
+   "3": 20,
+   "4": 24
+  },
+  "guard_formula": "ceil(9 lambda/2) + 6",
+  "max_l1": "169",
+  "witness": {
+   "[6, 9]": [
+    19441,
+    [
+     "L",
+     532
+    ],
+    [
+     "L",
+     470
+    ],
+    "-1/64"
+   ]
+  }
+ },
+ "source_4610/forward": {
+  "climbs_checked": 3290,
+  "front": [
+   [
+    5,
+    9
+   ]
+  ],
+  "guard": {
+   "1": 10,
+   "2": 14,
+   "3": 19,
+   "4": 23
+  },
+  "guard_formula": "ceil(9 lambda/2) + 5",
+  "max_l1": "457",
+  "witness": {
+   "[5, 9]": [
+    19466,
+    [
+     "L",
+     324
+    ],
+    [
+     "L",
+     359
+    ],
+    "-1/32"
+   ]
+  }
+ }
+}

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

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "1a3ced60b2f7a46bc70280a04f2eeb8ca027c700",
+  "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/eight-owned-relations/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "c62fcb59643f87919208100517a2fbc4b57cb7d7",
+      "sha256": "6412632c28e265597fb088087048091d81c19500fb28a0c9c9d2a48f61b8665b"
+    },
+    {
+      "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz",
+      "usage": "input",
+      "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e",
+      "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05"
+    },
+    {
+      "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py",
+      "usage": "input",
+      "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2",
+      "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962"
+    }
+  ]
+}

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

@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "1a3ced60b2f7a46bc70280a04f2eeb8ca027c700",
+  "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": "For the selected complex body (the #5383 eight-relation word used by #5392/#5398/#5413) and its #4610 source, what is the exact number of extra fractional bits that makes every atomic cut exact on a fixed dyadic Gaussian grid, at every payload tensor depth lambda, and is it attained?",
+  "scope_change_reason": "The selected record keeps precision_tape as a retained premise; for this word the repository only checks formal prefix l1 and denominators below a 2^192 envelope (eight-owned-relations/native.py). The P104 words have sharp exact-grid results (PR2772, PR2813, p104-joint-prefix-grid); this package supplies the corresponding sharp statement for the selected word instead of formalizing a new lemma. It is step 1 of target 7 in PR #5428.",
+  "bottleneck_link": "Side result; no new kappa. It replaces an envelope check by an exact, attained grid for the selected local word, a precondition for any precision-weighted invoice or approximate-supplier analysis.",
+  "budget_minutes": 180,
+  "stop_rule": "Stop at the exact attained guard for the two programs of the two pinned words; the #5413 caller packet and the recursive price of the guard are separate steps.",
+  "outcome": "completed",
+  "evidence": "verify.py replays both programs of the eight-relation body and the #4610 source exactly over Q: all coefficients are dyadic; per-term Fourier ranks from the repository Clifford compiler (checked equal to the paid rank on every climb) give the Pareto front {(6,9)} backward and {(5,9)} forward, so the guard is ceil(9 lambda/2)+6 (backward) and +5 (forward); a witness term (coefficient -1/64, rank 9, its input occurring once) shows attainment; max coefficient l1 457. test_verify.py rejects five mutations.",
+  "author": "Mark (Matarener)",
+  "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.",
+  "open_questions": [
+    {
+      "question": "What exact grid does the complete #5413 caller packet need (normalizers, coupled provider with ZW = 14 I, owned fields)?",
+      "why_it_matters": "The selected result runs the body through that caller; any odd division there would rule out a fixed dyadic grid.",
+      "first_step": "Replay the literal NEUTRAL-CALLER and WHOLECALLER-PLAN packets with the same coefficient and Fourier-rank census.",
+      "blocked_by": "A different packet format and the coupled provider's own native maps."
+    },
+    {
+      "question": "What does the attained 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.",
+      "first_step": "Express the guard as storage per packed word at depth lambda and compare with the retained precision_tape prescription.",
+      "blocked_by": "The retained packing and tape prescription have to be read from the compiler sources."
+    }
+  ]
+}