diff --git a/docs/ci-verification.md b/docs/ci-verification.md
index 006bf5a3d5..63ba3e9aa8 100644
--- a/docs/ci-verification.md
+++ b/docs/ci-verification.md
@@ -1,6 +1,23 @@
 # CI verification
 
-## Current selected-family replay: #5599
+## Current selected-family replay: #6030
+
+The [selected record](../certificates/selected-result.json) binds conditional
+κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md),
+[validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json),
+and [explicit source closure](../certificates/frontier6030-source.json).
+`make frontier6030-verify` follows that source-bound selected replay. The review
+separates retained normal primary macOS/Linux evidence from fresh independent
+word/invoice/native, original caller, adapted caller and optimized primary checks.
+Consult its receipts for exact commands, source heads and limits; the #5599
+checkpoint below retains its own historical replay details.
+
+The five inherited framework assumptions remain. Neither the full uniform word
+nor a complete rounded multiplier is materialized. A source/metadata check is
+not an operator replay or a formal theorem proof. Routine research submissions
+do not need to rerun this selected-family replay.
+
+## Historical selected-family replay: #5599
 
 The [selected record](../certificates/selected-result.json) binds conditional
 κ = 0.00310045 to the [proof review](research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md)
diff --git a/docs/research/current-status.md b/docs/research/current-status.md
index a84ac12213..c49a245adc 100644
--- a/docs/research/current-status.md
+++ b/docs/research/current-status.md
@@ -1,6 +1,6 @@
 # Current reviewed status
 
-Selected conditional κ: **0.003125804 = 781451/250000000**, DreamingOfClouds'
+Selected conditional κ: **0.003125804** = 781451/250000000, DreamingOfClouds'
 PR6030 on the cumulative P104 construction. The complete caller counts 13,444
 productive fields and 66,834 paid calls. The saving is about 0.81775% above the
 preceding selected PR5599 claim 0.00310045.
diff --git a/research/outer-representation-budget/PROOF.md b/research/outer-representation-budget/PROOF.md
new file mode 100644
index 0000000000..d1856c6d4b
--- /dev/null
+++ b/research/outer-representation-budget/PROOF.md
@@ -0,0 +1,169 @@
+# Precision, total stock and the paid outer fallback
+
+Prepared by [zxv](https://github.com/zxv), with substantial OpenAI Codex assistance. Apache-2.0. This is a scoped written proof about an explicitly changed admission contract, with exact arithmetic corroboration. It is not an implemented supplier or a complete multiplication theorem.
+
+## 1. Actual sources and the changed question
+
+The scientific baseline is canonical main `721c03822c421b7f7fcbb2598993b947c4d88419`, selected PR6030 at κ = 0.003125804, priority revision 8. Its `pricing.py` calls the unchanged `ledger` in `research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py`. That function supplies 54 strict and three functional predicates; pricing adds the fourth functional predicate `β(1−atom)>0`, with atom = 1/250. The source pins are in SOURCES.json.
+
+At the selected baseline, U is a completed complex uniform saving and B is the admitted ordinary BIT saving. For the hypothetical changed contract below, U and B are completed saving budgets on the above-cutoff outer call domains; all lower-width work is charged separately. Neither is a raw moment crossing, and an above-cutoff budget is not a newly admitted all-size ordinary supplier. Put
+
+$$M=\min(U,B,1/32),\qquad c=3/32.$$
+
+[Nick Petalas](https://github.com/petalas)'s [PR5984](https://github.com/CrocSwap/integer-mult-bounds/pull/5984) proves the original arithmetic region `OLD < κ < M`. Here OLD is the inherited bookkeeping constant 0.001730970419199163702738, not a mathematical lower limit on multiplication. We credit that result; the new question is what changes when the supplier's representation has a different precision and total-stock envelope, including the fallback's actual cost.
+
+The nine source savings, before the change, are exactly:
+
+| Source row | Saving below outer exponent one |
+|---|---|
+| main_transform | εq |
+| global_coordinate_router | a |
+| fused_gaussian | 1−ε+qβ |
+| group_bit_router | 1−ε+aβ |
+| group_scans | 1−ε+β |
+| boundary_algebraic_matrix | c+ξ−ε |
+| sparse_union_movement | ξ+1/2−ε |
+| polynomial_products | ε |
+| microbox_face_corrections | 79−ε−β |
+
+The source definition is `ξ=ε(1+q)−c+layout`. All nine savings must strictly exceed κ. The supplier-ordering checks give `0<q<a<b<min(U,1/32)` and `a<B`. The source membership calculation requires
+
+$$2\epsilon-1-\beta>0.$$ 
+
+This last condition matters once ε cannot approach one.
+
+## 2. A sufficient *interface*, not a constructed supplier
+
+The following is the declared changed contract. It retains the same analytic decomposition, fixed tapes, global complete-field calls, arbitrary/dirty inputs, completed endpoints, restoration, native correctness, finite compiler, and inherited precision/recovery hypotheses. The five selected assumptions are not discharged. Every constant below must be fixed and computable before input length varies.
+
+Let p = Θ(log n), total represented bit volume V = Θ(n), dimension d = Θ(p^ε), and group width g = Θ(p^β), as in the retained outer assembly. Fix rational parameters
+
+$$\rho\ge1,\qquad 0\le\nu<1,\qquad \zeta\ge0,\qquad s=\frac{\zeta}{1-\nu}.$$
+
+1. **Precision.** The prescribed common-grid storage and completed-defect propagation use at most `C d^ρ polylog(d)` guard bits globally, and `C h^ρ polylog(h)` at active width h. They must fit in Θ(p)-bit records with strict power slack: `ρε<1` and `ρβ<1`. A storage bound alone is not a completed-error guarantee.
+2. **Total stock.** The logarithmic reserve, measured in complete selectable chunks, is at most `C(log(2h)+h^ν p^ζ (log(2p))^A+1)`. This bounds the product of simultaneous stock requirements, not their maximum. Borrowing, row padding, layout exposure and restoration obey the retained contracts. This envelope includes inherited reserves.
+3. **Charged completion.** Above a cutoff `H(p)=ceil(p^t)` with **t>s**, the completed supplier meets its promised U/B runtime, including every internal charge. Below H, the wrapper processes axes individually in `O(V H(p) polylog(p))` time. The enclosing schedule has `O(p^(ε−β) polylog(p))` grouped windows. No other changed fee is omitted. A different fallback or extra per-window cost needs its own ledger.
+
+For h ≥ H and h ≤ p, the stock fraction is bounded by a fixed multiple of
+
+$$\frac{\log(2p)+1}{p^t}+p^{\zeta-t(1-\nu)}(\log(2p))^A=o(1).$$
+
+Thus all fixed reserve fractions are eventually available. At a root group we additionally need `t<β`. The strict `t>s` gap absorbs every fixed logarithm and constant; an exact p^s cutoff is not asserted sufficient.
+
+The source audit explicitly handles a polylogarithmic residual individually when ζ=0. Here that residual may have a positive power of p. Its grouped cost is
+
+$$O\!\left(n\,p^{\epsilon-\beta+t}\operatorname{polylog}p\right).$$
+
+Consequently the **group_scans** saving becomes
+
+$$\boxed{1-\epsilon+\beta-t}.$$
+
+This row conservatively pays both the original scans and the additional grouped fallback. It is a changed accounting contract; the selected source is never edited. A full-width main-layer fallback contributes saving `ε−t`. It needs no further binding row because
+
+$$1-\epsilon+\beta-t<\epsilon-t$$
+
+by the retained membership inequality. The new group row already funds it. This domination prevents an uncharged second residual.
+
+The precise arithmetic model retains every source check, strengthens `group_scans_above_kappa` as displayed, and appends five checks:
+
+$$1-\rho\epsilon>0,\quad 1-\rho\beta>0,\quad \beta(1-\nu)-\zeta>0,\quad t-s>0,\quad\beta-t>0.$$
+
+There are 63 predicates in total. They are *sufficient strict exponent tests under this interface*. Failing a test is an obstruction to this policy, not a lower bound for an algorithm with a tighter envelope, another representation, a faster fallback, or another outer schedule.
+
+## 3. Exact admitted region
+
+**Theorem.** Let U,B>0 and κ be rational, and let the rational envelope domain above hold. There are rational free outer parameters and a rational cutoff t satisfying all 63 predicates if and only if
+
+$$\boxed{\rho(1+s)<2,\qquad
+\mathrm{OLD}<\kappa<\min\left(\frac{M}{\rho},\frac1\rho-s\right).}$$
+
+Every inequality is strict. The right endpoint is a supremum and is not attained.
+
+### Necessity
+
+Set R=1/ρ. The guard gives ε<R. From `β>t>s` and membership, `2ε−1>β>s`. Hence `s<2R−1`. From the source ordering and main row, `κ<εq<εM<RM`. Finally the charged group row and membership give
+
+$$\kappa<1-\epsilon+\beta-t<\epsilon-t<R-s.$$
+
+Two exact positive-weight certificates make the obstruction especially easy to check. Denote the five relevant slacks by
+
+$$G=1-\rho\epsilon,\quad A=2\epsilon-1-\beta,\quad
+D=\beta-t,\quad E=t-s,\quad F=1-\epsilon+\beta-t-\kappa.$$
+
+Then
+
+$$\frac G\rho+\frac{A+D+E}{2}=R-\frac{1+s}{2},\qquad
+\frac G\rho+A+F+E=R-s-\kappa.$$
+
+All coefficients are positive. Either nonpositive right side contradicts strict feasibility. The baseline inequality is inherited directly.
+
+### Sufficiency: one rational construction for the whole region
+
+Assume the boxed conditions. Choose
+
+$$L=\max\left(\kappa/M,\kappa+s,(1+s)/2\right),\qquad
+\epsilon=(L+R)/2.$$
+
+Then `1/2<ε<R≤1`. Set
+
+$$q=(\kappa/\epsilon+M)/2,\qquad
+a=(2q+M)/3,\qquad b=(q+2M)/3.$$
+
+Thus `κ<εq<q<a<b<M≤1/32`. In particular both suppliers strictly fund the effective savings. Choose
+
+$$\eta=\min\left(\frac{2\epsilon-1-s}{2},\frac{\epsilon-s-\kappa}{2},\frac{1-\epsilon}{2}\right),
+\qquad\beta=2\epsilon-1-\eta.$$
+
+All three entries of the minimum are positive. Hence `s<β<2ε−1<ε<1`, and
+
+$$1-\epsilon+\beta-s-\kappa=\epsilon-s-\kappa-\eta>0.$$
+
+Take
+
+$$\delta=\frac14\min\{\beta-s,\ 1-\epsilon+\beta-s-\kappa,\ \epsilon-s-\kappa\},
+\qquad t=s+\delta.$$
+
+This gives `s<t<β`, positive stock slack `(1−ν)(β−s)`, positive charged group slack, and positive main residual slack `ε−t−κ`.
+
+For the remaining geometry take
+
+$$h=\min((\epsilon-1/2)/2,1/64),\quad
+\mathrm{layout}=c-\epsilon q-h,\quad
+r_0=(1-\rho\epsilon)/4,\quad
+\mathrm{stop}=(b-a)/(2b).$$
+
+Here `ξ=ε−h`; `layout>3/64`, `1/2<ξ<ε<1`, and `0<stop<1`. The following covers every source family of predicates.
+
+- **Endpoint and leaf order.** `0<q<a<b<M` supplies all supplier gaps. The leaf saving is `(1−stop)b=(a+b)/2>a>q`. Since b>a, the internal exponent is `1−a`. With `λ=1−(q+a)/2`, every λ/internal/leaf gap is strictly positive.
+- **Dimension and headers.** `0<β<2ε−1<ε<1` gives the positive group, support-span, key, membership, union-header and tag inequalities. `ε−a>0` because ε>1/2 and a<1/32. Both new precision guards hold because `β<ε<R`.
+- **Global and group gauges.** `0<r0≤(1−ε)/4`. Also `3−2ξ−β=4(1−ε)+2h+η>r0`; both group gauge checks and the global gamma checks hold. The positive logarithm-absorption row is r0 itself.
+- **Gaussian ordering.** `ε−β=1−ε+η≤3(1−ε)/2`. Thus `1−ε+qβ−εq≥(1−ε)(1−3q/2)>0`. The fused Gaussian saving exceeds the main saving; the group BIT saving is still larger because a>q and β>0.
+- **Other outer rows.** The global router saving a exceeds κ. The boundary saving is `c−h≥5/64>κ`; the sparse-union saving is `1/2−h≥31/64>κ`. The polynomial saving ε exceeds κ; the microbox saving `79−ε−β>77` does too. The group scan/fallback row was funded above.
+- **Constants and inherited functional predicates.** `2^45−7^16`, 2, 5 and 7/2 remain positive. The halo/microbox bounds follow from ε,β<1. All inherited functional checks are positive: `1−β`, `β(1−3/1000)`, `79−ε−β`, and `β(1−1/250)`. The original semantic `1−ε` guard is retained as well.
+
+This proves all 63 predicates, not merely their minimum or the nine outer rows. Exact source evaluation corroborates this construction on 4,056 parameter points, including points 10^-24 below their supremum. The written argument supplies the universal quantifiers; the finite grid does not.
+
+## 4. Recovery and the meaning of the precision hypothesis
+
+The retained upstream assembly has `Tp=Θ(n)`, radix digits with at most b bits, coefficient bound `q_digit(2^b−1)^2<2^(3b)`, no cyclic wraparound, two source-normalization factors S, and a strict final error below 1/2 before nearest-integer recovery. Its exact carry scan then costs O(n). These algebraic recovery facts do not impose a new supplier-saving conversion such as a/(1+a).
+
+A useful sufficient completed-error contract is
+
+$$|\widetilde c_j-c_j|\le p^J2^{A b+C d^\rho-p}$$
+
+for fixed computable A,C,J, with all producer/consumer defects, both S factors, input scales and restoration accounted for. If an applicable analytic implementation permits `p=K b` for fixed K>A, then `ρε<1` gives `C d^ρ=o(p)` and the displayed bound is eventually below 1/2. Record widths remain O(p). This is the elementary implication that justifies using the guard test; it does **not** construct implementations meeting that error contract or prove that a changed analytic implementation admits the chosen K. Those are explicit admission obligations.
+
+At error exactly 1/2 the observation 1/2 is consistent with coefficients zero and one, so strict recovery slack is necessary for unrestricted nearest-integer decoding. The verifier checks this calibration only; it does not replay the numerical Gaussian path. In particular a narrow local grid statement, a small endpoint defect or a favorable final exact operator does not alone imply the completed-error contract.
+
+## 5. Target-scale consequences and a falsified screen
+
+For some κ>.01 to be admissible under this policy, the exact necessary and sufficient conditions, apart from the harmless inherited OLD threshold, are
+
+$$M>.01\rho,\qquad s<1/\rho-.01,\qquad \rho(1+s)<2.$$
+
+- **Quadratic prescribed guards fail in this geometry.** If ρ≥2, even s=0 cannot pass. The contradiction already comes from precision, positive group width and membership. A tighter actual guard, cheaper membership representation or another outer schedule can escape it; an O(d²) upper bound alone is not a lower bound on the supplier's necessary precision.
+- **Linear precision with no power of p in stock recovers PR5984.** For ρ=1, ζ=0, ν<1, the region reduces exactly to `OLD<κ<M`. The selected admitted B=.0034 still excludes .01. No hypothetical precision change makes the selected suppliers sufficient.
+- **Superlinear precision need not be fatal.** Hypothetical completed suppliers U=B=.02, ρ=3/2, ν=1/2, ζ=.05 have s=.1 and permit κ=.011. RESULT.json provides all rational parameters and all nine savings. They do not supply the suppliers.
+- **Largest-call stock fit can falsely admit κ=.011.** Let U=B=.02, ρ=1, ν=1/2 and ζ=.4975, so s=.995. PR5984's original slack family at κ=.011 passes all original 58 checks. It also passes both new precision guards and stock fit at the largest group. Taking t=.995001 passes both cutoff checks. Nevertheless the paid fallback saving is only `16993/7000000` (about .00242757), so the new group row rejects. The exact supremum for *any* parameters under this policy is .005. The counterexample falsifies the free-fallback screen; it alleges no error in the source ζ=0 ledger or selected stock.
+
+The prescribed envelope and fallback can be conservative. The obstruction says exactly which contract has to change: reduce the actual guard exponent, reduce total stock or its precision dependence, supply a faster charged small-width routine, or replace the membership/group schedule. It is not a universal κ ceiling.
diff --git a/research/outer-representation-budget/README.md b/research/outer-representation-budget/README.md
new file mode 100644
index 0000000000..e18ef9beff
--- /dev/null
+++ b/research/outer-representation-budget/README.md
@@ -0,0 +1,58 @@
+# Quadratic prescribed guards cannot fit the current outer assembly
+
+**Scoped proof and exact arithmetic evidence. No new supplier or κ.**
+
+The current nine outer rows do not turn a favorable supplier moment into a multiplication theorem. A proposed representation must also fit its precision, total simultaneous stock and small-width fallback into the actual caller.
+
+For the explicitly declared contract in [PROOF.md](PROOF.md), let U and B be the completed above-cutoff complex and BIT saving budgets, and put
+
+$$M=\min(U,B,1/32),\qquad s=\frac{\zeta}{1-\nu}.$$
+
+The prescribed precision guard grows as `d^ρ polylog(d)`, and the complete logarithmic stock reserve at active width h is bounded by `h^ν p^ζ polylog(p)`, where ρ≥1 and 0≤ν<1. The outer schedule retains its complete-field, restoration, native, compiler, tape and analytic premises. A cutoff `p^t` with t>s is processed individually, with its cost charged.
+
+**The exact strict exponent region is**
+
+$$\boxed{\rho(1+s)<2,\qquad
+\mathrm{OLD}<\kappa<\min\left(M/\rho,\ 1/\rho-s\right).}$$
+
+OLD is the inherited ledger's bookkeeping threshold, not a general lower limit. The proof supplies rational parameters for every interior point and positive-weight obstruction identities for the two stock/fallback boundaries. The one changed outer saving is `group_scans: 1−ε+β → 1−ε+β−t`; the strengthened row also pays the full-width residual.
+
+For some κ>.01, this policy needs `M>.01ρ`, `s<1/ρ−.01`, and `ρ(1+s)<2`. In particular, quadratic or larger **prescribed** guards cannot satisfy the retained membership geometry even with ideal suppliers. A loose O(d²) upper bound is not a precision lower bound; a tighter actual envelope or another representation can escape this obstruction.
+
+## Significance for researchers
+
+This gives a representation-level admission target before another supplier search. Linear precision with ζ=0 recovers [Nick Petalas](https://github.com/petalas)'s [PR5984](https://github.com/CrocSwap/integer-mult-bounds/pull/5984) region `OLD<κ<M`, which is credited rather than claimed again. Precision-dependent stock introduces a paid fallback term that a largest-call fit test misses. The selected PR6030 remains complex-limited at κ=.003125804 with admitted BIT .0034; the hypothetical examples do not raise either budget.
+
+A concrete falsification sets U=B=.02, ρ=1, ν=1/2 and ζ=.4975. At κ=.011 the original 58 predicates, the two added precision checks, total-stock fit and both cutoff checks all pass. Only the charged fallback row fails: its saving is `16993/7000000 ≈ .00242757`. The exact supremum of this policy is .005. This falsifies a free-fallback screen, and alleges no fault in the retained ζ=0 construction.
+
+## Evidence and scope
+
+[RESULT.json](RESULT.json) records 4,056 rational witnesses, all 63 predicates at every witness, 300 arbitrary-parameter checks of the obstruction identities, independently restated nine-row formulas, strict-boundary exclusions and the false-positive control. Examples include points 10^-24 below their supremum and hypothetical κ=.011 contracts with linear and 3/2-power precision guards. The written proof supplies universal claims; finite samples corroborate them.
+
+All live sources are SHA256-authenticated before evaluation. The actual source ledger is executed unchanged from its authenticated text. Normal and optimized registered CPython 3.12 replays are read-only. [SOURCES.json](SOURCES.json) pins canonical main `721c03822c421b7f7fcbb2598993b947c4d88419`; the selected record and task catalogue are historical provenance. [TASK.json](TASK.json) records the explicit backward-interface assignment and changed scope. Coordination: [Discussion6056](https://github.com/CrocSwap/integer-mult-bounds/discussions/6056).
+
+No finite helper word, changed supplier, native map, fast fallback, complete rounded multiplier, selected replay, independent human review or proof-assistant check is supplied. Inherited assumptions remain. The theorem characterizes the declared strict accounting policy, not all representations or multiplication algorithms. A tighter guard, smaller stock, faster fallback or changed membership schedule requires reassessment.
+
+## Reproduce
+
+From the repository root, CPython 3.12 and the standard library:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/outer-representation-budget
+python3.12 -I -B research/outer-representation-budget/verify.py
+python3.12 -I -O -W error -B research/outer-representation-budget/verify.py
+```
+
+Expected final marker: `PASS_OUTER_REPRESENTATION_BUDGET witnesses=4056 predicates=63 dual_checks=300 RECEIPT_MATCH no_new_kappa`. `--emit` prints a fresh receipt without modifying files.
+
+## Open next questions
+
+1. **Bind an actual changed supplier to the growth contract.** First extract a complete chronological precision/error envelope and the product of simultaneous reserves at its real outer calls. This determines whether κ>.01 needs a different representation. Actual suppliers and their error/runtime guarantees remain missing; a raw moment or local grid statement is insufficient.
+2. **Replace the expensive individual-axis fallback.** First give one completed routine below `p^(ζ/(1−ν))` with a paid better exponent, arbitrary dirty inputs, storage and returned grid. That could improve the `1/ρ−s` cap. No such routine is implemented here.
+3. **Change the membership/record interface.** First derive a complete alternative to the source cost `β+2(1−ε)<1`, including headers, source-prime arithmetic and tape scans. This is the precise route by which a quadratic prescribed guard could reopen. Faster membership arithmetic is not assumed.
+
+The structured versions and blockers are in [TASK.json](TASK.json).
+
+## Credit
+
+Prepared by [zxv](https://github.com/zxv), with substantial OpenAI Codex assistance in proof, code, verification and writing. Apache-2.0. [Nick Petalas](https://github.com/petalas) supplied PR5984's unchanged-ledger theorem. The source outer formulas retain [Vlado Vojdanovski](https://github.com/Vlado-V)'s PR1673 and [Jeremy Kothe](https://github.com/jeremykothe2)'s PR1758 and [Chafik Boukhalfa](https://github.com/chafreaky)'s PR1786 attribution, the radix-union/Strassen/fine-prime lineage and its notices. The PR4359 ledger, finite-template semantic-precision and complete-stock arguments, [DreamingOfClouds](https://github.com/DreamingOfClouds)'s PR6030 caller, and retained Harvey–van der Hoeven/OpenAI manuscript framework remain predecessor work. No frozen source is changed.
diff --git a/research/outer-representation-budget/RESULT.json b/research/outer-representation-budget/RESULT.json
new file mode 100644
index 0000000000..20706e6deb
--- /dev/null
+++ b/research/outer-representation-budget/RESULT.json
@@ -0,0 +1,101 @@
+{
+  "dual_identity_checks": 300,
+  "exact_supremum": "min(M/rho, 1/rho-s)",
+  "examples": [
+    {
+      "cutoff": "43/192",
+      "kappa": "11/1000",
+      "label": "hypothetical_linear_pass",
+      "margins": {
+        "boundary_algebraic_matrix": "5/64",
+        "fused_gaussian": "5761/110400",
+        "global_coordinate_router": "34/2875",
+        "group_bit_router": "601/11500",
+        "group_scans": "137/192",
+        "main_transform": "9/800",
+        "microbox_face_corrections": "3703/48",
+        "polynomial_products": "23/24",
+        "sparse_union_movement": "31/64"
+      },
+      "minimum_strict_slack": "1/23000",
+      "nu": "1/250",
+      "parameters": {
+        "a": "34/2875",
+        "b": "137/11500",
+        "beta": "43/48",
+        "bit_saving": "3/250",
+        "complex_uniform_saving": "3/250",
+        "epsilon": "23/24",
+        "kappa": "11/1000",
+        "layout": "107/1600",
+        "q": "27/2300",
+        "r0": "1/96",
+        "stop": "1/274"
+      },
+      "rho": "1",
+      "zeta": "0"
+    },
+    {
+      "cutoff": "11/96",
+      "kappa": "11/1000",
+      "label": "hypothetical_superlinear_pass",
+      "margins": {
+        "boundary_algebraic_matrix": "5/64",
+        "fused_gaussian": "115247/292000",
+        "global_coordinate_router": "106/5475",
+        "group_bit_router": "259339/657000",
+        "group_scans": "209/480",
+        "main_transform": "139/12000",
+        "microbox_face_corrections": "2347/30",
+        "polynomial_products": "73/120",
+        "sparse_union_movement": "31/64"
+      },
+      "minimum_strict_slack": "7/43800",
+      "nu": "1/2",
+      "parameters": {
+        "a": "106/5475",
+        "b": "431/21900",
+        "beta": "19/120",
+        "bit_saving": "1/50",
+        "complex_uniform_saving": "1/50",
+        "epsilon": "73/120",
+        "kappa": "11/1000",
+        "layout": "1597/24000",
+        "q": "139/7300",
+        "r0": "7/320",
+        "stop": "7/862"
+      },
+      "rho": "3/2",
+      "zeta": "1/20"
+    }
+  ],
+  "excluded_grid_families": 2872,
+  "free_fallback_false_positive": {
+    "charged_fallback_saving": "16993/7000000",
+    "exact_supremum": "1/200",
+    "failures": [
+      "group_scans_above_kappa"
+    ],
+    "original_predicates_pass": 58,
+    "required_kappa": "11/1000",
+    "stock_fit_slack": "1/1750"
+  },
+  "geometry_condition": "rho*(1+s)<2",
+  "inherited_predicates": 58,
+  "representation_predicates": 5,
+  "scope": "Written scoped proof plus exact arithmetic corroboration. Hypothetical contracts only; no implemented supplier, new kappa or framework assumption discharge.",
+  "selected_B": "17/5000",
+  "selected_U": "10940329/3500000000",
+  "selected_target_001_supported": false,
+  "source_sha256": {
+    "certificates/frontier6030/CLAIM.json": "9cee8a1304fa893be3d3b641eda42fdd9b2fd6a5ac2124fb891de7a1a5e8d92e",
+    "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md": "67569961d068633c6ff3ac9dfde47a0c17f0da6d20432799dcc920cff92b5779",
+    "research/outer-ledger-kappa-region/PROOF.md": "ee523eeca3fc344fd4177ac345f605dbb04edad9732da2c23ca60365f56897e9",
+    "research/p104-helper470-twin-rung-removal/pricing.py": "3c6cf2966ccfe5a5fb6c90f89f46ac224ea455127e35dd34975683c68c36d710",
+    "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15",
+    "upstream/build/sections/08-assembly.tex": "763d7945b1e1ec4ebae9b799bcefcc45fa9bae6e2ffad799868a9c3d513dbd4a"
+  },
+  "status": "PASS_OUTER_REPRESENTATION_BUDGET",
+  "total_predicates": 63,
+  "witnesses": 4056
+}
diff --git a/research/outer-representation-budget/SOURCES.json b/research/outer-representation-budget/SOURCES.json
new file mode 100644
index 0000000000..2d46df422e
--- /dev/null
+++ b/research/outer-representation-budget/SOURCES.json
@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/frontier6030/CLAIM.json",
+      "usage": "input",
+      "git_blob": "f32ff3779274a349dc8af2e84a4c6234c6d62406",
+      "sha256": "9cee8a1304fa893be3d3b641eda42fdd9b2fd6a5ac2124fb891de7a1a5e8d92e"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md",
+      "usage": "input",
+      "git_blob": "e8b7ef8956ece5bd493cbf52113916e5dc288535",
+      "sha256": "67569961d068633c6ff3ac9dfde47a0c17f0da6d20432799dcc920cff92b5779"
+    },
+    {
+      "path": "research/outer-ledger-kappa-region/PROOF.md",
+      "usage": "input",
+      "git_blob": "300f2dd0dc745a6f55fbdb26c4abf70db7e2d5fa",
+      "sha256": "ee523eeca3fc344fd4177ac345f605dbb04edad9732da2c23ca60365f56897e9"
+    },
+    {
+      "path": "research/p104-helper470-twin-rung-removal/pricing.py",
+      "usage": "input",
+      "git_blob": "65bb723f8558dc60ff92764db1a43d8bf438aa09",
+      "sha256": "3c6cf2966ccfe5a5fb6c90f89f46ac224ea455127e35dd34975683c68c36d710"
+    },
+    {
+      "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py",
+      "usage": "input",
+      "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59",
+      "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15"
+    },
+    {
+      "path": "upstream/build/sections/08-assembly.tex",
+      "usage": "input",
+      "git_blob": "337810a1d9a58a2ecf14123420923c039ba322a6",
+      "sha256": "763d7945b1e1ec4ebae9b799bcefcc45fa9bae6e2ffad799868a9c3d513dbd4a"
+    }
+  ]
+}
diff --git a/research/outer-representation-budget/TASK.json b/research/outer-representation-budget/TASK.json
new file mode 100644
index 0000000000..68fceb9c93
--- /dev/null
+++ b/research/outer-representation-budget/TASK.json
@@ -0,0 +1,124 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Backward from the selected nine outer rows: exact strict admission region for prescribed d^rho precision, h^nu p^zeta total stock and a paid individual-axis fallback. No framework assumption is discharged.",
+  "scope_change_reason": "Explicit assignment asks for a changed outer/analytic interface supporting kappa>.01. PR5984 already resolves the unchanged ledger; this contribution changes representation growth and pays the newly polynomial fallback rather than repeating that theorem.",
+  "bottleneck_link": "Separates supplier-saving budgets from the precision, record geometry and total-stock/fallback contract needed to use them. Supplies exact target-scale requirements and a falsified optimistic screen.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after one quantified admission theorem and its counterexample pass source-bound normal/optimized bounded checks. No local helper optimization or construction expansion.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; RESULT.json: 4056 exact witnesses checking all 63 predicates, 300 dual-identity checks, independently restated nine rows and the free-fallback false positive. No selected cold replay or supplier implementation.",
+  "author": "zxv",
+  "ai_assistance": "Substantial OpenAI Codex assistance in mathematical derivation, implementation, verification, source review and writing. No subagents, independent human or formal-kernel review.",
+  "open_questions": [
+    {
+      "question": "Can an actual changed supplier meet this complete growth contract?",
+      "why_it_matters": "Tests whether both above-cutoff saving budgets can support kappa>.01 after representation costs.",
+      "first_step": "Extract all-prefix/completed-error and total simultaneous stock envelopes at one actual outer call, including every charged residual.",
+      "blocked_by": "A new admitted supplier and completed implementation/error contracts are not supplied."
+    },
+    {
+      "question": "Can a paid faster small-width routine improve the individual-axis fallback?",
+      "why_it_matters": "Would change the 1/rho-s cap.",
+      "first_step": "Implement one complete below-cutoff routine with arbitrary dirty inputs, returned grid, stock, restoration and tape costs.",
+      "blocked_by": "No such routine has been constructed or priced here."
+    },
+    {
+      "question": "Can a complete membership interface weaken beta+2(1-epsilon)<1?",
+      "why_it_matters": "Would reopen the quadratic prescribed-guard exclusion.",
+      "first_step": "Derive the actual headers, membership arithmetic and scans under a changed record representation.",
+      "blocked_by": "The existing membership formula is retained; no alternative implementation is assumed."
+    }
+  ],
+  "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/6056",
+  "freshness": {
+    "canonical_main": "721c03822c421b7f7fcbb2598993b947c4d88419",
+    "priority_revision": 8,
+    "initial_fetch_utc": "2026-10-28T03:34:21Z",
+    "overlap_open_prs_utc": "2026-10-28T03:41:39Z",
+    "overlap_discussions_utc": "2026-10-28T03:42:58Z",
+    "coverage": "326 open PR bodies and 5708 discussion records with complete remote pagination at first snapshot; sparse local corpus, historical diff contents and unpublished work remain limits. Exact HEAD README/PROOF grep for superlinear/quadratic/guard/stock terms found only distinct historical precision and helper-invoice notes.",
+    "final_fetch_utc": "2026-10-28T03:58:12Z",
+    "final_canonical_main": "721c03822c421b7f7fcbb2598993b947c4d88419",
+    "final_open_prs_utc": "2026-10-28T03:58:12Z",
+    "final_discussions_utc": "2026-10-28T03:59:24Z",
+    "final_coverage": "329 open PR bodies and 5715 Discussion records, complete remote pagination. Matches are the canonical claim itself, distinct PR3920 parent-row boundary and R437 pivot/fallback notes; sparse local notes, historical diff contents and unpublished work remain limits."
+  },
+  "validation": {
+    "environment": "macOS, CPython 3.12.8, standard library only",
+    "registered_normal_and_optimized": "PASS, each with 4056 rational witnesses, all 63 predicates, 300 dual-identity checks and meaningful failure controls",
+    "navigation_repair": "Unchanged PR6050 commit cherry-picked; six existing current-status/navigation tests pass",
+    "publication_bytes": "PASS before final metadata update; rerun at publication commit",
+    "global_sparse_replay_planner": "Stopped after more than two minutes waiting without a matrix. No complete global-plan result claimed.",
+    "not_run": [
+      "selected cold replay",
+      "numerical Gaussian implementation",
+      "Lean",
+      "Docker",
+      "full-history provenance preflight (checkout is shallow)",
+      "independent human review"
+    ]
+  }
+}
diff --git a/research/outer-representation-budget/VERIFY.json b/research/outer-representation-budget/VERIFY.json
new file mode 100644
index 0000000000..e4df5fda55
--- /dev/null
+++ b/research/outer-representation-budget/VERIFY.json
@@ -0,0 +1,41 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/frontier6030/CLAIM.json",
+    "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md",
+    "research/outer-ledger-kappa-region/PROOF.md",
+    "research/p104-helper470-twin-rung-removal/pricing.py",
+    "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py",
+    "upstream/build/sections/08-assembly.tex"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Authenticated source, 4056 rational witnesses across 63 predicates, all nine formulas, dual identities, strict boundaries and paid-fallback false positive."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Same scientific arithmetic and rejection controls under optimized Python."
+    }
+  ]
+}
diff --git a/research/outer-representation-budget/verify.py b/research/outer-representation-budget/verify.py
new file mode 100644
index 0000000000..a1fb4faf94
--- /dev/null
+++ b/research/outer-representation-budget/verify.py
@@ -0,0 +1,235 @@
+#!/usr/bin/env python3
+"""Exact outer region for prescribed precision/stock envelopes.
+
+zxv, with substantial OpenAI Codex assistance. Apache-2.0.
+Unchanged ledger: zxv PR4359. Unpenalized region: Nick Petalas PR5984.
+Arithmetic evidence only; no supplier admission or new kappa.
+"""
+from fractions import Fraction as F
+from hashlib import sha256
+from pathlib import Path
+import argparse
+import json
+import random
+import types
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+CAP, ATOM = F(1, 32), F(1, 250)
+LEDGER = 'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py'
+
+
+def need(value, message):
+    if not value:
+        raise ValueError(message)
+
+
+def authenticate():
+    manifest = json.loads((HERE/'SOURCES.json').read_text())
+    pins = {}
+    for row in manifest['files']:
+        if row['usage'] == 'input':
+            raw = (ROOT/row['path']).read_bytes()
+            need(sha256(raw).hexdigest() == row['sha256'], 'Source changed: '+row['path'])
+            pins[row['path']] = row['sha256']
+    # Direct compilation avoids a preexisting bytecode import.
+    module = types.ModuleType('pinned_outer_ledger')
+    module.__file__ = str(ROOT/LEDGER)
+    exec(compile((ROOT/LEDGER).read_bytes(), module.__file__, 'exec'), module.__dict__)
+    pricing = (ROOT/'research/p104-helper470-twin-rung-removal/pricing.py').read_text()
+    need('outer_module.ledger(params)' in pricing, 'Selected ledger call')
+    need("params['beta']*(1-atom)" in pricing, 'Fourth selected functional check')
+    return module, pins
+
+
+def source_values(module, p):
+    out = module.ledger(p)
+    need(len(out['strict_checks']) == 54 and len(out['functional_checks']) == 3,
+         'Pinned 54+3 inventory')
+    need(len(out['margins']) == 9, 'Nine actual outer rows')
+    values = dict(out['strict_checks'], **out['functional_checks'])
+    values['actual_new_BIT_stock_sublinear'] = p['beta']*(1-ATOM)
+    return out, values
+
+
+def evaluate(module, p, rho, nu, zeta, cutoff):
+    """Retain every original predicate, charge fallback, append five checks."""
+    out, values = source_values(module, p)
+    s = zeta/(1-nu)
+    margins = dict(out['margins'])
+    margins['group_scans'] -= cutoff
+    values['group_scans_above_kappa'] = margins['group_scans']-p['kappa']
+    values.update(representation_global_guard=1-rho*p['epsilon'],
+                  representation_group_guard=1-rho*p['beta'],
+                  representation_total_stock=p['beta']*(1-nu)-zeta,
+                  cutoff_above_stock_boundary=cutoff-s,
+                  cutoff_below_group=p['beta']-cutoff)
+    need(len(values) == 63, 'All 58 inherited and five representation checks')
+    return values, margins
+
+
+def region(module, U, B, kappa, rho, nu, zeta):
+    need(rho >= 1 and 0 <= nu < 1 and zeta >= 0 and U > 0 and B > 0,
+         'Declared envelope domain')
+    M, R, s = min(U, B, CAP), 1/rho, zeta/(1-nu)
+    return s < 2*R-1 and module.OLD_BASELINE < kappa < min(M*R, R-s)
+
+
+def witness(U, B, kappa, rho, nu, zeta):
+    M, R, s = min(U, B, CAP), 1/rho, zeta/(1-nu)
+    lower = max(kappa/M, kappa+s, (1+s)/2)
+    need(lower < R, 'Witness needs strict representation room')
+    eps = (lower+R)/2
+    q = (kappa/eps+M)/2
+    a, b = (2*q+M)/3, (q+2*M)/3
+    eta = min((2*eps-1-s)/2, (eps-s-kappa)/2, (1-eps)/2)
+    beta = 2*eps-1-eta
+    h = min((eps-F(1, 2))/2, F(1, 64))
+    p = dict(kappa=kappa, complex_uniform_saving=U, bit_saving=B,
+             q=q, a=a, b=b, epsilon=eps, beta=beta,
+             stop=(b-a)/(2*b), r0=(1-rho*eps)/4,
+             layout=F(3, 32)-eps*q-h)
+    gap = 1-eps+beta-s-kappa
+    delta = min(beta-s, gap, eps-s-kappa)/4
+    need(delta > 0, 'Strict cutoff absorbs fixed polylogarithms')
+    return p, s+delta
+
+
+def independent_rows(p, cutoff):
+    eps, beta, q, a = (p[x] for x in ('epsilon', 'beta', 'q', 'a'))
+    xi = eps*(1+q)-F(3, 32)+p['layout']
+    return dict(main_transform=eps*q, global_coordinate_router=a,
+                fused_gaussian=1-eps+q*beta, group_bit_router=1-eps+a*beta,
+                group_scans=1-eps+beta-cutoff,
+                boundary_algebraic_matrix=F(3, 32)+xi-eps,
+                sparse_union_movement=xi+F(1, 2)-eps,
+                polynomial_products=eps, microbox_face_corrections=79-eps-beta)
+
+
+def positive(values):
+    return all(x > 0 for x in values.values())
+
+
+def certificate_identities(values, p, rho, nu, zeta):
+    """Nonnegative-weight obstruction identities; no solver inference."""
+    R, s = 1/rho, zeta/(1-nu)
+    fit = (values['representation_global_guard']/rho
+           + (values['membership_arithmetic_fits_record']
+              + values['cutoff_below_group']
+              + values['cutoff_above_stock_boundary'])/2)
+    paid = (values['representation_global_guard']/rho
+            + values['membership_arithmetic_fits_record']
+            + values['group_scans_above_kappa']
+            + values['cutoff_above_stock_boundary'])
+    need(fit == R-(1+s)/2, 'Stock/geometry dual identity')
+    need(paid == R-s-p['kappa'], 'Paid fallback dual identity')
+
+
+def run():
+    module, pins = authenticate()
+    rng = random.Random(6056)
+    count = excluded = 0
+    grid = [F('.0034'), F('.011'), F('.02'), CAP, F('.05')]
+    rhos = [F(1), F(5, 4), F(3, 2), F(7, 4), F(199, 100), F(2), F(5, 2)]
+    nus = [F(0), ATOM, F(1, 2), F(9, 10)]
+    ss = [F(0), F('.001'), F('.05'), F('.25'), F('.5'), F('.98'), F('.995')]
+    for U in grid:
+        for B in grid:
+            for rho in rhos:
+                for nu in nus:
+                    for s in ss:
+                        zeta = s*(1-nu)
+                        M, R = min(U, B, CAP), 1/rho
+                        top = min(M*R, R-s)
+                        if s >= 2*R-1 or top <= module.OLD_BASELINE:
+                            excluded += 1
+                            continue
+                        for kappa in ((module.OLD_BASELINE+top)/2, top-F(1, 10**24)):
+                            need(region(module, U, B, kappa, rho, nu, zeta), 'Predicted interior')
+                            p, cutoff = witness(U, B, kappa, rho, nu, zeta)
+                            values, margins = evaluate(module, p, rho, nu, zeta, cutoff)
+                            need(positive(values), 'Every source and changed predicate passes')
+                            need(margins == independent_rows(p, cutoff), 'All nine formulas')
+                            need(p['epsilon']-cutoff > kappa, 'Full-width residual also paid')
+                            certificate_identities(values, p, rho, nu, zeta)
+                            count += 1
+                        need(not region(module, U, B, top, rho, nu, zeta), 'Supremum excluded')
+
+    # False positive when stock fit is checked but fallback is free.
+    U = B = F('.02')
+    kappa, rho, nu, zeta = F('.011'), F(1), F(1, 2), F('.4975')
+    d = (min(U, B, CAP)-kappa)/7
+    p = dict(kappa=kappa, complex_uniform_saving=U, bit_saving=B,
+             q=kappa+3*d, a=kappa+4*d, b=kappa+5*d,
+             epsilon=1-d, beta=1-3*d, r0=d/10, stop=d, layout=d)
+    _, old = source_values(module, p)
+    need(positive(old), 'False-positive control passes all original 58 predicates')
+    cutoff = F('.995001')
+    values, margins = evaluate(module, p, rho, nu, zeta, cutoff)
+    failures = sorted(k for k, v in values.items() if v <= 0)
+    need(failures == ['group_scans_above_kappa'], 'Only paid fallback rejects')
+    certificate_identities(values, p, rho, nu, zeta)
+    need(not region(module, U, B, kappa, rho, nu, zeta), 'Exact .005 supremum excludes .011')
+
+    # Corroborate both dual identities on arbitrary rational parameters.
+    for _ in range(300):
+        p0 = {key: F(rng.randint(-200, 200), rng.randint(1, 1000)) for key in
+              ('kappa', 'complex_uniform_saving', 'bit_saving', 'q', 'a', 'b',
+               'epsilon', 'beta', 'r0', 'stop', 'layout')}
+        rho0, nu0 = F(rng.randint(100, 300), 100), F(rng.randint(0, 90), 100)
+        zeta0, cut0 = F(rng.randint(0, 50), 100), F(rng.randint(0, 100), 100)
+        vv, _ = evaluate(module, p0, rho0, nu0, zeta0, cut0)
+        certificate_identities(vv, p0, rho0, nu0, zeta0)
+
+    # Calibration of the strict recovery radius, not a Gaussian replay.
+    for integer in range(-8, 9):
+        lo, hi = F(integer)-F(499, 1000), F(integer)+F(499, 1000)
+        need((lo+F(1, 2)).__floor__() == integer
+             and (hi+F(1, 2)).__floor__() == integer, 'Nearest integer recovery')
+    need(F(1, 2)-0 == 1-F(1, 2), 'Half-unit ambiguity')
+
+    selected = json.loads((ROOT/'certificates/frontier6030/CLAIM.json').read_text())
+    selected_U = next(F(t['saving']) for t in selected['uniform_templates'] if t['family'] == 'complex')
+    selected_B = F(selected['admitted_BIT_saving'])
+    examples = []
+    for label, U0, B0, rho0, nu0, zeta0, k0 in [
+            ('hypothetical_linear_pass', F('.012'), F('.012'), F(1), ATOM, F(0), F('.011')),
+            ('hypothetical_superlinear_pass', F('.02'), F('.02'), F(3, 2), F(1, 2), F('.05'), F('.011'))]:
+        pp, tt = witness(U0, B0, k0, rho0, nu0, zeta0)
+        vv, mm = evaluate(module, pp, rho0, nu0, zeta0, tt)
+        need(positive(vv), 'Explicit target-scale example')
+        examples.append(dict(label=label, kappa=str(k0), rho=str(rho0), nu=str(nu0),
+                             zeta=str(zeta0), parameters={k:str(v) for k,v in pp.items()},
+                             cutoff=str(tt), margins={k:str(v) for k,v in mm.items()},
+                             minimum_strict_slack=str(min(vv.values()))))
+    return dict(status='PASS_OUTER_REPRESENTATION_BUDGET', source_sha256=pins,
+                inherited_predicates=58, representation_predicates=5, total_predicates=63,
+                witnesses=count, excluded_grid_families=excluded,
+                dual_identity_checks=300, exact_supremum='min(M/rho, 1/rho-s)',
+                geometry_condition='rho*(1+s)<2',
+                selected_U=str(selected_U), selected_B=str(selected_B),
+                selected_target_001_supported=region(module, selected_U, selected_B, F('.01'), F(1), ATOM, F(0)),
+                free_fallback_false_positive=dict(original_predicates_pass=58,
+                    stock_fit_slack=str(values['representation_total_stock']),
+                    charged_fallback_saving=str(margins['group_scans']),
+                    required_kappa=str(kappa), failures=failures, exact_supremum='1/200'),
+                examples=examples,
+                scope='Written scoped proof plus exact arithmetic corroboration. Hypothetical contracts only; no implemented supplier, new kappa or framework assumption discharge.')
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--emit', action='store_true')
+    args = parser.parse_args()
+    result = run()
+    if args.emit:
+        print(json.dumps(result, indent=2, sort_keys=True))
+    else:
+        expected = json.loads((HERE/'RESULT.json').read_text())
+        need(result == expected, 'Receipt differs; review before regenerating')
+        print(result['status'], 'witnesses='+str(result['witnesses']),
+              'predicates=63 dual_checks=300 RECEIPT_MATCH no_new_kappa')
+
+
+if __name__ == '__main__':
+    main()