diff --git a/research/pr4538-cost-theorems-check/.gitattributes b/research/pr4538-cost-theorems-check/.gitattributes
new file mode 100644
index 0000000000..084eddade5
--- /dev/null
+++ b/research/pr4538-cost-theorems-check/.gitattributes
@@ -0,0 +1 @@
+PR4538-COST-THEOREMS.md -text
diff --git a/research/pr4538-cost-theorems-check/PR4538-COST-THEOREMS.md b/research/pr4538-cost-theorems-check/PR4538-COST-THEOREMS.md
new file mode 100644
index 0000000000..a5d940b205
--- /dev/null
+++ b/research/pr4538-cost-theorems-check/PR4538-COST-THEOREMS.md
@@ -0,0 +1,259 @@
+# Streaming Word RAM costs for the native layout layer
+
+These are constructive sufficient results for a Word RAM port. They establish
+primitive semantics and costs. They do not establish a new multiplication bound,
+a new κ, or a complete port of the analytic/recursion/compiler chain.
+
+## Model and representation
+
+The baseline instruction set has bounded-word ADD, truncated SUB, AND, NOT,
+left shift, indirect LOAD/STORE, conditional/unconditional jumps, and literals.
+Words and addresses have w bits, with w >= 6 so the fixed program and registers fit. Multiplication and division of words are not
+used by the constructions below. They remain legitimate optional instructions
+in the richer `Lax13.Ram` model; an n-bit input-sized unit multiplication is not
+being introduced. XOR and MOV are macros taking at most 4 and 2 instructions
+respectively in that existing model. JNZ expands to at most 2 instructions.
+
+A record consists of L >= 1 arbitrary words, stored at stride K = 2^s, where
+L <= K < 2L. Let N = 2^r and r <= w. The two record buffers, the column tables,
+and a constant register/scratch region are disjoint and lie strictly below
+2^w. This is stronger than r <= w; in particular r = w cannot fit these two buffers. No address calculation wraps. Initial values outside the
+written payload cells are arbitrary. The source is preserved.
+
+The supplied affine map has columns c_0,...,c_(r-1) in F_2^r, assumed linearly
+independent, and offset b in F_2^r. Preparing/checking supplied metadata is a
+separate caller action, not an uncharged gate-list compiler. Invertibility can
+be checked by ordinary word-packed elimination in O(r^2) word operations.
+A straightforward gate-word metadata compiler may instead cost O(m r^2) for m
+gates; no bound on that cost is hidden in the streaming theorem.
+
+## Theorem 1: affine permutation with a linear word count
+
+There is one fixed program that, from the above data, writes
+
+    destination[(A x XOR b)*K + j] = source[x*K+j]
+
+for every 0 <= x < N and 0 <= j < L, preserves every source/table cell and every
+untouched destination padding cell, and uses at most
+
+    8 N L + 40 N + 8
+
+expanded instructions. This count starts from preloaded buffers and parameters;
+input deserialization and final output serialization are caller costs.
+
+Proof. Start with x = 0 and y = b. Copy the L-word payload to destination record
+y. To advance x, visit exactly the bit positions flipped by binary increment,
+XORing c_j into y for every flipped bit j. Thus the invariant y = A x XOR b
+holds initially and after every increment, by linearity over F_2. Invertibility
+makes the N destination indices distinct, so every destination payload is
+written exactly once. The buffers are disjoint, so no source read is invalidated.
+No instruction writes a source, table, or padding address.
+
+For each bit j, binary increment between 0 and N-1 flips that bit exactly
+N/2^j - 1 times. The total number of flips is therefore
+
+    T = sum_(j=0)^(r-1) (N/2^j - 1) = 2N - r - 2,
+
+including r = 0, when T = 0. The displayed fixed program has 30 macro
+instructions, with loops but no instruction depending on r, L, or the input
+values. Its charged expansion count is
+
+    8 N L + 9 N + 11 T + 3
+      = 8 N L + 31 N - 11 r - 19
+      <= 8 N L + 40 N + 8.
+
+The r = 0 case costs 8L + 12 and satisfies the same formulas. Destination base
+addresses use y << s; multiplication is unnecessary. All masks, counters,
+indices, payload values, and effective addresses fit in a word by the stated
+bounds. This proves both semantics and the instruction bound. ∎
+
+`streaming_affine.py` is an executable fixed-program model. Its macro costs are
+upper bounds on `Lax13.Ram` expansions, rather than a claim that Python runtime
+measures Word RAM time. The model is not itself a Lean proof or a complete
+emitted `Lax13.Ram.Program`; resolving macro labels in such a compiler remains
+an integration task.
+
+## Theorem 2: all quadratic Gaussian phases in linear streaming time
+
+Let a_j be in Z/4, and let B be a symmetric binary r-by-r matrix with zero
+diagonal. Define
+
+    q(x) = sum_j a_j x_j + 2 sum_(j<k) B_jk x_j x_k  (mod 4).
+
+Suppose the r columns of B are packed as r-bit words. All N phases q(x), in
+ordinary binary x order, can be generated in O(N + r) Word RAM operations with
+O(r) metadata and O(1) scratch words. There is no parity instruction, population
+count, right shift, word multiplication, or word division in this algorithm.
+
+Proof. Maintain q(x) and the packed gradient g = B x over F_2. Initially x = 0,
+q = 0, and g = 0. When coordinate j flips, its old value is x_j. Let
+
+    d = (a_j + 2 g_j) mod 4.
+
+The new phase is q+d if x_j = 0 and q-d if x_j = 1, modulo 4. Indeed, only the
+linear term at j and quadratic terms incident to j change. Their total forward
+difference is a_j + 2 sum_(k != j) B_jk x_k. Replacing the sum by its parity
+changes the result by a multiple of 4. The reverse difference has the opposite
+sign. Update g by XORing column j of B. The zero diagonal ensures that the
+old g_j supplies the incident-term sum used in this update.
+
+Read g_j by AND with the same bit mask already used by the binary increment;
+branching on zero avoids extracting a numeric bit. Load a_j and column j using
+j as an address offset. Reduce a_j+2 by AND with 3. For reverse differences use
+(q+4-d) AND 3, whose subtraction never underflows. All these are constant-many
+word instructions when w >= 3. There are T < 2N bit flips by Theorem 1, and the
+metadata initialization takes O(r) instructions. The phase and gradient
+invariants therefore prove the result. ∎
+
+## Theorem 3: exact monomial Clifford action on limb records
+
+Let each coefficient be a pair of integers (u_x,v_x), represented modulo
+2^(kL) by L little-endian limbs of k bits, where 1 <= k <= w-2. For invertible
+A, offset b, and q as above, the map
+
+    (u+iv)_x -> i^q(x) (u+iv)_x at index A x XOR b
+
+can be evaluated by a uniform additive/Boolean Word RAM in O(NL + N + r)
+operations, preserving the source, using two disjoint padded output buffers
+and O(r) metadata words. All real/imaginary source and destination buffers and scratch cells must fit together below 2^w. This statement uses precomputed A,b,a,B metadata.
+
+Proof. Theorems 1 and 2 maintain the destination index and phase in constant
+amortized work per coefficient. Multiplication by i^q uses only a swap of the
+real/imaginary destinations and zero, one, or two integer negations:
+
+    q=0: (u,v); q=1: (-v,u); q=2: (-u,-v); q=3: (v,-u).
+
+To negate an L-limb residue, complement each digit within base beta = 2^k and
+add a carry initially equal to 1. At digit a, form beta-1-a+carry; store its
+residue modulo beta and set the carry to 1 exactly when this value is beta.
+Every temporary is at most beta, hence fits in a word; each digit takes
+constant-many instructions. The standard radix identity proves this is
+negation modulo beta^L. Copying, swapping destinations, and up to two such
+negations take O(L) instructions per coefficient. The disjoint-buffer argument
+from Theorem 1 proves the frame property. ∎
+
+The residue width here is exactly kL bits: no unmasked partial top limb is permitted. If a caller starts with B bits not divisible by k, it must pad to kL and establish the signed interpretation at that full width, or supply a separately proved top-mask operation.
+
+If the intended coefficients are signed integers strictly between
+-2^(kL-1) and 2^(kL-1), interpret the residues by signed decoding. Negation and
+Gaussian-unit phases then agree with ordinary integer arithmetic, provided the
+endpoint excluded above does not occur. In fact, an absolute-value headroom
+bound is invariant under these phases. This does not justify arbitrary
+finite-precision rounding or multiplication by roots other than Gaussian units.
+
+## Theorem 4: uniform metadata compiler, with global phase retained
+
+For a word of m gates from X_j, S_j, Z_j, CNOT_(j,k), SWAP_(j,k), and CZ_(j,k),
+there is an exact uniform metadata constructor using O((m+1)(r+1)^2) Word RAM
+operations and O(r) words of live metadata. It returns A,b,c,a,B such that
+
+    literal_word |x> = i^(c+q(x)) |A x XOR b>.
+
+The exponent c is retained modulo 4, including global phase; it is not discarded
+as physically irrelevant. The combined metadata compiler and streaming evaluator
+therefore costs O((m+1)(r+1)^2 + NL). This is a fully specified sufficient
+construction for monomial segments, not an assumed metadata oracle.
+
+Proof. Initially A is identity, b=0, c=0, a=0, and B=0. Maintain the stated
+identity after every appended gate. X_j toggles bit j of b. CNOT_(j,k) toggles
+bit k in every affine column whose bit j is set, and does the same to b. SWAP
+swaps those bits in every column and in b. These update the output affine map
+without changing the phase polynomial.
+
+For phase gates, write output coordinate j as b_j XOR u dot x, with u the
+j-th row of A. Its value modulo 4 is
+
+    b_j + (1-2*b_j) sum_l u_l*x_l
+        + 2 sum_(l<t) u_l*u_t*x_l*x_t.
+
+This follows from the parity expansion modulo 4: terms of degree at least 3
+have coefficient divisible by 4. Appending S_j therefore adds b_j to c,
+(1-2*b_j)*u_l to a_l, and toggles B_lt when u_l*u_t=1. Appending Z_j adds
+2*b_j to c and 2*u_l to a_l, with no quadratic change.
+
+For CZ_(j,k), let u,v be rows j,k and let their offsets be b_j,b_k. Since
+this gate contributes twice the product of those output bits, compute the
+product over F_2. Its constant is b_j*b_k; its linear coefficient at l is
+
+    b_j*v_l XOR b_k*u_l XOR u_l*v_l;
+
+its coefficient at x_l*x_t, for l<t, is
+
+    u_l*v_t XOR u_t*v_l.
+
+Add twice the constant and linear coefficients to c and a, and toggle the
+corresponding B edges. These exact formulas preserve the invariant.
+
+Each affine gate takes O(r) word work and each phase gate O(r^2) work. Store
+A and B by their r packed columns and a by r words. Bit tests require only
+AND with a left-shifted mask and a zero branch; the Python reference's use of
+right shifts for readability is not an additional machine instruction premise.
+All mod-4 signed updates can use an added constant before truncated subtraction,
+then AND with 3. Initializing the metadata is O(r) work. Thus the stated bound
+holds. Symmetry and zero diagonal of B are maintained by toggling both endpoint
+bits for each unordered pair. Gate-by-gate induction proves correctness. ∎
+
+Theorem 2 extends to c+q by initializing its phase to c instead of 0. Theorem 3
+then evaluates the result from this compiler with the same asymptotic count.
+`monomial_metadata.py` contains this constructor and an independent literal
+basis-state gate interpreter. It rejects H explicitly, because Hadamard leaves
+the monomial class. Its replays include a control requiring the nonzero global
+phase of X followed by S to remain present.
+
+## Direct scope for the integer multiplication port
+
+These theorems cover binary-linear coordinate relabelings, XOR translations,
+and quadratic Gaussian-unit phase diagonals: the monomial Clifford layer.
+A monomial is NOT an arbitrary symplectic/Fourier transformation. Hadamard and
+nonmonomial Fourier kernels still need their own numerical execution and error
+bounds. Likewise, a pre-existing long gate word must actually be compiled to
+this metadata and its compiler cost charged before the theorem can replace it.
+
+If a transfer contains m separate permutations of the same L-word coefficient
+records, executing them separately costs O(mNL). Composing their metadata and
+then materializing once costs O(NL + composition cost), provided intermediate
+stages do not observe or modify the intermediate layouts. This is a sufficient
+fusion rule, not permission to skip paid transforms across intervening ADDs.
+
+This gives a concrete RAM-specific port component beyond generic Turing-machine
+simulation. It does not imply a superior κ. The richer log-RAM model with word
+multiplication already has O(n)-time multiplication results, with n denoting
+input bits; comparison with such results must name the instruction model and
+input/output representation. See Fürer (2014), Theorems 4.1 and 4.2:
+https://arxiv.org/html/1402.1811v1 .
+
+## Reused project facts and evidence limits
+
+* `Problem18RAMLax13Ram20261001.lean`: `Lax13.Ram.Instr` and the uniform
+  bounded-word/indirect-memory semantics; macro expansions for XOR and MOV.
+* `MpLimbs20261007.lean`: `lv`, `lv_dig`, `addCode`, `add_run`, `mapCode`,
+  `map_run`, `copyIn_run`, `copyOut_run`, `compileC_sim`. In particular,
+  `add_run` gives exact limb addition in `40*L+20` IMP steps under explicit
+  array frame, operand, and no-overflow premises. These are predecessor facts,
+  not discoveries of this deliverable.
+* `Problem18TensorGatherRefinement20261002.lean`:
+  `parameters_at_entry`, `cells_tensorCoordinates`, `tensor_gather_run`, and
+  `source_tensor_gather_run`. All six tensor coordinate orders have literal
+  serialized semantics; the concrete gather bound is `210*(a*b*c*e+1)` IMP
+  steps. The new affine primitive generalizes the relevant binary-coordinate
+  layout operations, while supplying a separate amortized accounting argument.
+* `MpSparse20261007.lean` and `Problem18RAMRootLog20261007.lean`:
+  `tdWidth`, `allFormatRootRAMLog` provide the existing trans-dichotomous
+  short-word route. Its stated runtime is polynomial with unspecified degree,
+  so that theorem alone does not transfer the multiplication exponent sharply.
+* `Problem18Lax13BitCost20261007.lean`: `runCost_le` and `runsTo_bitCost`
+  give bit-cost accounting for existing bounded-word runs. This is an abstract
+  instruction charge, not an independently implemented gate-level simulator.
+
+The project sources above were read and SHA-256 pinned; no Lean process was
+started here, so these citations are current-source inspection, not a fresh
+kernel/axiom audit. The shared source/DAG lexical query for `WordRAM` found the
+registered external `formal-math-3sum-apsp` collection; a precise query for
+`Problem18RAMRootBitCost` returned no entries although that source is present.
+No claim of complete current-source DAG coverage is made. The root team is
+reconciling whole-catalog coverage separately.
+
+The affine enumeration, radix arithmetic, and quadratic phase identities are
+standard mathematics. The contribution is a concrete sufficient interface and
+cost proof for this port, with executable replays, rather than a claim of
+historical priority for those identities.
diff --git a/research/pr4538-cost-theorems-check/README.md b/research/pr4538-cost-theorems-check/README.md
new file mode 100644
index 0000000000..29ab7136f5
--- /dev/null
+++ b/research/pr4538-cost-theorems-check/README.md
@@ -0,0 +1,48 @@
+# Independent check of #4538: native-layout cost theorems 1–4
+
+**Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ.**
+
+Dugongue's #4538 (head `dffc7939`) states four Word RAM cost theorems for the monomial Clifford layer, in `cost/COST-THEOREMS.md`:
+- affine record permutations in at most `8NL + 40N + 8` instructions;
+- streaming quadratic Z/4 phases;
+- limb negation for Gaussian-unit phases;
+- a metadata compiler for X/S/Z/CNOT/SWAP/CZ words that keeps the global phase.
+
+This package checks all four with separately written code. The theorem text is vendored as `PR4538-COST-THEOREMS.md` (blob `a5d940b2`, SHA256-pinned). Nothing is imported from #4538's `streaming_affine.py`, `quadratic_phase.py` or `monomial_metadata.py`.
+
+## Results
+
+All checked claims are confirmed.
+
+- **Theorem 1 (affine permutation).**
+  - **Count arithmetic.** Literal increments give the flip count `T = 2N − r − 2` for `r ≤ 8`, and the identity `8NL + 9N + 11T + 3 = 8NL + 31N − 11r − 19 ≤ 8NL + 40N + 8` holds.
+  - **My own program.** I wrote a separate fixed program (30 instructions, plus a HALT) on a small additive/Boolean RAM with truncated SUB and no multiplication, division or right shift, using the stated macro costs (XOR 4, MOV 2, JNZ 2, others 1). Over 36 runs (`r ≤ 8`, `L ∈ {1, 2, 3, 5}`, random invertible `A` and offset `b`), it writes `dst[(Ax⊕b)K + j] = src[xK + j]` exactly. It preserves source, table and destination padding cells, and uses at most **0.82×** the bound.
+  - **Control.** A mutated program (XOR → ADD in the carry chain) is rejected.
+
+  So the bound is attainable by an independent implementation, not only by #4538's.
+- **Theorem 2 (quadratic phases).** The update `d = (a_j + 2g_j) mod 4`, applied with `+d` on a 0→1 flip and `−d` on a 1→0 flip, with `g ^= Bcol_j`, reproduces `q(x)` at all 3,012 visited `x`. Here `r ≤ 8`, there are random `a` and symmetric zero-diagonal `B`, and there are fewer than `2N` flips.
+- **Theorem 3 (limb negation).** Digit complement plus carry equals negation modulo `2^(kL)` in 800 random cases (`k ∈ {1, 2, 3, 8, 16}`, `L ≤ 5`), with every temporary `≤ β`. The four Gaussian-unit cases equal multiplication by `i^q`.
+- **Theorem 4 (metadata compiler).** My compiler, written from the stated update rules, satisfies `word|x⟩ = i^(c+q(x))|Ax⊕b⟩` for every basis state. This holds on 360 random words (`r ≤ 6`, up to 40 gates of all six types), against a literal Gaussian-integer state-vector interpreter. `B` stays symmetric with zero diagonal. The X-then-S control needs `c = 1`, and dropping `c` is caught.
+- **Binding.** 9 formulas are bound verbatim to the vendored text.
+
+I also replayed #4538's registered package at its head: `PASS_REGISTERED_RESEARCH_PACKAGE research/word-ram-transfer outcome=partial` in 9.1 s.
+
+## Verify
+
+```text
+python3 -B research/pr4538-cost-theorems-check/verify.py
+```
+
+This runs in about 1 s with the standard library only.
+
+## Limitations
+
+- **Out of scope:** #4538's TM emitter, the Lean bridge, and packed tapes. My earlier #4552 and #4553 cover #4541's packed tapes, which follow #4538's model.
+- **Macro costs.** The macro expansion costs (XOR 4, MOV 2, JNZ 2) are taken as stated for `Lax13.Ram`, not re-derived from the Lean source.
+- **Finite checks.** The universal statements rest on #4538's written inductions, which these finite checks corroborate.
+
+## Open next questions
+
+- An emitted `Lax13.Ram` program for Theorem 1, with resolved labels and an exact instruction count checked against `RamStd.step`. First step: lower my 30-instruction program or #4538's 30-macro program, and count expansions mechanically.
+
+Credit: Dugongue (#4538). Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
diff --git a/research/pr4538-cost-theorems-check/SOURCES.json b/research/pr4538-cost-theorems-check/SOURCES.json
new file mode 100644
index 0000000000..a2a5ea8bbd
--- /dev/null
+++ b/research/pr4538-cost-theorems-check/SOURCES.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    }
+  ]
+}
diff --git a/research/pr4538-cost-theorems-check/TASK.json b/research/pr4538-cost-theorems-check/TASK.json
new file mode 100644
index 0000000000..37a0a527e5
--- /dev/null
+++ b/research/pr4538-cost-theorems-check/TASK.json
@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/staged544-mixed-fourth-entry/README.md",
+      "research/staged-fourth-mixture-ceiling/README.md",
+      "research/r437-two-window-carrier/README.md"
+    ],
+    "methods": [
+      "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+      "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+    ],
+    "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+    "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
+    "allowed_variations": [
+      "Reconstruct either a source ledger or a numeric enclosure with a different method."
+    ],
+    "scope_change_triggers": [
+      "Importing the primary function and calling its output independent verification.",
+      "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering",
+      "4088",
+      "4091",
+      "4067",
+      "staged544-mixed-fourth-entry",
+      "staged-fourth-mixture-ceiling",
+      "r437-two-window-carrier"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "unchanged",
+  "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+  "scope_change_reason": null,
+  "bottleneck_link": "Independent coverage of the RAM-native monomial layer proposed as a replacement for paid tape routing in a Word RAM port.",
+  "budget_minutes": 40,
+  "stop_rule": "Stop at COST-THEOREMS.md Theorems 1-4.",
+  "outcome": "completed",
+  "evidence": "T1: flip count and count identity, and my own 30-instruction additive/Boolean RAM program within 0.82x of 8NL+40N+8 over 36 runs with exact semantics and frame preservation, plus a mutation control; T2: 3,012 streamed phases; T3: 812 negation/unit cases; T4: own compiler vs literal Gaussian-integer interpreter on 360 random words with global phase and drop-c control; 9 statements bound.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Emitted Lax13.Ram program for Theorem 1 with mechanically counted expansions.",
+      "why_it_matters": "Turns the macro-cost bound into an exact checked count.",
+      "first_step": "Lower one fixed program and count against RamStd.step.",
+      "blocked_by": "None."
+    }
+  ]
+}
diff --git a/research/pr4538-cost-theorems-check/VERIFY.json b/research/pr4538-cost-theorems-check/VERIFY.json
new file mode 100644
index 0000000000..3abf1149ca
--- /dev/null
+++ b/research/pr4538-cost-theorems-check/VERIFY.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Independent checks of #4538 cost theorems 1-4: own RAM program for affine permutation within 8NL+40N+8, streamed quadratic phases, limb negation, own monomial metadata compiler vs literal interpreter with global phase; controls; binding to vendored text (sha256)."
+    }
+  ]
+}
diff --git a/research/pr4538-cost-theorems-check/verify.py b/research/pr4538-cost-theorems-check/verify.py
new file mode 100644
index 0000000000..5cfa01a950
--- /dev/null
+++ b/research/pr4538-cost-theorems-check/verify.py
@@ -0,0 +1,396 @@
+#!/usr/bin/env python3
+"""Independent check of PR #4538 (Dugongue) native-layout cost theorems 1-4, from the vendored COST-THEOREMS.md text.
+
+Nothing is imported from #4538's streaming_affine.py, quadratic_phase.py or monomial_metadata.py.
+  T1. Flip count T = sum_j (N/2^j - 1) = 2N - r - 2 by literal increments, and the identity
+      8NL + 9N + 11T + 3 = 8NL + 31N - 11r - 19 <= 8NL + 40N + 8. Then my own fixed program on a small
+      additive/Boolean RAM (no multiplication, division or right shift; costs XOR 4, MOV 2, JNZ 2, others 1, as
+      stated) performs destination[(Ax^b)K + j] = source[xK + j], preserves source, table and padding cells, and its
+      expanded count stays within 8NL + 40N + 8.
+  T2. The streaming update d = (a_j + 2 g_j) mod 4, q += d on a 0->1 flip and q -= d on 1->0, g ^= column j,
+      reproduces q(x) = sum a_j x_j + 2 sum_{j<k} B_jk x_j x_k (mod 4) at every x, with fewer than 2N flips.
+  T3. Limb negation by digit complement plus carry equals negation modulo 2^(kL); the four Gaussian-unit cases equal
+      multiplication by i^q.
+  T4. My own metadata compiler from the stated update rules for X, S, Z, CNOT, SWAP, CZ satisfies
+      word|x> = i^(c+q(x)) |Ax ^ b> against a literal Gaussian-integer state-vector interpreter on random words, global
+      phase included; dropping c is caught (X then S).
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+import hashlib
+import json
+from pathlib import Path
+import random
+import sys
+
+HERE = Path(__file__).resolve().parent
+SPEC = HERE / "PR4538-COST-THEOREMS.md"  # #4538 head dffc7939, research/word-ram-transfer/cost/COST-THEOREMS.md, blob a5d940b2
+SPEC_SHA256 = "79eef859eb2ae32a66879f294d626c3947bcfe55434b4a38a296d271b3aa9675"
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+# ---------------------------------------------------------------- T1: a small RAM and my own fixed program
+COST = {"LI": 1, "MOV": 2, "ADD": 1, "SUB": 1, "AND": 1, "XOR": 4, "SHL": 1, "LOAD": 1, "STORE": 1,
+        "JZ": 1, "JNZ": 2, "JMP": 1, "HALT": 0}
+
+
+def run(prog, regs, mem, w, limit):
+    labels = {ins[1]: i for i, ins in enumerate(prog) if ins[0] == "LABEL"}
+    mask = (1 << w) - 1
+    pc = cost = 0
+    while True:
+        ins = prog[pc]
+        op = ins[0]
+        pc += 1
+        if op == "LABEL":
+            continue
+        cost += COST[op]
+        need(cost <= limit, "instruction limit")
+        R = regs
+        if op == "LI":
+            R[ins[1]] = ins[2] & mask
+        elif op == "MOV":
+            R[ins[1]] = R[ins[2]]
+        elif op == "ADD":
+            R[ins[1]] = (R[ins[2]] + R[ins[3]]) & mask
+        elif op == "SUB":
+            R[ins[1]] = max(0, R[ins[2]] - R[ins[3]])  # truncated subtraction
+        elif op == "AND":
+            R[ins[1]] = R[ins[2]] & R[ins[3]]
+        elif op == "XOR":
+            R[ins[1]] = R[ins[2]] ^ R[ins[3]]
+        elif op == "SHL":
+            R[ins[1]] = (R[ins[2]] << R[ins[3]]) & mask
+        elif op == "LOAD":
+            R[ins[1]] = mem.get(R[ins[2]], 0)
+        elif op == "STORE":
+            need(R[ins[1]] < (1 << w), "address fits")
+            mem[R[ins[1]]] = R[ins[2]]
+        elif op == "JZ":
+            if R[ins[1]] == 0:
+                pc = labels[ins[2]]
+        elif op == "JNZ":
+            if R[ins[1]] != 0:
+                pc = labels[ins[2]]
+        elif op == "JMP":
+            pc = labels[ins[1]]
+        elif op == "HALT":
+            return cost
+
+
+# Inputs: SRC, DST, COL (r column words), NM1 = N-1, L, S = log2 K, Y = b. Constants: ONE.
+AFFINE = [
+    ("LI", "ONE", 1), ("LI", "X", 0),
+    ("LABEL", "record"),
+    ("SHL", "SA", "X", "S"), ("ADD", "SA", "SA", "SRC"),
+    ("SHL", "DA", "Y", "S"), ("ADD", "DA", "DA", "DST"),
+    ("MOV", "J", "L"),
+    ("LABEL", "copy"),
+    ("LOAD", "V", "SA"), ("STORE", "DA", "V"),
+    ("ADD", "SA", "SA", "ONE"), ("ADD", "DA", "DA", "ONE"), ("SUB", "J", "J", "ONE"),
+    ("JNZ", "J", "copy"),
+    ("SUB", "T", "NM1", "X"), ("JZ", "T", "done"),
+    ("LI", "M", 1), ("MOV", "CA", "COL"),
+    ("LABEL", "carry"),
+    ("AND", "T", "X", "M"), ("JZ", "T", "set"),
+    ("SUB", "X", "X", "M"), ("LOAD", "C", "CA"), ("XOR", "Y", "Y", "C"),
+    ("ADD", "M", "M", "M"), ("ADD", "CA", "CA", "ONE"), ("JMP", "carry"),
+    ("LABEL", "set"),
+    ("ADD", "X", "X", "M"), ("LOAD", "C", "CA"), ("XOR", "Y", "Y", "C"), ("JMP", "record"),
+    ("LABEL", "done"), ("HALT",),
+]
+
+
+def flips(r):
+    N = 1 << r
+    return sum(bin(x ^ (x + 1)).count("1") for x in range(N - 1))
+
+
+def check_t1(rng, program=AFFINE):
+    cases = worst = 0
+    for r in range(0, 9):
+        N = 1 << r
+        T = flips(r)
+        need(T == sum(N // (1 << j) - 1 for j in range(r)) == 2 * N - r - 2, "flip count")
+        for L in (1, 2, 3, 5):
+            need(8 * N * L + 9 * N + 11 * T + 3 == 8 * N * L + 31 * N - 11 * r - 19 <= 8 * N * L + 40 * N + 8,
+                 "count identity and bound")
+            s = max(0, (L - 1).bit_length())
+            K = 1 << s
+            need(L <= K < 2 * L, "stride")
+            while True:  # random invertible A over F_2
+                cols = [rng.getrandbits(r) if r else 0 for _ in range(r)]
+                basis = []
+                for v in cols:
+                    for bv in basis:
+                        v = min(v, v ^ bv)
+                    if v:
+                        basis.append(v)
+                if len(basis) == r:
+                    break
+            b = rng.getrandbits(r) if r else 0
+            w = 32
+            SRC, COL, DST = 1 << 12, 1 << 11, 1 << 20
+            mem = {}
+            for x in range(N):
+                for j in range(K):
+                    mem[SRC + x * K + j] = rng.getrandbits(16) if j < L else 7777
+                    mem[DST + x * K + j] = 5555
+            for j, c in enumerate(cols):
+                mem[COL + j] = c
+            before = dict(mem)
+            regs = {"SRC": SRC, "DST": DST, "COL": COL, "NM1": N - 1, "L": L, "S": s, "Y": b}
+            limit = 8 * N * L + 40 * N + 8
+            cost = run(program, regs, mem, w, limit)
+
+            def image(x):
+                y = b
+                for j in range(r):
+                    if x >> j & 1:
+                        y ^= cols[j]
+                return y
+
+            for x in range(N):
+                y = image(x)
+                for j in range(K):
+                    if j < L:
+                        need(mem[DST + y * K + j] == before[SRC + x * K + j], "payload moved")
+                    else:
+                        need(mem[DST + y * K + j] == 5555, "destination padding preserved")
+            need(all(mem[a] == v for a, v in before.items() if a < DST), "source and table preserved")
+            worst = max(worst, cost / limit)
+            cases += 1
+    return cases, round(worst, 4)
+
+
+# ---------------------------------------------------------------- T2
+def check_t2(rng):
+    cases = 0
+    for r in range(1, 9):
+        N = 1 << r
+        for _ in range(6):
+            a = [rng.randrange(4) for _ in range(r)]
+            B = [[0] * r for _ in range(r)]
+            for j in range(r):
+                for k in range(j + 1, r):
+                    B[j][k] = B[k][j] = rng.randrange(2)
+            colB = [sum(B[k][j] << k for k in range(r)) for j in range(r)]
+
+            def q(x):
+                v = sum(a[j] * (x >> j & 1) for j in range(r))
+                v += 2 * sum(B[j][k] * (x >> j & 1) * (x >> k & 1) for j in range(r) for k in range(j + 1, r))
+                return v % 4
+
+            x = qq = g = nflips = 0
+            need(q(0) == 0, "q(0)")
+            for _ in range(N - 1):
+                j = 0
+                while True:  # binary increment, flip by flip
+                    gj = g >> j & 1
+                    d = (a[j] + 2 * gj) & 3
+                    if x >> j & 1:
+                        qq = (qq + 4 - d) & 3
+                        x ^= 1 << j
+                        g ^= colB[j]
+                        nflips += 1
+                        j += 1
+                    else:
+                        qq = (qq + d) & 3
+                        x ^= 1 << j
+                        g ^= colB[j]
+                        nflips += 1
+                        break
+                need(qq == q(x), "streamed phase")
+                cases += 1
+            need(nflips < 2 * N, "fewer than 2N flips")
+    return cases
+
+
+# ---------------------------------------------------------------- T3
+def check_t3(rng):
+    cases = 0
+    for k in (1, 2, 3, 8, 16):
+        for L in (1, 2, 3, 5):
+            beta = 1 << k
+            for _ in range(40):
+                v = rng.getrandbits(k * L)
+                digits = [(v >> (k * i)) & (beta - 1) for i in range(L)]
+                carry, out = 1, []
+                for a in digits:
+                    t = beta - 1 - a + carry
+                    need(t <= beta, "temporary at most beta")
+                    out.append(t & (beta - 1))
+                    carry = 1 if t == beta else 0
+                need(sum(d << (k * i) for i, d in enumerate(out)) == (-v) % (beta ** L), "limb negation")
+                cases += 1
+    units = {0: lambda u, v: (u, v), 1: lambda u, v: (-v, u), 2: lambda u, v: (-u, -v), 3: lambda u, v: (v, -u)}
+    for qv in range(4):
+        for u, v in ((3, 5), (-2, 7), (0, 1)):
+            z = complex(u, v) * (1j ** qv)
+            need(units[qv](u, v) == (round(z.real), round(z.imag)), "Gaussian unit")
+            cases += 1
+    return cases
+
+
+# ---------------------------------------------------------------- T4
+def gmul_i(z, e):
+    u, v = z
+    for _ in range(e % 4):
+        u, v = -v, u
+    return (u, v)
+
+
+def literal(word, r, x):
+    """Apply the gate word to basis state |x>; returns (index, Gaussian-integer amplitude)."""
+    amp, y = (1, 0), x
+    for g in word:
+        op = g[0]
+        if op == "X":
+            y ^= 1 << g[1]
+        elif op == "S":
+            if y >> g[1] & 1:
+                amp = gmul_i(amp, 1)
+        elif op == "Z":
+            if y >> g[1] & 1:
+                amp = gmul_i(amp, 2)
+        elif op == "CNOT":
+            if y >> g[1] & 1:
+                y ^= 1 << g[2]
+        elif op == "SWAP":
+            bj, bk = y >> g[1] & 1, y >> g[2] & 1
+            if bj != bk:
+                y ^= (1 << g[1]) | (1 << g[2])
+        elif op == "CZ":
+            if (y >> g[1] & 1) and (y >> g[2] & 1):
+                amp = gmul_i(amp, 2)
+    return y, amp
+
+
+def compile_metadata(word, r):
+    """Metadata from the stated update rules. A is stored by rows: row j is the output coordinate j."""
+    rows = [1 << j for j in range(r)]
+    b = [0] * r
+    c = 0
+    a = [0] * r
+    B = [[0] * r for _ in range(r)]
+    bit = lambda u, l: u >> l & 1
+    for g in word:
+        op = g[0]
+        if op == "X":
+            b[g[1]] ^= 1
+        elif op == "CNOT":
+            j, k = g[1], g[2]
+            rows[k] ^= rows[j]
+            b[k] ^= b[j]
+        elif op == "SWAP":
+            j, k = g[1], g[2]
+            rows[j], rows[k] = rows[k], rows[j]
+            b[j], b[k] = b[k], b[j]
+        elif op in ("S", "Z"):
+            j = g[1]
+            u = rows[j]
+            if op == "S":
+                c = (c + b[j]) % 4
+                for l in range(r):
+                    a[l] = (a[l] + (1 - 2 * b[j]) * bit(u, l)) % 4
+                for l in range(r):
+                    for t in range(l + 1, r):
+                        if bit(u, l) and bit(u, t):
+                            B[l][t] ^= 1
+                            B[t][l] ^= 1
+            else:
+                c = (c + 2 * b[j]) % 4
+                for l in range(r):
+                    a[l] = (a[l] + 2 * bit(u, l)) % 4
+        elif op == "CZ":
+            j, k = g[1], g[2]
+            u, v = rows[j], rows[k]
+            c = (c + 2 * (b[j] & b[k])) % 4
+            for l in range(r):
+                lin = (b[j] & bit(v, l)) ^ (b[k] & bit(u, l)) ^ (bit(u, l) & bit(v, l))
+                a[l] = (a[l] + 2 * lin) % 4
+            for l in range(r):
+                for t in range(l + 1, r):
+                    if (bit(u, l) & bit(v, t)) ^ (bit(u, t) & bit(v, l)):
+                        B[l][t] ^= 1
+                        B[t][l] ^= 1
+    for j in range(r):
+        need(B[j][j] == 0 and all(B[j][t] == B[t][j] for t in range(r)), "B symmetric, zero diagonal")
+    return rows, b, c, a, B
+
+
+def apply_metadata(meta, r, x, keep_c=True):
+    rows, b, c, a, B = meta
+    y = 0
+    for j in range(r):
+        y |= ((bin(rows[j] & x).count("1") + b[j]) & 1) << j
+    qv = sum(a[j] * (x >> j & 1) for j in range(r))
+    qv += 2 * sum(B[j][t] * (x >> j & 1) * (x >> t & 1) for j in range(r) for t in range(j + 1, r))
+    return y, gmul_i((1, 0), (c if keep_c else 0) + qv)
+
+
+def check_t4(rng):
+    words = 0
+    for r in range(1, 7):
+        for _ in range(60):
+            m = rng.randrange(0, 41)
+            word = []
+            for _ in range(m):
+                op = rng.choice(("X", "S", "Z", "CNOT", "SWAP", "CZ"))
+                if op in ("X", "S", "Z") or r == 1:
+                    word.append((op if r > 1 or op in ("X", "S", "Z") else "S", rng.randrange(r)))
+                else:
+                    j, k = rng.sample(range(r), 2)
+                    word.append((op, j, k))
+            meta = compile_metadata(word, r)
+            for x in range(1 << r):
+                need(literal(word, r, x) == apply_metadata(meta, r, x), "word|x> = i^(c+q(x))|Ax^b>")
+            words += 1
+    # Control: X then S has global phase i on |0>; dropping c is caught.
+    meta = compile_metadata([("X", 0), ("S", 0)], 1)
+    need(meta[2] == 1 and literal([("X", 0), ("S", 0)], 1, 0) == apply_metadata(meta, 1, 0), "global phase kept")
+    need(literal([("X", 0), ("S", 0)], 1, 0) != apply_metadata(meta, 1, 0, keep_c=False), "dropping c caught")
+    return words
+
+
+def check_binding():
+    raw = SPEC.read_bytes()
+    need(hashlib.sha256(raw).hexdigest() == SPEC_SHA256, "vendored COST-THEOREMS.md bytes")
+    text = raw.decode("utf-8")
+    for s in ("8 N L + 40 N + 8", "T = sum_(j=0)^(r-1) (N/2^j - 1) = 2N - r - 2,", "8 N L + 9 N + 11 T + 3",
+              "d = (a_j + 2 g_j) mod 4.", "q=0: (u,v); q=1: (-v,u); q=2: (-u,-v); q=3: (v,-u).",
+              "literal_word |x> = i^(c+q(x)) |A x XOR b>.", "b_j*v_l XOR b_k*u_l XOR u_l*v_l;",
+              "u_l*v_t XOR u_t*v_l.", "2*b_j to c and 2*u_l to a_l"):
+        need(s in text, f"COST-THEOREMS.md states: {s!r}")
+    return 9
+
+
+def t1_rejection_control(rng):
+    """Replacing the carry-chain XOR by ADD breaks the affine invariant and must be caught."""
+    bad = [("ADD", "Y", "Y", "C") if ins == ("XOR", "Y", "Y", "C") else ins for ins in AFFINE]
+    need(bad != AFFINE, "mutation applied")
+    try:
+        check_t1(rng, bad)
+    except AssertionError:
+        return True
+    raise AssertionError("mutated program accepted")
+
+
+def main():
+    rng = random.Random(4538)
+    t1_cases, t1_worst = check_t1(rng)
+    t1_control = t1_rejection_control(random.Random(1))
+    report = {"status": "PASS_PR4538_COST_THEOREMS_CHECK",
+              "t1_affine_programs_run": t1_cases, "t1_worst_cost_over_bound": t1_worst,
+              "t1_rejection_control_caught": t1_control,
+              "t2_streamed_phases": check_t2(rng), "t3_negation_and_unit_cases": check_t3(rng),
+              "t4_random_words_all_basis_states": check_t4(rng), "spec_statements_bound": check_binding(),
+              "new_kappa_claimed": False}
+    print(json.dumps(report, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())