From ab2435cf5ba7a1f4650cb1d43bd31b09271043a3 Mon Sep 17 00:00:00 2001
From: zxv <zxv@zxv>
Date: Wed, 28 Oct 2026 00:05:53 -0400
Subject: [PATCH 1/2] Show current p19 address protocol fails the
 complete-controller identity

---
 .../p19-current-head-binding-audit/README.md  |  121 ++
 .../RESULT.json                               | 1100 +++++++++++++++++
 .../SOURCES.json                              |   54 +
 .../SOURCE_EXPORTS.json                       |   77 ++
 .../p19-current-head-binding-audit/TASK.json  |   97 ++
 .../VALIDATION.json                           |  136 ++
 .../VERIFY.json                               |   37 +
 .../source/pr5270/P19_BANK.json               |   20 +
 .../source/pr5270/P19_CLAIM.json              |  175 +++
 .../source/pr5270/P19_LIFT.json               |   16 +
 .../source/pr5270/P19_PLAIN.json              |  182 +++
 .../source/pr5270/README.md                   |  152 +++
 .../source/pr5270/VERIFY.json                 |   49 +
 .../source/pr5270/p19_bank.py                 |  143 +++
 .../source/pr5270/p19_claim.py                |  388 ++++++
 .../source/pr5270/p19_lift.py                 |  145 +++
 .../source/pr5270/p19_plain.py                |  158 +++
 .../p19-current-head-binding-audit/verify.py  |  333 +++++
 18 files changed, 3383 insertions(+)
 create mode 100644 research/p19-current-head-binding-audit/README.md
 create mode 100644 research/p19-current-head-binding-audit/RESULT.json
 create mode 100644 research/p19-current-head-binding-audit/SOURCES.json
 create mode 100644 research/p19-current-head-binding-audit/SOURCE_EXPORTS.json
 create mode 100644 research/p19-current-head-binding-audit/TASK.json
 create mode 100644 research/p19-current-head-binding-audit/VALIDATION.json
 create mode 100644 research/p19-current-head-binding-audit/VERIFY.json
 create mode 100644 research/p19-current-head-binding-audit/source/pr5270/P19_BANK.json
 create mode 100644 research/p19-current-head-binding-audit/source/pr5270/P19_CLAIM.json
 create mode 100644 research/p19-current-head-binding-audit/source/pr5270/P19_LIFT.json
 create mode 100644 research/p19-current-head-binding-audit/source/pr5270/P19_PLAIN.json
 create mode 100644 research/p19-current-head-binding-audit/source/pr5270/README.md
 create mode 100644 research/p19-current-head-binding-audit/source/pr5270/VERIFY.json
 create mode 100644 research/p19-current-head-binding-audit/source/pr5270/p19_bank.py
 create mode 100644 research/p19-current-head-binding-audit/source/pr5270/p19_claim.py
 create mode 100644 research/p19-current-head-binding-audit/source/pr5270/p19_lift.py
 create mode 100644 research/p19-current-head-binding-audit/source/pr5270/p19_plain.py
 create mode 100644 research/p19-current-head-binding-audit/verify.py

diff --git a/research/p19-current-head-binding-audit/README.md b/research/p19-current-head-binding-audit/README.md
new file mode 100644
index 0000000000..dcf06e8bbb
--- /dev/null
+++ b/research/p19-current-head-binding-audit/README.md
@@ -0,0 +1,121 @@
+# PR5270's p19 address protocol fails its claimed complete-controller identity
+
+**Exact current-head complete-word counterexample, with reproduced price gates. No new κ or supplier admission.**
+
+Audited [PR #5270](https://github.com/CrocSwap/integer-mult-bounds/pull/5270) at `225a19a184296d12120203a1f43b981d55465241`. Applying its submitted address-loop protocol to its emitted 241-gate p19 trace changes **72 entries** of the complete 38-by-38 controller matrix. With Q=1, D37=i and every other stage eigenvalue 1, input role 36 should contribute zero to output role 0; the submitted protocol contributes **i−1**. This is an exact realizable Gaussian eigencharacter, not a random-state or floating-point discrepancy.
+
+The invoice arithmetic is favorable separately. Adding **2,016 H1 jobs**, while retaining every target, makes its signed moment strictly negative for **every 0<C<1**. This threshold is sharp: 2,015 extra H1 jobs leave a positive moment at some sufficiently small positive C. At C=.0034, only **1,103** extra H1 jobs fit. The discussed 2,128-job and 4,256-job repairs exceed the all-exponent threshold. These statements concern those named fixed bills, not a universal decoder lower bound.
+
+## What the numbers mean
+
+The remembered .0039 BIT result resolves to this PR's proposed **outer κ=.003399996428…**, with inherited admitted BIT **.0034**. It proposes no new BIT construction.
+
+| Quantity at the audited head | Value | Scope |
+|---|---:|---|
+| Raw complex moment crossing | between .007578535189 and .007578535191 | Exact rational sign enclosure for an optimistic invoice; not an admitted uniform supplier or universal ceiling |
+| Tested complex saving | 2380001/700000000 = .003400001428… | The arithmetic tested by `p19_claim.py` |
+| Candidate covered uniform complex saving | 4760001/1400000000 = .003400000714… | The saving that compiler instance attempts to cover; actual physical/closure hypotheses remain necessary |
+| Inherited ordinary BIT saving | .0034363538396 | Reused source cover/bootstrap arithmetic |
+| Inherited admitted BIT saving | 17/5000 = .0034 | Unchanged |
+| Proposed outer κ | 951999/280000000 = .003399996428… | Five grid steps below admitted BIT, conditional on the missing supplier |
+
+Canonical main at entry was `721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8. Its selected record admits κ=.003125804 under five retained assumptions. Neither the raw .0075785 figure nor a hypothetical .0039 BIT component changes that selected complex-limited result. The proposed endpoint would improve that value by about 8.772% if its new physical obligations were closed; the percentages in PR5270 compare older records.
+
+## Complete-word decoder counterexample
+
+The current emitter stores an IDLE as **literal stage indices**, while the formal `term` converts that list to an indicator vector. The actual address loop runs `for s, bit in enumerate(sel)` and applies block **s** when `bit` is nonzero. It confuses a position with a stage label. The p19 terminal event on pair 17 has `sel=(37,38)`: correct thinning requires D37; the submitted protocol applies D1. All nine retained terminal events of I⁹T⁹ are displaced.
+
+`p19_bank.py` itself fixes p=2, pattern I. This audit instantiates its **unmodified gate-loop AST** on the actual emitted p19 gates with the intended fresh-block map. It does not claim that the original default command runs p19. The default control omits terminal IDLEs, hiding this case.
+
+For the canonical Gaussian,
+
+```text
+G = 1/2 [[1+i,1−i],[1−i,1+i]],
+G(1,1)=(1,1),     G(1,−1)=i(1,−1).
+```
+
+Take the tensor-product character negative on one axis of stage 37 and positive on every other axis, including the shared centre. Its 2^153 conceptual addresses are specified by one character mask. Every ideal address gate preserves this one-dimensional address subspace. A 38-by-38 coefficient calculation therefore computes its complete action without approximating or enumerating the addresses. Coefficient vectors represent independent **input roles**, not truncated address arrays.
+
+The intended authenticated controller and emitted trace are evaluated over exact Gaussian integers. The literal submitted address loop is evaluated over F65537 with i=256. A separate execution with only residue reductions removed recovers the exact Gaussian-integer outputs, agreeing with the residue loop on every entry. In particular i−1 has nonzero residue 255, refuting exact equality.
+
+| Test | Submitted decoder | Literal-stage IDLE repair |
+|---|---:|---:|
+| p2 I, all 32 physical central/block eigenvalue triples | 0 failures | 0 failures |
+| p2 T, same 32 triples | 24 failures | 0 failures |
+| p2 T: Q=1, D3=i, others 1 | 4 differing entries | 0 |
+| p3 IT: Q=1, D5=i, others 1 | 8 differing entries | 0 |
+| p19 I⁹T⁹: Q=1, D37=i, others 1 | 72 differing entries | 0 |
+
+At f=1 the central Gaussian has eigenvalues 1 and i; an eight-axis block has all four fourth roots. Thus the p2 grid has 2·4·4=32 physical triples. The repair is an **in-memory positive control** consuming literal stage labels. Frozen sources are never edited. Unchanged invertible factorization boundaries cannot make two unequal complete controller matrices equal; a changed boundary or caller requires its own proof.
+
+## The ideal lift does not supply the priced native call
+
+A genuine homomorphism for the correctly assigned commuting Gaussian variables preserves polynomial identities. The lifting script's sampled checks neither consume the emitted IDLE tuples nor identify the uncoded ideal shear with the coupled native producer. These are separate bindings.
+
+The PR's pinned historical `PHYSICAL.md` gives
+
+```text
+B = diag(D,D) [[I,−Q C],[0,I]],    C_ij=A_ij K_i^-1 K_j.
+```
+
+The all-ones uncoded trace requires C=I. All 112 diagonal entries of the pinned A are zero, hence C_jj=0. Put nonzero v in Y_j only, with all other main inputs zero. The inherited native reverse returns X_j=0, while the ideal uncoded reverse returns X_j=−DQv≠0. This local substitution failure holds at every positive width since D and Q are invertible.
+
+This corroborates the existing exact-head review; it does not exclude a newly proved adapter or whole-word cancellation. The signature `invoice(p,pattern,thick,profile)` does not prove that its supplied profile implements an arbitrary desired operator. Removing a coding argument does not turn C into I for free. Correcting IDLE indices alone leaves this native-to-invoice obligation open.
+
+A model control substitutes the source's pre-PR4929 profile `{1:2237,2:388,3:494,4:147,5:36,8:8}` into the same optimistic p19 targets. Its raw crossing lies in (.003004145206,.003004145208), below selected κ=.003125804. This does not construct that alternative caller or exclude other uncoded producers.
+
+## Reproduced fee theorem and its sharpness
+
+[Ali Romman](https://github.com/aliromman) already proves the 2,016 all-exponent bound, with an integer hinge certificate and the same .0034 budget, in the [physical-boundary cost finding](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19149724). The calculation below independently reproduces that result with the equivalent truncated-mass certificate. The observation that one fewer H1 fee admits a positive moment near t=1 is the elementary continuity sharpness check, not a new general theorem.
+
+Independent enumeration reproduces 12,008 targets and 68,782 paid jobs, with rank masses 265,533 and 263,517. Let T and P be these multisets and define
+
+```text
+A_h(u) = sum_{r in P} min(r,u) + h min(1,u) − sum_{r in T} min(r,u).
+```
+
+For h=2016, exact integers in `RESULT.json` give A_h≥0 at every rank breakpoint, strictly positive below the largest rank 153 and zero from 153 onward. Between breakpoints A_h is linear; its slope near zero is 58,790. Therefore A_h is nonnegative everywhere and positive on an interval. For 0<t<1,
+
+```text
+x^t = t(1−t) integral_0^infinity min(x,u) u^(t−2) du.
+```
+
+Integrating proves `sum(P r^t)+2016 > sum(T r^t)` for every such t. Thus every positive saving C=1−t fails after 2,016 or more extra H1 jobs. At h=2015 the target-minus-paid moment is 1 at t=1, so continuity makes it positive for some t<1 sufficiently close to 1. This proves sharpness, extending the earlier endpoint rank-mass screen to the whole exponent interval.
+
+At C=.0034, exact interval arithmetic bounds the unfunded surplus strictly between 1103 and 1104. A separate 90-digit Decimal sum gives approximately **1103.2761222689533**. This is the integer H1 budget at that saving, distinct from the all-exponent threshold 2,016.
+
+The earlier 2,128-H1 repair loses even if every original target remains credited. Losing a central target rank only worsens that bill; 2,128 H2 jobs cost at least as much for 0<t<1; the 4,256-H1 full-R-letter repair also loses. These implications price named additive bills and do not establish that every possible physical repair costs that much.
+
+## Relation to previous and later work
+
+[ahrazzle](https://github.com/ahrazzle)'s [PR #5349](https://github.com/CrocSwap/integer-mult-bounds/pull/5349) and [PR #5385](https://github.com/CrocSwap/integer-mult-bounds/pull/5385) audit and repair the older hand-transcribed reference. The current head replaces it with an emitted trace. This audit does not transfer the old three transcription failures to that revised emitter.
+
+[Chris R](https://github.com/Clear1nsight)'s [exact-head handoff](https://github.com/CrocSwap/integer-mult-bounds/pull/5270#issuecomment-6378014056) already identifies the local IDLE mismatch and zero-diagonal native witness. The new contribution is the **complete-word** literal-decoder check, p19 pulse output and controls, plus independent reproduction of the **prior all-exponent fee bound**. [Matarener](https://github.com/Matarener)'s [terminal-gauge review](https://github.com/CrocSwap/integer-mult-bounds/pull/5270#issuecomment-6374430946) supplies the earlier repair charges and budget observations. [James Reed](https://github.com/jwr404)'s compiler review and [zxv](https://github.com/zxv)'s geometry review retain their separate credit.
+
+The central ledger leaves [PR #5440](https://github.com/CrocSwap/integer-mult-bounds/pull/5440), head `c0f52b5b18bba78a6a5e8057edf9571bade88549`, open over its full-R/D binding and missing charges. It is a different coded word, not replayed here; the tuple counterexample is not automatically transferred to it.
+
+[PR #5027](https://github.com/CrocSwap/integer-mult-bounds/pull/5027) already provides conditional p19 compiler arithmetic. [PR #5069](https://github.com/CrocSwap/integer-mult-bounds/pull/5069) provides a priced physical pair, and [PR #5563](https://github.com/CrocSwap/integer-mult-bounds/pull/5563) provides paid central-Q decoders with losing complete bills. They retain constructive alternatives and the distinction between a correct paid repair and a profitable supplier. Their full replays are not repeated.
+
+## Reproduction and verification limits
+
+```sh
+python3.12 -I -B research/p19-current-head-binding-audit/verify.py
+python3.12 -I -O -B research/p19-current-head-binding-audit/verify.py
+python3.12 -B scripts/research_package.py --package research/p19-current-head-binding-audit
+```
+
+The default verifier is read-only and compares a freshly calculated mathematical receipt. `--write` explicitly regenerates it. Small exact exports from the unmerged head retain their paths, commit/blob IDs and SHA256 values in `SOURCE_EXPORTS.json`. Canonical inputs and historical guidance are pinned in `SOURCES.json`. No external PR-head availability is required for replay; exports are retained evidence, not edits to the predecessor.
+
+`VALIDATION.json` separates fresh normal/optimized scoped checks, author arithmetic runs, source-corruption controls and the bounded original bank-run timeout. A timeout is not a pass. No full p19 Laurent factorization, native archive replay, enormous address enumeration, Lean, Docker, machine compiler, precision/tape/stock closure or analytic recovery theorem is newly verified. The selected five assumptions remain unchanged. The selected-baseline helper could not authenticate its full certificate closure in the intentionally sparse checkout; selected values were instead read directly from the pinned Git record, certificate and maintainer review.
+
+## Significance for researchers
+
+The favorable raw price survives arithmetic checks, while its asserted implementation bridge fails on an exact complete-word input. This identifies the useful next task: an actual compatible physical caller with every correction and target change charged. The independently reproduced fee certificate supplies an early stopping test for this fixed invoice. Its all-exponent force was already established in the credited boundary-budget finding; this package adds a different exact certificate and the elementary sharpness control.
+
+## Open next questions
+
+The structured questions in `TASK.json` concern a physical producer/adapter for the uncoded trace and a changed current-query/terminal contract meeting the complete budget. Start with arbitrary owner inputs and the exact causal source version. The IDLE patch is a control, not a profitable construction. A changed profile, reused query, joint target or different operator is outside the fixed-fee theorem and needs its own source-bound bill.
+
+## Credit and assistance
+
+Prepared for [zxv](https://github.com/zxv) with substantial OpenAI Codex assistance in mathematics, implementation, verification and writing. One worker, no subagents. Retained source credit: [DaysSky](https://github.com/DaysSky); [Seth Burkart](https://github.com/SethBurkart123), as credited in [PR #4940](https://github.com/CrocSwap/integer-mult-bounds/pull/4940); [Dillon Amburgey](https://github.com/dillona), [PR #4933](https://github.com/CrocSwap/integer-mult-bounds/pull/4933); [David Ganz](https://github.com/Dugongue), [PR #4929](https://github.com/CrocSwap/integer-mult-bounds/pull/4929); [Cinna Davis](https://github.com/1337isnot1337), [Cao Yifan](https://github.com/intqwq), and their retained native, helper, Clifford, compiler, BIT and analytic predecessors. Original source notices remain intact. New work is Apache-2.0; no independent human or proof-kernel acceptance is implied.
diff --git a/research/p19-current-head-binding-audit/RESULT.json b/research/p19-current-head-binding-audit/RESULT.json
new file mode 100644
index 0000000000..d8669a1a59
--- /dev/null
+++ b/research/p19-current-head-binding-audit/RESULT.json
@@ -0,0 +1,1100 @@
+{
+  "native_same_owner_zero_blocks": 112,
+  "p2_eigenvalue_grid": {
+    "I": {
+      "repaired_loop_failures": 0,
+      "submitted_loop_failures": 0,
+      "triples": 32
+    },
+    "T": {
+      "repaired_loop_failures": 0,
+      "submitted_loop_failures": 24,
+      "triples": 32
+    }
+  },
+  "price": {
+    "admitted_BIT": "17/5000",
+    "at_BIT_0034_extra_H1_budget": 1103,
+    "claimed_outer_kappa": "951999/280000000",
+    "conditional_uniform_complex": "4760001/1400000000",
+    "decimal_margin_at_BIT_0034": "1103.276122268953300416864498123214428144963675676350652081574855696343764575778138250172",
+    "fees_2128_and_4256_excluded_for_every_0_t_1": true,
+    "paid_count": 68782,
+    "paid_rank_mass": 263517,
+    "pre_PR4929_profile_control": {
+      "negative_margin_at_selected_kappa_003125804": true,
+      "profile": {
+        "1": 2237,
+        "2": 388,
+        "3": 494,
+        "4": 147,
+        "5": 36,
+        "8": 8
+      },
+      "raw_crossing_sign_bracket": [
+        "1502072603/500000000000",
+        "375518151/125000000000"
+      ]
+    },
+    "raw_crossing_sign_bracket": [
+      "7578535189/1000000000000",
+      "7578535191/1000000000000"
+    ],
+    "sharp_extra_H1_threshold": 2016,
+    "target_count": 12008,
+    "target_rank_mass": 265533,
+    "tested_complex": "2380001/700000000",
+    "truncated_mass_gaps_after_2016_H1": {
+      "1": 58790,
+      "153": 0,
+      "16": 34272,
+      "17": 33600,
+      "2": 71505,
+      "24": 32032,
+      "25": 31360,
+      "3": 76392,
+      "32": 29792,
+      "33": 29120,
+      "4": 71589,
+      "40": 27552,
+      "41": 26880,
+      "48": 25312,
+      "49": 24640,
+      "5": 64905,
+      "56": 23072,
+      "57": 22400,
+      "64": 20832,
+      "65": 20160,
+      "7": 50017,
+      "72": 18592,
+      "73": 17920,
+      "8": 42706,
+      "9": 35840
+    }
+  },
+  "scope": "Exact source-bound counterexamples and fixed-invoice fee theorem; no new supplier, admission, global decoder lower bound or kappa.",
+  "source_head": "225a19a184296d12120203a1f43b981d55465241",
+  "status": "PASS_P19_CURRENT_HEAD_BINDING_AUDIT",
+  "whole_word_witnesses": {
+    "19": {
+      "active_eigenvalue": [
+        0,
+        1
+      ],
+      "active_stage": 37,
+      "all_other_stage_eigenvalues": [
+        1,
+        0
+      ],
+      "central_eigenvalue": [
+        1,
+        0
+      ],
+      "gate_count": 241,
+      "mismatches": [
+        [
+          0,
+          18,
+          [
+            1,
+            -1
+          ],
+          0
+        ],
+        [
+          0,
+          36,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          2,
+          18,
+          [
+            -1,
+            1
+          ],
+          0
+        ],
+        [
+          2,
+          36,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          4,
+          18,
+          [
+            1,
+            -1
+          ],
+          0
+        ],
+        [
+          4,
+          36,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          6,
+          18,
+          [
+            -1,
+            1
+          ],
+          0
+        ],
+        [
+          6,
+          36,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          8,
+          18,
+          [
+            1,
+            -1
+          ],
+          0
+        ],
+        [
+          8,
+          36,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          10,
+          18,
+          [
+            -1,
+            1
+          ],
+          0
+        ],
+        [
+          10,
+          36,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          12,
+          18,
+          [
+            1,
+            -1
+          ],
+          0
+        ],
+        [
+          12,
+          36,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          14,
+          18,
+          [
+            -1,
+            1
+          ],
+          0
+        ],
+        [
+          14,
+          36,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          16,
+          18,
+          [
+            1,
+            -1
+          ],
+          0
+        ],
+        [
+          16,
+          36,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          18,
+          18,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          18,
+          36,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          19,
+          1,
+          [
+            1,
+            -1
+          ],
+          0
+        ],
+        [
+          19,
+          3,
+          [
+            -1,
+            1
+          ],
+          0
+        ],
+        [
+          19,
+          5,
+          [
+            1,
+            -1
+          ],
+          0
+        ],
+        [
+          19,
+          7,
+          [
+            -1,
+            1
+          ],
+          0
+        ],
+        [
+          19,
+          9,
+          [
+            1,
+            -1
+          ],
+          0
+        ],
+        [
+          19,
+          11,
+          [
+            -1,
+            1
+          ],
+          0
+        ],
+        [
+          19,
+          13,
+          [
+            1,
+            -1
+          ],
+          0
+        ],
+        [
+          19,
+          15,
+          [
+            -1,
+            1
+          ],
+          0
+        ],
+        [
+          19,
+          17,
+          [
+            1,
+            -1
+          ],
+          0
+        ],
+        [
+          19,
+          19,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          20,
+          20,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          20,
+          36,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          21,
+          21,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          22,
+          22,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          22,
+          36,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          23,
+          23,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          24,
+          24,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          24,
+          36,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          25,
+          25,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          26,
+          26,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          26,
+          36,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          27,
+          27,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          28,
+          28,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          28,
+          36,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          29,
+          29,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          30,
+          30,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          30,
+          36,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          31,
+          31,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          32,
+          32,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          32,
+          36,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          33,
+          33,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          34,
+          34,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          34,
+          36,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          35,
+          35,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          37,
+          1,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          37,
+          3,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          37,
+          5,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          37,
+          7,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          37,
+          9,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          37,
+          11,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          37,
+          13,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          37,
+          15,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          37,
+          17,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          37,
+          19,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          37,
+          21,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          37,
+          23,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          37,
+          25,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          37,
+          27,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          37,
+          29,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          37,
+          31,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          37,
+          33,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          37,
+          35,
+          [
+            0,
+            0
+          ],
+          65282
+        ]
+      ],
+      "pattern": "IIIIIIIIITTTTTTTTT",
+      "pulse_actual": [
+        -1,
+        1
+      ],
+      "pulse_expected": [
+        0,
+        0
+      ],
+      "pulse_input_role": 36,
+      "pulse_output_role": 0,
+      "retained_terminal_events": [
+        {
+          "kind": "terminal",
+          "pair": 9,
+          "retained": true,
+          "sel": [
+            21,
+            22,
+            23,
+            24,
+            25,
+            26,
+            27,
+            28,
+            29,
+            30,
+            31,
+            32,
+            33,
+            34,
+            35,
+            36,
+            37,
+            38
+          ]
+        },
+        {
+          "kind": "terminal",
+          "pair": 10,
+          "retained": true,
+          "sel": [
+            23,
+            24,
+            25,
+            26,
+            27,
+            28,
+            29,
+            30,
+            31,
+            32,
+            33,
+            34,
+            35,
+            36,
+            37,
+            38
+          ]
+        },
+        {
+          "kind": "terminal",
+          "pair": 11,
+          "retained": true,
+          "sel": [
+            25,
+            26,
+            27,
+            28,
+            29,
+            30,
+            31,
+            32,
+            33,
+            34,
+            35,
+            36,
+            37,
+            38
+          ]
+        },
+        {
+          "kind": "terminal",
+          "pair": 12,
+          "retained": true,
+          "sel": [
+            27,
+            28,
+            29,
+            30,
+            31,
+            32,
+            33,
+            34,
+            35,
+            36,
+            37,
+            38
+          ]
+        },
+        {
+          "kind": "terminal",
+          "pair": 13,
+          "retained": true,
+          "sel": [
+            29,
+            30,
+            31,
+            32,
+            33,
+            34,
+            35,
+            36,
+            37,
+            38
+          ]
+        },
+        {
+          "kind": "terminal",
+          "pair": 14,
+          "retained": true,
+          "sel": [
+            31,
+            32,
+            33,
+            34,
+            35,
+            36,
+            37,
+            38
+          ]
+        },
+        {
+          "kind": "terminal",
+          "pair": 15,
+          "retained": true,
+          "sel": [
+            33,
+            34,
+            35,
+            36,
+            37,
+            38
+          ]
+        },
+        {
+          "kind": "terminal",
+          "pair": 16,
+          "retained": true,
+          "sel": [
+            35,
+            36,
+            37,
+            38
+          ]
+        },
+        {
+          "kind": "terminal",
+          "pair": 17,
+          "retained": true,
+          "sel": [
+            37,
+            38
+          ]
+        }
+      ]
+    },
+    "2": {
+      "active_eigenvalue": [
+        0,
+        1
+      ],
+      "active_stage": 3,
+      "all_other_stage_eigenvalues": [
+        1,
+        0
+      ],
+      "central_eigenvalue": [
+        1,
+        0
+      ],
+      "gate_count": 20,
+      "mismatches": [
+        [
+          0,
+          0,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          0,
+          2,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          1,
+          1,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          3,
+          1,
+          [
+            0,
+            0
+          ],
+          65282
+        ]
+      ],
+      "pattern": "T",
+      "pulse_actual": [
+        1,
+        -1
+      ],
+      "pulse_expected": [
+        0,
+        0
+      ],
+      "pulse_input_role": 2,
+      "pulse_output_role": 0,
+      "retained_terminal_events": [
+        {
+          "kind": "terminal",
+          "pair": 0,
+          "retained": true,
+          "sel": [
+            3,
+            4
+          ]
+        }
+      ]
+    },
+    "3": {
+      "active_eigenvalue": [
+        0,
+        1
+      ],
+      "active_stage": 5,
+      "all_other_stage_eigenvalues": [
+        1,
+        0
+      ],
+      "central_eigenvalue": [
+        1,
+        0
+      ],
+      "gate_count": 33,
+      "mismatches": [
+        [
+          0,
+          2,
+          [
+            1,
+            -1
+          ],
+          0
+        ],
+        [
+          0,
+          4,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          2,
+          2,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          2,
+          4,
+          [
+            0,
+            0
+          ],
+          65282
+        ],
+        [
+          3,
+          1,
+          [
+            1,
+            -1
+          ],
+          0
+        ],
+        [
+          3,
+          3,
+          [
+            0,
+            1
+          ],
+          1
+        ],
+        [
+          5,
+          1,
+          [
+            0,
+            0
+          ],
+          255
+        ],
+        [
+          5,
+          3,
+          [
+            0,
+            0
+          ],
+          65282
+        ]
+      ],
+      "pattern": "IT",
+      "pulse_actual": [
+        -1,
+        1
+      ],
+      "pulse_expected": [
+        0,
+        0
+      ],
+      "pulse_input_role": 4,
+      "pulse_output_role": 0,
+      "retained_terminal_events": [
+        {
+          "kind": "terminal",
+          "pair": 1,
+          "retained": true,
+          "sel": [
+            5,
+            6
+          ]
+        }
+      ]
+    }
+  }
+}
diff --git a/research/p19-current-head-binding-audit/SOURCES.json b/research/p19-current-head-binding-audit/SOURCES.json
new file mode 100644
index 0000000000..ac6a2652ca
--- /dev/null
+++ b/research/p19-current-head-binding-audit/SOURCES.json
@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/coded-native-caller/CODE.json",
+      "usage": "input",
+      "git_blob": "03170f4a31f7a8a3db7228f1cd5a6fdcb32720ae",
+      "sha256": "8be7f3f073b7981ec91c6af43edff0ac8a89f4824ef6026ae758c287dd6c03d0"
+    },
+    {
+      "path": "research/coded-native-caller/NORMALIZERS.json",
+      "usage": "input",
+      "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f",
+      "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da"
+    },
+    {
+      "path": "research/coded-native-caller/PHYSICAL.md",
+      "usage": "input",
+      "git_blob": "da8837ba67423ef08ef1afb8e8297a8032aafe9f",
+      "sha256": "4321b159ff8d3fe705419adaaa1beef75606e869e34341bda553f17d598a6078"
+    },
+    {
+      "path": "research/coded-reverse-controller/verify.py",
+      "usage": "input",
+      "git_blob": "71f3d8929f28d7b4b854be7177ca8dfecf81ea5c",
+      "sha256": "05a898d3af329dc4665590b4ec4b2801e588843efe9618eec55b4028fd104b67"
+    },
+    {
+      "path": "research/higher-moment-strictification/verify.py",
+      "usage": "input",
+      "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699",
+      "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326"
+    },
+    {
+      "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py",
+      "usage": "input",
+      "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59",
+      "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15"
+    }
+  ]
+}
diff --git a/research/p19-current-head-binding-audit/SOURCE_EXPORTS.json b/research/p19-current-head-binding-audit/SOURCE_EXPORTS.json
new file mode 100644
index 0000000000..10cf53b3ff
--- /dev/null
+++ b/research/p19-current-head-binding-audit/SOURCE_EXPORTS.json
@@ -0,0 +1,77 @@
+{
+  "schema_version": 1,
+  "source_pr": 5270,
+  "source_head": "225a19a184296d12120203a1f43b981d55465241",
+  "files": [
+    {
+      "path": "source/pr5270/p19_plain.py",
+      "source_path": "research/coded-reverse-word-p19/p19_plain.py",
+      "source_commit": "225a19a184296d12120203a1f43b981d55465241",
+      "source_blob": "b060f5a8fcf1d40773091fa7c16a10b4e87f48c4",
+      "sha256": "b9b01861a78272aa08f498b4510cea3249a058f8d713afca2c68bc6bcdbdc8d9"
+    },
+    {
+      "path": "source/pr5270/p19_bank.py",
+      "source_path": "research/coded-reverse-word-p19/p19_bank.py",
+      "source_commit": "225a19a184296d12120203a1f43b981d55465241",
+      "source_blob": "164c3b6d4105f42a2ab08d3d543592de37be77ef",
+      "sha256": "bacd9084f79b60826db14d82ed5389cfd514771228729df21f2862b660aa9533"
+    },
+    {
+      "path": "source/pr5270/p19_lift.py",
+      "source_path": "research/coded-reverse-word-p19/p19_lift.py",
+      "source_commit": "225a19a184296d12120203a1f43b981d55465241",
+      "source_blob": "2a1aa4c4980da7df22b5ec4ee91bde66db6d6567",
+      "sha256": "93b4c4f95931191c724578bc2d483420bbb9a7e188f455d90ec8b711a6b54d53"
+    },
+    {
+      "path": "source/pr5270/p19_claim.py",
+      "source_path": "research/coded-reverse-word-p19/p19_claim.py",
+      "source_commit": "225a19a184296d12120203a1f43b981d55465241",
+      "source_blob": "92ae6514e45c679f7855cd36580cb047d2d6b321",
+      "sha256": "7ae0925f3542ad980cb6030717b3fdc468825169ed2d47cacc91810e510b64d5"
+    },
+    {
+      "path": "source/pr5270/P19_PLAIN.json",
+      "source_path": "research/coded-reverse-word-p19/P19_PLAIN.json",
+      "source_commit": "225a19a184296d12120203a1f43b981d55465241",
+      "source_blob": "f06e82ac51a7fb91e013f2f762e39d3b8b619442",
+      "sha256": "4ca0cac96f2fb865e82b8e47afcf818048758e17d0b99518698b6ab68bc07346"
+    },
+    {
+      "path": "source/pr5270/P19_BANK.json",
+      "source_path": "research/coded-reverse-word-p19/P19_BANK.json",
+      "source_commit": "225a19a184296d12120203a1f43b981d55465241",
+      "source_blob": "4fe0ceeb89a8525ed5301a510de53de1b13131f9",
+      "sha256": "cb78c185947d1dd03d97a94ca6e7239b5fa9d6e0f4a9a51a89fa8e4b58158472"
+    },
+    {
+      "path": "source/pr5270/P19_CLAIM.json",
+      "source_path": "research/coded-reverse-word-p19/P19_CLAIM.json",
+      "source_commit": "225a19a184296d12120203a1f43b981d55465241",
+      "source_blob": "f92d36216cc5b87b52efde5a3740127a6e1faaea",
+      "sha256": "d9c53d0c5563189c6c83b50089048ca65727d58d4457ac373d8a404ba3ba3b50"
+    },
+    {
+      "path": "source/pr5270/P19_LIFT.json",
+      "source_path": "research/coded-reverse-word-p19/P19_LIFT.json",
+      "source_commit": "225a19a184296d12120203a1f43b981d55465241",
+      "source_blob": "6b42f7266ed5c7410992f4120815bfc28062f14d",
+      "sha256": "b1c500cdb609492dbd8d0d95a365b614ca1f10ef8c82134e6baa37330324f085"
+    },
+    {
+      "path": "source/pr5270/VERIFY.json",
+      "source_path": "research/coded-reverse-word-p19/VERIFY.json",
+      "source_commit": "225a19a184296d12120203a1f43b981d55465241",
+      "source_blob": "ee9fc201a9afb404c20b4a1b6b243fbb3309bce8",
+      "sha256": "26eaef50e5d8312b1bc90d46bf520534a645b605834066199b843a35ba012cae"
+    },
+    {
+      "path": "source/pr5270/README.md",
+      "source_path": "research/coded-reverse-word-p19/README.md",
+      "source_commit": "225a19a184296d12120203a1f43b981d55465241",
+      "source_blob": "066d9ded0ff93e2b6e46b7002ec477f83e98096d",
+      "sha256": "1e8b4eade89db46a81198167596b1b729ce25f65b6a24597a5608791d57d9cf6"
+    }
+  ]
+}
diff --git a/research/p19-current-head-binding-audit/TASK.json b/research/p19-current-head-binding-audit/TASK.json
new file mode 100644
index 0000000000..db47dbf433
--- /dev/null
+++ b/research/p19-current-head-binding-audit/TASK.json
@@ -0,0 +1,97 @@
+{
+  "schema_version": 1,
+  "task_id": "supplier-boundary-audit",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "original_card": {
+    "id": "supplier-boundary-audit",
+    "question": "Does one changed supplier have complete source-bound native, caller, ordinary and outer admission coverage?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose one latest uncovered candidate and build a delta coverage map against the selected review. For P104, #5717 changes owned-lifetime assumptions and #5719 covers exact #5713 causal premises; neither automatically transfers to #5718. For BIT, #5679/#5708 need component admission and compatible outer use. Check controls and exact source identity before reuse; stop with one resolved gap or explicit remaining obligation. A heavy full replay requires a separate serial resource budget.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "supplier admission",
+      "5717",
+      "5719",
+      "5708",
+      "owned lifetime"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3801: successor scatter-boundary decision package.",
+        "evidence": "research/scatter-boundary-decision/README.md",
+        "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.",
+        "status": "author-checked",
+        "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Explicit audit of PR5270 at 225a19a184296d12120203a1f43b981d55465241: complete current IDLE-decoder counterexample on exact Gaussian eigencharacters, native-to-uncoded substitution, and sharp fixed-invoice extra-H1 budget.",
+  "scope_change_reason": "The explicit assignment identifies PR5270 rather than the selected P104 caller in the generic card. Existing exact-head local objections are credited; the new scope binds the actual address-loop AST to complete p19 outputs and proves a sharp all-exponent fee threshold. The final live refresh located Ali Romman\u2019s prior all-exponent boundary-cost proof (Discussion4930#discussioncomment-19149724); the fee certificate is explicitly an independent reproduction, not a novel threshold claim. The new endpoint witness remains distinct.",
+  "bottleneck_link": "A favorable invoice and compiler arithmetic cannot raise the selected exponent without a physical supplier realizing the same independent Gaussian targets and paid jobs. PR5270 inherits BIT .0034 and proposes a complex improvement; it supplies no new BIT saving.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the exact current-head binding counterexample and fixed-invoice fee theorem. Do not construct a new caller, rerun the full historical corpus, or change admission/frontier/queue decisions.",
+  "outcome": "completed",
+  "evidence": "RESULT.json: p19 has 72 complete controller entry mismatches on one exact eigencharacter; the submitted p2 I control passes all 32 physical eigenvalue triples while T fails 24; literal-stage IDLE repair passes the tested complete words; exact truncated-mass certificate reproduces the prior extra-H1 threshold 2016 with a continuity sharpness control. Arithmetic passes separately. See VALIDATION.json for commands and bounded author-run limits.",
+  "author": "zxv (https://github.com/zxv)",
+  "ai_assistance": "Substantial OpenAI Codex assistance in source reading, mathematical derivation, implementation, verification and writing. One worker, no subagents; no independent human or proof-kernel acceptance.",
+  "open_questions": [
+    {
+      "question": "Can an actual changed native producer or adapter realize the all-ones p19 trace under a favorable complete bill?",
+      "why_it_matters": "The original coupled producer has C_jj=0 while the ideal uncoded reverse has a nonzero same-owner block; correcting IDLE indices does not bridge this gap.",
+      "first_step": "Exhibit one physical reverse/thin pair on arbitrary independent owner inputs, preserving all helper returns and recording every recursive and ordinary charge, then compose the complete caller.",
+      "blocked_by": "No source-bound implementation with the claimed profile and zero recoding bill is supplied by the audited head."
+    },
+    {
+      "question": "Can a changed terminal/query contract require fewer than the fixed-invoice fee budget without losing target credit?",
+      "why_it_matters": "At saving .0034 only 1103 extra H1 jobs fit; 2016 already defeats every positive saving with unchanged targets.",
+      "first_step": "Bind a genuinely reused query to its current causal input and whole output contract, and recompute the complete signed invoice before expanding a construction search.",
+      "blocked_by": "The fee theorem does not provide or price a cheaper physical adapter, and is not a universal decoder lower bound."
+    }
+  ]
+}
diff --git a/research/p19-current-head-binding-audit/VALIDATION.json b/research/p19-current-head-binding-audit/VALIDATION.json
new file mode 100644
index 0000000000..6696e1c8b9
--- /dev/null
+++ b/research/p19-current-head-binding-audit/VALIDATION.json
@@ -0,0 +1,136 @@
+{
+  "schema_version": 1,
+  "canonical_main": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "priority_revision": 8,
+  "audited_pr": 5270,
+  "audited_head": "225a19a184296d12120203a1f43b981d55465241",
+  "live_head_rechecked_UTC": "2026-10-28T04:03:24.662400+00:00",
+  "author_arithmetic_environment": "CPython 3.11.11 on macOS 26.5.1 arm64; working head remained unchanged. The normal and optimized claim scripts regenerate their original receipt byte-identically.",
+  "scoped_environment": "3.12.8 (main, Dec  7 2024, 10:11:37) [Clang 15.0.0 (clang-1500.3.9.4)]\nmacOS-26.5.1-arm64-arm-64bit",
+  "bounded_runs": {
+    "claim-normal": {
+      "argv": [
+        "python3",
+        "-I",
+        "-B",
+        "research/coded-reverse-word-p19/p19_claim.py"
+      ],
+      "cwd": "/tmp/integer-p19-source",
+      "seconds": 3.331884082988836,
+      "peak_sampled_descendant_rss_kib": 35696,
+      "exit_code": 0,
+      "stop": null,
+      "stdout_sha256": "bf3515b8fab4cf64e68cfdf65b925a4b88d8e9aac50004480f78d858296150fd",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "claim-optimized": {
+      "argv": [
+        "python3",
+        "-I",
+        "-O",
+        "-B",
+        "research/coded-reverse-word-p19/p19_claim.py"
+      ],
+      "cwd": "/tmp/integer-p19-source",
+      "seconds": 3.6183614580659196,
+      "peak_sampled_descendant_rss_kib": 37264,
+      "exit_code": 0,
+      "stop": null,
+      "stdout_sha256": "bf3515b8fab4cf64e68cfdf65b925a4b88d8e9aac50004480f78d858296150fd",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "bank-normal-ready": {
+      "argv": [
+        "python3",
+        "-B",
+        "research/coded-reverse-word-p19/p19_bank.py"
+      ],
+      "cwd": "/tmp/integer-p19-source",
+      "seconds": 180.13060004194267,
+      "peak_sampled_descendant_rss_kib": 132752,
+      "exit_code": -15,
+      "stop": "timeout",
+      "stdout_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "audit-normal": {
+      "argv": [
+        "/opt/local/bin/python3.12",
+        "-I",
+        "-B",
+        "research/p19-current-head-binding-audit/verify.py"
+      ],
+      "cwd": "/tmp/integer-bit0039-audit",
+      "seconds": 1.993826457997784,
+      "peak_sampled_descendant_rss_kib": 27632,
+      "exit_code": 0,
+      "stop": null,
+      "stdout_sha256": "6dc0a4cd356c93ebdf6a0764b6e9f0a3ff7b9ba03a563c6f572f4efef28b04a5",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "audit-optimized": {
+      "argv": [
+        "/opt/local/bin/python3.12",
+        "-I",
+        "-O",
+        "-B",
+        "research/p19-current-head-binding-audit/verify.py"
+      ],
+      "cwd": "/tmp/integer-bit0039-audit",
+      "seconds": 1.6472067920258269,
+      "peak_sampled_descendant_rss_kib": 27712,
+      "exit_code": 0,
+      "stop": null,
+      "stdout_sha256": "6dc0a4cd356c93ebdf6a0764b6e9f0a3ff7b9ba03a563c6f572f4efef28b04a5",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    }
+  },
+  "export_control": {
+    "export_path": "/var/folders/y2/rqpdcbzj7_98322kfb3v7_kr0000gq/T/integer-p19-audit-export-oxvzgxdu",
+    "python": "/opt/local/bin/python3.12",
+    "PATH": "",
+    "git_free_replay_exit_code": 0,
+    "files_unchanged": true,
+    "stdout": "PASS_P19_CURRENT_HEAD_BINDING_AUDIT head=225a19a184296d12120203a1f43b981d55465241 p19_mismatches=72 sharp_H1_fee=2016 no_new_kappa",
+    "source_corruption_exit_code": 1,
+    "source_corruption_rejected_before_execution": true
+  },
+  "registered_package": "Normal and optimized CPython 3.12 manifest commands and metadata/source pins pass; no scientific admission follows.",
+  "not_run": [
+    "complete original p19 Laurent factorization and diagonalization",
+    "full native archive replay",
+    "large address-space enumeration",
+    "Lean",
+    "Docker",
+    "full machine/compiler/precision/tape/stock/analytic recovery proof"
+  ],
+  "limitations": [
+    "Original p2 bank command stopped at 180 seconds with no pass receipt. An earlier sparse setup import failure was resolved before this bounded run.",
+    "The complete-word p19 result instantiates the actual gate-loop semantics with p19 gates; the submitted main remains hardcoded to p2 pattern I.",
+    "Fresh source-bound mathematical checks are author-side AI-assisted checks, not independent human or proof-kernel acceptance."
+  ],
+  "live_pr_state": {
+    "draft": true,
+    "state": "open",
+    "head": "225a19a184296d12120203a1f43b981d55465241",
+    "updated_at": "2026-10-24T01:13:39Z"
+  },
+  "source_worktree_status": "",
+  "author_normal_optimized_stdout_identical": true,
+  "final_overlap": {
+    "open_prs": {
+      "fetched_at": "2026-10-28T04:02:06.490762+00:00",
+      "complete_pagination": true,
+      "records": 331
+    },
+    "discussions": {
+      "fetched_at": "2026-10-28T04:03:24.983323+00:00",
+      "complete_pagination": true,
+      "records": 5718
+    }
+  },
+  "final_overlap_local_scope": "Sparse local inventory incomplete; relevant retained native/controller/reference/decoder notes were materialized. Live PR/Discussion searches are provisional leads, not novelty proof.",
+  "prior_fee_proof": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19149724",
+  "original_contribution": "Complete-word execution of the exact current address-loop protocol on emitted p19 gates, with the role-36 to role-0 pulse witness, p2 eigenvalue controls and narrow repair controls. The fee threshold is independently reproduced prior work.",
+  "frozen_source_whitespace": "git diff --check reports one pre-existing trailing space in retained source/pr5270/p19_claim.py:370. Exact source bytes/hashes are preserved; new authored files pass the scoped whitespace check."
+}
diff --git a/research/p19-current-head-binding-audit/VERIFY.json b/research/p19-current-head-binding-audit/VERIFY.json
new file mode 100644
index 0000000000..60e7c397c1
--- /dev/null
+++ b/research/p19-current-head-binding-audit/VERIFY.json
@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/coded-native-caller/CODE.json",
+    "research/coded-native-caller/NORMALIZERS.json",
+    "research/coded-native-caller/PHYSICAL.md",
+    "research/coded-reverse-controller/verify.py",
+    "research/higher-moment-strictification/verify.py",
+    "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact current-head source bindings, Gaussian-integer/controller and literal address-loop eigencharacter checks, p2 controls, physical zero-diagonal witness, independently recounted invoice, exact crossing signs and sharp concave-order fee certificate."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Same semantic checks and deterministic receipt with assertions disabled."
+    }
+  ]
+}
diff --git a/research/p19-current-head-binding-audit/source/pr5270/P19_BANK.json b/research/p19-current-head-binding-audit/source/pr5270/P19_BANK.json
new file mode 100644
index 0000000000..4fe0ceeb89
--- /dev/null
+++ b/research/p19-current-head-binding-audit/source/pr5270/P19_BANK.json
@@ -0,0 +1,20 @@
+{
+  "addresses_per_role": 131072,
+  "binding": "the trace gate list and the controller matrix agree on every address of every role at the smallest faithful ambient (two blocks plus the shared centre)",
+  "differing_entries": [
+    0,
+    0,
+    0,
+    0
+  ],
+  "gates": 20,
+  "p": 2,
+  "pattern": "I",
+  "retained_stages": [
+    1,
+    3
+  ],
+  "roles": 4,
+  "scope": "p=19 needs 2**153 addresses, so the address-level check is done at p=2 and the p=19 word is certified by the trace identity in the controller algebra",
+  "status": "PASS_ADDRESS_LEVEL_TRACE_REPLAY"
+}
diff --git a/research/p19-current-head-binding-audit/source/pr5270/P19_CLAIM.json b/research/p19-current-head-binding-audit/source/pr5270/P19_CLAIM.json
new file mode 100644
index 0000000000..f92d36216c
--- /dev/null
+++ b/research/p19-current-head-binding-audit/source/pr5270/P19_CLAIM.json
@@ -0,0 +1,175 @@
+{
+  "admitted_bit_saving": "17/5000",
+  "bit_supplier": "17/5000",
+  "budgets": {
+    "field_bill_bucket": "raw",
+    "field_bill_records": 896000,
+    "local_allowance": 10000000,
+    "local_routes": 4794000,
+    "local_scalar": 158168,
+    "raw_allowance": 1000000000,
+    "raw_bound": 190964096
+  },
+  "compiler": {
+    "B": "(5+8h)v",
+    "H0": 5170423668736,
+    "H0_check": "H0 >= 8v",
+    "H1": 49222448837637726209,
+    "N": "2^49222448837637726209",
+    "classification": "numerical instantiation under an applicability premise, not a proof",
+    "h": "1/64",
+    "majorant": "shape-correct power majorant (query-thinned-controllers constants)",
+    "uninstantiated_hypotheses": [
+      "rank completion below b^v",
+      "job splitting at c^v",
+      "whole-job normalizers",
+      "distinct-owner child allocation",
+      "rank-one surplus retention",
+      "fresh-block replay of the trace"
+    ],
+    "v": 1024
+  },
+  "compiler_obligations": {
+    "distinct-owner child allocation": "inherited; the word introduces no new owner",
+    "rank completion below b^v": "checked on this census: max target rank 153 < 256",
+    "rank-one surplus retention": "inherited; the census is unchanged by the word",
+    "splitting at c^v": "checked on this census: 20^64 < 21^63",
+    "whole-job normalizers": "inherited from the producer; the word adds no job and consumes the same T/D interface"
+  },
+  "complex_saving": 0.007578535,
+  "complex_supplier": "0.007578535",
+  "field_level_bill": {
+    "monomial_field_maps": 0,
+    "owned_clears": 0,
+    "recodings": 0,
+    "recursive_gaussian_children": 0,
+    "scalar_adds": 0,
+    "terminal_gauge_decoder": 0
+  },
+  "frontier_reported": "302728823/100000000000",
+  "frontier_reported_provenance": "maintainer-reported in review; no certificate in this tree",
+  "frontier_selected_record": "60403/20000000",
+  "gain_vs_reported_percent": 12.312,
+  "gain_vs_selected_record_percent": 12.577,
+  "guards": {
+    "alpha": 0.9957941423234126,
+    "delta": 0.9515606084977414,
+    "gamma": 0.9637633130133417
+  },
+  "helper_profile": {
+    "4": 28,
+    "7": 7,
+    "8": 47,
+    "9": 326
+  },
+  "idles": {
+    "gauge_neutral": true,
+    "initial": 9,
+    "middle": 18,
+    "rank_applied": 198,
+    "retained": 36,
+    "role_rank": 396,
+    "terminal": 9
+  },
+  "kappa": "951999/280000000",
+  "kappa_decimal": 0.0033999964285714285,
+  "kappa_under_logarithmic_majorant": "1194/390625",
+  "logarithmic_cap": "611329/200000000",
+  "paid_profile": {
+    "1": 2201,
+    "2": 412,
+    "3": 510,
+    "4": 127,
+    "5": 40
+  },
+  "premises": [
+    "the 7752 inherited helper units are disjoint from the main roles and ABI compatible (not replayed here)",
+    "compiler applicability to this word (numerical instantiation only)",
+    "physical realizability of the rank-153 trace (no bank replay)",
+    "field-level bill admitted under the caller fixed-tape/precision ABI",
+    "inherited all-size/compiler, hosting, tape and analytic interfaces",
+    "kernel review"
+  ],
+  "record_only_overlay": {
+    "gates": 259,
+    "gates_by_kind": {
+      "BRIDGE": 108,
+      "FORWARD": 20,
+      "GAUGE_LOAD": 19,
+      "GAUGE_UNLOAD": 19,
+      "IDLE": 36,
+      "LETTER": 19,
+      "REVERSE": 19,
+      "SWAP": 19
+    },
+    "monomial_field_maps": 17248,
+    "owned_clears": 1232,
+    "recodings": 77,
+    "scalar_adds": 68992,
+    "status": "historical record, NOT the priced word"
+  },
+  "scope": "exact arithmetic for the word, the bill, the compiler and the ledger",
+  "status": "CLAIM_P19_UNCODED_WORD_SUPPLIER",
+  "uncoded_word": {
+    "ambient_rank": 153,
+    "denominators": [
+      1
+    ],
+    "gate_kinds": {
+      "BRIDGE": 108,
+      "FORWARD": 20,
+      "IDLE": 36,
+      "LETTER": 39,
+      "REVERSE": 19,
+      "SWAP": 19
+    },
+    "gates": 241,
+    "idle_rank": 198,
+    "outputs": [
+      [
+        1,
+        4
+      ],
+      [
+        2,
+        4
+      ],
+      [
+        3,
+        4
+      ],
+      [
+        4,
+        4
+      ],
+      [
+        5,
+        4
+      ],
+      [
+        6,
+        4
+      ],
+      [
+        7,
+        4
+      ],
+      [
+        8,
+        4
+      ],
+      [
+        9,
+        4
+      ],
+      [
+        19,
+        2
+      ]
+    ],
+    "p19_entries_checked": "none (operator-level certification)",
+    "physical_bank_replay": "not performed; ambient rank 153 exceeds a 512-address bank",
+    "retained_idles": 36,
+    "trace_identity": "replayed in the controller algebra"
+  }
+}
diff --git a/research/p19-current-head-binding-audit/source/pr5270/P19_LIFT.json b/research/p19-current-head-binding-audit/source/pr5270/P19_LIFT.json
new file mode 100644
index 0000000000..6b42f7266e
--- /dev/null
+++ b/research/p19-current-head-binding-audit/source/pr5270/P19_LIFT.json
@@ -0,0 +1,16 @@
+{
+  "addresses": 131072,
+  "blocks": 2,
+  "consequence": "any polynomial identity between the gate list and the controller matrix lifts to address operators for every block count k, so the p=19 word realises the p=19 matrix once the p=2 control confirms the implementation of Phi",
+  "control_status": "the p=2 address replay is randomised (one dense seed), not exhaustive",
+  "differing_entries": 0,
+  "gate_kinds_checked": [
+    "FORWARD",
+    "REVERSE",
+    "LETTER",
+    "IDLE"
+  ],
+  "lemma": "Phi is a homomorphism from the retained-stage monomial ring to address operators: distinct-axis Gaussians commute, powers on one axis add, Phi fixes the identity",
+  "status": "PASS_LIFTING_LEMMA",
+  "trials": 24
+}
diff --git a/research/p19-current-head-binding-audit/source/pr5270/P19_PLAIN.json b/research/p19-current-head-binding-audit/source/pr5270/P19_PLAIN.json
new file mode 100644
index 0000000000..f06e82ac51
--- /dev/null
+++ b/research/p19-current-head-binding-audit/source/pr5270/P19_PLAIN.json
@@ -0,0 +1,182 @@
+{
+  "p19": {
+    "ambient_rank": 153,
+    "denominators": [
+      1
+    ],
+    "gates": 241,
+    "idle_rank": 198,
+    "invoice_root": 0.007578535189897761,
+    "kinds": {
+      "BRIDGE": 108,
+      "FORWARD": 20,
+      "IDLE": 36,
+      "LETTER": 39,
+      "REVERSE": 19,
+      "SWAP": 19
+    },
+    "max_role": 37,
+    "monomial_field_maps": 0,
+    "note": "no code, so no recoding bill and no terminal-gauge decoder",
+    "outputs": [
+      [
+        1,
+        4
+      ],
+      [
+        2,
+        4
+      ],
+      [
+        3,
+        4
+      ],
+      [
+        4,
+        4
+      ],
+      [
+        5,
+        4
+      ],
+      [
+        6,
+        4
+      ],
+      [
+        7,
+        4
+      ],
+      [
+        8,
+        4
+      ],
+      [
+        9,
+        4
+      ],
+      [
+        19,
+        2
+      ]
+    ],
+    "owned_clears": 0,
+    "recodings": 0,
+    "retained_idles": 36,
+    "role_set": [
+      0,
+      1,
+      2,
+      3,
+      4,
+      5,
+      6,
+      7,
+      8,
+      9,
+      10,
+      11,
+      12,
+      13,
+      14,
+      15,
+      16,
+      17,
+      18,
+      19,
+      20,
+      21,
+      22,
+      23,
+      24,
+      25,
+      26,
+      27,
+      28,
+      29,
+      30,
+      31,
+      32,
+      33,
+      34,
+      35,
+      36,
+      37
+    ],
+    "scalar_adds": 0,
+    "terminal_gauge_decoder": 0,
+    "trace_identity": "replayed in the controller algebra"
+  },
+  "p2": {
+    "denominators": [
+      1
+    ],
+    "gates": 20,
+    "idle_rank": 3,
+    "kinds": {
+      "BRIDGE": 6,
+      "FORWARD": 3,
+      "IDLE": 2,
+      "LETTER": 5,
+      "REVERSE": 2,
+      "SWAP": 2
+    },
+    "max_role": 3,
+    "outputs": [
+      [
+        1,
+        2
+      ],
+      [
+        2,
+        2
+      ]
+    ],
+    "retained_idles": 2,
+    "role_set": [
+      0,
+      1,
+      2,
+      3
+    ],
+    "trace_identity": "replayed in the controller algebra"
+  },
+  "p3": {
+    "denominators": [
+      1
+    ],
+    "gates": 33,
+    "idle_rank": 6,
+    "kinds": {
+      "BRIDGE": 12,
+      "FORWARD": 4,
+      "IDLE": 4,
+      "LETTER": 7,
+      "REVERSE": 3,
+      "SWAP": 3
+    },
+    "max_role": 5,
+    "outputs": [
+      [
+        1,
+        4
+      ],
+      [
+        3,
+        2
+      ]
+    ],
+    "retained_idles": 4,
+    "role_set": [
+      0,
+      1,
+      2,
+      3,
+      4,
+      5
+    ],
+    "trace_identity": "replayed in the controller algebra"
+  },
+  "scope": "controller trace identity, p=2/3/19 diagonalisation, census and price; ambient rank 153 precludes a literal 512-address replay",
+  "status": "PASS_P19_UNCODED_WORD"
+}
diff --git a/research/p19-current-head-binding-audit/source/pr5270/README.md b/research/p19-current-head-binding-audit/source/pr5270/README.md
new file mode 100644
index 0000000000..066d9ded0f
--- /dev/null
+++ b/research/p19-current-head-binding-audit/source/pr5270/README.md
@@ -0,0 +1,152 @@
+# The p=19 word without the code: trace-certified word, exact price, kappa 0.0034
+
+**The p=19 controller word is emitted as the controller's own gate trace and
+re-priced. The invoice never sees the code — `invoice(p, pattern, thick, profile)`
+takes no coding argument — so the coded reverse was an overlay the endpoint does not
+need, and dropping it removes the terminal-gauge decoder that the coded words cannot
+pay for. Complex side 0.007578535, BIT supplier 0.0034, outer
+`kappa = 951999/280000000 = 0.0033999964`: **+12.58 %** over the selected repository
+record `60403/20000000 = 0.00302015` and **+12.31 %** over the maintainer-reported
+`0.00302728823` (reported in review; no certificate for it in this tree), with zero
+recodings and zero decoder.
+
+The endpoint is **conditional**: the 7,752 helper units are inherited rather than
+replayed, the compiler result is a numerical instantiation of the majorant under an
+applicability premise, and the word is certified as the controller's operator rather
+than by a physical bank replay.**
+
+## Why there is no code
+
+The retained native reverse call is atomic, `X ← D(X − QCY)`, `Y ← DY`
+(`coded-native-caller/PHYSICAL.md`), so its letter is `D` while `[C,D] ≠ 0` and
+`[C,Q] ≠ 0`. A role that carries the code through a stage therefore leaves the
+terminal gauge `Q⁻¹BᵢQ`, one `Q` decoder per owner per thick stage: **2,128 rank-1
+units at p=19**, against a root budget of **1,103 units** (this receipt computes both;
+1,104 extra rank-1 units drop the root to 0.0034). The alternative — code fewer
+stages — does not exist: every proper subset of coded pairs fails the
+diagonalisation at p=3, 4 and 5, so the code is all-or-nothing and always costs
+`112·p`.
+
+Nothing forces that overlay. `invoice()` prices a word by its rank census (the T
+targets and the D paid reads), and the census is independent of the coding, so the
+word without the code keeps the identical root 0.007578535 while its field bill
+collapses to zero recodings.
+
+## The word, without hand transcription
+
+A prior audit showed that a hand-written `standard()` reference can drift from the
+controller it is meant to mirror. This package therefore does not transcribe: the
+controller's own loop is re-executed with a gate log, and the log is replayed in the
+controller's monomial algebra. The replay must reproduce `controller()`'s matrix
+**exactly**, and the word must diagonalise.
+
+`p19_plain.py` checks, for p = 2, 3 and 19:
+
+- the trace identity: replayed trace == `controller(p, keep_of(p, pat), all-ones)`;
+- the diagonalisation: `diagonalize(p, pat, all-ones)` returns the standard outputs
+  with denominators `[1]`;
+- the census at p=19: 20 forward stages, 19 reverse stages, **39 stage letters** (the controller applies the stage gate at every stage 0..2p), 36 retained idle calls, 108 bridges and 19 closing swaps = **241 gates**, with zero recodings (the idles are the
+  controller's own, 198 rank across 396 role-rank).
+
+## The price and the paid accounting
+
+| item | value |
+|---|---|
+| invoice root | 0.007578535 (reproduced from the p16 published root) |
+| ambient target rank | 153 |
+| recodings / field maps / adds / clears | **0 / 0 / 0 / 0** |
+| terminal-gauge decoder | **0** |
+| guards at the endpoint | alpha 0.99579414, gamma 0.963763, delta 0.951561 |
+| compiler | shape-correct majorant: H0 = 5,170,423,668,736, H1 = 49,224,448,837,637,726,209 |
+| compiler premises | `20⁶⁴ < 21⁶³` ✓, `max target rank 153 < 256` ✓ |
+| BIT | atom 0.004 > ordinary 0.0034363538 > admitted 0.0034 |
+| ledger | 54 strict + 4 functional predicates positive at kappa; at exactly 0.0034 only `actual_bit_above_effective` fails |
+
+The compiler constants matter and were wrong in an earlier draft: the p7 pair
+(`h = 1/7`, `B = (4+7h)v`, `H0 ≥ 7v`) needs `10 < 2⁴` and `121 < 2⁷`, which fail here
+(`20 < 2⁴`, `153 < 2⁷` and `20⁷ < 21⁶` are all false). The constants used here are
+the ones `research/query-thinned-controllers/verify.py::tail` derives for exactly this
+complex shape (`h = 1/64`, `B = (5+8h)v`, `debt = 1 + 8v(1−z₀)`, `H0 ≥ 8v`).
+
+## What this package corrected
+
+- the code is unnecessary: the invoice is code-blind, so the coded overlay only adds
+  the decoder;
+- the compiler constants of the p7 unit do not apply to a unit that splits at 20,
+  completes at 21 and has ambient rank 153;
+- an idle call is `term(0, sel)`, a product of stage letters, so its physical form is a
+  Gaussian power and it needs no recoding;
+- the closing swap carries the −1 sign and must sit after any gauge unload.
+
+## Physical binding: the lifting lemma
+
+The p=19 word needs 2^153 addresses, so it cannot be replayed literally. The binding is
+therefore proved rather than sampled. The controller's word is a polynomial in the
+retained stage variables plus one central variable; give stage `s` its own eight-axis
+block and give the word one shared centre axis, and every monomial becomes an operator
+on 2^(8k+1) addresses. That map `Φ` is a **ring homomorphism**: distinct-axis Gaussians
+commute, powers on one axis add, and `Φ` fixes the identity. Hence any polynomial
+identity between the gate list and the controller matrix lifts to address operators for
+every block count `k`, and the p=19 word realises the p=19 controller matrix by
+construction (`p19_lift.py`, receipt `P19_LIFT.json`).
+
+The p=2 address replay (`p19_bank.py`) is then a **control on the implementation**, not
+the proof: two blocks plus the shared centre, 2^17 addresses per role, four roles, twenty
+gates, one dense seed. It is randomised, not exhaustive, and is labelled as such.
+
+The lemma also caught a real bug: the selection bits of a monomial are **exponents**,
+and an implementation that applies one gate per selected stage is not multiplicative once
+an exponent reaches 2 — which the p=19 word does constantly.
+
+## The tail limit is settled
+
+δ = 0.9515606085 and γ = 0.963763. The source tail argument uses its limits only through
+"each bound to the power 128 is below 1/16", and it closes at `L = 97/100`:
+`0.97¹²⁸ = 0.0202666 < 1/16`, `0.97¹⁰²⁴ < 2⁻³²`, then `1/(1+1024·10⁻⁹) + 4·2⁻³² < 1`.
+γ additionally meets the source's own tighter `31/32 = 0.96875`. So the `19/20` guard
+written into the source certificates is a stronger choice this word does not need, and
+the independent review on the earlier draft reached the same conclusion.
+
+## Inherited interfaces, and what is discharged here
+
+The word is new; the producer and the compiler are not. Every obligation is either
+discharged against this word or consumed from an inherited interface unchanged.
+
+| obligation | status |
+|---|---|
+| word realises the controller matrix | **discharged** — lifting lemma, plus the p=2 address control |
+| rank completion below `b^v` | **discharged** — this census has `max target rank 153 < 256` |
+| splitting at `c^v` | **discharged** — `20⁶⁴ < 21⁶³` |
+| whole-job normalizers | inherited; the word adds no job and consumes the same T/D interface |
+| distinct-owner child allocation | inherited; the word introduces no new owner |
+| rank-one surplus retention | inherited; the census is unchanged by the word |
+| helper fields disjoint from the word | **discharged mechanically** — the trace's roles are exactly `0…2p−1`, so no gate reads or writes helper-owned state |
+| 7,752 helper units materialised | **not built here**; inherited from PR4929 with its ownership and ABI |
+| field-bill admission under the caller ABI | inherited; the word's only paid operations are the inherited ones |
+| precision, tape, hosting, hosted CI, kernel review | inherited external obligations |
+
+## Open next questions
+
+- Can the block-decomposed replay be made exhaustive rather than randomised, e.g. by
+  comparing the two operators on a spanning set of the 2^17 address space?
+- Does one materialised helper stage-unit agree with the inherited profile, closing the
+  last helper obligation?
+- Is the endpoint's `0.97` tail limit worth pushing into the source package so later
+  words can cite it instead of re-deriving it?
+
+## Reproduce
+
+```sh
+python3 -B research/coded-reverse-word-p19/p19_plain.py     # trace identity, diagonalisation, price
+python3 -B research/coded-reverse-word-p19/p19_claim.py     # invoice, guards, compiler, BIT, budgets, ledger
+python3 -B research/coded-reverse-word-p19/verify.py        # fast receipt
+python3 -B research/coded-reverse-word-p19/p19_word.py      # the coded overlay, kept as a record
+```
+
+## Credit
+
+PR4940 coded reverse controller: Cayden Burkart / SethBurkart123. PR4933 signed
+physical code: Dillon. PR4929 center-free producer: Dugongue / mdumitrean. PR4433 and
+PR4359 compiler and outer ledger: retained with attribution. PR4470 controller and
+query thinning: Cinna Davis / 1337isnot1337. Retained lineage as credited in those
+packages.
diff --git a/research/p19-current-head-binding-audit/source/pr5270/VERIFY.json b/research/p19-current-head-binding-audit/source/pr5270/VERIFY.json
new file mode 100644
index 0000000000..ee9fc201a9
--- /dev/null
+++ b/research/p19-current-head-binding-audit/source/pr5270/VERIFY.json
@@ -0,0 +1,49 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/coded-reverse-controller/verify.py",
+    "research/coded-reverse-controller/README.md",
+    "research/coded-native-caller/CODE.json",
+    "research/coded-native-caller/NORMALIZERS.json",
+    "research/coded-native-caller/PHYSICAL.md",
+    "research/higher-moment-strictification/verify.py",
+    "research/kappa-rebuild/bit/complex_controller_factor.py",
+    "research/kappa-native-resume/causal-controller/sources/research/joint-query/certificate.json.gz",
+    "research/query-thinned-controllers/PROOF.md",
+    "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py",
+    "research/native-center-free-code/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "formal p=19 controller diagonalisation, the trace-certified word receipt and the claim receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/p19_claim.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "code and prefix bounds, raw moment sign in two engines, charged tail ratios, shape-correct compiler ranks, BIT admission, budgets and the strict outer ledger at the claimed kappa."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/p19_word.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "the coded overlay record: its 259-gate listing, replay and field bill."
+    }
+  ]
+}
diff --git a/research/p19-current-head-binding-audit/source/pr5270/p19_bank.py b/research/p19-current-head-binding-audit/source/pr5270/p19_bank.py
new file mode 100644
index 0000000000..164c3b6d41
--- /dev/null
+++ b/research/p19-current-head-binding-audit/source/pr5270/p19_bank.py
@@ -0,0 +1,143 @@
+#!/usr/bin/env python3
+"""Address-level replay of the trace word: the gate list against the controller matrix.
+
+The controller's monomials live over the retained stage variables.  Give every retained
+stage its own eight-axis block and give the word one shared centre line, and each
+monomial becomes a concrete Gaussian on 2**(8k+1) addresses.  The smallest faithful
+instance is p=2, where the retained stages are {1, 3}: two blocks plus the centre, so
+2**17 = 131,072 addresses per role.
+
+The check applies the trace's gate list to a dense state and compares it with the
+controller's own thinned matrix evaluated in the same representation.  This is the
+physical binding the earlier draft only asserted: if the two agree on every address of
+every role, the listed gates realise the controller's operator as concrete address
+operations, not merely as an equality of formal expressions.
+"""
+import importlib.util, json
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+P, IMAG = 65537, 256
+
+def need(ok, why):
+    if not ok: raise ValueError(why)
+
+def load(name, path):
+    spec = importlib.util.spec_from_file_location(name, path)
+    mod = importlib.util.module_from_spec(spec); spec.loader.exec_module(mod)
+    return mod
+
+def butterfly(state, axis, power=1):
+    """Apply the Gaussian gate to the given power on one axis, in one pass."""
+    ik = pow(IMAG, power, P)
+    a = (1+ik)*pow(2, -1, P) % P
+    b = (1-ik)*pow(2, -1, P) % P
+    step = 1 << axis
+    for st in range(0, len(state), 2*step):
+        for x in range(st, st+step):
+            u, v = state[x], state[x+step]
+            state[x] = (a*u+b*v) % P
+            state[x+step] = (b*u+a*v) % P
+
+def new_state(naddr, seed):
+    import random
+    rng = random.Random(seed)
+    return [rng.randrange(P) for _ in range(naddr)]
+
+def differ(x, y):
+    return sum(1 for a, b in zip(x, y) if a != b)
+
+def main():
+    mod = load('c4940', ROOT/'research/coded-reverse-controller/verify.py')
+    C, controller, keep_of, thin = mod.C, mod.controller, mod.keep_of, mod.thin
+
+    p, pat = 2, 'I'
+    thick = sorted(range(1, 2*p, 2))                 # retained stages
+    naddr = 1 << (8*len(thick)+1)
+    centre = 8*len(thick)
+    blocks = {s: i for i, s in enumerate(thick)}
+    def monomial_apply(state, key):
+        q, sel = key[0], key[1:]
+        if q: butterfly(state, centre, q)
+        for s, bit in enumerate(sel):
+            if bit and s in blocks:
+                base = 8*blocks[s]
+                for j in range(8): butterfly(state, base+j, bit)
+    need(naddr == 131072 and len(thick) == 2, 'p=2 realisation is 2^17 addresses')
+
+    keep = keep_of(p, pat)
+    co, _ = controller(p, keep, {s: 1 for s in range(2*p+1)})
+    matrix = thin(co, set(thick))
+    need(matrix, 'the thinned controller matrix is non-empty')
+    n = 2*p
+
+    # a) the trace's gate list, applied as concrete address operations
+    import p19_plain
+    _, _, gates, _ = p19_plain.traced_controller(C, p, keep, {s: 1 for s in range(2*p+1)})
+
+    base = [new_state(naddr, 100+i) for i in range(n)]
+    state = [s[:] for s in base]
+    for g in gates:
+        kind = g[0]
+        if kind == 'FORWARD':
+            _, stage, y, x, coef = g
+            src = state[x][:]
+            butterfly(src, centre, -1)
+            state[y] = [(a+coef*b) % P for a, b in zip(state[y], src)]
+        elif kind == 'REVERSE':
+            _, stage, y, x, coef = g
+            src = state[x][:]
+            butterfly(src, centre, 1)
+            state[y] = [(a+coef*b) % P for a, b in zip(state[y], src)]
+        elif kind == 'LETTER':
+            _, stage, x, y, _s = g
+            if stage in blocks:
+                for role in (x, y):
+                    for j in range(8): butterfly(state[role], 8*blocks[stage]+j)
+        elif kind == 'IDLE':
+            _, kindname, x, y, sel = g
+            for role in (x, y):
+                for s, bit in enumerate(sel):
+                    if bit and s in blocks:
+                        for j in range(8): butterfly(state[role], 8*blocks[s]+j)
+        elif kind == 'BRIDGE':
+            _, coef, d, s, _none = g
+            state[d] = [(a+coef*b) % P for a, b in zip(state[d], state[s])]
+        elif kind == 'SWAP':
+            _, _c, x, y, _n = g
+            hold = state[x]
+            state[x] = state[y]
+            state[y] = [(-v) % P for v in hold]
+        else:
+            raise ValueError('unknown gate ' + kind)
+
+    # b) the controller's own matrix, evaluated on the same addresses
+    # the thinned controller matrix is stored as term -> matrix
+    want = [[0]*naddr for _ in range(n)]
+    for j in range(n):
+        col = base[j]
+        for term, m in matrix.items():
+            for i in range(n):
+                coeff = m[i][j]
+                if not coeff: continue
+                img = col[:]
+                monomial_apply(img, term)
+                want[i] = [(a+int(coeff)*b) % P for a, b in zip(want[i], img)]
+
+    bad = [differ(state[i], want[i]) for i in range(n)]
+    print('address-level replay p=%d: %d addresses per role, %d roles, %d gates' % (p, naddr, n, len(gates)))
+    print('  gate list vs controller matrix, differing entries per role:', bad)
+    need(sum(bad) == 0, 'the gate list realises the controller matrix at address level')
+    receipt = {'status': 'PASS_ADDRESS_LEVEL_TRACE_REPLAY', 'p': p, 'pattern': pat,
+               'retained_stages': thick, 'addresses_per_role': naddr, 'roles': n,
+               'gates': len(gates), 'differing_entries': bad,
+               'binding': ('the trace gate list and the controller matrix agree on every address of every '
+                           'role at the smallest faithful ambient (two blocks plus the shared centre)'),
+               'scope': ('p=19 needs 2**153 addresses, so the address-level check is done at p=2 and the p=19 '
+                         'word is certified by the trace identity in the controller algebra')}
+    (HERE/'P19_BANK.json').write_text(json.dumps(receipt, indent=2, sort_keys=True)+'\n')
+    print(json.dumps({'status': receipt['status']}, sort_keys=True))
+
+if __name__ == '__main__':
+    main()
diff --git a/research/p19-current-head-binding-audit/source/pr5270/p19_claim.py b/research/p19-current-head-binding-audit/source/pr5270/p19_claim.py
new file mode 100644
index 0000000000..92ae6514e4
--- /dev/null
+++ b/research/p19-current-head-binding-audit/source/pr5270/p19_claim.py
@@ -0,0 +1,388 @@
+#!/usr/bin/env python3
+"""The p=19 uncoded word: trace identity, price, compiler, BIT chain and outer ledger.
+
+Chain:
+
+  1. the word is the controller's own gate trace, replayed in the controller algebra
+     and required to equal controller() exactly; at p=19 it is 241 gates and
+     diagonalises to the standard outputs with denominators [1] (p19_plain.py);
+  2. the invoice takes no coding argument, so the word carries NO code: the field
+     level bill is zero recodings, zero monomial field maps, zero scalar adds, zero
+     owned clears and zero terminal-gauge decoder;
+  3. the invoice prices the word at 0.007578535 with the PR4929 paid profile and
+     reproduces the published p16 root; the raw moment sign at the tested saving is
+     positive in exact interval arithmetic and in a 60-digit decimal control;
+  4. the shape-correct power majorant (the constants research/query-thinned-controllers
+     derives for a unit that splits at c = 20, completes at b = 21 with v = 1024)
+     gives H0 = 5,170,423,668,736 and H1 = 49,224,448,837,637,726,209.  This is a
+     numerical instantiation of the majorant, not an instantiation of every hypothesis
+     of the source compiler theorem, which remains an applicability premise;
+  5. the admitted ordinary BIT saving 0.0034 funds the endpoint;
+  6. the strict outer ledger passes at the endpoint and at exactly 0.0034 fails only
+     actual_bit_above_effective, so the endpoint is bit_saving - 5*gap.
+
+The coded overlay is retained under P19_WORD.json as a historical record.  It is not
+priced here: its terminal-gauge decoder costs 2,128 rank-1 units against a 1,103-unit
+root budget, which is why it was dropped.
+"""
+import importlib.util, json
+from collections import Counter
+from fractions import Fraction as Q
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+OWNERS, SIZE = 112, 512
+SELECTED_CERT = ROOT/'certificates/selected-result.json'
+FRONTIER = Q(json.loads(SELECTED_CERT.read_text())['kappa'])   # the selected repository record
+REPORTED_FRONTIER = Q(302728823, 100000000000)                  # 0.00302728823, maintainer-reported, no certificate here
+BIT_SAVING = Q(17, 5000)
+GAP = Q(1, 1400000000)
+KAPPA = Q(951999, 280000000)
+TESTED = Q(951999, 280000000) + 7*Q(1, 1400000000)
+H = {4: 28, 7: 7, 8: 47, 9: 326}
+P_NEW = {1: 2201, 2: 412, 3: 510, 4: 127, 5: 40}
+MAPS, ADDS, CLEARS = 224, 896, 16
+
+def need(ok, why):
+    if not ok: raise ValueError(why)
+
+def load(name, path):
+    spec = importlib.util.spec_from_file_location(name, path)
+    mod = importlib.util.module_from_spec(spec); spec.loader.exec_module(mod)
+    return mod
+
+def invoice(p, pat, thick, prof):
+    full = frozenset(range(2*p+1)); T, D = Counter(), Counter()
+    outs = [full, full]
+    for i, ch in enumerate(pat, 1):
+        outs += [frozenset(range(0, 2*i+1)) if ch == 'I' else frozenset(range(2*i, 2*p+1))]*2
+    for s in outs: T[1+8*len(s & thick)] += 112
+    for i, ch in enumerate(pat, 1):
+        if ch == 'I': D[8*len(frozenset(range(0, 2*i)) & thick)] += 224
+        else: D[8*len(frozenset(range(2*i+1, 2*p+1)) & thick)] += 224
+    for j in range(1, p): D[8*len(frozenset([2*j]) & thick)] += 224
+    for r, n in H.items(): T[r] += len(thick)*n
+    for r, n in prof.items(): D[r] += len(thick)*n
+    D[1] += 112*(2*p+1-len(thick))
+    T.pop(0, None); D.pop(0, None)
+    return T, D
+
+def ledger_failures(mod, kappa, certified, bit_saving=BIT_SAVING):
+    prm = {'kappa': kappa, 'tested_saving': certified, 'complex_uniform_saving': kappa+6*GAP,
+           'b': kappa+5*GAP, 'a': kappa+4*GAP, 'q': kappa+3*GAP, 'bit_saving': bit_saving,
+           'epsilon': 1-GAP, 'beta': 1-3*GAP, 'r0': GAP/10, 'stop': GAP, 'layout': GAP, 'd': GAP}
+    out = mod.ledger(prm)
+    out['functional_checks']['actual_new_BIT_stock_sublinear'] = prm['beta']*(1-Q(1, 250))
+    fails = [k for part in ('strict_checks', 'functional_checks') for k, x in out[part].items() if x <= 0]
+    if not prm['complex_uniform_saving'] < certified: fails.append('uniform_above_certified_complex')
+    if not prm['a'] < bit_saving: fails.append('effective_above_bit_saving')
+    return fails
+
+def shape_majorant(v, tested, uniform, cutoff, floor, max_rank):
+    """The compiler constants for THIS complex shape, not the p7 unit's.
+
+    research/query-thinned-controllers/verify.py::tail (lines 151-155) derives them for
+    c = 20, b = 21, v = 1024: h = 1/64, B = (5+8h)v, debt = 1 + 8v(1-z0), H0 >= 8v.
+    The p7 constants (h = 1/7, B = (4+7h)v, H0 >= 7v) come from 10 < 2^4 and 121 < 2^7 and
+    fail here: 20 < 2^4 is false, 153 < 2^7 is false, and 20^7 < 21^6 is false.
+    """
+    t, z, h = 1-tested, 1-uniform, Q(1, 64)
+    z0 = (t+z)/2
+    gap = z0-t
+    B, debt = (5+8*h)*v, 1+8*v*(1-z0)
+    ratio = (gap*B+debt)/(h*gap)
+    H0 = -((-ratio.numerator)//ratio.denominator)
+    ratio = H0*(1-z0)/(z-z0)
+    H1 = ratio.numerator//ratio.denominator+1
+    need(cutoff**64 < floor**63, 'ranks after completion and splitting')
+    need(max_rank < 256, 'raw ambient ranks below 256')
+    need(H0 >= 8*v and H0*h*gap >= gap*B+debt, 'effective integer compiler bound')
+    need((H0-1)*h*gap < gap*B+debt, 'previous threshold rejected')
+    need(H1*(z-z0) > H0*(1-z0) >= (H1-1)*(z-z0), 'strict winning uniform rank')
+    return H0, H1
+
+def main():
+    global L_phys, E_eng
+    E_eng = load('lifteng', HERE/'physical_gauge_lift.py')
+    receipt = json.loads((ROOT/'research/coded-native-caller/NORMALIZERS.json').read_text())
+    _modes = [[(i, s) for i, s in enumerate(c) if s] for c in [[int(v) for v in x] for x in receipt['mode_columns']]]
+    L_phys = lambda x, inv: E_eng.physical_code(x, receipt['ports'], _modes, inv)
+    cols = [[int(v) for v in c] for c in receipt['mode_columns']]
+    N = OWNERS
+
+    A = [[Q(int(i == j)) - Q(sum(cols[m][i]*cols[m][j] for m in range(len(cols))), 4) for j in range(N)]
+         for i in range(N)]
+    Ainv = [[Q(int(i == j)) + (A[i][j]-Q(int(i == j)))/13 for j in range(N)] for i in range(N)]
+    eye = [[Q(int(i == j)) for j in range(N)] for i in range(N)]
+    need([[sum(A[i][k]*Ainv[k][j] for k in range(N) if A[i][k]) for j in range(N)] for i in range(N)] == eye,
+         'A A^-1 = I')
+    need(all(Ainv[i][j] == eye[i][j] - Q(sum(cols[m][i]*cols[m][j] for m in range(len(cols))), 52)
+             for i in range(N) for j in range(N)), 'A^-1 = I - M M^T/52')
+    for rec in receipt['ports']:
+        seen, signs = set(), set()
+        for x in range(SIZE):
+            y, sg = E_eng.signed_map(rec, x)
+            seen.add(y); signs.add(sg)
+        need(len(seen) == SIZE and signs <= {1, -1}, 'port map is a signed address permutation')
+    bank = [[0]*SIZE for _ in range(OWNERS)]
+    for i in range(OWNERS): bank[i][7] = (i*13+7) % 65537 or 1
+    mixed = E_eng.scalar_code(bank, [[(i, s) for i, s in enumerate(c) if s] for c in cols])
+    need(all(v == 0 for i in range(OWNERS) for j, v in enumerate(mixed[i]) if j != 7),
+         'scalar program moves no address')
+    print('PASS rank-free: every port map is a signed address permutation and the scalar program moves no '
+          'address, so a recoding adds no Gaussian rank')
+    tmax = max(sum(abs(c) for c in col) for col in cols)
+    prefix = (1 + Q(4*tmax, 4), 1 + Q(4*tmax, 52))
+    need((tmax, prefix) == (56, (57, Q(69, 13))), 'published prefix bounds')
+    print('PASS code: A = I - M M^T/4, A^-1 = I + (A - I)/13 = I - M M^T/52, A A^-1 = I; '
+          'prefix bounds %d and %s, no recursive Gaussian child' % (prefix[0], prefix[1]))
+
+    plain = json.loads((HERE/'P19_PLAIN.json').read_text())
+    pw = plain['p19']
+    need(pw['outputs'] == [[1, 4], [2, 4], [3, 4], [4, 4], [5, 4], [6, 4], [7, 4], [8, 4], [9, 4], [19, 2]],
+         'p=19 diagonalisation outputs')
+    need(pw['denominators'] == [1] and pw['trace_identity'] == 'replayed in the controller algebra',
+         'trace identity and standard denominators')
+    need((pw['retained_idles'], pw['idle_rank']) == (36, 198), 'idle census')
+    need((pw['recodings'], pw['monomial_field_maps'], pw['scalar_adds'], pw['owned_clears'],
+          pw['terminal_gauge_decoder']) == (0, 0, 0, 0, 0), 'no recoding bill')
+    print('PASS word: the controller trace at p=19 gives %d gates %s, %d retained idles of rank %d, outputs %s '
+          'with denominators %s, and no recoding bill'
+          % (pw['gates'], pw['kinds'], pw['retained_idles'], pw['idle_rank'], pw['outputs'], pw['denominators']))
+    word = json.loads((HERE/'P19_WORD.json').read_text())
+    if isinstance(word, list): word = word[0]
+    need(word['gate_records'] == 259 and word['recodings'] == 77, 'the coded overlay record is intact')
+    print('RECORDED: the coded overlay (%d gates, %d recodings) is kept for reference only; it is not priced here'
+          % (word['gate_records'], word['recodings']))
+
+    p, pat = 19, 'I'*9+'T'*9
+    thick = frozenset(range(1, 2*p, 2))
+    T, Dp = invoice(p, pat, thick, P_NEW)
+    E = load('moment', ROOT/'research/higher-moment-strictification/verify.py')
+    t = 1-TESTED
+    mt, mp = E.moment(T, t), E.moment(Dp, t)
+    need(mt[0] > mp[1], 'raw moment sign at the tested saving')
+    lim_a, lim_g, lim_d = 1-Q(1, 10**9), Q(97, 100), Q(97, 100)
+    tk = 1-KAPPA
+    mtk = E.moment(T, tk)
+    alpha = E.divide(E.moment(Dp, tk), mtk)
+    gamma = E.divide(E.moment(Dp, tk+Q(1, 5)), E.mul(E.power(20, Q(1, 5)), mtk))
+    delta = E.divide((Q(sum(T.values())*21),)*2, E.mul(E.power(20, KAPPA), mtk))
+    need(alpha[1] < lim_a and gamma[1] < lim_g and delta[1] < lim_d, 'charged tail ratios at the endpoint')
+    need(lim_g**128 < Q(1, 16) and lim_d**128 < Q(1, 16), 'decay blocks')
+    need(1/(1+1024*Q(1, 10**9)) + Q(4, 2**32) < 1, 'power-1024 tails')
+    print('PASS invoice: raw moment sign positive at %s; at kappa the ratios are alpha %.8f, gamma %.6f, '
+          'delta %.6f with both decay blocks under 1/16' % (TESTED, float(alpha[1]), float(gamma[1]), float(delta[1])))
+
+    from decimal import Decimal, getcontext
+    getcontext().prec = 60
+    def dmoment(profile, c):
+        total = Decimal(0)
+        e = Decimal(1) - Decimal(c.numerator)/Decimal(c.denominator)
+        for r, n in profile.items():
+            total += Decimal(n)*((Decimal(r).ln()*e).exp())
+        return total
+    need((TESTED-KAPPA)/7 == GAP and GAP.numerator == 1, 'integer compiler grid')
+    gap_at = dmoment(T, TESTED) - dmoment(Dp, TESTED)
+    gap_below = dmoment(T, TESTED-Q(1, 10**3)) - dmoment(Dp, TESTED-Q(1, 10**3))
+    gap_above = dmoment(T, TESTED+Q(5, 10**3)) - dmoment(Dp, TESTED+Q(5, 10**3))
+    need(gap_at > 0 and gap_below > 0 and gap_above < 0, 'independent decimal sign check')
+    print('PASS independent decimal engine (60 digits): signed moment +%s at the tested saving, '
+          '+%s a step below, %s a step above' % (('%.6e' % gap_at), ('%.6e' % gap_below), ('%.6e' % gap_above)))
+
+    H0, H1 = shape_majorant(1024, TESTED, KAPPA+6*GAP, 20, 21, max(T))
+    print('PASS compiler: shape-correct majorant (h = 1/64, B = (5+8h)v, H0 >= 8v) at v=1024 gives '
+          'H0 = %d, H1 = %d, N = 2^%d' % (H0, H1, H1))
+
+    C1, a_old, atom = Q(345, 100000), Q(384599, 10000000000), Q(4, 1000)
+    ordinary = (1-atom)*C1 + atom*a_old
+    need(atom == Q(4, 1000) and atom > ordinary > BIT_SAVING and atom < 1-ordinary,
+         'admitted ordinary BIT saving')
+    print('PASS BIT: atom %.3f > ordinary saving %.10f > admitted cap 0.0034' % (float(atom), float(ordinary)))
+
+    mod = load('ledger', ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py')
+    need(ledger_failures(mod, KAPPA, TESTED) == [], 'ledger passes at the endpoint')
+    need(ledger_failures(mod, Q(34, 10000), Q(34, 10000)+7*GAP) == ['actual_bit_above_effective', 'effective_above_bit_saving'],
+         'at 0.0034 only the BIT side binds')
+    need(ledger_failures(mod, KAPPA, TESTED, bit_saving=Q(27, 10000)) != [], 'old BIT saving rejected')
+    print('PASS ledger: all predicates pass at kappa=%s; at exactly 0.0034 only the BIT predicate fails' % KAPPA)
+
+    local_scalar, adapters, charts = 158168, 2*408, 688
+    local_routes = (sum(P_NEW.values()) + adapters + charts)*1000
+    need(local_routes + local_scalar < 10**7, 'local scalar and route allowance')
+    raw = 19*10**7 + 16*1792 + 32*112*(word['gate_records'] + 2)
+    field_records = (pw['monomial_field_maps'] + 448 + 448)*1000
+    need(raw < 10**9 and raw + field_records < 10**9, 'raw nonrecursive bound with the field bill')
+    need(local_routes + field_records < 10**7, 'with no recoding bill the local allowance holds')
+    print('PASS budgets: local routes %d + local scalar %d < 10^7; raw %d + field bill %d = %d < 10^9, '
+          'so with no recoding bill the local allowance now holds'
+          % (local_routes, local_scalar, raw, field_records, raw+field_records))
+
+    need(ledger_failures(mod, Q(3401, 1000000), Q(3401, 1000000)+7*GAP) != [], 'kappa above the BIT cap rejected')
+    need(ledger_failures(mod, KAPPA, KAPPA+4*GAP) != [], 'unfunded uniform bracket rejected')
+    rng = __import__('random').Random(3)
+    C = lambda x: L_phys(x, False)
+    Ci = lambda x: L_phys(x, True)
+    Dg = lambda x, inv=False: E_eng.gaussian(x, range(1, 9), inv)
+    Rg = lambda x, inv=False: E_eng.gaussian(x, range(9), inv)
+    dense = [[rng.randrange(65537) for _ in range(SIZE)] for _ in range(OWNERS)]
+    need(E_eng.diff(Dg(C(dense)), C(Dg(dense))) != 0, 'rank-8 letter does not commute with the code')
+    need(E_eng.diff(Rg(C(dense)), C(Rg(dense))) == 0, 'full Gaussian letter commutes')
+    print('PASS controls: kappa above the BIT cap, an unfunded uniform bracket, and the rank-8 letter are rejected')
+
+    # Why the shape-correct constants and not the p7 pair: the p7 proof's premises are
+    # 10 < 2^4 (split at 10^v) and 121 < 2^7 (ambient 121^v) with theta < 6/7.  This unit
+    # splits at 20, completes at 21 and has ambient rank 153, so all three fail.
+    need(not (20 < 2**4) and not (153 < 2**7) and not (20**7 < 21**6),
+         'the p7 premises genuinely fail for this shape')
+    A = E.power(153, TESTED)
+    Pw = A
+    for _ in range(10): Pw = E.mul(Pw, Pw)
+    eta = E.divide((1-TESTED, 1-TESTED), Pw)
+    lo, hi = 3000000, 4000000
+    while hi - lo > 1:
+        mid = (lo+hi)//2
+        t2 = mid*Q(1, 10**9)
+        A2 = E.power(153, t2); P2 = A2
+        for _ in range(10): P2 = E.mul(P2, P2)
+        if E.divide((1-t2, 1-t2), P2)[0] > (Q(63, 64))**1000: lo = mid
+        else: hi = mid
+    log_cap = lo*Q(1, 10**9)
+    need(log_cap < TESTED, 'the logarithmic cap lies below the tested saving, so it cannot be the majorant here')
+    print('PASS compiler: shape-correct majorant (query-thinned-controllers::tail constants) gives '
+          'H0 = %d, H1 = %d' % (H0, H1))
+    print('RECORDED: the p7 constants do not apply here (20 < 2^4 false, 153 < 2^7 false, 20^7 < 21^6 false), '
+          'and the logarithmic majorant at ambient rank 153 caps the tested saving at %s (eta = %s below '
+          '(63/64)^1000)' % (log_cap, E.display((eta[0]-((Q(63,64))**1000), eta[1]-((Q(63,64))**1000)))))
+    need(delta[1] < Q(97, 100), 'the 0.97 delta limit holds')
+    kappa_logmax = log_cap - 7*GAP
+    # ---- discharging the three premises at the source's own level ----
+    # H: the tail lemma, source structure, with the weaker but sufficient 0.97 limit.
+    LIM = Q(97, 100)
+    need(gamma[1] < LIM and delta[1] < LIM, 'gamma and delta under the 0.97 limit')
+    need(LIM**128 < Q(1, 16), '0.97^128 < 1/16')
+    need(LIM**1024 < (Q(1, 16))**8, 'block bound at power 1024, i.e. below 2^-32')
+    need(Q(4)*LIM**1024 < Q(4, 2**32), 'four block failures below 4*2^-32')
+    alpha_gap = Q(1, 10**9)
+    need(alpha[1] < 1-alpha_gap, 'alpha under the Bernoulli gap')
+    need(1/(1+1024*alpha_gap) + Q(4)*LIM**1024 < 1, 'tail assembly at power 1024')
+    print('DISCHARGED tail limit: with L = 97/100, L^128 < 1/16, L^1024 < 2^-32, and '
+          '1/(1+1024e-9) + 4*L^1024 < 1, so the source tail argument closes at the weaker limit; '
+          '19/20 is a stronger unused choice')
+
+    # F: the majorant's hypotheses are the unit's rank data, which the invoice census supplies.
+    saved_H = dict(H)
+    for r in list(H): del H[r]
+    T_roles, _ = invoice(p, pat, thick, P_NEW)
+    H.update(saved_H)
+    helper_mass = Counter(T); helper_mass.subtract(T_roles)
+    need(+helper_mass == Counter({r: len(thick)*n for r, n in H.items()}),
+         'helper T mass is additive and separate from the role mass')
+    need(sum(T.values()) == 12008, 'productive census')
+    print('DISCHARGED compiler choice: the constants come from the pinned shape-correct derivation '
+          '(query-thinned-controllers::tail) applied to this unit\'s ranks and completion bases, not from the p7 '
+          'unit; the logarithmic route is not used and its cap %s is recorded above' % log_cap)
+
+    # D: the helper block is autonomous with independent fields, so the main-role gauge cannot touch it.
+    print('INHERITED helper materialisation: the 7752 units (19*{4:28,7:7,8:47,9:326}) are priced on the T side '
+          'and not rebuilt here; what this package discharges is compatibility, below')
+
+    # ---- the lifting lemma: the word's block realisation is a ring homomorphism ----
+    lift = json.loads((HERE/'P19_LIFT.json').read_text())
+    need(lift['status'] == 'PASS_LIFTING_LEMMA' and lift['differing_entries'] == 0, 'lifting lemma receipt')
+    need(lift['control_status'].startswith('the p=2 address replay is randomised'),
+         'the address replay is labelled a randomised control')
+    print('PASS lifting lemma: Phi is multiplicative on the monomial ring (%d sampled pairs, 0 differing entries), '
+          'so any polynomial identity between the gate list and the controller matrix lifts to address operators '
+          'for every block count; the p=2 replay is a randomised control on the implementation'
+          % lift['trials'])
+
+    # ---- helper compatibility, the mechanical half ----
+    need(pw['max_role'] == 37 and pw['role_set'] == list(range(38)),
+         'the trace touches exactly the main roles 0..2p-1 and no helper index')
+    print('PASS helper compatibility (mechanical): the trace\'s roles are exactly 0..37 (2p-1), so no gate reads '
+          'or writes helper-owned state; the 7752 inherited helper units remain a separate T block')
+
+    # ---- the controller's retained idle calls, now materialized in the listing ----
+    pp, patq = 19, 'I'*9+'T'*9
+    init = [((st+1)//2, st+1) for st in range(1, 2*pp) if st % 2 and st <= 2*pp-3]
+    mid = [(1,) for st in range(1, 2*pp) if st % 2 == 0 and 2 <= st <= 2*pp-2]
+    term = [(j, 2*pp+1-(2*j+3)) for j in range(pp-1)]
+    keep_i = [r for pr, r in init if patq[pr-1] in 'IB']
+    keep_t = [r for j, r in term if patq[j] in 'TB']
+    idle_n = len(keep_i)+len(mid)+len(keep_t)
+    idle_rank = sum(keep_i)+len(mid)*1+sum(keep_t)
+    need((len(keep_i), len(mid), len(keep_t)) == (9, 18, 9), 'idle census matches the controller run')
+    need(idle_n == 36 and idle_rank == 198, 'idle rank total')
+    need(pw['retained_idles'] == idle_n and pw['idle_rank'] == idle_rank,
+         'the word carries every retained idle')
+    print('IDLES IN THE WORD: %d retained idle calls (9 initial rank %d, 18 middle rank 18, 9 terminal rank %d) '
+          'apply %d rank across %d role-rank to main roles; the word carries no code, so they need no recoding '
+          'and the field bill is zero' % (idle_n, sum(keep_i), sum(keep_t), idle_rank, 2*idle_rank))
+
+    need(KAPPA > FRONTIER, 'claim above the frontier')
+    claim = {'status': 'CLAIM_P19_UNCODED_WORD_SUPPLIER',
+             'kappa': str(KAPPA), 'kappa_decimal': float(KAPPA),
+             'complex_supplier': '0.007578535', 'bit_supplier': '17/5000',
+             'kappa_under_logarithmic_majorant': str(kappa_logmax), 'logarithmic_cap': str(log_cap),
+             'frontier_selected_record': str(FRONTIER),
+             'gain_vs_selected_record_percent': round(100*(float(KAPPA)/float(FRONTIER)-1), 3),
+             'frontier_reported': str(REPORTED_FRONTIER),
+             'frontier_reported_provenance': 'maintainer-reported in review; no certificate in this tree',
+             'gain_vs_reported_percent': round(100*(float(KAPPA)/float(REPORTED_FRONTIER)-1), 3),
+             'complex_saving': float(Q(7578535, 1000000))/1000,
+             'uncoded_word': {'gates': pw['gates'], 'gate_kinds': pw['kinds'],
+                              'retained_idles': pw['retained_idles'], 'idle_rank': pw['idle_rank'],
+                              'outputs': pw['outputs'], 'denominators': pw['denominators'],
+                              'trace_identity': pw['trace_identity'], 'ambient_rank': pw['ambient_rank'],
+                              'physical_bank_replay': 'not performed; ambient rank 153 exceeds a 512-address bank',
+                              'p19_entries_checked': 'none (operator-level certification)'},
+             'field_level_bill': {'recodings': pw['recodings'],
+                                  'monomial_field_maps': pw['monomial_field_maps'],
+                                  'scalar_adds': pw['scalar_adds'], 'owned_clears': pw['owned_clears'],
+                                  'terminal_gauge_decoder': pw['terminal_gauge_decoder'],
+                                  'recursive_gaussian_children': 0},
+             'record_only_overlay': {'gates': word['gate_records'], 'gates_by_kind': word['gate_kinds'],
+                                     'recodings': word['recodings'],
+                                     'monomial_field_maps': word['monomial_field_maps'],
+                                     'scalar_adds': word['scalar_adds'], 'owned_clears': word['owned_clears'],
+                                     'status': 'historical record, NOT the priced word'},
+             'paid_profile': P_NEW, 'helper_profile': H,
+             'guards': {'alpha': float(alpha[1]), 'gamma': float(gamma[1]), 'delta': float(delta[1])},
+             'compiler_obligations': {
+                 'rank completion below b^v': 'checked on this census: max target rank 153 < 256',
+                 'splitting at c^v': 'checked on this census: 20^64 < 21^63',
+                 'whole-job normalizers': 'inherited from the producer; the word adds no job and consumes the same T/D interface',
+                 'distinct-owner child allocation': 'inherited; the word introduces no new owner',
+                 'rank-one surplus retention': 'inherited; the census is unchanged by the word'},
+             'compiler': {'majorant': 'shape-correct power majorant (query-thinned-controllers constants)',
+                          'v': 1024, 'h': '1/64', 'B': '(5+8h)v', 'H0_check': 'H0 >= 8v',
+                          'H0': H0, 'H1': H1, 'N': '2^%d' % H1,
+                          'classification': 'numerical instantiation under an applicability premise, not a proof',
+                          'uninstantiated_hypotheses': [
+                              'rank completion below b^v', 'job splitting at c^v',
+                              'whole-job normalizers', 'distinct-owner child allocation',
+                              'rank-one surplus retention', 'fresh-block replay of the trace']},
+             'admitted_bit_saving': str(BIT_SAVING),
+             'budgets': {'local_routes': local_routes, 'local_scalar': local_scalar,
+                         'local_allowance': 10**7, 'raw_bound': raw, 'field_bill_records': field_records,
+                         'raw_allowance': 10**9, 'field_bill_bucket': 'raw'}, 
+             'idles': {'retained': idle_n, 'initial': len(keep_i), 'middle': len(mid),
+                       'terminal': len(keep_t), 'rank_applied': idle_rank, 'role_rank': 2*idle_rank,
+                       'gauge_neutral': True},
+             'premises': ['the 7752 inherited helper units are disjoint from the main roles and ABI compatible (not replayed here)',
+                          'compiler applicability to this word (numerical instantiation only)',
+                          'physical realizability of the rank-153 trace (no bank replay)',
+                          'field-level bill admitted under the caller fixed-tape/precision ABI',
+                          'inherited all-size/compiler, hosting, tape and analytic interfaces',
+                          'kernel review'],
+             'scope': 'exact arithmetic for the word, the bill, the compiler and the ledger'}
+    (HERE/'P19_CLAIM.json').write_text(json.dumps(claim, indent=2, sort_keys=True)+'\n')
+    print('CLAIM kappa %s = %.10f: +%.2f%% over the selected record %s, +%.2f%% over the reported frontier %s; '
+          'complex supplier 0.007578535, BIT supplier 0.0034, zero field bill'
+          % (KAPPA, float(KAPPA), claim['gain_vs_selected_record_percent'], FRONTIER,
+             claim['gain_vs_reported_percent'], REPORTED_FRONTIER))
+
+if __name__ == '__main__':
+    main()
diff --git a/research/p19-current-head-binding-audit/source/pr5270/p19_lift.py b/research/p19-current-head-binding-audit/source/pr5270/p19_lift.py
new file mode 100644
index 0000000000..2a1aa4c498
--- /dev/null
+++ b/research/p19-current-head-binding-audit/source/pr5270/p19_lift.py
@@ -0,0 +1,145 @@
+#!/usr/bin/env python3
+"""Lifting lemma: the block realisation of the controller's monomial ring is a homomorphism.
+
+The controller's word is a polynomial in the retained stage variables plus one central
+variable.  Give stage s its own eight-axis block and give the word one shared centre
+axis, and every monomial becomes a concrete operator on 2**(8k+1) addresses.  Call that
+map Phi.
+
+If Phi is a ring homomorphism on monomials, then any polynomial identity between the
+gate list and the controller matrix lifts to the address operators for every k, because
+Phi respects addition, scalar multiplication and multiplication.  The three facts Phi
+needs are checked here:
+
+  (a) distinct blocks and the centre act on disjoint axes, so their Gaussians commute;
+  (b) powers on one axis add, so Phi(m1 m2) has the exponent sums Phi(m1) and Phi(m2) share;
+  (c) the word's gate kinds are exactly the Phi-images of the controller's elementary
+      monomial operations, so the composed gate list is Phi of the composed matrix.
+
+The p=2 address replay (p19_bank.py) is then a control on the implementation rather than
+the proof, and it is randomised, not exhaustive: this receipt says so.
+"""
+import importlib.util, json, random
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+P, IMAG = 65537, 256
+
+def need(ok, why):
+    if not ok: raise ValueError(why)
+
+def butterfly(state, axis, power=1):
+    ik = pow(IMAG, power, P)
+    a = (1+ik)*pow(2, -1, P) % P
+    b = (1-ik)*pow(2, -1, P) % P
+    step = 1 << axis
+    for st in range(0, len(state), 2*step):
+        for x in range(st, st+step):
+            u, v = state[x], state[x+step]
+            state[x] = (a*u+b*v) % P
+            state[x+step] = (b*u+a*v) % P
+
+class Blocks:
+    def __init__(self, k):
+        self.k = k
+        self.centre = 8*k
+        self.naddr = 1 << (8*k+1)
+    def apply(self, state, key):
+        q, sel = key[0], key[1:]
+        if q: butterfly(state, self.centre, q)
+        for s, bit in enumerate(sel):
+            if bit and s < self.k:
+                for j in range(8): butterfly(state, 8*s+j, bit)
+
+def mul(k1, k2):
+    return (k1[0]+k2[0],)+tuple(a+b for a, b in zip(k1[1:], k2[1:]))
+
+def main():
+    rng = random.Random(7)
+    k = 2                                     # the smallest faithful instance: 2 blocks + centre
+    B = Blocks(k)
+    need(B.naddr == 131072, '2^17 addresses')
+    trials, differs = 24, []
+
+    def dense():
+        return [rng.randrange(P) for _ in range(B.naddr)]
+
+    # (a) commutation of distinct-axis Gaussians, and (b) powers adding on one axis
+    v = dense()
+    for axis_pair in ((0, 1), (3, B.centre), (7, 9)):
+        x, y = v[:], v[:]
+        butterfly(x, axis_pair[0]); butterfly(x, axis_pair[1])
+        butterfly(y, axis_pair[1]); butterfly(y, axis_pair[0])
+        need(x == y, 'distinct-axis Gaussians commute')
+    x, y = v[:], v[:]
+    butterfly(x, 5, 1); butterfly(x, 5, 2)
+    butterfly(y, 5, 3)
+    need(x == y, 'powers on one axis add')
+    print('PASS (a) distinct-axis Gaussians commute; (b) powers on one axis add')
+
+    # (c) multiplicativity of Phi on the monomial ring
+    for _ in range(trials):
+        k1 = (rng.choice([-1, 0, 1, 2]),)+tuple(rng.randrange(2) for _ in range(2*k+1))
+        k2 = (rng.choice([-1, 0, 1, 2]),)+tuple(rng.randrange(2) for _ in range(2*k+1))
+        prod = mul(k1, k2)
+        v0 = dense()
+        x, y = v0[:], v0[:]
+        B.apply(x, prod)
+        B.apply(y, k1); B.apply(y, k2)
+        differs.append(sum(1 for a, b in zip(x, y) if a != b))
+    need(sum(differs) == 0, 'Phi is multiplicative for every sampled monomial pair')
+    print('PASS (c) Phi(m1 m2) == Phi(m1) Phi(m2) on %d sampled monomial pairs, 0 differing entries' % trials)
+
+    # additivity and scalar step, on the same space
+    x = dense(); y = dense()
+    z = [(a+b) % P for a, b in zip(x, y)]
+    B.apply(z, (0,)+tuple(0 for _ in range(2*k+1)))
+    need(z == [(a+b) % P for a, b in zip(x, y)], 'Phi fixes the empty monomial')
+    print('PASS Phi(1) is the identity, so addition and scalars pass through Phi')
+
+    # (d) every gate kind is Phi of its monomial, checked one gate at a time
+    zero_key = (0,)+tuple(0 for _ in range(2*k+1))
+    centre_key = (1,)+tuple(0 for _ in range(2*k+1))
+    stage_key = lambda s: (0,)+tuple(1 if i == s else 0 for i in range(2*k+1))
+    v = dense(); w = v[:]
+    # FORWARD / REVERSE read: y += coef * Phi(centre^{+-1}) x
+    for coef, q in ((-1, 1), (1, -1)):
+        x, y = dense(), dense()
+        src = x[:]; butterfly(src, B.centre, q)
+        want = [(a+coef*b) % P for a, b in zip(y, src)]
+        got = y[:]
+        tmp = x[:]; B.apply(tmp, (q,)+tuple(0 for _ in range(2*k+1)))
+        got = [(a+coef*b) % P for a, b in zip(got, tmp)]
+        need(want == got, 'the forward/reverse read is Phi of the central monomial')
+    # LETTER and IDLE: role <- Phi(stage) role and Phi(product) role
+    for key in (stage_key(0), stage_key(1), (0,)+tuple(1 for _ in range(2*k+1))):
+        x = dense()
+        want = x[:]; B.apply(want, key)
+        got = x[:]
+        q, sel = key[0], key[1:]
+        if q: butterfly(got, B.centre, q)
+        for s, bit in enumerate(sel):
+            if bit and s < k:
+                for j in range(8): butterfly(got, 8*s+j, bit)
+        need(want == got, 'the letter and idle multiplications are Phi of their monomials')
+    # BRIDGE and SWAP are linear combinations and a signed swap, independent of Phi
+    x, y = dense(), dense()
+    need([(a+3*b) % P for a, b in zip(x, y)] != [], 'bridge is a linear combination')
+    print('PASS (d) every gate kind is the Phi-image of its monomial (reads, letters, idles); '
+          'bridges and swaps are linear and signed, independent of Phi')
+
+    receipt = {'status': 'PASS_LIFTING_LEMMA', 'blocks': k, 'addresses': B.naddr,
+               'trials': trials, 'differing_entries': sum(differs),
+               'lemma': ('Phi is a homomorphism from the retained-stage monomial ring to address operators: '
+                         'distinct-axis Gaussians commute, powers on one axis add, Phi fixes the identity'),
+               'gate_kinds_checked': ['FORWARD', 'REVERSE', 'LETTER', 'IDLE'],
+               'consequence': ('any polynomial identity between the gate list and the controller matrix lifts to '
+                               'address operators for every block count k, so the p=19 word realises the p=19 '
+                               'matrix once the p=2 control confirms the implementation of Phi'),
+               'control_status': 'the p=2 address replay is randomised (one dense seed), not exhaustive'}
+    (HERE/'P19_LIFT.json').write_text(json.dumps(receipt, indent=2, sort_keys=True)+'\n')
+    print(json.dumps({'status': receipt['status']}, sort_keys=True))
+
+if __name__ == '__main__':
+    main()
diff --git a/research/p19-current-head-binding-audit/source/pr5270/p19_plain.py b/research/p19-current-head-binding-audit/source/pr5270/p19_plain.py
new file mode 100644
index 0000000000..b060f5a8fc
--- /dev/null
+++ b/research/p19-current-head-binding-audit/source/pr5270/p19_plain.py
@@ -0,0 +1,158 @@
+#!/usr/bin/env python3
+"""The uncoded p=19 controller word: trace, diagonalisation, census and price.
+
+The invoice prices a word by its rank census, and the census never sees the code:
+``invoice(p, pattern, thick, profile)`` takes no coding argument.  The coded reverse
+was therefore an overlay the endpoint does not need, and it is the overlay that costs
+the terminal-gauge decoder (one Q per owner per thick stage = 2128 rank-1 units
+against a 1103-unit root budget).  This receipt builds the word without it.
+
+The word is not transcribed by hand: the controller loop is re-executed with a log of
+every role update, the log is replayed in the controller's own monomial algebra, and
+the replay must reproduce the controller's matrix exactly.  A hand transcription is
+what a prior audit showed can drift (#5349); an instrumented trace cannot.
+
+Scope: the trace identity, the p=19 diagonalisation, the census and the price.  The
+ambient rank of this word is 153, so a literal 512-address replay cannot host it; the
+local physical identities stay with the companion package.
+"""
+import importlib.util, json
+from collections import Counter
+from fractions import Fraction as Q
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+H = {4: 28, 7: 7, 8: 47, 9: 326}
+PROF = {1: 2201, 2: 412, 3: 510, 4: 127, 5: 40}
+
+def need(ok, why):
+    if not ok: raise ValueError(why)
+
+def load(name, path):
+    spec = importlib.util.spec_from_file_location(name, path)
+    mod = importlib.util.module_from_spec(spec); spec.loader.exec_module(mod)
+    return mod
+
+def traced_controller(C, p, keep, coupling):
+    """The controller's own loop, emitting the gate sequence as it goes."""
+    n, stages = 2*p, 2*p+1
+    zero = (0,)*(stages+1)
+    matrix = [[{zero: 1} if i == j else {} for j in range(n)] for i in range(n)]
+    gates, idle = [], []
+    term = lambda q, sel: (q,)+tuple(int(s in sel) for s in range(stages))
+    def idle_call(pair, sel, kind):
+        retained = bool(keep >> len(idle) & 1)
+        idle.append(dict(kind=kind, pair=pair, retained=retained, sel=list(sel)))
+        if retained:
+            for role in (2*pair, 2*pair+1):
+                matrix[role] = [C.monomial_times(x, term(0, sel)) for x in matrix[role]]
+            gates.append(('IDLE', kind, 2*pair, 2*pair+1, tuple(sel)))
+    def local(stage, pair, reverse):
+        x, y = 2*pair, 2*pair+1
+        if reverse: x, y = y, x
+        coef = (-1 if reverse else 1)*coupling[stage]
+        matrix[y] = [C.plus(a, C.monomial_times(b, term(1 if reverse else -1, []), coef)) for a, b in zip(matrix[y], matrix[x])]
+        gates.append(('REVERSE' if reverse else 'FORWARD', stage, y, x, coef))
+        for role in (x, y): matrix[role] = [C.monomial_times(z, term(0, [stage])) for z in matrix[role]]
+        gates.append(('LETTER', stage, x, y, stage))
+        if stage % 2 and stage <= 2*p-3: idle_call((stage+1)//2, list(range(stage+1)), 'initial')
+        elif stage % 2 == 0 and 2 <= stage <= 2*p-2: idle_call(stage//2, [stage], 'middle')
+        elif stage == 2*p:
+            for j in range(p-1): idle_call(j, list(range(2*j+3, 2*p+1)), 'terminal')
+    def bridge(dst, src, c):
+        for d, s, cc in ((2*dst, 2*src, c), (2*src+1, 2*dst+1, -c)):
+            matrix[d] = [C.plus(a, b, cc) for a, b in zip(matrix[d], matrix[s])]
+            gates.append(('BRIDGE', cc, d, s, None))
+    local(0, 0, False)
+    for j in range(p):
+        local(2*j+1, j, True)
+        if j < p-1: bridge(j, j+1, 1)
+        local(2*j+2, j, False)
+        if j < p-1: bridge(j, j+1, -1)
+    for j in reversed(range(p-1)): bridge(j+1, j, 1)
+    for j in range(p):
+        matrix[2*j], matrix[2*j+1] = matrix[2*j+1], [C.monomial_times(x, zero, -1) for x in matrix[2*j]]
+        gates.append(('SWAP', -1, 2*j, 2*j+1, None))
+    co = {}
+    for i, row in enumerate(matrix):
+        for j, poly in enumerate(row):
+            for key, v in poly.items(): co.setdefault(key, [[Q(0)]*n for _ in range(n)])[i][j] += v
+    return matrix, {k: m for k, m in co.items() if any(any(r) for r in m)}, gates, idle
+
+def invoice(p, pat, thick, prof):
+    full = frozenset(range(2*p+1)); T, D = Counter(), Counter()
+    outs = [full, full]
+    for i, ch in enumerate(pat, 1):
+        outs += [frozenset(range(0, 2*i+1)) if ch == 'I' else frozenset(range(2*i, 2*p+1))]*2
+    for s in outs: T[1+8*len(s & thick)] += 112
+    for i, ch in enumerate(pat, 1):
+        D[8*len((frozenset(range(0, 2*i)) if ch == 'I' else frozenset(range(2*i+1, 2*p+1))) & thick)] += 224
+    for j in range(1, p): D[8*len(frozenset([2*j]) & thick)] += 224
+    for r, n in H.items(): T[r] += len(thick)*n
+    for r, n in prof.items(): D[r] += len(thick)*n
+    D[1] += 112*(2*p+1-len(thick)); T.pop(0, None); D.pop(0, None)
+    return T, D
+
+def root(T, D):
+    f = lambda c: sum(n*r**(1-c) for r, n in T.items())-sum(n*r**(1-c) for r, n in D.items())
+    lo, hi = 0.0, 0.05
+    for _ in range(200):
+        mid = (lo+hi)/2
+        if f(mid) > 0: lo = mid
+        else: hi = mid
+    return lo
+
+def main():
+    mod = load('c4940', ROOT/'research/coded-reverse-controller/verify.py')
+    C = mod.C
+    receipt = {}
+    for p, pat in ((2, 'I'), (3, 'IT'), (19, 'I'*9+'T'*9)):
+        coupling = {s: Q(1) for s in range(2*p+1)}
+        keep = mod.keep_of(p, pat)
+        want_co, want_idle = mod.controller(p, keep, coupling)
+        got, got_co, gates, idle = traced_controller(C, p, keep, coupling)
+        need(got_co == want_co, 'the trace reproduces the controller matrix exactly')
+        need([r['retained'] for r in idle] == [r['retained'] for r in want_idle],
+             'the trace reproduces the retention pattern')
+        std = mod.diagonalize(p, pat, coupling)
+        need(std is not None, 'the uncoded word diagonalises at p=%d' % p)
+        kinds = Counter(g[0] for g in gates)
+        ret = [r for r in idle if r['retained']]
+        roles = set()
+        for g in gates:
+            if g[0] in ('REVERSE', 'FORWARD', 'LETTER', 'BRIDGE', 'SWAP'):
+                roles.update(x for x in g[2:4] if isinstance(x, int) and x >= 0)
+            elif g[0] == 'IDLE':
+                roles.update((g[2], g[3]))
+        receipt['p%d' % p] = {'gates': len(gates), 'kinds': dict(kinds),
+                      'role_set': sorted(roles), 'max_role': max(roles) if roles else -1,
+                      'retained_idles': len(ret),
+                      'idle_rank': sum(len(r['sel']) for r in ret),
+                      'outputs': std[0], 'denominators': std[1],
+                      'trace_identity': 'replayed in the controller algebra'}
+        need(std[1] == [1], 'standard denominators are [1] at p=%d' % p)
+        print('PASS p=%2d trace == controller: %d gates %s, %d retained idles, rank %d; diagonalises to %s with '
+              'denominators %s' % (p, len(gates), dict(kinds), len(ret),
+                                   sum(len(r['sel']) for r in ret), std[0], std[1]))
+
+    p, pat = 19, 'I'*9+'T'*9
+    thick = frozenset(range(1, 2*p, 2))
+    T, D = invoice(p, pat, thick, PROF)
+    r = root(T, D)
+    need(abs(r-0.007578535189897761) < 1e-9, 'p19 coded root, unchanged without the code')
+    need(max(T) == 153, 'ambient target rank')
+    print('PASS price: the invoice is code-blind, so the uncoded word keeps the root %.12f '
+          '(T %d units, D %d units, ambient rank %d)' % (r, sum(T.values()), sum(D.values()), max(T)))
+    receipt['p19'] = dict(receipt['p19'], invoice_root=r, ambient_rank=max(T),
+                          recodings=0, monomial_field_maps=0, scalar_adds=0, owned_clears=0,
+                          terminal_gauge_decoder=0,
+                          note='no code, so no recoding bill and no terminal-gauge decoder')
+    receipt['status'] = 'PASS_P19_UNCODED_WORD'
+    receipt['scope'] = ('controller trace identity, p=2/3/19 diagonalisation, census and price; '
+                        'ambient rank 153 precludes a literal 512-address replay')
+    (HERE/'P19_PLAIN.json').write_text(json.dumps(receipt, indent=2, sort_keys=True)+'\n')
+    print(json.dumps({k: receipt[k] for k in ('status',)}, sort_keys=True))
+
+if __name__ == '__main__':
+    main()
diff --git a/research/p19-current-head-binding-audit/verify.py b/research/p19-current-head-binding-audit/verify.py
new file mode 100644
index 0000000000..ff646e7489
--- /dev/null
+++ b/research/p19-current-head-binding-audit/verify.py
@@ -0,0 +1,333 @@
+#!/usr/bin/env python3
+"""Source-bound whole-word counterexample and sharp unit-rank fee gate for PR5270.
+
+Prepared for zxv with substantial OpenAI Codex assistance. Apache-2.0.
+Source exports retain DaysSky's and the credited controller authors' work.
+Only authenticated function ASTs are executed; submitted modules are not imported.
+"""
+import argparse
+import ast
+from collections import Counter
+from dataclasses import dataclass
+from decimal import Decimal, localcontext
+from fractions import Fraction as Q
+from hashlib import sha256
+import json
+from pathlib import Path
+from types import SimpleNamespace
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+P, IMAG = 65537, 256
+
+
+def need(ok, why):
+    if not ok:
+        raise ValueError(why)
+
+
+@dataclass(frozen=True)
+class ZI:
+    """Exact Gaussian integers, independent of the address-loop residue field."""
+    a: int = 0
+    b: int = 0
+
+    @staticmethod
+    def of(x):
+        if isinstance(x, ZI):
+            return x
+        q = Q(x)
+        need(q.denominator == 1, 'integral specialized controller coefficient')
+        return ZI(q.numerator)
+
+    def __add__(self, other):
+        x = self.of(other)
+        return ZI(self.a+x.a, self.b+x.b)
+
+    __radd__ = __add__
+
+    def __neg__(self):
+        return ZI(-self.a, -self.b)
+
+    def __mul__(self, other):
+        x = self.of(other)
+        return ZI(self.a*x.a-self.b*x.b, self.a*x.b+self.b*x.a)
+
+    __rmul__ = __mul__
+
+    def __pow__(self, n):
+        if n < 0:
+            need(self.a*self.a+self.b*self.b == 1, 'inverse only of Gaussian units')
+            return ZI(self.a, -self.b)**(-n)
+        value, base = ZI(1), self
+        while n:
+            if n & 1:
+                value = value*base
+            n //= 2
+            base = base*base
+        return value
+
+    def __bool__(self):
+        return bool(self.a or self.b)
+
+    def residue(self):
+        return (self.a+IMAG*self.b) % P
+
+
+UNITS = [ZI(1), ZI(0, 1), ZI(-1), ZI(0, -1)]
+
+
+class EigenAlgebra:
+    """Evaluate monomials on a physical Gaussian eigencharacter, over Z[i]."""
+    def __init__(self, q_power, stage_powers):
+        self.q = UNITS[q_power]
+        self.stages = {s: UNITS[e] for s, e in stage_powers.items()}
+
+    def plus(self, a, b, coefficient=1):
+        out = dict(a)
+        for key, value in b.items():
+            out[key] = out.get(key, ZI())+coefficient*value
+            if not out[key]:
+                del out[key]
+        return out
+
+    def monomial_times(self, polynomial, exponents, coefficient=1):
+        value = coefficient*(self.q**exponents[0])
+        for s, exponent in enumerate(exponents[1:]):
+            value = value*self.stages.get(s, ZI(1))**exponent
+        return {key: v*value for key, v in polynomial.items() if v*value}
+
+
+def parse(raw):
+    return ast.parse(raw.decode('utf-8'))
+
+
+def function(tree, name, namespace):
+    nodes = [n for n in tree.body if isinstance(n, ast.FunctionDef) and n.name == name]
+    need(len(nodes) == 1, 'one authenticated definition of '+name)
+    exec(compile(ast.Module(body=nodes, type_ignores=[]), '<authenticated '+name+'>', 'exec'), namespace)
+    return namespace[name]
+
+
+def address_loop(tree, repaired=False, exact=False):
+    import copy
+    main = next(n for n in tree.body if isinstance(n, ast.FunctionDef) and n.name == 'main')
+    loops = [n for n in main.body if isinstance(n, ast.For)
+             and isinstance(n.target, ast.Name) and n.target.id == 'g'
+             and isinstance(n.iter, ast.Name) and n.iter.id == 'gates']
+    need(len(loops) == 1, 'unique actual address gate loop')
+    loop = copy.deepcopy(loops[0])
+    candidates = [n for n in ast.walk(loop) if isinstance(n, ast.For)
+                  and ast.dump(n.iter) == ast.dump(ast.parse('enumerate(sel)', mode='eval').body)]
+    need(len(candidates) == 1, 'actual IDLE decoder is enumerate(sel)')
+    bad = candidates[0]
+    need(ast.dump(bad.target) == ast.dump(ast.parse('for s, bit in []:\n pass').body[0].target),
+         'IDLE decoder binds positions and literal stage numbers')
+    need(len(bad.body) == 1 and isinstance(bad.body[0], ast.If)
+         and ast.dump(bad.body[0].test) == ast.dump(ast.parse('bit and s in blocks', mode='eval').body),
+         'actual IDLE condition')
+    if repaired:
+        bad.target = ast.Name(id='s', ctx=ast.Store())
+        bad.iter = ast.Name(id='sel', ctx=ast.Load())
+        bad.body[0].test = ast.parse('s in blocks', mode='eval').body
+    if exact:
+        class RemoveResidue(ast.NodeTransformer):
+            def visit_BinOp(self, node):
+                self.generic_visit(node)
+                if isinstance(node.op, ast.Mod):
+                    need(isinstance(node.right, ast.Name) and node.right.id == 'P', 'only reduce modulo P')
+                    return node.left
+                return node
+        loop = RemoveResidue().visit(loop)
+    module = ast.fix_missing_locations(ast.Module(body=[loop], type_ignores=[]))
+    return compile(module, '<actual p19_bank gate loop>', 'exec')
+
+
+def address_matrix(loop, p, gates, q_power, stage_powers, exact=False):
+    """Execute the submitted loop on its invariant Walsh-character subspace.
+
+    Each row holds independent ROLE coefficients, not a truncated address array.
+    Axis Gaussians act diagonally here, so no physical address is approximated.
+    """
+    thick = list(range(1, 2*p, 2))
+    blocks = {s: k for k, s in enumerate(thick)}
+    centre = 8*len(thick)
+    axis_powers = {centre: q_power}
+    for s, exponent in stage_powers.items():
+        for j in range(exponent):
+            axis_powers[8*blocks[s]+j] = 1
+
+    def butterfly(row, axis, power=1):
+        if exact:
+            factor = UNITS[axis_powers.get(axis, 0)]**power
+            row[:] = [v*factor for v in row]
+        else:
+            factor = pow(IMAG, axis_powers.get(axis, 0)*power, P)
+            row[:] = [v*factor % P for v in row]
+
+    n = 2*p
+    state = [[ZI(int(i == j)) if exact else int(i == j) for j in range(n)] for i in range(n)]
+    exec(loop, dict(gates=gates, state=state, butterfly=butterfly, centre=centre, blocks=blocks, P=P))
+    return state
+
+
+def specialized(plain, controller_tree, p, pattern, q_power, stage_powers):
+    algebra = EigenAlgebra(q_power, stage_powers)
+    ns = {'Q': Q, 'C': algebra}
+    controller = function(controller_tree, 'controller', ns)
+    keep_of = function(controller_tree, 'keep_of', ns)
+    trace = function(plain, 'traced_controller', {'Q': Q})
+    coupling = {s: 1 for s in range(2*p+1)}
+    keep = keep_of(p, pattern)
+    co, _ = controller(p, keep, coupling)
+    matrix, trace_co, gates, idle = trace(algebra, p, keep, coupling)
+    need(co == trace_co, 'source controller and emitted trace agree on eigencharacter')
+    wanted = [[sum((ZI.of(v) for v in cell.values()), ZI()) for cell in row] for row in matrix]
+    return wanted, gates, idle
+
+
+def mismatch(wanted, actual):
+    return [[i, j, [v.a, v.b], actual[i][j]] for i, row in enumerate(wanted)
+            for j, v in enumerate(row) if v.residue() != actual[i][j]]
+
+
+def authenticate():
+    manifest = json.loads((HERE/'SOURCE_EXPORTS.json').read_text())
+    need(manifest['source_head'] == '225a19a184296d12120203a1f43b981d55465241', 'reviewed PR head')
+    raw = {}
+    for item in manifest['files']:
+        data = (HERE/item['path']).read_bytes()
+        need(sha256(data).hexdigest() == item['sha256'], 'export source hash '+item['path'])
+        raw[Path(item['source_path']).name] = data
+    for item in json.loads((HERE/'SOURCES.json').read_text())['files']:
+        if item['usage'] == 'input':
+            need(sha256((ROOT/item['path']).read_bytes()).hexdigest() == item['sha256'], 'live source hash '+item['path'])
+    return raw
+
+
+def invoice_checks(raw):
+    tree = parse(raw['p19_plain.py'])
+    literals = {n.targets[0].id: ast.literal_eval(n.value) for n in tree.body
+                if isinstance(n, ast.Assign) and len(n.targets) == 1
+                and isinstance(n.targets[0], ast.Name) and n.targets[0].id in ('H', 'PROF')}
+    source_invoice = function(tree, 'invoice', dict(Counter=Counter, H=literals['H']))
+    targets, paid = source_invoice(19, 'I'*9+'T'*9, set(range(1, 38, 2)), literals['PROF'])
+    # Independent list census of all target banks, idle intervals and producer jobs.
+    t, d = [153]*224, [1]*(20*112)
+    for i, side in enumerate('I'*9+'T'*9, 1):
+        length = i if side == 'I' else 19-i
+        t += [1+8*length]*224
+        d += [8*length]*224
+    for r, n in literals['H'].items():
+        t += [r]*(19*n)
+    for r, n in literals['PROF'].items():
+        d += [r]*(19*n)
+    need(Counter(t) == targets and Counter(d) == paid, 'independent complete invoice')
+    need((len(t), len(d), sum(t), sum(d)) == (12008, 68782, 265533, 263517), 'counts and rank masses')
+    thresholds = sorted(set(targets)|set(paid))
+    gaps = {k: 2016+sum(n*min(r, k) for r, n in paid.items())
+               -sum(n*min(r, k) for r, n in targets.items()) for k in thresholds}
+    need(gaps[153] == 0 and all(v > 0 for r, v in gaps.items() if r < 153), 'sharp truncated-mass certificate')
+    need(sum(t)-sum(d)-2015 == 1, 'one fewer fee retains positive moment at t=1')
+    path = ROOT/'research/higher-moment-strictification/verify.py'
+    env = {'__name__': 'retained_intervals', '__file__': str(path)}
+    exec(compile(path.read_bytes(), str(path), 'exec'), env)
+    engine = SimpleNamespace(**env)
+
+    def margin(c):
+        x, y = engine.moment(targets, 1-c), engine.moment(paid, 1-c)
+        return x[0]-y[1], x[1]-y[0]
+
+    bracket = [Q('0.007578535189'), Q('0.007578535191')]
+    need(margin(bracket[0])[0] > 0 and margin(bracket[1])[1] < 0, 'raw crossing bracket signs')
+    bit, kappa, gap = Q('0.0034'), Q(951999, 280000000), Q(1, 1400000000)
+    bit_margin = margin(bit)
+    need(bit_margin[0] > 1103 and bit_margin[1] < 1104, 'sharp integer fee budget at admitted BIT cap')
+    need(bit-kappa == 5*gap, 'outer endpoint is five grid steps below admitted BIT')
+    controller = parse((ROOT/'research/coded-reverse-controller/verify.py').read_bytes())
+    old_profile = next(ast.literal_eval(n.value) for n in controller.body if isinstance(n, ast.Assign)
+                       and any(isinstance(t, ast.Name) and t.id == 'P_OLD' for t in n.targets))
+    old_targets, old_paid = source_invoice(19, 'I'*9+'T'*9, set(range(1, 38, 2)), old_profile)
+    need(old_targets == targets, 'pre-PR4929 profile comparison keeps optimistic targets')
+    def old_margin(c):
+        x, y = engine.moment(old_targets, 1-c), engine.moment(old_paid, 1-c)
+        return x[0]-y[1], x[1]-y[0]
+    old_bracket = [Q('0.003004145206'), Q('0.003004145208')]
+    need(old_margin(old_bracket[0])[0] > 0 and old_margin(old_bracket[1])[1] < 0,
+         'pre-PR4929 profile raw crossing')
+    need(old_margin(Q('0.003125804'))[1] < 0, 'pre-PR4929 profile misses selected kappa')
+    with localcontext() as ctx:
+        ctx.prec = 90
+        exponent = Decimal(1)-Decimal(bit.numerator)/Decimal(bit.denominator)
+        dm = sum(Decimal(n)*Decimal(r)**exponent for r, n in targets.items())
+        dm -= sum(Decimal(n)*Decimal(r)**exponent for r, n in paid.items())
+        need(Decimal(1103) < dm < Decimal(1104), 'independent Decimal price control')
+    return {'target_count': len(t), 'paid_count': len(d), 'target_rank_mass': sum(t), 'paid_rank_mass': sum(d),
+            'raw_crossing_sign_bracket': list(map(str, bracket)), 'sharp_extra_H1_threshold': 2016,
+            'truncated_mass_gaps_after_2016_H1': {str(r): v for r, v in gaps.items()},
+            'at_BIT_0034_extra_H1_budget': 1103, 'decimal_margin_at_BIT_0034': str(dm),
+            'claimed_outer_kappa': str(kappa), 'admitted_BIT': str(bit),
+            'tested_complex': str(kappa+7*gap), 'conditional_uniform_complex': str(kappa+6*gap),
+            'pre_PR4929_profile_control': {'profile': old_profile,
+                'raw_crossing_sign_bracket': list(map(str, old_bracket)),
+                'negative_margin_at_selected_kappa_003125804': True},
+            'fees_2128_and_4256_excluded_for_every_0_t_1': True}
+
+
+def check():
+    raw = authenticate()
+    plain, bank = parse(raw['p19_plain.py']), parse(raw['p19_bank.py'])
+    controller = parse((ROOT/'research/coded-reverse-controller/verify.py').read_bytes())
+    original, repaired = address_loop(bank), address_loop(bank, repaired=True)
+    integral_loop = address_loop(bank, exact=True)
+    need(pow(IMAG, 2, P) == P-1, 'Gaussian integer residue homomorphism')
+    grid = {}
+    for pattern in ('I', 'T'):
+        failures = fixed = 0
+        for q in range(2):
+            for e1 in range(4):
+                for e3 in range(4):
+                    wanted, gates, _ = specialized(plain, controller, 2, pattern, q, {1: e1, 3: e3})
+                    failures += bool(mismatch(wanted, address_matrix(original, 2, gates, q, {1: e1, 3: e3})))
+                    fixed += bool(mismatch(wanted, address_matrix(repaired, 2, gates, q, {1: e1, 3: e3})))
+        need(failures == (0 if pattern == 'I' else 24) and fixed == 0, 'p2 Gaussian eigenvalue triples')
+        grid[pattern] = {'triples': 32, 'submitted_loop_failures': failures, 'repaired_loop_failures': fixed}
+    witnesses = {}
+    for p, pattern, active, count in [(2, 'T', 3, 4), (3, 'IT', 5, 8), (19, 'I'*9+'T'*9, 37, 72)]:
+        wanted, gates, idle = specialized(plain, controller, p, pattern, 0, {active: 1})
+        physical = address_matrix(original, p, gates, 0, {active: 1})
+        integral = address_matrix(integral_loop, p, gates, 0, {active: 1}, exact=True)
+        need(all(v.residue() == physical[i][j] for i, row in enumerate(integral) for j, v in enumerate(row)),
+             'independent exact Gaussian-integer and submitted residue-loop agreement')
+        bad = mismatch(wanted, physical)
+        need(len(bad) == count, 'whole-word eigencharacter mismatch p='+str(p))
+        need(not mismatch(wanted, address_matrix(repaired, p, gates, 0, {active: 1})), 'protocol repair positive control')
+        witnesses[str(p)] = {'pattern': pattern, 'central_eigenvalue': [1, 0], 'active_stage': active,
+                            'active_eigenvalue': [0, 1], 'all_other_stage_eigenvalues': [1, 0],
+                            'gate_count': len(gates), 'mismatches': bad,
+                            'pulse_input_role': 2*p-2, 'pulse_output_role': 0,
+                            'pulse_expected': [wanted[0][2*p-2].a, wanted[0][2*p-2].b],
+                            'pulse_actual': [integral[0][2*p-2].a, integral[0][2*p-2].b],
+                            'retained_terminal_events': [r for r in idle if r['retained'] and r['kind'] == 'terminal']}
+    A = [[Q(v) for v in row] for row in json.loads((ROOT/'research/coded-native-caller/CODE.json').read_text())['A']]
+    need(len(A) == 112 and all(len(row) == 112 and row[j] == 0 for j, row in enumerate(A)), '112 zero native diagonal blocks')
+    return {'status': 'PASS_P19_CURRENT_HEAD_BINDING_AUDIT', 'source_head': '225a19a184296d12120203a1f43b981d55465241',
+            'p2_eigenvalue_grid': grid, 'whole_word_witnesses': witnesses, 'native_same_owner_zero_blocks': 112,
+            'price': invoice_checks(raw), 'scope': 'Exact source-bound counterexamples and fixed-invoice fee theorem; no new supplier, admission, global decoder lower bound or kappa.'}
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument('--write', action='store_true')
+    args = parser.parse_args()
+    result = check()
+    encoded = json.dumps(result, indent=2, sort_keys=True)+'\n'
+    if args.write:
+        (HERE/'RESULT.json').write_text(encoded)
+    else:
+        need((HERE/'RESULT.json').read_text() == encoded, 'fresh result equals committed mathematical receipt')
+    print(result['status']+' head='+result['source_head']+' p19_mismatches=72 sharp_H1_fee=2016 no_new_kappa')
+
+
+if __name__ == '__main__':
+    main()

From 1afd30774ee72c96b6973c9c04ac3741f61b831e Mon Sep 17 00:00:00 2001
From: zxv <zxv@zxv>
Date: Wed, 28 Oct 2026 00:10:07 -0400
Subject: [PATCH 2/2] Record passing original p2 control and exact prior
 fee-proof credit

---
 .../p19-current-head-binding-audit/README.md  |  2 +-
 .../p19-current-head-binding-audit/TASK.json  |  2 +-
 .../VALIDATION.json                           | 29 +++++++++++++++++--
 3 files changed, 29 insertions(+), 4 deletions(-)

diff --git a/research/p19-current-head-binding-audit/README.md b/research/p19-current-head-binding-audit/README.md
index dcf06e8bbb..ddd1d8537a 100644
--- a/research/p19-current-head-binding-audit/README.md
+++ b/research/p19-current-head-binding-audit/README.md
@@ -106,7 +106,7 @@ python3.12 -B scripts/research_package.py --package research/p19-current-head-bi
 
 The default verifier is read-only and compares a freshly calculated mathematical receipt. `--write` explicitly regenerates it. Small exact exports from the unmerged head retain their paths, commit/blob IDs and SHA256 values in `SOURCE_EXPORTS.json`. Canonical inputs and historical guidance are pinned in `SOURCES.json`. No external PR-head availability is required for replay; exports are retained evidence, not edits to the predecessor.
 
-`VALIDATION.json` separates fresh normal/optimized scoped checks, author arithmetic runs, source-corruption controls and the bounded original bank-run timeout. A timeout is not a pass. No full p19 Laurent factorization, native archive replay, enormous address enumeration, Lean, Docker, machine compiler, precision/tape/stock closure or analytic recovery theorem is newly verified. The selected five assumptions remain unchanged. The selected-baseline helper could not authenticate its full certificate closure in the intentionally sparse checkout; selected values were instead read directly from the pinned Git record, certificate and maintainer review.
+`VALIDATION.json` separates fresh normal/optimized scoped checks, author arithmetic runs, source-corruption controls and original bank runs. The original one-dense-seed p2 pattern-I bank control passes freshly in CPython 3.12 in 131.23 seconds under the 360-second/1-GiB guard (203120 KiB peak sampled descendant RSS). An earlier CPython 3.11 attempt timed out at 180 seconds; both outcomes are preserved separately. A timeout is not a pass. The optional full source-history preflight is unavailable in this shallow checkout; metadata/pins and exact committed bytes pass. No full p19 Laurent factorization, native archive replay, enormous address enumeration, Lean, Docker, machine compiler, precision/tape/stock closure or analytic recovery theorem is newly verified. The selected five assumptions remain unchanged. The selected-baseline helper could not authenticate its full certificate closure in the intentionally sparse checkout; selected values were instead read directly from the pinned Git record, certificate and maintainer review.
 
 ## Significance for researchers
 
diff --git a/research/p19-current-head-binding-audit/TASK.json b/research/p19-current-head-binding-audit/TASK.json
index db47dbf433..7a03201214 100644
--- a/research/p19-current-head-binding-audit/TASK.json
+++ b/research/p19-current-head-binding-audit/TASK.json
@@ -72,7 +72,7 @@
   },
   "scope_status": "changed",
   "actual_scope": "Explicit audit of PR5270 at 225a19a184296d12120203a1f43b981d55465241: complete current IDLE-decoder counterexample on exact Gaussian eigencharacters, native-to-uncoded substitution, and sharp fixed-invoice extra-H1 budget.",
-  "scope_change_reason": "The explicit assignment identifies PR5270 rather than the selected P104 caller in the generic card. Existing exact-head local objections are credited; the new scope binds the actual address-loop AST to complete p19 outputs and proves a sharp all-exponent fee threshold. The final live refresh located Ali Romman\u2019s prior all-exponent boundary-cost proof (Discussion4930#discussioncomment-19149724); the fee certificate is explicitly an independent reproduction, not a novel threshold claim. The new endpoint witness remains distinct.",
+  "scope_change_reason": "The explicit assignment identifies PR5270 rather than the selected P104 caller in the generic card. Existing exact-head local objections are credited; the new scope binds the actual address-loop AST to complete p19 outputs and independently checks the complete price budget. The final live refresh located Ali Romman\u2019s prior all-exponent boundary-cost proof (Discussion4930#discussioncomment-19149724); the fee certificate is explicitly an independent reproduction, not a novel threshold claim. The new endpoint witness remains distinct.",
   "bottleneck_link": "A favorable invoice and compiler arithmetic cannot raise the selected exponent without a physical supplier realizing the same independent Gaussian targets and paid jobs. PR5270 inherits BIT .0034 and proposes a complex improvement; it supplies no new BIT saving.",
   "budget_minutes": 60,
   "stop_rule": "Stop at the exact current-head binding counterexample and fixed-invoice fee theorem. Do not construct a new caller, rerun the full historical corpus, or change admission/frontier/queue decisions.",
diff --git a/research/p19-current-head-binding-audit/VALIDATION.json b/research/p19-current-head-binding-audit/VALIDATION.json
index 6696e1c8b9..f08058d653 100644
--- a/research/p19-current-head-binding-audit/VALIDATION.json
+++ b/research/p19-current-head-binding-audit/VALIDATION.json
@@ -83,6 +83,21 @@
       "stop": null,
       "stdout_sha256": "6dc0a4cd356c93ebdf6a0764b6e9f0a3ff7b9ba03a563c6f572f4efef28b04a5",
       "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "bank-python312": {
+      "argv": [
+        "/opt/local/bin/python3.12",
+        "-u",
+        "-B",
+        "research/coded-reverse-word-p19/p19_bank.py"
+      ],
+      "cwd": "/tmp/integer-p19-source",
+      "seconds": 131.23299658298492,
+      "peak_sampled_descendant_rss_kib": 203120,
+      "exit_code": 0,
+      "stop": null,
+      "stdout_sha256": "44923100db2573e031478019879cd07a43018dc4bacaf5623017f20f3492a439",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
     }
   },
   "export_control": {
@@ -105,7 +120,7 @@
     "full machine/compiler/precision/tape/stock/analytic recovery proof"
   ],
   "limitations": [
-    "Original p2 bank command stopped at 180 seconds with no pass receipt. An earlier sparse setup import failure was resolved before this bounded run.",
+    "An initial CPython 3.11 bank command stopped at 180 seconds. A fresh explicitly budgeted CPython 3.12 run then passed in 131.23 seconds (203120 KiB peak sampled descendant RSS). This is the original one-dense-seed p2 pattern-I control, not a p19 native admission.",
     "The complete-word p19 result instantiates the actual gate-loop semantics with p19 gates; the submitted main remains hardcoded to p2 pattern I.",
     "Fresh source-bound mathematical checks are author-side AI-assisted checks, not independent human or proof-kernel acceptance."
   ],
@@ -132,5 +147,15 @@
   "final_overlap_local_scope": "Sparse local inventory incomplete; relevant retained native/controller/reference/decoder notes were materialized. Live PR/Discussion searches are provisional leads, not novelty proof.",
   "prior_fee_proof": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19149724",
   "original_contribution": "Complete-word execution of the exact current address-loop protocol on emitted p19 gates, with the role-36 to role-0 pulse witness, p2 eigenvalue controls and narrow repair controls. The fee threshold is independently reproduced prior work.",
-  "frozen_source_whitespace": "git diff --check reports one pre-existing trailing space in retained source/pr5270/p19_claim.py:370. Exact source bytes/hashes are preserved; new authored files pass the scoped whitespace check."
+  "frozen_source_whitespace": "git diff --check reports one pre-existing trailing space in retained source/pr5270/p19_claim.py:370. Exact source bytes/hashes are preserved; new authored files pass the scoped whitespace check.",
+  "committed_byte_preflight": {
+    "status": "PASS_RESEARCH_COMMIT_BYTES",
+    "commit": "ab2435cf5ba7a1f4650cb1d43bd31b09271043a3",
+    "files": 24
+  },
+  "source_history_preflight": {
+    "status": "unavailable",
+    "reason": "source-history check requires full Git history; checkout is shallow. Exact available source bytes/pins pass metadata and committed-byte checks; no full-history availability claim is made."
+  },
+  "source_worktree_status_after_bank": ""
 }