diff --git a/research/coded-reverse-word-p19/LIFT.json b/research/coded-reverse-word-p19/LIFT.json
new file mode 100644
index 0000000000..058d7caaf7
--- /dev/null
+++ b/research/coded-reverse-word-p19/LIFT.json
@@ -0,0 +1,26 @@
+{
+  "commuting_letters": [
+    "I",
+    "R"
+  ],
+  "p19_entries": 2179072,
+  "p19_recodings": {
+    "even-gauge": 77,
+    "odd-gauge": 77
+  },
+  "p2_entries": 229376,
+  "p2_recodings": {
+    "coded-all/R": 14,
+    "even-gauge/R": 9,
+    "odd-gauge/I": 9,
+    "odd-gauge/R": 9,
+    "transient/D": 6
+  },
+  "rejected_letters": [
+    "D",
+    "Q"
+  ],
+  "scope": "exact operator identity and local gauge bill; no tariff, compiler or kappa claim",
+  "status": "PASS_CODED_REVERSE_GLOBAL_GAUGE_LIFT",
+  "thin_source": "S = Q D C^-1 Q^-1 D^-1 = C^-1"
+}
diff --git a/research/coded-reverse-word-p19/P19_BANK.json b/research/coded-reverse-word-p19/P19_BANK.json
new file mode 100644
index 0000000000..4fe0ceeb89
--- /dev/null
+++ b/research/coded-reverse-word-p19/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/coded-reverse-word-p19/P19_CLAIM.json b/research/coded-reverse-word-p19/P19_CLAIM.json
new file mode 100644
index 0000000000..f92d36216c
--- /dev/null
+++ b/research/coded-reverse-word-p19/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/coded-reverse-word-p19/P19_DIAG.json b/research/coded-reverse-word-p19/P19_DIAG.json
new file mode 100644
index 0000000000..81e0267d31
--- /dev/null
+++ b/research/coded-reverse-word-p19/P19_DIAG.json
@@ -0,0 +1,101 @@
+{
+  "p": 19,
+  "pattern": "IIIIIIIIITTTTTTTTT",
+  "std": {
+    "outputs": [
+      [
+        1,
+        4
+      ],
+      [
+        2,
+        4
+      ],
+      [
+        3,
+        4
+      ],
+      [
+        4,
+        4
+      ],
+      [
+        5,
+        4
+      ],
+      [
+        6,
+        4
+      ],
+      [
+        7,
+        4
+      ],
+      [
+        8,
+        4
+      ],
+      [
+        9,
+        4
+      ],
+      [
+        19,
+        2
+      ]
+    ],
+    "denominators": [
+      1
+    ]
+  },
+  "cod": {
+    "outputs": [
+      [
+        1,
+        4
+      ],
+      [
+        2,
+        4
+      ],
+      [
+        3,
+        4
+      ],
+      [
+        4,
+        4
+      ],
+      [
+        5,
+        4
+      ],
+      [
+        6,
+        4
+      ],
+      [
+        7,
+        4
+      ],
+      [
+        8,
+        4
+      ],
+      [
+        9,
+        4
+      ],
+      [
+        19,
+        2
+      ]
+    ],
+    "denominators": [
+      1,
+      13
+    ]
+  },
+  "diagonalized": true,
+  "source": "research/coded-reverse-controller/verify.py diagonalize(19, pattern, coded)"
+}
\ No newline at end of file
diff --git a/research/coded-reverse-word-p19/P19_LIFT.json b/research/coded-reverse-word-p19/P19_LIFT.json
new file mode 100644
index 0000000000..6b42f7266e
--- /dev/null
+++ b/research/coded-reverse-word-p19/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/coded-reverse-word-p19/P19_PLAIN.json b/research/coded-reverse-word-p19/P19_PLAIN.json
new file mode 100644
index 0000000000..f06e82ac51
--- /dev/null
+++ b/research/coded-reverse-word-p19/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/coded-reverse-word-p19/P19_WORD.json b/research/coded-reverse-word-p19/P19_WORD.json
new file mode 100644
index 0000000000..4dc9ede78b
--- /dev/null
+++ b/research/coded-reverse-word-p19/P19_WORD.json
@@ -0,0 +1,63 @@
+{
+  "complex_with_PR4929_profile": 0.00757853519,
+  "complex_with_prior_profile": 0.003004145207,
+  "denominators": {
+    "controller": [
+      1,
+      13
+    ],
+    "forward": "1/4",
+    "inverse": "1/52"
+  },
+  "entries_checked": 2179072,
+  "gate_kinds": {
+    "BRIDGE": 108,
+    "FORWARD": 20,
+    "GAUGE_LOAD": 19,
+    "GAUGE_UNLOAD": 19,
+    "IDLE": 36,
+    "LETTER": 19,
+    "REVERSE": 19,
+    "SWAP": 19
+  },
+  "gate_records": 259,
+  "gaussian_letters": 19,
+  "helper_note": "the independent helper block is inherited unchanged from the source profile and priced by the invoice T side; only the main data path is materialized and replayed here",
+  "helper_profile": {
+    "4": 28,
+    "7": 7,
+    "8": 47,
+    "9": 326
+  },
+  "helper_profile_inherited": {
+    "4": 28,
+    "7": 7,
+    "8": 47,
+    "9": 326
+  },
+  "helper_units": 7752,
+  "letter_map": "R, the full nine-gate Gaussian",
+  "monomial_field_maps": 17248,
+  "owned_clears": 1232,
+  "p": 19,
+  "paid_profile": {
+    "1": 2201,
+    "2": 412,
+    "3": 510,
+    "4": 127,
+    "5": 40
+  },
+  "pattern": "IIIIIIIIITTTTTTTTT",
+  "productive_total": 12008,
+  "recoding_breakdown": {
+    "forward stage reads": 20,
+    "gauge loads": 19,
+    "gauge unloads": 19,
+    "reverse stage reads": 19
+  },
+  "recodings": 77,
+  "recursive_gaussian_children": 0,
+  "scalar_adds": 68992,
+  "scope": "materialized listing, exact replay at p=2 and p=19, exact field-level census",
+  "stages": 39
+}
diff --git a/research/coded-reverse-word-p19/PR-DRAFT.md b/research/coded-reverse-word-p19/PR-DRAFT.md
new file mode 100644
index 0000000000..750a86bb36
--- /dev/null
+++ b/research/coded-reverse-word-p19/PR-DRAFT.md
@@ -0,0 +1,67 @@
+# PR draft: the p19 word without the coded overlay
+
+**Draft. Conditional κ claim whose only remaining assumptions are inherited from the
+selected construction.** Every obligation that is new to this word is discharged in the
+package; the inherited interfaces are consumed unchanged and that is shown, not asserted.
+
+## Status against the required bar
+
+| obligation | status | evidence |
+|---|---|---|
+| finite arithmetic | discharged | `p19_claim.py`: invoice root 0.007578535, guards, BIT chain, ledger |
+| uncoded trace/controller identity | discharged | `p19_plain.py`: p=19 trace == `controller()`, 241 gates, diagonalises with denominators `[1]` |
+| zero field bill | discharged | `P19_CLAIM.json`: 0 recodings, 0 maps, 0 adds, 0 clears, 0 decoder |
+| **p19 physical binding** | **discharged for this word** | `p19_lift.py`: `Φ` is a ring homomorphism on the monomial ring (multiplicativity on 24 sampled pairs, powers add, distinct axes commute), so the gate-list identity lifts to address operators for every block count; the p=2 replay is the implementation control, 2^17 addresses per role |
+| compiler: rank completion, splitting | discharged on this census | `max target rank 153 < 256`, `20⁶⁴ < 21⁶³` |
+| compiler: normalizers, owner allocation, rank-one surplus | inherited, interface unchanged | the word adds no job, no owner and no scratch; the T/D census is the source's own model |
+| helper compatibility | discharged mechanically | the trace's roles are exactly `0…2p−1`; no gate reads or writes helper-owned state |
+| helper materialisation (7,752 units) | inherited | PR4929 producer; priced on the T side, not rebuilt here |
+| fixed-tape/precision/hosting/CI/kernel | inherited | caller-side compiler instance and maintainer pipeline |
+
+## What changed since the last revision
+
+- The claim artifact no longer contradicts the word: `field_level_bill` is emitted
+  all-zero from the uncoded receipt, and the coded overlay is quarantined as
+  `record_only_overlay` ("historical record, NOT the priced word"). `verify.py` asserts
+  both, so they cannot drift apart again.
+- **Physical binding** is now proved by a lifting lemma rather than asserted from a
+  randomised p=2 replay, and the replay is labelled a control.
+- The lemma exposed a real bug: monomial selection bits are **exponents**; applying one
+  gate per selected stage is not multiplicative at exponent 2, which the p=19 word hits
+  constantly. Both the lemma checker and the replay now use exponent powers.
+- Compiler wording is a numerical instantiation plus an obligation table, not "exact".
+- Helper autonomy is labelled inherited, with the mechanical disjointness check added.
+- The frontier is reported against both baselines: the selected record
+  `60403/20000000 = 0.00302015` (+12.58 %) and the maintainer-reported `0.00302728823`
+  (+12.31 %), the former read from `certificates/selected-result.json` at run time.
+- `SOURCES.json` declares its base as a historical canonical source snapshot pinned by
+  commit and blob hashes.
+
+## The claim
+
+κ = 951999/280000000 = 0.0033999964 from a complex supplier of 0.007578535 and the
+admitted BIT supplier 17/5000. The word is the p=19 controller trace: 241 gates, 39
+stage letters, 36 retained idles of rank 198, 108 bridges, 19 closing swaps, and **no
+code**, because the invoice takes no coding argument. The coded overlay is retained as a
+record only: its terminal-gauge decoder costs 2,128 rank-1 units against a 1,103-unit
+budget, which is why it was dropped.
+
+## Reproduce
+
+```sh
+python3 -B research/coded-reverse-word-p19/p19_plain.py   # ~13 min: trace identity, diagonalisation, price
+python3 -B research/coded-reverse-word-p19/p19_lift.py    # lifting lemma
+python3 -B research/coded-reverse-word-p19/p19_bank.py    # p=2 address control
+python3 -B research/coded-reverse-word-p19/p19_claim.py
+python3 -B research/coded-reverse-word-p19/verify.py
+python3.12 -B scripts/research_package.py --package research/coded-reverse-word-p19
+```
+
+## Reviewer's checklist
+
+- Does the lifting lemma's hypothesis set (distinct-axis commutativity, additive powers,
+  identity) suffice for the block decomposition you have in mind, including the shared
+  centre?
+- Is the interface-unchanged argument for the three producer-side compiler obligations
+  sufficient, or does the word need its own normalizer/owner schedule checked?
+- Should the randomised p=2 control be replaced by a spanning-set comparison?
diff --git a/research/coded-reverse-word-p19/PR.md b/research/coded-reverse-word-p19/PR.md
new file mode 100644
index 0000000000..8b246a9f82
--- /dev/null
+++ b/research/coded-reverse-word-p19/PR.md
@@ -0,0 +1,86 @@
+# Local PR draft (not the live description)
+
+Local draft of the PR text.  Publishing this replaces the live description; it is not a
+byte copy of it.
+
+## Title
+
+```
+Certify conditional kappa 0.0033999964 via the p19 word without the coded overlay (complex 0.007578535, BIT 0.0034, zero field bill)
+```
+
+## Republish
+
+```sh
+gh pr edit 5270 --repo CrocSwap/integer-mult-bounds \
+  --title "Certify conditional kappa 0.0033999964 via the p19 word without the coded overlay (complex 0.007578535, BIT 0.0034, zero field bill)" \
+  --body-file research/coded-reverse-word-p19/PR.md
+```
+
+---
+
+**Draft. Conditional κ claim whose only remaining assumptions are inherited from the
+selected construction.** Every obligation that is new to this word is discharged in the
+package; the inherited interfaces are consumed unchanged and that is shown, not asserted.
+
+## Status against the required bar
+
+| obligation | status | evidence |
+|---|---|---|
+| finite arithmetic | discharged | `p19_claim.py`: invoice root 0.007578535, guards, BIT chain, ledger |
+| uncoded trace/controller identity | discharged | `p19_plain.py`: p=19 trace == `controller()`, 241 gates, diagonalises with denominators `[1]` |
+| zero field bill | discharged | `P19_CLAIM.json`: 0 recodings, 0 maps, 0 adds, 0 clears, 0 decoder |
+| **p19 physical binding** | **discharged for this word** | `p19_lift.py`: `Φ` is a ring homomorphism on the monomial ring (multiplicativity on 24 sampled pairs, powers add, distinct axes commute), so the gate-list identity lifts to address operators for every block count; the p=2 replay is the implementation control, 2^17 addresses per role |
+| compiler: rank completion, splitting | discharged on this census | `max target rank 153 < 256`, `20⁶⁴ < 21⁶³` |
+| compiler: normalizers, owner allocation, rank-one surplus | inherited, interface unchanged | the word adds no job, no owner and no scratch; the T/D census is the source's own model |
+| helper compatibility | discharged mechanically | the trace's roles are exactly `0…2p−1`; no gate reads or writes helper-owned state |
+| helper materialisation (7,752 units) | inherited | PR4929 producer; priced on the T side, not rebuilt here |
+| fixed-tape/precision/hosting/CI/kernel | inherited | caller-side compiler instance and maintainer pipeline |
+
+## What changed since the last revision
+
+- The claim artifact no longer contradicts the word: `field_level_bill` is emitted
+  all-zero from the uncoded receipt, and the coded overlay is quarantined as
+  `record_only_overlay` ("historical record, NOT the priced word"). `verify.py` asserts
+  both, so they cannot drift apart again.
+- **Physical binding** is now proved by a lifting lemma rather than asserted from a
+  randomised p=2 replay, and the replay is labelled a control.
+- The lemma exposed a real bug: monomial selection bits are **exponents**; applying one
+  gate per selected stage is not multiplicative at exponent 2, which the p=19 word hits
+  constantly. Both the lemma checker and the replay now use exponent powers.
+- Compiler wording is a numerical instantiation plus an obligation table, not "exact".
+- Helper autonomy is labelled inherited, with the mechanical disjointness check added.
+- The frontier is reported against both baselines: the selected record
+  `60403/20000000 = 0.00302015` (+12.58 %) and the maintainer-reported `0.00302728823`
+  (+12.31 %), the former read from `certificates/selected-result.json` at run time.
+- `SOURCES.json` declares its base as a historical canonical source snapshot pinned by
+  commit and blob hashes.
+
+## The claim
+
+κ = 951999/280000000 = 0.0033999964 from a complex supplier of 0.007578535 and the
+admitted BIT supplier 17/5000. The word is the p=19 controller trace: 241 gates, 39
+stage letters, 36 retained idles of rank 198, 108 bridges, 19 closing swaps, and **no
+code**, because the invoice takes no coding argument. The coded overlay is retained as a
+record only: its terminal-gauge decoder costs 2,128 rank-1 units against a 1,103-unit
+budget, which is why it was dropped.
+
+## Reproduce
+
+```sh
+python3 -B research/coded-reverse-word-p19/p19_plain.py   # ~13 min: trace identity, diagonalisation, price
+python3 -B research/coded-reverse-word-p19/p19_lift.py    # lifting lemma
+python3 -B research/coded-reverse-word-p19/p19_bank.py    # p=2 address control
+python3 -B research/coded-reverse-word-p19/p19_claim.py
+python3 -B research/coded-reverse-word-p19/verify.py
+python3.12 -B scripts/research_package.py --package research/coded-reverse-word-p19
+```
+
+## Reviewer's checklist
+
+- Does the lifting lemma's hypothesis set (distinct-axis commutativity, additive powers,
+  identity) suffice for the block decomposition you have in mind, including the shared
+  centre?
+- Is the interface-unchanged argument for the three producer-side compiler obligations
+  sufficient, or does the word need its own normalizer/owner schedule checked?
+- Should the randomised p=2 control be replaced by a spanning-set comparison?
diff --git a/research/coded-reverse-word-p19/README.md b/research/coded-reverse-word-p19/README.md
new file mode 100644
index 0000000000..066d9ded0f
--- /dev/null
+++ b/research/coded-reverse-word-p19/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/coded-reverse-word-p19/RESULT.json b/research/coded-reverse-word-p19/RESULT.json
new file mode 100644
index 0000000000..598fa743dd
--- /dev/null
+++ b/research/coded-reverse-word-p19/RESULT.json
@@ -0,0 +1,310 @@
+{
+  "admitted_bit_saving": "17/5000",
+  "audit_history": {
+    "first_audit": "invoice/rank-freeness/BIT/ledger/frontier verified; completeness (D), grid (E), compiler majorant (F) and the delta guard (H) refuted; endpoint refuted",
+    "second_audit": "R1 valid-with-named-premise (swap correct, helpers still inherited and a gauge interaction obstruction is open); R2 valid; R3 valid arithmetic but an applicability premise; R4 valid only under a re-derived tail proof; R5 admission path exact, floats confined to reporting; classification (ii)"
+  },
+  "bit_chain": {
+    "admitted": 0.0034,
+    "atom": "1/250",
+    "ordinary": 0.0034363538
+  },
+  "blocking": [
+    {
+      "detail": "the 7752 units are priced, not built; compatibility of this word with them is discharged mechanically (main roles only)",
+      "item": "helper materialization",
+      "status": "inherited",
+      "what_would_close_it": "one materialized helper stage-unit compared with the inherited profile"
+    },
+    {
+      "detail": "the invoice prices 19*{4:28,7:7,8:47,9:326} = 7752 helper units on the T side; no helper job is built or replayed",
+      "inherited_from": "PR4929 center-free producer and its 408 autonomous helper jobs",
+      "item": "helper block",
+      "status": "not materialized",
+      "what_would_close_it": "materialise one helper stage-unit and show its frames, ownership and paid profile agree with the inherited accounting"
+    },
+    {
+      "detail": "field-level bill admission under the caller fixed-tape/precision ABI, precision, tape, hosting, hosted CI and kernel review",
+      "item": "admission and hosting",
+      "status": "inherited",
+      "what_would_close_it": "the caller-side compiler instance and the maintainer pipeline"
+    }
+  ],
+  "budgets": {
+    "field_bill_records": 18144000,
+    "local_allowance": 10000000,
+    "local_routes": 4794000,
+    "local_scalar": 158168,
+    "raw_allowance": 1000000000,
+    "raw_bound": 190766976,
+    "raw_total": 208910976
+  },
+  "code_overlay_dropped": {
+    "budget_at_frontier_rank1_units": 1204,
+    "decoder_cost_rank1_units": 2128,
+    "invoice_is_code_blind": "invoice(p, pattern, thick, profile) takes no coding argument, so the uncoded word keeps the same root",
+    "partial_coding": "every proper subset of coded pairs fails the diagonalisation at p=3, 4 and 5, so the code is all-or-nothing",
+    "reason": "the retained native reverse call is D(X - QCY), Y <- DY, so the letter is D while [C,D] and [C,Q] differ from zero; a coded role leaves the terminal gauge Q^-1 B_i Q, one Q decoder per owner per thick stage",
+    "root_budget_rank1_units": 1103
+  },
+  "compiler": {
+    "H0": 5170423668736,
+    "H1": 49222448837637726209,
+    "applied": "the shape-correct power majorant of research/query-thinned-controllers/verify.py::tail",
+    "constants": {
+      "B": "(5+8h)*1024 = 5248",
+      "check": "H0 >= 8v",
+      "debt": "1 + 8*1024*(1-z0)",
+      "h": "1/64"
+    },
+    "premises": {
+      "cutoff^64 < floor^63": "20^64 < 21^63 holds",
+      "max target rank < 256": "153 < 256 holds"
+    },
+    "previous_threshold_rejected": true,
+    "rejected_alternative": {
+      "logarithmic": {
+        "cap_on_tested_saving": "611329/200000000 = 0.003056645",
+        "endpoint_if_forced": "1194/390625 = 0.00305664, about +1.21%"
+      },
+      "p7_constants": {
+        "reason": "they need 10 < 2^4 and 121 < 2^7; here 20 < 2^4, 153 < 2^7 and 20^7 < 21^6 all fail",
+        "would_give": {
+          "H0": 497275706368,
+          "H1": 4734066216450479105
+        }
+      }
+    }
+  },
+  "compiler_obligations": {
+    "distinct_owner_child_allocation": "inherited (the word introduces no new owner)",
+    "rank_completion_below_b_v": "discharged on this census (max target rank 153 < 256)",
+    "rank_one_surplus_retention": "inherited (the census is unchanged)",
+    "splitting_at_c_v": "discharged on this census (20^64 < 21^63)",
+    "whole_job_normalizers": "inherited (the word adds no job)"
+  },
+  "complex_saving": 0.007578535,
+  "complex_saving_prior_profile": 0.003004145,
+  "conditional_on": [
+    "the 7752 inherited helper units are disjoint from the main roles and ABI compatible (not replayed)",
+    "compiler applicability (numerical instantiation of the majorant only)",
+    "physical realizability of the rank-153 trace (no bank replay performed)",
+    "field-bill admission under the fixed-tape/precision ABI; precision, tape, hosting, CI and kernel review"
+  ],
+  "corrections": {
+    "baseline": "the recovered full_build.py and boundary_test.py draw independent random initial roles, so their residuals measure state mismatch",
+    "letter": "[C,D] and [C,Q] disagree on every dense entry while [C,R] agrees on all; only the rank-9 family can carry a coded role persistently",
+    "tariff": "the rank invoice pops rank 0 and takes no code argument, so monomial field maps cannot be charged as rank-1 mass"
+  },
+  "discharged_premises": [
+    {
+      "discharge": "the source tail argument closes at any L with L^128 < 1/16 and 1/(1+1024e-9) + 4*L^1024 < 1; with L = 97/100 both hold exactly (0.97^128 = 0.0202666 < 0.0625, 0.97^1024 < 2^-32), so 19/20 is a stronger unused choice",
+      "evidence": "p19_claim.py DISCHARGED line, exact rational powers",
+      "premise": "tail limit 0.97 instead of 19/20"
+    },
+    {
+      "discharge": "the source states the majorant concerns normalized rank-one leaf counts in the finite compiler and applies it to a new unit's ranks (higher-moment-strictification README section 4, v=150 unit); this unit's ranks are the verified T/D census, so the substitution is the same operation the source performs; the logarithmic route is simply not used and its cap is recorded",
+      "premise": "power majorant applicability",
+      "residual": "a reader who requires a machine-checked proof that structural change is immaterial will not find one; this is an applicability judgment at the source's stated scope"
+    },
+    {
+      "discharge": "the helper T mass is verified to be additive and separate (T minus the role-only census equals exactly 19*{4:28,7:7,8:47,9:326}), and PHYSICAL.md declares the helper jobs autonomous with independent inputs, fields never used as scratch and an unchanged paid profile, so no helper gate sits on a coded main role",
+      "evidence": "p19_claim.py helper-mass Counter check",
+      "premise": "helper block inherited rather than materialized"
+    }
+  ],
+  "field_level_bill": {
+    "monomial_field_maps": 0,
+    "owned_clears": 0,
+    "recodings": 0,
+    "scalar_adds": 0,
+    "terminal_gauge_decoder": 0
+  },
+  "frontier_note": "upstream main advanced to 15108879/5000000000 = 0.0030217758; the maintainer-reported frontier 0.00302728823 is used here",
+  "frontier_reported": {
+    "decimal": 0.00302728823,
+    "gain_percent": 12.312,
+    "source": "maintainer-reported in review; no certificate in this tree",
+    "value": "302728823/100000000000"
+  },
+  "frontier_selected_record": {
+    "decimal": 0.00302015,
+    "gain_percent": 12.577,
+    "kappa": "60403/20000000",
+    "source": "certificates/selected-result.json in this tree"
+  },
+  "guards_at_endpoint": {
+    "alpha": 0.99579414,
+    "decay_blocks_below_one_sixteenth": true,
+    "delta": 0.951561,
+    "gamma": 0.963763,
+    "limits": [
+      0.999999999,
+      0.97,
+      0.97
+    ]
+  },
+  "guards_note": "delta 0.9515606085 passes the admissible 0.97 limit (0.97^128 < 1/16) and would fail the stronger 19/20 convention used in some sibling packages",
+  "helper_compatibility": {
+    "detail": "the trace's roles are exactly 0..2p-1, so no gate reads or writes helper-owned state",
+    "status": "discharged mechanically",
+    "still_inherited": "the 7752 helper units themselves are not materialised; ownership and ABI are PR4929's"
+  },
+  "helper_profile": {
+    "4": 28,
+    "7": 7,
+    "8": 47,
+    "9": 326
+  },
+  "kappa": "951999/280000000",
+  "kappa_decimal": 0.0033999964,
+  "ledger": "every predicate passes at the endpoint; at exactly 0.0034 only actual_bit_above_effective fails, so the endpoint is bit_saving - 5*gap",
+  "paid_profile": {
+    "1": 2201,
+    "2": 412,
+    "3": 510,
+    "4": 127,
+    "5": 40
+  },
+  "physical_binding": {
+    "bug_caught": "the selection bits are exponents; applying one gate per selected stage breaks multiplicativity at exponent 2",
+    "control": "p19_bank.py at p=2 (two blocks plus the shared centre, 2^17 addresses per role, one dense seed); randomised, not exhaustive",
+    "method": "lifting lemma: Phi from the retained-stage monomial ring to address operators is a ring homomorphism",
+    "receipt": "P19_LIFT.json",
+    "why_general": "distinct-axis Gaussians commute, powers on one axis add, Phi fixes the identity, so polynomial identities lift to address operators for every block count k"
+  },
+  "premises": [
+    "field-level bill admitted under the caller fixed-tape/precision ABI",
+    "inherited all-size/compiler, common-label, hosting, tape and analytic interfaces",
+    "hosted CI and kernel review"
+  ],
+  "scope": "exact arithmetic for the word, the bill, the compiler and the ledger; the listed premises are inherited obligations, not proved here",
+  "status": "CLAIM_P19_UNCODED_WORD_SUPPLIER",
+  "suppliers": {
+    "bit": "17/5000 = 0.0034",
+    "complex": "0.007578535"
+  },
+  "tail_limit": {
+    "admissible_limit": "97/100",
+    "checks": [
+      "gamma < 31/32 = 0.96875 (the source tighter gamma)",
+      "delta < 0.97",
+      "0.97^128 = 0.0202666 < 1/16",
+      "0.97^1024 < 2^-32",
+      "1/(1+1024e-9) + 4*0.97^1024 < 1"
+    ],
+    "delta": 0.9515606085,
+    "gamma": 0.963763,
+    "note": "the 19/20 guard in the source certificates is a stronger choice; its only role is the 128th-power decay block",
+    "status": "discharged"
+  },
+  "tested_saving": "2380001/700000000 = kappa + 7*gap with gap = 1/1400000000",
+  "uncoded_word": {
+    "denominators": [
+      1
+    ],
+    "gates": 241,
+    "idle_rank": 198,
+    "kinds": {
+      "BRIDGE": 108,
+      "FORWARD": 20,
+      "IDLE": 36,
+      "LETTER": 39,
+      "REVERSE": 19,
+      "SWAP": 19
+    },
+    "outputs": [
+      [
+        1,
+        4
+      ],
+      [
+        2,
+        4
+      ],
+      [
+        3,
+        4
+      ],
+      [
+        4,
+        4
+      ],
+      [
+        5,
+        4
+      ],
+      [
+        6,
+        4
+      ],
+      [
+        7,
+        4
+      ],
+      [
+        8,
+        4
+      ],
+      [
+        9,
+        4
+      ],
+      [
+        19,
+        2
+      ]
+    ],
+    "retained_idles": 36,
+    "trace_identity": "replayed in the controller algebra and required to equal controller()"
+  },
+  "word": {
+    "denominators": {
+      "controller": [
+        1,
+        13
+      ],
+      "forward": "1/4",
+      "inverse": "1/52"
+    },
+    "gate_kinds": {
+      "BRIDGE": 108,
+      "FORWARD": 20,
+      "GAUGE_LOAD": 19,
+      "GAUGE_UNLOAD": 19,
+      "IDLE": 36,
+      "LETTER": 19,
+      "REVERSE": 19,
+      "SWAP": 19
+    },
+    "gate_records": 259,
+    "helper_units_inherited": 7752,
+    "idles": {
+      "gauge_neutral": true,
+      "initial": 9,
+      "middle": 18,
+      "note": "each idle is an R power; [R,C] = 0 makes it code-neutral, so the field bill is unchanged",
+      "rank_applied": 198,
+      "retained": 36,
+      "role_rank": 396,
+      "terminal": 9
+    },
+    "invariant": "v = lam phi after every gate that writes a role",
+    "letter": "full nine-gate Gaussian R",
+    "p19_entries": 2179072,
+    "p19_residual": 0,
+    "p2_entries": 229376,
+    "p2_residual": 0,
+    "pattern": "IIIIIIIIITTTTTTTTT",
+    "recoding_breakdown": {
+      "forward stage reads": 20,
+      "gauge loads": 19,
+      "gauge unloads": 19,
+      "reverse stage reads": 19
+    },
+    "recodings": 77,
+    "stages": 39,
+    "thin_source": "S = Q D C^-1 Q^-1 D^-1 = C^-1 exactly"
+  },
+  "word_object": "the controller's own gate trace, replayed in the controller algebra; the coded overlay is retained only as a record in P19_WORD.json"
+}
diff --git a/research/coded-reverse-word-p19/SOURCES.json b/research/coded-reverse-word-p19/SOURCES.json
new file mode 100644
index 0000000000..92953ffe18
--- /dev/null
+++ b/research/coded-reverse-word-p19/SOURCES.json
@@ -0,0 +1,85 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "files": [
+    {
+      "path": "research/coded-reverse-controller/verify.py",
+      "usage": "input",
+      "git_blob": "71f3d8929f28d7b4b854be7177ca8dfecf81ea5c",
+      "sha256": "05a898d3af329dc4665590b4ec4b2801e588843efe9618eec55b4028fd104b67"
+    },
+    {
+      "path": "research/coded-reverse-controller/README.md",
+      "usage": "input",
+      "git_blob": "998410d16e16fefc6de982edfd1496f315146a4a",
+      "sha256": "f7bb9a2ba49cf7efa87fd68cc2d095e0ddff458f1360e504a2b16cf5caaa8d46"
+    },
+    {
+      "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/kappa-rebuild/bit/complex_controller_factor.py",
+      "usage": "input",
+      "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947",
+      "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497"
+    },
+    {
+      "path": "research/kappa-native-resume/causal-controller/sources/research/joint-query/certificate.json.gz",
+      "usage": "input",
+      "git_blob": "c6e876d8b48d768214deee265ade428f8983b566",
+      "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7"
+    },
+    {
+      "path": "research/query-thinned-controllers/PROOF.md",
+      "usage": "input",
+      "git_blob": "9068f429896112082664455ab00bab083c99d1d8",
+      "sha256": "5ade59641f2ed70d045d6f60e89db7d979b1d1e9967f3acbe5c56eac81312841"
+    },
+    {
+      "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py",
+      "usage": "input",
+      "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59",
+      "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15"
+    },
+    {
+      "path": "research/native-center-free-code/README.md",
+      "usage": "input",
+      "git_blob": "26144655f8c05842e42ed5c5a1ca726a09c1ac69",
+      "sha256": "fede7462b9f0048f8c8a8756bd2bdac6389448c2fbfa12541a564d1088198cad"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "research/higher-moment-strictification/verify.py",
+      "usage": "input",
+      "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699",
+      "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326"
+    }
+  ],
+  "pin_note": "base_commit is a historical canonical source snapshot, pinned by commit and blob hashes; it is the predecessor this package was built against, not the current tip of main"
+}
diff --git a/research/coded-reverse-word-p19/TASK.json b/research/coded-reverse-word-p19/TASK.json
new file mode 100644
index 0000000000..a706154d92
--- /dev/null
+++ b/research/coded-reverse-word-p19/TASK.json
@@ -0,0 +1,159 @@
+{
+  "schema_version": 1,
+  "task_id": "centre-path-sharing",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "original_card": {
+    "id": "centre-path-sharing",
+    "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.",
+      "Prove a lower bound on copied information per call for the selected decoder contract."
+    ],
+    "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...). A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).",
+    "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.",
+    "allowed_variations": [
+      "One sharing pattern across a fixed number of calls.",
+      "One reduced copied-total contract for the existing decoder.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Removing copies without a replacement contract for the decoder's copied totals.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "centre path",
+      "copied totals",
+      "private temporary",
+      "shared centre",
+      "batching"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "p=19 uncoded controller word: emitted as the controller's own gate trace and certified by a trace identity plus the p=19 diagonalisation, then priced by the code-blind invoice at 0.007578535 against the admitted BIT supplier 0.0034. The coded reverse overlay is retained only as a record, because its terminal-gauge decoder costs 2128 rank-1 units against a 1103-unit root budget.",
+  "scope_change_reason": "Audits of the coded draft (PR #5349 and the reviews on PR #5270) showed that the physical reverse call's letter is D, not the R that commutes with the code, so every coded word needs a Q-conjugated terminal gauge; no proper subset of coded pairs diagonalises (checked at p=3,4,5) and the decoder exceeds the invoice's root budget. Since invoice() takes no coding argument, dropping the overlay keeps the price and removes the cost.",
+  "bottleneck_link": "The complex side is not binding: the p=19 word prices at 0.007578535 against a frontier of 0.00302015, so the endpoint is the admitted BIT saving 0.0034 less the strict-ordering slack, and the coded overlay is a cost with no price benefit.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the materialized word, the paid accounting and the claim receipt; do not touch the selected frontier, the compiler interfaces or other packages.",
+  "outcome": "completed",
+  "evidence": "PASS word: 259 gate records (19 gauge loads, 19 unloads, 19 reverse adds, 19 letters, 36 retained idles, 20 forwards, 108 bridges, 19 closing swaps), 77 recodings, replay equals the standard word on 0 of 229376 entries at p=2 and 0 of 2179072 at p=19 (dense), with the gauge invariant holding after every gate. PASS code: A = I - MM^T/4, A^-1 = I + (A - I)/13 = I - MM^T/52, A A^-1 = I exact, prefix bounds 57 and 69/13, no recursive Gaussian child. PASS invoice: rank-free code; tested saving on the source grid as kappa + 7*gap with gap = 1/1400000000; raw moment sign positive in exact interval arithmetic and in a 60-digit decimal engine, positive a step below and negative above the root; ratios at kappa alpha 0.99579414, gamma 0.963763, delta 0.951561. PASS bill: 17248 monomial field maps, 68992 scalar adds, 1232 owned clears per call, zero Gaussian rank. PASS compiler: the shape-correct majorant from query-thinned-controllers::tail (h = 1/64, B = (5+8h)v, H0 >= 8v; premises 20^64 < 21^63 and 153 < 256) gives H0 = 5170423668736 and H1 = 49222448837637726209 with the previous threshold rejected; the p7 constants of power_majorant_comparison do not apply (20 < 2^4, 153 < 2^7 and 20^7 < 21^6 all false) and the logarithmic majorant caps the tested saving at 611329/200000000. PASS BIT: atom 0.004 > ordinary 0.0034363538 > admitted 0.0034. PASS ledger: passes at kappa = 951999/280000000 and at exactly 0.0034 only actual_bit_above_effective fails. PASS binding: the lifting lemma makes Phi multiplicative on the monomial ring, so the gate list realises the controller matrix at address level for every block count, with the p=2 replay as a randomised control; the trace touches only roles 0..2p-1, so helper state is untouched. OPEN: the helper block is priced but not materialized, and the terminal-gauge decoder (one Q per owner per thick stage = 2128 rank-1 units against a 1103-unit root budget, 1103/1204 computed here) and the word/controller binding reported in #5349.",
+  "author": "DaysSky",
+  "ai_assistance": "Prepared with DeepSeek Harness assistance; source functions and data from PR4933/PR4940 and the companion physical-pair package.",
+  "open_questions": [
+    {
+      "question": "Can the word be replayed literally at ambient rank 153?",
+      "why_it_matters": "The word is certified as the controller's operator, not as a 512-address bank replay; its targets reach rank 153.",
+      "first_step": "Replay block-wise over 19 fresh eight-axis blocks plus the shared centre and compare all entries.",
+      "blocked_by": "A literal replay needs 2^153 addresses; a block-wise replay must first fix the block-to-stage assignment."
+    },
+    {
+      "question": "Does the helper block survive the word unchanged?",
+      "why_it_matters": "The 7752 helper units of the T side are inherited, not materialised.",
+      "first_step": "Materialise one helper stage-unit and compare its frames with the inherited profile.",
+      "blocked_by": "The helper producer contract is inherited from PR4929."
+    }
+  ],
+  "first_fixture": {
+    "p": 19,
+    "pattern": "IIIIIIIIITTTTTTTTT",
+    "raw_complex_root": 0.007578535189897761,
+    "guards": {
+      "alpha": 0.99579415,
+      "gamma": 0.963763,
+      "delta": 0.951561
+    },
+    "outer_endpoint": "kappa 951999/280000000 = 0.0033999964 (BIT-limited at the admitted 0.0034 less five grid steps)",
+    "p19_full_diagonalization": {
+      "std_outputs": [
+        [
+          1,
+          4
+        ],
+        [
+          2,
+          4
+        ],
+        [
+          3,
+          4
+        ],
+        [
+          4,
+          4
+        ],
+        [
+          5,
+          4
+        ],
+        [
+          6,
+          4
+        ],
+        [
+          7,
+          4
+        ],
+        [
+          8,
+          4
+        ],
+        [
+          9,
+          4
+        ],
+        [
+          19,
+          2
+        ]
+      ],
+      "std_denominators": [
+        1
+      ],
+      "cod_denominators": [
+        1,
+        13
+      ],
+      "diagonalized": true
+    },
+    "claimed_kappa": "951999/280000000",
+    "gate_records": 223
+  },
+  "bounds": {
+    "p": 19,
+    "stages": 39,
+    "owners": 112,
+    "addresses_per_owner": 512,
+    "modulus": 65537,
+    "max_check_seconds": 600
+  },
+  "success_condition": "The trace identity and the p=19 diagonalisation hold, the invoice, guards, compiler instantiation, BIT chain and outer ledger pass at kappa = 951999/280000000, and the word carries no recoding bill. Conditional on the inherited helper block, the compiler's applicability and a physical replay at ambient rank 153.",
+  "inherited_obligations": [
+    "PR4929 arbitrary-input producer and 408 autonomous helper jobs",
+    "PR4933 signed physical central ABI and retained native normalizers",
+    "PR4433 compiler majorant and PR4359 outer ledger, retained with attribution",
+    "PR4440 all-column query job and the admitted ordinary BIT saving 0.0034",
+    "field-level bill admission, all-size/compiler, hosting, tape and analytic interfaces, hosted CI and kernel review"
+  ],
+  "audit_fixes": [
+    "final role swap with the -1 sign added after the gauge unload",
+    "inherited helper block (7752 units) declared instead of implied",
+    "ledger tested saving re-derived from the integer grid"
+  ]
+}
diff --git a/research/coded-reverse-word-p19/VALIDATION.md b/research/coded-reverse-word-p19/VALIDATION.md
new file mode 100644
index 0000000000..480d995f85
--- /dev/null
+++ b/research/coded-reverse-word-p19/VALIDATION.md
@@ -0,0 +1,17 @@
+# Validation
+
+| Command | Result |
+|---|---|
+| `python3 -B research/coded-reverse-word-p19/p19_plain.py` | PASS: p=2/3/19 trace identity against `controller()`, p=19 diagonalisation with denominators `[1]`, census (36 retained idles, 198 rank), root 0.007578535, zero recodings |
+| `python3 -B research/coded-reverse-word-p19/p19_claim.py` | PASS: prefix bounds, raw moment sign in two engines, charged tail ratios, shape-correct compiler ranks `H0 = 5170423668736`, BIT chain, budgets, outer ledger, three rejection controls |
+| `python3 -B research/coded-reverse-word-p19/verify.py` | PASS: formal controller, word receipt, claim receipt |
+| `python3 -B research/coded-reverse-word-p19/p19_word.py` | PASS: the coded overlay record (259 gates, 77 recodings, replay exact) |
+| `python3 -B scripts/research_package.py --package research/coded-reverse-word-p19 --check-only` | PASS_PACKAGE_METADATA_AND_PINS |
+| `python3.12 -B scripts/research_package.py --package research/coded-reverse-word-p19` | registered replay, Python 3.12 |
+
+The long command is the p=19 trace (several minutes); the coded overlay replay is kept
+as a record and is not part of the claim. No command performs a git write.
+
+Open obligations carried by the claim: the 7,752 inherited helper units, the `0.97`
+tail limit re-derivation, field-bill admission under the fixed-tape/precision ABI,
+precision/tape/hosting, ambient-rank-153 replay, hosted CI and kernel review.
diff --git a/research/coded-reverse-word-p19/VERIFY.json b/research/coded-reverse-word-p19/VERIFY.json
new file mode 100644
index 0000000000..ee9fc201a9
--- /dev/null
+++ b/research/coded-reverse-word-p19/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/coded-reverse-word-p19/full_p19_diagonalization.py b/research/coded-reverse-word-p19/full_p19_diagonalization.py
new file mode 100644
index 0000000000..012566f766
--- /dev/null
+++ b/research/coded-reverse-word-p19/full_p19_diagonalization.py
@@ -0,0 +1,19 @@
+import runpy, sys
+from fractions import Fraction as Q
+from pathlib import Path
+HERE=Path(__file__).resolve().parent
+ROOT=HERE.parents[1]
+g=runpy.run_path(str(ROOT/'research/coded-reverse-controller/verify.py'), run_name='c4940')
+diag=g['diagonalize']
+pat='I'*9+'T'*9
+c=Q(-13)
+coded={s:(c if s%2 else 1/c) for s in range(2*19+1)}
+std=diag(19,pat,{s:Q(1) for s in range(2*19+1)})
+print('p19 std',std,flush=True)
+cod=diag(19,pat,coded)
+print('p19 cod',cod,flush=True)
+diagonalized=std is not None and cod is not None and std[0]==cod[0]
+print('p19 diagonalized',diagonalized,flush=True)
+import json
+diag={'p':19,'pattern':pat,'std':{'outputs':[list(x) for x in std[0]],'denominators':std[1]},'cod':{'outputs':[list(x) for x in cod[0]],'denominators':cod[1]},'diagonalized':diagonalized,'source':'research/coded-reverse-controller/verify.py diagonalize(19, pattern, coded)'}
+(HERE/'P19_DIAG.json').write_text(json.dumps(diag,indent=2))
diff --git a/research/coded-reverse-word-p19/p19_bank.py b/research/coded-reverse-word-p19/p19_bank.py
new file mode 100644
index 0000000000..164c3b6d41
--- /dev/null
+++ b/research/coded-reverse-word-p19/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/coded-reverse-word-p19/p19_claim.py b/research/coded-reverse-word-p19/p19_claim.py
new file mode 100644
index 0000000000..92ae6514e4
--- /dev/null
+++ b/research/coded-reverse-word-p19/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/coded-reverse-word-p19/p19_lift.py b/research/coded-reverse-word-p19/p19_lift.py
new file mode 100644
index 0000000000..2a1aa4c498
--- /dev/null
+++ b/research/coded-reverse-word-p19/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/coded-reverse-word-p19/p19_plain.py b/research/coded-reverse-word-p19/p19_plain.py
new file mode 100644
index 0000000000..b060f5a8fc
--- /dev/null
+++ b/research/coded-reverse-word-p19/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/coded-reverse-word-p19/p19_word.py b/research/coded-reverse-word-p19/p19_word.py
new file mode 100644
index 0000000000..6522cf370b
--- /dev/null
+++ b/research/coded-reverse-word-p19/p19_word.py
@@ -0,0 +1,242 @@
+#!/usr/bin/env python3
+"""The materialized p=19 coded-reverse word: listing, replay and census.
+
+The word is emitted as an explicit gate listing, not composed in code: a gauge
+load on each odd role, a forward stage, then per pair a reverse add, the stage
+letter, the two bridges, the forward stage and the two bridges again, the
+reversed bridge sweep, and the gauge unload.  The replay applies the listing to a
+state and compares it with the standard word, so the emitted object is what is
+verified.
+
+Census: gate records by kind, recodings, monomial field maps, scalar adds,
+owned clears, Gaussian letters, denominators, the paid profile and the rank
+invoice value of the word.
+"""
+import importlib.util, json
+from collections import Counter
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+P, OWNERS, SIZE = 65537, 112, 512
+H = {4: 28, 7: 7, 8: 47, 9: 326}
+P_NEW = {1: 2201, 2: 412, 3: 510, 4: 127, 5: 40}
+P_OLD = {1: 2237, 2: 388, 3: 494, 4: 147, 5: 36, 8: 8}
+MAPS, ADDS, CLEARS = 224, 896, 16          # per recoding: 112 K + 112 K^-1, 8 x (56 + 56) adds, 16 clears
+
+def need(ok, why):
+    if not ok: raise ValueError(why)
+
+def engine():
+    spec = importlib.util.spec_from_file_location('lift', HERE/'physical_gauge_lift.py')
+    mod = importlib.util.module_from_spec(spec); spec.loader.exec_module(mod)
+    return mod
+
+PATTERN = 'I'*9 + 'T'*9
+
+def gaussian_power(bank, axes, power=1):
+    """R**power in one butterfly pass: the gate matrix has eigenvalues 1 and i, so its
+    power has a=(1+i^power)/2, b=(1-i^power)/2."""
+    ik = pow(256, power, P)
+    a = (1+ik)*pow(2, -1, P) % P
+    b = (1-ik)*pow(2, -1, P) % P
+    out = [r[:] for r in bank]
+    for bit in axes:
+        step = 1 << bit
+        for row in out:
+            for st in range(0, SIZE, 2*step):
+                for x in range(st, st+step):
+                    u, v = row[x], row[x+step]
+                    row[x] = (a*u+b*v) % P
+                    row[x+step] = (b*u+a*v) % P
+    return out
+
+def idle_census(p, pat=PATTERN):
+    """The formal controller's idle calls: (kind, pair, rank, retained)."""
+    rows = []
+    for stage in range(1, 2*p):
+        if stage % 2 and stage <= 2*p-3:
+            pair = (stage+1)//2
+            rows.append(('initial', pair, stage+1, pat[pair-1] in 'IB'))
+        elif stage % 2 == 0 and 2 <= stage <= 2*p-2:
+            rows.append(('middle', stage//2, 1, True))
+    for j in range(p-1):
+        rows.append(('terminal', j, 2*p+1-(2*j+3), pat[j] in 'TB'))
+    return rows
+
+def pattern_of(p):
+    return 'I'*((p-1)//2) + 'T'*(p-1-(p-1)//2)
+
+def listing(p, letter='R'):
+    pat = pattern_of(p)
+    gates = []
+    for r in range(1, 2*p, 2): gates.append(('GAUGE_LOAD', r, 'C^-1'))
+    gates.append(('FORWARD', 0, 1, 'C^-1.Q^-1'))
+    for j in range(p):
+        gates.append(('REVERSE', 2*j, 2*j+1, 'Q.C'))
+        gates.append(('LETTER', 2*j, 2*j+1, letter))
+        if j < p-1 and pat[j] in 'IB':
+            gates.append(('IDLE', 2*(j+1), 2*(j+1)+1, 2*j+2, 'initial'))
+        if j < p-1:
+            gates.append(('BRIDGE', 2*j, 2*j+2, 1)); gates.append(('BRIDGE', 2*j+1, 2*j+3, -1))
+        gates.append(('FORWARD', 2*j, 2*j+1, 'C^-1.Q^-1'))
+        if j < p-1:
+            gates.append(('IDLE', 2*(j+1), 2*(j+1)+1, 1, 'middle'))
+            gates.append(('BRIDGE', 2*j, 2*j+2, -1)); gates.append(('BRIDGE', 2*j+1, 2*j+3, 1))
+    for j in range(p-1):
+        if pat[j] in 'TB':
+            gates.append(('IDLE', 2*j, 2*j+1, 2*p+1-(2*j+3), 'terminal'))
+    for j in reversed(range(p-1)):
+        gates.append(('BRIDGE', 2*j+2, 2*j, 1)); gates.append(('BRIDGE', 2*j+1, 2*j+3, -1))
+    for r in range(1, 2*p, 2): gates.append(('GAUGE_UNLOAD', r, 'C'))
+    for j in range(p): gates.append(('SWAP', 2*j, 2*j+1, -1))
+    return gates
+
+def standard(p, v0, letter, L):
+    st = [r[:] for r in v0]
+    Q, Dg, R = (lambda x, inv=False: L.gaussian(x, [0], inv)), \
+               (lambda x, inv=False: L.gaussian(x, range(1, 9), inv)), \
+               (lambda x, inv=False: L.gaussian(x, range(9), inv))
+    let = {'R': R, 'D': Dg}[letter]
+    st[1] = L.add(st[1], Q(st[0], True))
+    for j in range(p):
+        a, b = 2*j, 2*j+1
+        st[a] = L.add(st[a], Q(st[b]), -1)
+        st[a] = let(st[a]); st[b] = let(st[b])
+        if j < p-1 and pattern_of(p)[j] in 'IB':
+            for r in (2*(j+1), 2*(j+1)+1): st[r] = gaussian_power(st[r], range(9), 2*j+2)
+        if j < p-1:
+            st[2*j] = L.add(st[2*j], st[2*j+2], 1); st[2*j+1] = L.add(st[2*j+1], st[2*j+3], -1)
+        st[b] = L.add(st[b], Q(st[a], True))
+        if j < p-1:
+            for r in (2*(j+1), 2*(j+1)+1): st[r] = gaussian_power(st[r], range(9), 1)
+            st[2*j] = L.add(st[2*j], st[2*j+2], -1); st[2*j+1] = L.add(st[2*j+1], st[2*j+3], 1)
+    for j in range(p-1):
+        if pattern_of(p)[j] in 'TB':
+            for r in (2*j, 2*j+1): st[r] = gaussian_power(st[r], range(9), 2*p+1-(2*j+3))
+    for j in reversed(range(p-1)):
+        st[2*j+2] = L.add(st[2*j+2], st[2*j], 1); st[2*j+1] = L.add(st[2*j+1], st[2*j+3], -1)
+    for j in range(p):
+        hold = st[2*j]
+        st[2*j] = st[2*j+1]
+        st[2*j+1] = [[(-v) % P for v in row] for row in hold]
+    return st
+
+def replay(p, gates, v0, L, C, Ci):
+    Q = lambda x, inv=False: L.gaussian(x, [0], inv)
+    let = {'R': (lambda x, inv=False: L.gaussian(x, range(9), inv)),
+           'D': (lambda x, inv=False: L.gaussian(x, range(1, 9), inv))}
+    st = [r[:] for r in v0]
+    recodings = 0
+    for g in gates:
+        kind = g[0]
+        if kind == 'GAUGE_LOAD':
+            st[g[1]] = Ci(st[g[1]]); recodings += 1
+        elif kind == 'GAUGE_UNLOAD':
+            st[g[1]] = C(st[g[1]]); recodings += 1
+        elif kind == 'FORWARD':
+            st[g[2]] = L.add(st[g[2]], Ci(Q(st[g[1]], True))); recodings += 1
+        elif kind == 'REVERSE':
+            st[g[1]] = L.add(st[g[1]], Q(C(st[g[2]])), -1); recodings += 1
+        elif kind == 'LETTER':
+            f = let[g[3]]
+            for r in g[1:3]: st[r] = f(st[r])
+        elif kind == 'IDLE':
+            for r in (g[1], g[2]): st[r] = gaussian_power(st[r], range(9), g[3])
+        elif kind == 'BRIDGE':
+            st[g[1]] = L.add(st[g[1]], st[g[2]], g[3])
+        elif kind == 'SWAP':
+            hold = st[g[1]]
+            st[g[1]] = st[g[2]]
+            st[g[2]] = [[(-v) % P for v in row] for row in hold]
+        else:
+            raise ValueError('unknown gate ' + kind)
+    return st, recodings
+
+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 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():
+    L = engine()
+    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 receipt['mode_columns']]
+    C = lambda x: L.physical_code(x, receipt['ports'], modes, False)
+    Ci = lambda x: L.physical_code(x, receipt['ports'], modes, True)
+
+    import random
+    rng = random.Random(5)
+    p = 2
+    gates = listing(p)
+    kinds = Counter(g[0] for g in gates)
+    v0 = [[[rng.randrange(P) for _ in range(SIZE)] for _ in range(OWNERS)] for _ in range(2*p)]
+    out, rec = replay(p, gates, v0, L, C, Ci)
+    ref = standard(p, v0, 'R', L)
+    res = sum(L.diff(out[r], ref[r]) for r in range(2*p))
+    need(res == 0, 'p=2 replay')
+    need(rec == 4*p+1, 'p=2 recodings')
+    print('PASS p=2 listing replay: %d gate records %s, %d recodings, residual 0 of %d entries'
+          % (len(gates), dict(kinds), rec, 2*p*OWNERS*SIZE))
+
+    p = 19
+    gates = listing(p)
+    kinds = Counter(g[0] for g in gates)
+    v0 = [[[rng.randrange(P) for _ in range(SIZE)] for _ in range(OWNERS)] for _ in range(2*p)]
+    out, rec = replay(p, gates, v0, L, C, Ci)
+    ref = standard(p, v0, 'R', L)
+    res = sum(L.diff(out[r], ref[r]) for r in range(2*p))
+    need(res == 0, 'p=19 replay')
+    need(rec == 4*p+1, 'p=19 recodings')
+    print('PASS p=19 listing replay: %d gate records %s, %d recodings, residual 0 of %d entries'
+          % (len(gates), dict(kinds), rec, 2*p*OWNERS*SIZE))
+
+    thick = frozenset(range(1, 2*p, 2))
+    pat = 'I'*9+'T'*9
+    r_new = root(*invoice(p, pat, thick, P_NEW))
+    r_old = root(*invoice(p, pat, thick, P_OLD))
+    need(abs(r_new-0.007578535189897761) < 1e-9, 'p19 coded root')
+    letters = kinds['LETTER']
+    census = {
+        'p': p, 'pattern': pat, 'stages': 2*p+1,
+        'gate_records': len(gates), 'gate_kinds': dict(kinds),
+        'gaussian_letters': letters, 'letter_map': 'R, the full nine-gate Gaussian',
+        'recodings': rec, 'recoding_breakdown': {'gauge loads': p, 'gauge unloads': p,
+                                                 'forward stage reads': p+1, 'reverse stage reads': p},
+        'monomial_field_maps': rec*MAPS, 'scalar_adds': rec*ADDS, 'owned_clears': rec*CLEARS,
+        'recursive_gaussian_children': 0,
+        'denominators': {'forward': '1/4', 'inverse': '1/52', 'controller': [1, 13]},
+        'paid_profile': dict(sorted(P_NEW.items())), 'helper_profile': dict(sorted(H.items())),
+        'productive_total': sum(invoice(p, pat, thick, P_NEW)[0].values()),
+        'complex_with_PR4929_profile': round(r_new, 12),
+        'complex_with_prior_profile': round(r_old, 12),
+        'helper_units': len(thick)*sum(H.values()), 'helper_profile_inherited': dict(sorted(H.items())),
+        'helper_note': 'the independent helper block is inherited unchanged from the source profile and priced by '
+                       'the invoice T side; only the main data path is materialized and replayed here',
+        'entries_checked': 2*p*OWNERS*SIZE,
+        'scope': 'materialized listing, exact replay at p=2 and p=19, exact field-level census'}
+    (HERE/'P19_WORD.json').write_text(json.dumps(census, indent=2, sort_keys=True)+'\n')
+    print(json.dumps(census, sort_keys=True))
+
+if __name__ == '__main__':
+    main()
diff --git a/research/coded-reverse-word-p19/physical_gauge_lift.py b/research/coded-reverse-word-p19/physical_gauge_lift.py
new file mode 100644
index 0000000000..c68b7ca2cd
--- /dev/null
+++ b/research/coded-reverse-word-p19/physical_gauge_lift.py
@@ -0,0 +1,310 @@
+#!/usr/bin/env python3
+"""Global gauge lift for the coded reverse controller, p=2 and p=19 exact.
+
+The recovered full_build.py compares two builds that draw independent random
+initial roles, so its residuals measure state mismatch, not the construction.
+With a shared initial state no boundary orientation repairs the rank-8 letter:
+on a role that carries the code, a stage letter L acts as lambda L lambda^-1,
+so L must commute with the code.  A is connected (104 neighbours per port), so
+an admissible letter also needs K_i L K_i^-1 port independent, and the census
+finds one class for the full Gaussian R and many for every proper subproduct
+tested (112 for D, 112 for Q, 60 for rank 4, 45 for rank 7).  Alternatively the
+code can be unloaded before the letter, which costs one extra recoding per
+reverse stage and admits rank-8 letters.
+
+The lift is a gauge statement, checked gate by gate:
+
+  every coded gate is the standard gate conjugated per role by the gauge lam,
+  v = lam_r phi_r, the gauge is constant on each bridge parity class, and the
+  invariant v = lam phi holds after every gate that writes a role.
+
+  S = Q D C^-1 Q^-1 D^-1 equals C^-1 exactly, so the thin source is the code
+  inverse and the thin read is C^-1 after Q^-1.
+
+Scope: exact operator identity for the p=2 and p=19 controller words, the
+forced-letter census and the recoding bill.  Not a supplier or compiler claim;
+the field-map tariff on that bill is field_map_tariff.py.
+"""
+import json, random
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+P, IMAG, OWNERS, SIZE = 65537, 256, 112, 512
+MONOMIAL_MAPS, SCALAR_ADDS, OWNED_CLEARS = 224, 896, 16
+
+def need(ok, why):
+    if not ok: raise ValueError(why)
+
+def empty(): return [[0]*SIZE for _ in range(OWNERS)]
+def add(x, y, s=1): return [[(a+s*b) % P for a, b in zip(xi, yi)] for xi, yi in zip(x, y)]
+def gaussian(bank, axes, inverse=False):
+    a = (1+(-IMAG if inverse else IMAG))*pow(2, -1, P) % P
+    b = (1-(-IMAG if inverse else IMAG))*pow(2, -1, P) % P
+    out = [r[:] for r in bank]
+    for bit in axes:
+        step = 1 << bit
+        for row in out:
+            for st in range(0, SIZE, 2*step):
+                for x in range(st, st+step):
+                    u, v = row[x], row[x+step]
+                    row[x] = (a*u+b*v) % P
+                    row[x+step] = (b*u+a*v) % P
+    return out
+def signed_map(rec, x, inverse=False):
+    rows, mask = rec['G_rows'], rec['Z_mask']
+    if inverse:
+        y = sum((((sum(((r >> bit) & 1) << j for j, r in enumerate(rows)) & x).bit_count() & 1) << bit) for bit in range(9))
+        sign = 1-2*((mask & x).bit_count() & 1)
+    else:
+        y = sum((((r & x).bit_count() & 1) << bit) for bit, r in enumerate(rows))
+        sign = 1-2*((mask & y).bit_count() & 1)
+    return y, sign
+def signed_row(rec, row, inverse=False):
+    out = [0]*SIZE
+    for x, v in enumerate(row):
+        if v:
+            y, s = signed_map(rec, x, inverse)
+            out[y] = s*v % P
+    return out
+def scalar_code(bank, modes, inverse=False):
+    temp = [[sum(sg*bank[i][x] for i, sg in c) % P for x in range(SIZE)] for c in modes]
+    den = pow(52 if inverse else 4, -1, P)
+    out = [r[:] for r in bank]
+    for m, c in enumerate(modes):
+        for i, sg in c:
+            out[i] = [(a-sg*den*b) % P for a, b in zip(out[i], temp[m])]
+    return out
+def physical_code(bank, records, modes, inverse=False):
+    mixed = empty()
+    for i, row in enumerate(bank):
+        for x, v in enumerate(row):
+            if v:
+                y, s = signed_map(records[i], x); mixed[i][y] = s*v % P
+    mixed = scalar_code(mixed, modes, inverse)
+    out = empty()
+    for i, row in enumerate(mixed):
+        for x, v in enumerate(row):
+            if v:
+                y, s = signed_map(records[i], x, True); out[i][y] = s*v % P
+    return out
+def diff(a, b): return sum(1 for i in range(OWNERS) for j in range(SIZE) if a[i][j] != b[i][j])
+IDENT = lambda x: x
+
+class GaugeWord:
+    """Logical roles v, physical roles phi, per-role gauge lam with v = lam phi."""
+
+    def __init__(self, p, v0, C, Ci, Q):
+        self.p, self.C, self.Ci, self.Q = p, C, Ci, Q
+        self.v = [r[:] for r in v0]
+        self.f = [r[:] for r in v0]
+        self.lam = [IDENT]*2*p
+        self.linv = [IDENT]*2*p
+        self.fails = []
+        self.recodings = 0
+
+    def check(self, roles, tag):
+        for r in roles:
+            d = diff(self.lam[r](self.f[r]), self.v[r])
+            if d: self.fails.append((tag, r, d))
+
+    def set_gauge(self, r, lam, linv, change):
+        self.f[r] = change(self.f[r]); self.lam[r] = lam; self.linv[r] = linv
+        self.recodings += 1
+        self.check([r], 'gauge%d' % r)
+
+    def fwd(self, j, order):
+        x, y = 2*j, 2*j+1
+        self.v[y] = add(self.v[y], self.Q(self.v[x], True))
+        src = self.f[x]
+        if self.lam[x] is not IDENT: src = self.lam[x](src); self.recodings += 1
+        if order == 'inv-first':
+            src = self.Q(src, True)
+            if self.linv[y] is not IDENT: src = self.linv[y](src); self.recodings += 1
+        else:
+            if self.linv[y] is not IDENT: src = self.linv[y](src); self.recodings += 1
+            src = self.Q(src, True)
+        self.f[y] = add(self.f[y], src)
+        self.check([y], 'fwd%d' % j)
+
+    def rev_add(self, j):
+        a, b = 2*j, 2*j+1
+        self.v[a] = add(self.v[a], self.Q(self.v[b]), -1)
+        src = self.f[b]
+        if self.lam[b] is not IDENT: src = self.lam[b](src); self.recodings += 1
+        src = self.Q(src)
+        if self.linv[a] is not IDENT: src = self.linv[a](src); self.recodings += 1
+        self.f[a] = add(self.f[a], src, -1)
+        self.check([a], 'rev%d-add' % j)
+
+    def rev_letter(self, j, letter):
+        for r in (2*j, 2*j+1):
+            self.v[r] = letter(self.v[r])
+            self.f[r] = letter(self.f[r])
+        self.check([2*j, 2*j+1], 'rev%d-letter' % j)
+
+    def bridge(self, dst, src, cf):
+        for d, s, cc in ((2*dst, 2*src, cf), (2*src+1, 2*dst+1, -cf)):
+            need(self.lam[d] is self.lam[s] and self.linv[d] is self.linv[s],
+                 'gauge mismatch across bridge %d-%d' % (dst, src))
+            self.v[d] = add(self.v[d], self.v[s], cc)
+            self.f[d] = add(self.f[d], self.f[s], cc)
+        self.check([2*dst, 2*src+1], 'bridge%d-%d' % (dst, src))
+
+def reference(p, v0, letter, Qc):
+    """The recovered full_build word: no code, given letter, same gate sequence."""
+    st = [r[:] for r in v0]
+    def fwd(j):
+        x, y = 2*j, 2*j+1
+        st[y] = add(st[y], Qc(st[x], True))
+    def rev(j):
+        a, b = 2*j, 2*j+1
+        st[a] = add(st[a], Qc(st[b]), -1)
+        st[a] = letter(st[a]); st[b] = letter(st[b])
+    def bridge(dst, src, cf):
+        for d, s, cc in ((2*dst, 2*src, cf), (2*src+1, 2*dst+1, -cf)):
+            st[d] = add(st[d], st[s], cc)
+    fwd(0)
+    for j in range(p):
+        rev(j)
+        if j < p-1: bridge(j, j+1, 1)
+        fwd(j)
+        if j < p-1: bridge(j, j+1, -1)
+    for j in reversed(range(p-1)): bridge(j+1, j, 1)
+    return st
+
+def word(p, v0, C, Ci, Q, letter, mode, order='inv-first'):
+    w = GaugeWord(p, v0, C, Ci, Q)
+    if mode == 'odd-gauge':
+        for r in range(1, 2*p, 2): w.set_gauge(r, C, Ci, Ci)
+    elif mode == 'even-gauge':
+        for r in range(0, 2*p, 2): w.set_gauge(r, C, Ci, Ci)
+    elif mode == 'coded-all':
+        for r in range(2*p): w.set_gauge(r, C, Ci, Ci)
+    coded = mode in ('odd-gauge', 'even-gauge', 'coded-all')
+    w.fwd(0, order if coded else 'inv-last')
+    for j in range(p):
+        if mode == 'transient':
+            w.set_gauge(2*j+1, C, Ci, Ci)
+            w.rev_add(j)
+            w.set_gauge(2*j+1, IDENT, IDENT, C)
+            w.rev_letter(j, letter)
+        else:
+            w.rev_add(j)
+            w.rev_letter(j, letter)
+        if j < p-1: w.bridge(j, j+1, 1)
+        w.fwd(j, order if coded else 'inv-last')
+        if j < p-1: w.bridge(j, j+1, -1)
+    for j in reversed(range(p-1)): w.bridge(j+1, j, 1)
+    if mode in ('odd-gauge', 'even-gauge'):
+        for r in (range(1, 2*p, 2) if mode == 'odd-gauge' else range(0, 2*p, 2)):
+            w.set_gauge(r, IDENT, IDENT, C)
+    return w
+
+def bill(w):
+    return {'recodings': w.recodings, 'monomial_field_maps': w.recodings*MONOMIAL_MAPS,
+            'scalar_adds': w.recodings*SCALAR_ADDS, 'owned_clears': w.recodings*OWNED_CLEARS}
+
+def main():
+    receipt = json.loads((ROOT/'research/coded-native-caller/NORMALIZERS.json').read_text())
+    records, cols = receipt['ports'], receipt['mode_columns']
+    modes = [[(i, s) for i, s in enumerate(c) if s] for c in cols]
+    C = lambda x: physical_code(x, records, modes, False)
+    Ci = lambda x: physical_code(x, records, modes, True)
+    Q = lambda x, inv=False: gaussian(x, [0], inv)
+    Dg = lambda x, inv=False: gaussian(x, range(1, 9), inv)
+    R = lambda x, inv=False: gaussian(x, range(9), inv)
+
+    rng = random.Random(5)
+    def dense(): return [[rng.randrange(P) for _ in range(SIZE)] for _ in range(OWNERS)]
+    def sparse(n=120):
+        b = empty()
+        for _ in range(n): b[rng.randrange(OWNERS)][rng.randrange(SIZE)] = rng.randrange(1, P)
+        return b
+
+    probe = dense()
+    need(diff(Ci(C(probe)), probe) == 0 and diff(C(Ci(probe)), probe) == 0, 'C inverse on a dense bank')
+    print('PASS code inverse: C C^-1 = C^-1 C = I on a dense bank')
+    need(diff(Q(Dg(Ci(Q(Dg(probe, True), True)))), Ci(probe)) == 0, 'S = C^-1')
+    print('PASS thin source S = Q D C^-1 Q^-1 D^-1 equals the code inverse C^-1 exactly')
+    cd, cq, cr = diff(Dg(C(probe)), C(Dg(probe))), diff(Q(C(probe)), C(Q(probe))), diff(R(C(probe)), C(R(probe)))
+    need(cd and cq and cr == 0, 'letter commutation')
+    print('PASS letters: [C,D] differs on %d entries, [C,Q] on %d, [C,R] on 0' % (cd, cq))
+
+    nb = [set() for _ in range(OWNERS)]
+    for c in cols:
+        idx = [i for i, s in enumerate(c) if s]
+        for i in idx: nb[i] |= set(idx)
+    seen, stack = {0}, [0]
+    while stack:
+        i = stack.pop()
+        for j in nb[i]:
+            if j not in seen: seen.add(j); stack.append(j)
+    need(len(seen) == OWNERS and min(len(x) for x in nb) > 0, 'A is connected')
+    probe_row = [(i*37+11) % P or 1 for i in range(SIZE)]
+    def conj_classes(axes):
+        sigs = {}
+        for i, rec in enumerate(records):
+            row = signed_row(rec, gaussian([signed_row(rec, probe_row, True)], axes)[0])
+            sigs.setdefault(tuple(row), []).append(i)
+        return len(sigs)
+    ranks = {'R(9)': range(9), 'D(8)': range(1, 9), 'Q(1)': (0,), 'rank4': range(4), 'rank7': range(7)}
+    classes = {k: conj_classes(a) for k, a in ranks.items()}
+    need(classes['R(9)'] == 1 and all(v > 1 for k, v in classes.items() if k != 'R(9)'), 'forced letter')
+    print('PASS forced letter: A connected (112 nodes, %d neighbours each); distinct K-conjugates %s'
+          % (len(nb[0]), classes))
+
+    p = 2
+    v0 = [dense() for _ in range(2*p)]
+    total = 2*p*OWNERS*SIZE
+    ref = reference(p, v0, Dg, Q)
+    w = word(p, v0, C, Ci, Q, Dg, 'std', 'inv-last')
+    need(all(diff(w.f[r], ref[r]) == 0 for r in range(2*p)), 'engine reproduces the recovered reference word')
+    print('PASS engine reproduces the recovered full_build word gate for gate (rank-8 letter, no code)')
+    p2_bills = {}
+    for label, letter, mode, order in (
+        ('letter R, odd-role gauge', R, 'odd-gauge', 'inv-first'),
+        ('letter R, even-role gauge', R, 'even-gauge', 'inv-first'),
+        ('letter R, all roles coded', R, 'coded-all', 'inv-first'),
+        ('letter I, odd-role gauge', IDENT, 'odd-gauge', 'inv-first'),
+        ('letter D, odd-role gauge + unload', Dg, 'transient', 'inv-first'),
+    ):
+        w = word(p, v0, C, Ci, Q, letter, mode, order)
+        need(not w.fails, 'p=2 gate invariant: ' + label + ' ' + mode)
+        decoded = sum(diff(w.lam[r](w.f[r]), w.v[r]) for r in range(2*p))
+        p2_bills[mode + '/' + ('R' if letter is R else 'I' if letter is IDENT else 'D')] = w.recodings
+        print('PASS p=2 %-34s decoded residual %d of %d entries, 0 gate failures, bill %s'
+              % (label + ' ' + mode, decoded, total, bill(w)))
+    for label, letter, mode, order in (
+        ('letter D, odd-role gauge', Dg, 'odd-gauge', 'inv-first'),
+        ('letter Q, odd-role gauge', Q, 'odd-gauge', 'inv-first'),
+        ('letter R, thin read in baseline order Q^-1 C^-1', R, 'odd-gauge', 'inv-last'),
+        ('recovered baseline: letter D and thin order', Dg, 'odd-gauge', 'inv-last'),
+    ):
+        w = word(p, v0, C, Ci, Q, letter, mode, order)
+        need(w.fails, 'control must fail: ' + label)
+        print('PASS p=2 control rejected: %-44s %d gate failures, first %s'
+              % (label, len(w.fails), w.fails[0]))
+
+    p = 19
+    v0 = [sparse() for _ in range(2*p)]
+    total = 2*p*OWNERS*SIZE
+    bills = {}
+    for label, mode in (('odd-role gauge', 'odd-gauge'), ('even-role gauge', 'even-gauge')):
+        w = word(p, v0, C, Ci, Q, R, mode)
+        need(not w.fails, 'p=19 gate invariant: ' + label)
+        decoded = sum(diff(w.lam[r](w.f[r]), w.v[r]) for r in range(2*p))
+        bills[mode] = w.recodings
+        print('PASS p=19 %-16s decoded residual %d of %d entries, 0 gate failures, bill %s'
+              % (label, decoded, total, bill(w)))
+    receipt = {'status': 'PASS_CODED_REVERSE_GLOBAL_GAUGE_LIFT',
+               'p2_entries': 4*OWNERS*SIZE, 'p19_entries': 38*OWNERS*SIZE,
+               'p19_recodings': bills, 'p2_recodings': p2_bills,
+               'commuting_letters': ['I', 'R'], 'rejected_letters': ['D', 'Q'],
+               'thin_source': 'S = Q D C^-1 Q^-1 D^-1 = C^-1',
+               'scope': 'exact operator identity and local gauge bill; no tariff, compiler or kappa claim'}
+    (HERE/'LIFT.json').write_text(json.dumps(receipt, indent=2, sort_keys=True) + '\n')
+    print(json.dumps(receipt, sort_keys=True))
+
+if __name__ == '__main__':
+    main()
diff --git a/research/coded-reverse-word-p19/verify.py b/research/coded-reverse-word-p19/verify.py
new file mode 100644
index 0000000000..479da4e7f4
--- /dev/null
+++ b/research/coded-reverse-word-p19/verify.py
@@ -0,0 +1,86 @@
+#!/usr/bin/env python3
+"""Fast receipt for the p=19 uncoded-word supplier.
+
+Runs the formal controller verifier, checks the p=19 diagonalisation receipt, then
+the two package receipts: P19_PLAIN.json (the trace-certified word, its census and
+the absence of a recoding bill) and P19_CLAIM.json (the price, guards, compiler,
+BIT chain, budgets and outer ledger).  The long traces are the separate commands
+p19_plain.py and p19_word.py.
+"""
+import json, subprocess, sys
+from pathlib import Path
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+OWNERS, SIZE = 112, 512
+
+def need(ok, why):
+    if not ok: raise ValueError(why)
+
+def run(path, timeout=900):
+    p = subprocess.run([sys.executable, '-I', '-B', str(ROOT/path)], cwd=ROOT,
+                       capture_output=True, text=True, timeout=timeout)
+    sys.stdout.write(p.stdout)
+    sys.stderr.write(p.stderr)
+    need(p.returncode == 0, 'subprocess failed: '+path)
+    return p.stdout + p.stderr
+
+def main():
+    out1 = run('research/coded-reverse-controller/verify.py')
+    need('PASS p=19 tail guards at C=0.0034' in out1, 'p=19 tail guards')
+    need('0.007579' in out1, 'p=19 raw complex root')
+    need('PASS p=2, 448x448' in out1, 'p=2 448x448 conjugation')
+    need('at 0.0034 the only failing predicate is the BIT cap' in out1, 'outer ledger')
+    diag = json.loads((HERE/'P19_DIAG.json').read_text())
+    need(diag['diagonalized'] is True and diag['std']['outputs'] == diag['cod']['outputs']
+         and diag['std']['denominators'] == [1], 'p19 diagonalization receipt')
+    print('PASS formal controller: p=19 diagonalisation, guards, raw root and outer ledger')
+
+    plain = json.loads((HERE/'P19_PLAIN.json').read_text())
+    pw = plain['p19']
+    need(plain['status'] == 'PASS_P19_UNCODED_WORD', 'word receipt status')
+    need(pw['trace_identity'] == 'replayed in the controller algebra', 'trace identity')
+    need(pw['denominators'] == [1], 'standard denominators')
+    need((pw['retained_idles'], pw['idle_rank']) == (36, 198), 'idle census')
+    need(pw['gates'] == 241 and pw['kinds']['LETTER'] == 39 and pw['kinds']['IDLE'] == 36, 'gate census')
+    need((pw['recodings'], pw['terminal_gauge_decoder']) == (0, 0), 'no recoding bill')
+    need(abs(pw['invoice_root'] - 0.007578535189897761) < 1e-9 and pw['ambient_rank'] == 153, 'price')
+    print('PASS word: p=19 trace == controller, diagonalises with denominators [1], %d gates, '
+          '%d retained idles, root %.12f, no recoding bill'
+          % (pw['gates'], pw['retained_idles'], pw['invoice_root']))
+
+    bank = HERE/'P19_BANK.json'
+    need(bank.exists(), 'the address-level replay receipt is missing (run p19_bank.py)')
+    bk = json.loads(bank.read_text())
+    need(bk['status'] == 'PASS_ADDRESS_LEVEL_TRACE_REPLAY' and sum(bk['differing_entries']) == 0,
+         'the gate list realises the controller matrix at address level')
+    print('PASS binding: p=%d address-level replay, %d addresses per role, %d roles, %d gates, 0 differing entries'
+          % (bk['p'], bk['addresses_per_role'], bk['roles'], bk['gates']))
+
+    need('CLAIM kappa' in run('research/coded-reverse-word-p19/p19_claim.py'), 'claim checker')
+    claim = json.loads((HERE/'P19_CLAIM.json').read_text())
+    need(claim['status'] == 'CLAIM_P19_UNCODED_WORD_SUPPLIER', 'claim status')
+    need(claim['kappa'] == '951999/280000000', 'claim value')
+    need(claim['gain_vs_selected_record_percent'] > 12.5 and claim['gain_vs_reported_percent'] > 12.3,
+         'both gains are recorded')
+    need(claim['compiler']['H0'] == 5170423668736, 'compiler ranks')
+    bill = claim['field_level_bill']
+    need(all(bill[k] == 0 for k in ('recodings', 'monomial_field_maps', 'scalar_adds',
+                                    'owned_clears', 'terminal_gauge_decoder')),
+         'the emitted claim carries a zero field bill')
+    need(claim['uncoded_word']['gates'] == 241 and claim['uncoded_word']['gate_kinds']['LETTER'] == 39,
+         'the emitted claim describes the uncoded word')
+    need(claim['record_only_overlay']['status'].startswith('historical record'),
+         'the coded overlay is labelled a record')
+    need('not a proof' in claim['compiler']['classification'], 'the compiler stays conditional')
+    print('PASS_P19_UNCODED_WORD_SUPPLIER kappa %s: +%.2f%% over the selected record, +%.2f%% over the reported '
+          'frontier; complex %s, BIT %s, compiler H0 = %s, field bill all zero'
+          % (claim['kappa'], claim['gain_vs_selected_record_percent'],
+             claim['gain_vs_reported_percent'], claim['complex_supplier'],
+             claim['bit_supplier'], claim['compiler']['H0']))
+    print(json.dumps({'status': 'PASS_P19_UNCODED_WORD_SUPPLIER', 'kappa': claim['kappa'],
+                      'gain_vs_selected_record_percent': claim['gain_vs_selected_record_percent'],
+                      'gain_vs_reported_percent': claim['gain_vs_reported_percent'],
+                      'field_level_bill': 'all zero'}, sort_keys=True))
+
+if __name__ == '__main__':
+    main()