diff --git a/research/typed-primitive-price/.gitattributes b/research/typed-primitive-price/.gitattributes
new file mode 100644
index 0000000000..b7823e3f34
--- /dev/null
+++ b/research/typed-primitive-price/.gitattributes
@@ -0,0 +1 @@
+inputs/* -text
diff --git a/research/typed-primitive-price/FROZEN-INPUTS.json b/research/typed-primitive-price/FROZEN-INPUTS.json
new file mode 100644
index 0000000000..29080fcb6b
--- /dev/null
+++ b/research/typed-primitive-price/FROZEN-INPUTS.json
@@ -0,0 +1,26 @@
+[
+  {
+    "repository": "CrocSwap/integer-mult-bounds",
+    "commit": "dca175fed8ebde8980635fd3b4508b8cba89a1b0",
+    "path": "research/native-quotient-interface/REPAIRED-WARP-WORD.json.gz",
+    "snapshot": "inputs/typed-word.json.gz",
+    "git_blob": "b22174e7a93716a394f2feb45f57a3da4331275a",
+    "sha256": "143b655bdc7aa719d0e3f2a527ed748c50a186997c01c2f3134dd5653d42ae7d"
+  },
+  {
+    "repository": "CrocSwap/integer-mult-bounds",
+    "commit": "dca175fed8ebde8980635fd3b4508b8cba89a1b0",
+    "path": "research/native-quotient-interface/TYPED-QUOTIENT-INTERFACE.md",
+    "snapshot": "inputs/typed-interface.md",
+    "git_blob": "bf4ff1af66ecd566685b481b459b1d846b8f5edb",
+    "sha256": "5e48990d78d0e0b7ca2f79f24338be81e7b2fa2732c261f046d46877f2febbf3"
+  },
+  {
+    "repository": "CrocSwap/integer-mult-bounds",
+    "commit": "1eb8da6cfb35512c0cc2533413e5ca42f48e13c6",
+    "path": "research/kappa-round3-warp-20261022/ARITHMETIC.json",
+    "snapshot": "inputs/round3-arithmetic.json",
+    "git_blob": "c89e009ca4a5ad316c69f0371d885d72045ba415",
+    "sha256": "ab10f6a4a8a4f589d4b094aac663e002c43ec44774e6bd181c51915c7fa7e521"
+  }
+]
diff --git a/research/typed-primitive-price/PROOF.md b/research/typed-primitive-price/PROOF.md
new file mode 100644
index 0000000000..86b640dd4e
--- /dev/null
+++ b/research/typed-primitive-price/PROOF.md
@@ -0,0 +1,156 @@
+# The typed quotient has no recursive primitive discount
+
+Prepared for Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0.
+
+## 1. Exact direct implementations of the supplied interface
+
+Assume the exact typed ABI of PR4654 at
+`dca175fed8ebde8980635fd3b4508b8cba89a1b0`. Its 112 main pairs consist
+of 56 type A and 56 type B. On each pair, Q is a symmetric rank-one
+Gaussian and D a symmetric rank-seven Gaussian on disjoint axes:
+
+```
+A = diag(D,D) S_y(Q^-1),
+B = diag(D,QD) S_y(Q^-1) = S_y(1) diag(D,QD).
+```
+
+The second identity is exact: both B expressions send (X,Y) to
+`(DX, DX+QD Y)`. There is no order-two relation for Q in this proof.
+
+A direct A implementation uses two rank-seven D jobs and one rank-one
+query shear. The query copies X into an owned zero temporary, applies
+Q^-1 with its actual monomial normalizer, adds into Y and clears the
+temporary. This retains the predecessor's owned-erasure hypothesis; it
+does not erase a dirty borrowed field. A direct B uses two D jobs, one
+Q job on Y and one ordinary output addition. Thus each type costs exactly
+`2*7^t+1` in recursive paid moment, t=1-C.
+
+The raw inverse transposes have equally explicit implementations:
+
+```
+A^-T = diag(D^-1,D^-1) S_x(-Q^-1),
+B^-T = S_x(-1) diag(D^-1,Q^-1 D^-1).
+```
+
+The B scalar addition is on the left and acts last. Gaussian inverses
+retain their actual monomial normalizers; rank does not change. The
+verifier checks all four Laurent matrix identities, with independent D
+and Q symbols and every sign and inverse exponent intact.
+
+Across all 112 pairs, direct main execution costs **224 rank-seven jobs
+and 112 rank-one jobs**, in either orientation. It uses at most one owned
+query temporary at a time. The source's 408 helpers remain independent
+arbitrary inputs; implementing each source-normalized helper job directly
+adds its complete actual target moment H_t to the paid list. All helper
+monomial normalizers are retained. No helper target is counted twice.
+
+Some direct helper jobs have rank nine. The fallback therefore does not
+preserve the native word's rank-eight local child cap. The price comparison
+is not drop-in compiler admission: any replacement must recheck child ranks,
+strictification tails and allocation. If a consumer introduces these helpers
+only as fresh independent bystanders, its direct main implementation can
+instead omit both their inputs/targets and their matching direct paid jobs;
+that cancellation preserves the surplus, but changes the caller's inventory.
+
+This is an operator-level fallback and a comparison of recursive paid
+moments. ADDs, copies, clear/erase, monomial wrappers, fixed routing and
+helper normalizers have finite volume-linear work. We do not assert
+identical machine costs, construct a practical multiplier, or independently
+reprove the typed source's native/all-width/phase theorem.
+
+## 2. Strict dominance at every concave exponent
+
+Recounting both emitted source words and their helper endpoints gives
+
+```
+P = {1:2177,2:424,3:389,4:147,5:50,8:8},
+H = {3:2,6:7,7:47,8:139,9:213}.
+```
+
+The native minus direct recursive paid moment is
+
+```
+G(C) = P_t - H_t -224*7^t -112,  t=1-C.
+```
+
+It has G(0)=8. Normalize K(C)=G(C)/7^t. The constant -224
+has derivative zero. In `(P_t-H_t-112)/7^t` the rank coefficients are
+
+```
+{1:2065,2:424,3:387,4:147,5:50,6:-7,7:-47,8:-131,9:-213}.
+```
+
+For 0<=C<1, all derivative contributions are nonnegative except the
+rank-six term. The rank-one term alone contributes at least
+`2065/7 * log(7)`; the rank-six negative contribution has magnitude at
+most `7 log(7/6)`. Since log(7)>1 and log(7/6)<1,
+
+```
+K'(C) > 2065/7 -7 = 288 > 0.
+```
+
+The elementary log inequalities are also enclosed by the pinned exact
+rational interval engine. Therefore
+
+```
+G(C) >= 8 * 7^(-C) > 0,   0<=C<1.
+```
+
+The typed native word is strictly more expensive in recursive paid moment
+than the direct implementation of the *same* main ABI and helper targets,
+for every exponent in the range, including rank mass at C=0.
+
+This is stronger than a failed controller search and different from the
+A-only-path obstruction of PR4660. It applies to the local offer before
+any controller is chosen. A profitable consumer using this offer could
+instead use the cheaper direct implementation, with the same operator
+and independent helper targets. It does **not** prove that every such
+consumer or every Gaussian algorithm is impossible.
+
+## 3. Comparison with the actual round-three native discount
+
+Freeze PR4610 at `1eb8da6cfb35512c0cc2533413e5ca42f48e13c6`:
+
+```
+H0 = {4:28,7:7,8:47,9:326},
+P0 = {1:2201,2:412,3:510,4:127,5:40,8:8}.
+```
+
+Its ordinary all-A, block-eight main interface has direct paid cost
+`H0_t+224*8^t+112`. Put G0=P0_t-H0_t-224*8^t-112.
+Its normalized rank-eight gap G0/8^t starts at -6. The corresponding
+rank-one coefficient is 2089; the only negative derivative contribution
+below rank eight is -7 at rank seven. Hence
+
+```
+(G0/8^t)' > 2089/8 -7 = 2033/8 > 0.
+```
+
+Exact outward enclosures give G0<0 at C=0.0062073960 and G0>0 at
+C=0.0062073961. Thus the original supplier's unique direct-price crossing
+is in that interval. Above it the original offer, too, has no recursive
+discount over direct main jobs and direct helpers. This is a **local price
+crossing**, not an integer-multiplication exponent or a universal ceiling.
+
+At C=.004, the original offer still discounts the direct price by about
+16.9818753 per full invocation. This is useful controller budget; the
+typed quotient instead has a positive surcharge. Complete controller,
+strictification, compiler, BIT, precision and outer conditions remain
+necessary for any actual K claim.
+
+## 4. Source and verification boundary
+
+The source word, typed interface and round-three arithmetic are retained
+byte for byte, with Git blob and SHA256 authentication. Both paid censuses
+and every helper rank are recomputed from the emitted word. The source's
+Clifford and free-group proofs are premises here, not newly audited.
+
+The registered Python replay uses exact Laurent arithmetic and outward
+rational power/log enclosures. It rejects an unpaid B query, a wrong Q
+inverse, missing owned charges and source/profile drift. Passing it does
+not establish a new native construction, selected frontier or theorem.
+
+Credit Dugongue and PR4654, DaysSky's quotient source, Cao Yifan and PR4610,
+Cinna Davis and the PR4440/PR4470/native lineage, zxv, Jacob Alan Sussman,
+the PR4660 B-autonomy observation and all retained predecessor authors.
+The direct factorization of B is credited, not rediscovered here.
diff --git a/research/typed-primitive-price/README.md b/research/typed-primitive-price/README.md
new file mode 100644
index 0000000000..6828a89cdd
--- /dev/null
+++ b/research/typed-primitive-price/README.md
@@ -0,0 +1,52 @@
+# The typed quotient costs more than its direct main primitives
+
+**No new K.** Under the exact A/B interface supplied by PR4654, the native
+word's recursive paid moment is strictly greater than a direct implementation
+of the same main operator and all independent helper jobs, for every
+`0<=C<1`. Its surcharge is at least **8 * 7^(-C)** per invocation.
+
+Read [PROOF.md](PROOF.md). A direct main implementation needs 224 rank-seven
+jobs and 112 rank-one jobs; all 408 helper jobs are also paid. Four exact
+Laurent identities cover both types in both orientations. Every sign,
+inverse power and helper normalizer is retained. This is a comparison of
+recursive prices; fixed routing, scalar, ownership and native admission
+obligations are stated separately.
+
+The direct helper implementation includes rank-nine jobs, so it does not
+retain the native word's rank-eight child cap. Its use in a compiler needs
+new rank/tail checks, or a caller that removes neutral fresh helper jobs
+from both target and paid lists. Local price dominance alone is not admission.
+
+For comparison, PR4610's original block-eight offer has a real discount
+until its unique local price crossing in
+**(0.0062073960, 0.0062073961)**. This crossing is a local budget threshold,
+not a new multiplication exponent or a global controller bound.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/typed-primitive-price
+```
+
+The standard-library replay authenticates the frozen source Git blobs and
+SHA256 values, recounts both emitted paid profiles and all helper targets,
+checks the operator identities, proves the monotone all-exponent bounds,
+and verifies the committed [RESULT.json](RESULT.json). Original compressed
+and CRLF source bytes remain unchanged. `--write` is only an authoring path.
+
+No selected source or shared verifier changes. No selected cold replay,
+new phase/native audit, complete multiplier or independent human theorem
+acceptance is claimed. The typed source remains a constructive local
+interface; this result shows why its lower nominal paid profile alone
+does not justify another controller construction round.
+
+## Open next questions
+
+Seek a changed native word or centre recipe that restores a genuine local
+discount before searching large controllers. The original supplier still
+has about 16.9818753 units of direct-price discount at C=.004; any new
+controller must turn that into a positive complete moment with every idle,
+query, ownership and completion cost included.
+
+Credit Dugongue/PR4654, DaysSky, Cao Yifan/PR4610, the PR4660 B-autonomy
+observation, Cinna Davis's PR4470/controller lineage, zxv, Jacob Alan Sussman
+and the retained source authors. Prepared for Cinna Davis with substantial
+OpenAI Codex assistance; no subagents. Apache-2.0.
diff --git a/research/typed-primitive-price/RESULT.json b/research/typed-primitive-price/RESULT.json
new file mode 100644
index 0000000000..48172ad9e4
--- /dev/null
+++ b/research/typed-primitive-price/RESULT.json
@@ -0,0 +1,90 @@
+{
+  "direct_main_paid": {
+    "1": 112,
+    "7": 224
+  },
+  "new_kappa": false,
+  "normalized_derivative_lower_bound": "288",
+  "original_discount_endpoint": [
+    "1551849/250000000",
+    "62073961/10000000000"
+  ],
+  "original_gap_above": {
+    "lower": "0.000000609979802177861027451394",
+    "upper": "0.000000609979802177861027451395"
+  },
+  "original_gap_below": {
+    "lower": "-0.000000157165757402536960401596",
+    "upper": "-0.000000157165757402536960401595"
+  },
+  "samples": {
+    "0": {
+      "original_direct_minus_native": {
+        "lower": "47.999999999999999999999999999999",
+        "upper": "48.000000000000000000000000000001"
+      },
+      "typed_native_minus_direct": {
+        "lower": "7.999999999999999999999999999999",
+        "upper": "8.000000000000000000000000000001"
+      }
+    },
+    "1/100": {
+      "original_direct_minus_native": {
+        "lower": "-28.953945191895344577529449792159",
+        "upper": "-28.953945191895344577529449792158"
+      },
+      "typed_native_minus_direct": {
+        "lower": "77.902661003205805150124181011979",
+        "upper": "77.902661003205805150124181011980"
+      }
+    },
+    "1/250": {
+      "original_direct_minus_native": {
+        "lower": "16.981875310258539619945498940638",
+        "upper": "16.981875310258539619945498940639"
+      },
+      "typed_native_minus_direct": {
+        "lower": "36.169081320591341659262855607882",
+        "upper": "36.169081320591341659262855607883"
+      }
+    },
+    "3/1000": {
+      "original_direct_minus_native": {
+        "lower": "24.706677945572085198228228950536",
+        "upper": "24.706677945572085198228228950537"
+      },
+      "typed_native_minus_direct": {
+        "lower": "29.152950244683753346945507106141",
+        "upper": "29.152950244683753346945507106142"
+      }
+    },
+    "3/500": {
+      "original_direct_minus_native": {
+        "lower": "1.591451854306711455285971916073",
+        "upper": "1.591451854306711455285971916074"
+      },
+      "typed_native_minus_direct": {
+        "lower": "50.149300571869503859726803947717",
+        "upper": "50.149300571869503859726803947718"
+      }
+    }
+  },
+  "scope": "Exact typed ABI and direct helper normalization; local moment comparison only",
+  "status": "PASS_TYPED_DIRECT_PRIMITIVE_DOMINANCE",
+  "typed_H": {
+    "3": 2,
+    "6": 7,
+    "7": 47,
+    "8": 139,
+    "9": 213
+  },
+  "typed_P": {
+    "1": 2177,
+    "2": 424,
+    "3": 389,
+    "4": 147,
+    "5": 50,
+    "8": 8
+  },
+  "uniform_gap_lower_bound": "8 * 7^(-C), 0<=C<1"
+}
diff --git a/research/typed-primitive-price/SOURCES.json b/research/typed-primitive-price/SOURCES.json
new file mode 100644
index 0000000000..9710f0a5a1
--- /dev/null
+++ b/research/typed-primitive-price/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/higher-moment-strictification/verify.py",
+      "usage": "input",
+      "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699",
+      "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326"
+    }
+  ]
+}
diff --git a/research/typed-primitive-price/TASK.json b/research/typed-primitive-price/TASK.json
new file mode 100644
index 0000000000..f1e3854ab5
--- /dev/null
+++ b/research/typed-primitive-price/TASK.json
@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-new-helper-inventory",
+  "priority_revision": 7,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "original_card": {
+    "id": "complex-new-helper-inventory",
+    "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/heterogeneous-owner-assembly/README.md",
+      "certificates/selected-result.json",
+      "research/selected-k8-unrestricted-ends/README.md"
+    ],
+    "methods": [
+      "Propose a changed helper inventory and derive an optimistic exact moment.",
+      "Design a small completed instance and independently verify its endpoint and rank bill."
+    ],
+    "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.",
+    "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.",
+    "allowed_variations": [
+      "Narrow to one changed boundary or helper type with explicit counts.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Mixing only providers already inside the pinned catalogue.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "helper inventory",
+      "heterogeneous-owner",
+      "mutable leaver"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Construct a direct implementation of the exact mixed A/B main interface, prove strict paid-moment dominance over the typed quotient for every exponent, and quantify the original native discount endpoint.",
+  "scope_change_reason": "User-directed higher-K continuation: establish whether the new mixed supplier offers an arithmetic benefit before searching larger controllers.",
+  "bottleneck_link": "The typed local word must offer a real moment discount over direct main jobs and direct helper normalization to justify controller exploration.",
+  "budget_minutes": 60,
+  "stop_rule": "Finish exact operator identities, source-bound profile recount, all-exponent comparison and publication; do not promote local dominance to a universal controller obstruction.",
+  "outcome": "completed",
+  "evidence": "PROOF.md, RESULT.json, source snapshots and verify.py",
+  "author": "Cinna Davis / 1337isnot1337, with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance; no subagents or independent human review.",
+  "open_questions": [
+    {
+      "question": "Can a changed native word or centre recipe restore a useful main-interface discount?",
+      "why_it_matters": "The exact typed quotient is more expensive than direct Gaussian jobs at every exponent.",
+      "first_step": "Emit a source-compatible lower paid profile and compare its complete local moments with the direct fallback before controller search.",
+      "blocked_by": "No cheaper source-compatible centre or stronger local word established."
+    }
+  ]
+}
diff --git a/research/typed-primitive-price/VERIFY.json b/research/typed-primitive-price/VERIFY.json
new file mode 100644
index 0000000000..1ff33ddcc9
--- /dev/null
+++ b/research/typed-primitive-price/VERIFY.json
@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/higher-moment-strictification/verify.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Authenticate source bytes and Git blobs; recount all paid and helper jobs; verify both forward/backward Laurent factorizations; certify all-exponent dominance and the original discount root with actual charge controls."
+    }
+  ]
+}
diff --git a/research/typed-primitive-price/inputs/round3-arithmetic.json b/research/typed-primitive-price/inputs/round3-arithmetic.json
new file mode 100644
index 0000000000..c89e009ca4
--- /dev/null
+++ b/research/typed-primitive-price/inputs/round3-arithmetic.json
@@ -0,0 +1,241 @@
+{
+  "compiler": {
+    "H": 31385200000000,
+    "N": "2^31385200000000",
+    "eta": {
+      "lower": "0.000000204541256425394083726654",
+      "upper": "0.000000204541256425394083726655"
+    },
+    "gap": "1/700000000",
+    "integer_test_exponent": 44836,
+    "logarithm_power": 1000,
+    "theta": "63/64",
+    "uniform_saving": "1057619/350000000",
+    "word_materialized": false
+  },
+  "gain_over_PR4535": "319/200000000",
+  "kappa": "9443/3125000",
+  "local_helpers": {
+    "4": 28,
+    "7": 7,
+    "8": 47,
+    "9": 326
+  },
+  "local_paid": {
+    "1": 2201,
+    "2": 412,
+    "3": 510,
+    "4": 127,
+    "5": 40,
+    "8": 8
+  },
+  "margin_at_old_root_upper": [
+    "78072058023577019965454984044224523228758899702419408235/196159429230833773869868419475239575503198607639501078528",
+    "1249152928377232319447279744707592371660142395238823308861/3138550867693340381917894711603833208051177722232017256448"
+  ],
+  "native_receipt_sha256": "eec3b14241430b6c9f5de3cbf0e3d45a172d8071d2dccd2b59d56a1fbac3d428",
+  "negative_controls": {
+    "closed_epsilon": [
+      "epsilon_below_one",
+      "global_gamma_power_slack",
+      "actual_logarithmic_gamma_guard",
+      "source_axis_superpolynomial",
+      "gaussian_above_main",
+      "new_semantic_guard_with_C1_one"
+    ],
+    "closed_uniform": [
+      "new_complex_uniform_saving_above_b"
+    ],
+    "old_BIT": [
+      "actual_bit_above_effective"
+    ],
+    "unfunded_endpoint": [
+      "main_transform_above_kappa",
+      "global_coordinate_router_above_kappa",
+      "fused_gaussian_above_kappa",
+      "group_bit_router_above_kappa",
+      "boundary_algebraic_matrix_above_kappa"
+    ]
+  },
+  "nonrecursive": {
+    "local_routes": 4802000,
+    "local_scalar": 158168,
+    "raw_scalar_upper": 181098496
+  },
+  "ordinary_BIT": {
+    "admitted": "17/5000",
+    "after_cover": "69/20000",
+    "atom": "1/250",
+    "before_cover": "3459/1000000",
+    "ordinary_saving": "8590884599/2500000000000",
+    "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses"
+  },
+  "outer": {
+    "functional_checks": {
+      "actual_new_BIT_stock_sublinear": "174299999253/175000000000",
+      "fixed_halo_explicit_metadata_branch": "13475000001/175000000",
+      "new_BIT_row_stock_sublinear_in_active_group": "697899997009/700000000000",
+      "new_semantic_group_guard": "3/700000000"
+    },
+    "margins": {
+      "boundary_algebraic_matrix": "296133039576953/98000000000000000",
+      "fused_gaussian": "296133038730859/98000000000000000",
+      "global_coordinate_router": "528809/175000000",
+      "group_bit_router": "370166473413573/122500000000000000",
+      "group_scans": "349999999/350000000",
+      "main_transform": "296132899576953/98000000000000000",
+      "microbox_face_corrections": "13475000001/175000000",
+      "polynomial_products": "699999999/700000000",
+      "sparse_union_movement": "40108633039576953/98000000000000000"
+    },
+    "parameters": {
+      "a": "528809/175000000",
+      "b": "2115237/700000000",
+      "beta": "699999997/700000000",
+      "bit_saving": "17/5000",
+      "cap_xi": "89108632899576953/98000000000000000",
+      "complex_uniform_saving": "1057619/350000000",
+      "d": "1/700000000",
+      "epsilon": "699999999/700000000",
+      "kappa": "9443/3125000",
+      "lambda_": "199395647/200000000",
+      "lambda_prime": "139576953/140000000",
+      "layout": "1/700000000",
+      "q": "423047/140000000",
+      "r0": "1/7000000000",
+      "stop": "1/700000000",
+      "tested_saving": "302177/100000000"
+    },
+    "strict_checks": {
+      "actual_bit_above_effective": "66191/175000000",
+      "actual_logarithmic_gamma_guard": "1/700000000",
+      "actual_logarithmic_group_guard": "8891367310423047/49000000000000000",
+      "alpha_logarithm_absorption": "1/7000000000",
+      "boundary_algebraic_matrix_above_kappa": "559576953/98000000000000000",
+      "cap_above_band": "40108632899576953/98000000000000000",
+      "cap_below_cell": "8891366960423047/98000000000000000",
+      "cap_below_phase_cell_power": "106891367100423047/98000000000000000",
+      "complex_above_effective": "1/700000000",
+      "complex_below_one_over_32": "19759763/700000000",
+      "complex_endpoint": "1/350000000",
+      "epsilon_below_one": "1/700000000",
+      "epsilon_positive": "699999999/700000000",
+      "fine_prime_halo_umbrella": "7/2",
+      "fused_gaussian_above_kappa": "558730859/98000000000000000",
+      "gaussian_above_main": "69576953/49000000000000000",
+      "global_coordinate_router_above_kappa": "1/175000000",
+      "global_gamma_power_slack": "9/7000000000",
+      "group_below_dimension": "1/350000000",
+      "group_bit_router_above_kappa": "873413573/122500000000000000",
+      "group_gauge_power_slack": "8891367303423047/49000000000000000",
+      "group_key_fits_record": "1/350000000",
+      "group_positive": "699999997/700000000",
+      "group_scans_above_kappa": "348942383/350000000",
+      "halo_covers_generic_inverse_radius": "5",
+      "improvement_over_user_baseline": "645394790400418148631/500000000000000000000000",
+      "lambda_above_internal": "1/1400000000",
+      "lambda_above_sigma": "3/1400000000",
+      "lambda_above_tau": "1/1400000000",
+      "lambda_prime_above_lambda": "1/1400000000",
+      "lambda_prime_above_leaf": "1397884763/490000000000000000",
+      "leaf_saving_above_effective": "697884763/490000000000000000",
+      "main_transform_above_kappa": "419576953/98000000000000000",
+      "membership_arithmetic_fits_record": "1/700000000",
+      "microbox_face_corrections_above_kappa": "13474471193/175000000",
+      "microbox_halo_volume": "55300000003/700000000",
+      "new_complex_uniform_saving_above_b": "1/700000000",
+      "new_semantic_guard_with_C1_one": "1/700000000",
+      "polynomial_products_above_kappa": "697884767/700000000",
+      "positive_layout_slack": "1/700000000",
+      "q_below_effective": "1/700000000",
+      "q_below_internal": "1/700000000",
+      "q_below_leaf": "1397884763/490000000000000000",
+      "q_positive": "423047/140000000",
+      "short_record_fallback": "697884763/700000000",
+      "source_axis_superpolynomial": "1/700000000",
+      "sparse_union_movement_above_kappa": "39812500559576953/98000000000000000",
+      "stop_below_one": "699999999/700000000",
+      "stop_positive": "1/700000000",
+      "strassen_integer_power_gap": "1951441519231",
+      "support_router_span": "3/700000000",
+      "theta_positive_polynomial_power": "2",
+      "union_header_fits_record": "3/700000000",
+      "union_tag_work_per_visit_fits_record": "3/700000000"
+    }
+  },
+  "paid": {
+    "1": 41298,
+    "16": 448,
+    "2": 7416,
+    "24": 448,
+    "3": 9180,
+    "32": 448,
+    "4": 2286,
+    "40": 448,
+    "48": 448,
+    "5": 720,
+    "56": 448,
+    "64": 448,
+    "72": 224,
+    "8": 144
+  },
+  "paid_calls": 64404,
+  "productive_fields": 10928,
+  "rank_mass_surplus": 752,
+  "raw_root_interval": [
+    "15108879/5000000000",
+    "30217759/10000000000"
+  ],
+  "scope": "Exact changed-profile arithmetic only. Requires separately admitted changed native programs, paid transports and absolute phases. Retained compiler/native/precision/tape/analytic/recovery assumptions.",
+  "source_sha256": {
+    "research/fresh-helper-boundary/native.py": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29",
+    "research/higher-moment-strictification/verify.py": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326",
+    "research/joint-helper-lattice/CONTROLLER.json": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f",
+    "research/joint-helper-lattice/native_joint.py": "50869b1bcad7493e6b4cb2a4cd5d2fd9a193a5921100483fa2c3f2c999ddfd46",
+    "research/joint-helper-lattice/verify.py": "8eb13f77a94315f811612cb557a17edeecb6b9d9a75dfa238b112dd6520c336f",
+    "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85",
+    "research/kappa-interface-round2-20261022/price_profile.py": "adde619968d3ac37147d239e25145b28150650e9ce0f76035f680f22589adcbb",
+    "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a",
+    "research/kappa-rebuild/bit/complex_controller_factor.py": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497",
+    "research/kappa-rebuild/bit/mixed_productive_bit.py": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e",
+    "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15",
+    "research/query-thinned-controllers/RESULT.json": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f",
+    "research/query-thinned-controllers/controller.py": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2"
+  },
+  "status": "PASS_CHANGED_PROFILE_ARITHMETIC_NATIVE_ADMISSION_SEPARATE",
+  "strictification": {
+    "alpha": {
+      "lower": "0.999999993884252622740095906769",
+      "upper": "0.999999993884252622740095906770"
+    },
+    "cutoff": 20,
+    "delta": {
+      "lower": "0.958285305508943939401236992035",
+      "upper": "0.958285305508943939401236992036"
+    },
+    "floor": 21,
+    "gamma": {
+      "lower": "0.956217506703714253758457710273",
+      "upper": "0.956217506703714253758457710274"
+    },
+    "normalized_paid_upper": "2097152001953127/2097154147483648",
+    "power": 1024,
+    "tail_offset": "1/5",
+    "tested": "302177/100000000"
+  },
+  "targets": {
+    "145": 224,
+    "17": 448,
+    "25": 448,
+    "33": 448,
+    "4": 504,
+    "41": 448,
+    "49": 448,
+    "57": 448,
+    "65": 448,
+    "7": 126,
+    "73": 224,
+    "8": 846,
+    "9": 5868
+  }
+}
diff --git a/research/typed-primitive-price/inputs/typed-interface.md b/research/typed-primitive-price/inputs/typed-interface.md
new file mode 100644
index 0000000000..bf4ff1af66
--- /dev/null
+++ b/research/typed-primitive-price/inputs/typed-interface.md
@@ -0,0 +1,136 @@
+# A physically realized mixed seven-axis quotient supplier
+
+Prepared for Dugongue with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Sufficient constructive statement
+
+Starting with the credited kernel-153 complex quotient word, there is an explicit replacement of its 72 shared native address maps and explicit monomial input/output normalizers on every main port such that:
+
+- Every actual shared native warp has rank zero and an exact monomial realization, including its absolute phase and inverse-transpose orientation.
+- The complete local paid profile is unchanged:
+
+      P={1:2177,2:424,3:389,4:147,5:50,8:8}.
+
+- All 408 arbitrary independent helpers retain their actual whole-job target census:
+
+      H={3:2,6:7,7:47,8:139,9:213}.
+
+- Of the 112 independent main pairs, exactly 56 realize
+
+      F_A=D S_y(Q⁻¹),
+
+  and exactly 56 realize
+
+      F_B=diag(D,QD) S_y(Q⁻¹).
+
+Here D is the Gaussian transform on seven fresh address axes, Q is the Gaussian transform on a separate central axis, and the ninth axis is a spectator. In the field ordering X=roles 0 through 111 and Y=roles 112 through 223, the extra central Q in type B acts on Y, the target of the forward shear. The backward interface is the inverse transpose of the corresponding forward matrix. These statements hold at every digit-column fiber width f, with D and Q replaced by their f-column counterparts.
+
+This is a sufficient typed local interface. It establishes neither the old common rank-eight interface nor a completed improved multiplication bound. Its main purpose is to give a controller an actual proved operator to consume, instead of pricing changed output charts as though they were unchanged.
+
+## 1. Repair all shared native maps constructively
+
+Let H₈ denote the image of the nine-dimensional ambient under the kernel-153 quotient. Before spectator padding it is the coordinate eight-plane. Every native operator has a shared contract H₈→H₈ and one additional equal-dimensional pair A→B. Twelve operators also have a nonzero line a→b. In the submitted finite word the line belongs to A if and only if b belongs to B. These incidences are checked explicitly, not inferred from dimensions alone.
+
+For a two-subspace contract, choose bases of A and B and extend each to H₈. Mapping corresponding basis vectors gives an invertible map on H₈. For a line plus subspace, put a and b first in their respective bases if they belong to A and B; otherwise first choose bases of A and B, then append a and b. Extend both lists to bases of H₈. Map the corresponding bases, and fix the unused ninth coordinate. This constructs one invertible G for every operator, satisfying all occurrences of that operator simultaneously. Negative occurrences use its inverse.
+
+Use the native monomial K_G specified by the retained source. Every actual physical warp is
+
+      C_input.adjoint().then(K_G).then(C_output),
+
+or uses K_G⁻¹ for a negative occurrence. The canonical-frame Lagrangian formula implies its Fourier rank is zero whenever G maps the input subspace onto the output subspace. The exact Clifford lowering constructs the monomial and checks its tableau and absolute phase. Shared-map consistency is essential: separately choosing a map at each occurrence would not preserve the arbitrary-input symbolic identity.
+
+The exact emitted word passes both retained literal interpreters on all 632 arbitrary-input fields in both orientations. Therefore replacing the shared operators preserves the source's formal all-column identity, with no initialized-helper assumption. All 180 actual warp classes were freshly lowered in both orientations and had exact rank zero, including absolute phases. No Fourier call is hidden inside a supposed free warp. The eight paid center operations and every helper-final repadding call are included in P.
+
+## 2. The exact two-field endpoint before normalization
+
+At every main pair, X starts in the central line c and ends in H₈. Y starts at ground and ends in a subspace A. Writing C_H, C_c and C_A for the exact canonical frame operators, the forward physical block matrix is
+
+          [ C_H C_c⁻¹       0 ]
+      M = [ C_A C_c⁻¹     C_A ].
+
+There are precisely two cases:
+
+- Type A: dim A=7, A⊂H₈, and c∉A, so A⊕c=H₈.
+- Type B: A=H₈.
+
+Both cases occur 56 times. These are properties of the literal source frames, independently checked for each port. The distinction is why a uniform common rank-eight replacement was invalid.
+
+## 3. Explicit monomial normalizers
+
+Choose standard central axis e₀ and standard seven-plane E=span(e₁,…,e₇). Put Q=C_e₀ and D=C_E. They act on disjoint axes, so they commute.
+
+In type A, choose an invertible binary map G sending e₀ to c and E to A. It consequently sends span(e₀,E) to H₈. In type B, choose G sending e₀ to c and span(e₀,E) to H₈. Extend it on the spectator coordinate. Let N=K_G, an explicit native monomial. Define
+
+      T_Y=D               in type A,
+      T_Y=QD              in type B,
+
+      M_Y=N,
+      M_X=C_c N Q⁻¹,
+      O_X=D Q N⁻¹ C_H⁻¹,
+      O_Y=T_Y N⁻¹ C_A⁻¹.
+
+All products use ordinary matrix multiplication, with the rightmost factor applied first.
+
+Each of the four M_X,M_Y,O_X,O_Y is monomial. To see this without assuming an oracle, use
+
+      L_U=C_U(L₀)={(x,z):x∈U, x+z∈U⊥}.
+
+The monomial K_G sends L_U to L_GU. Every canonical frame is involutory at the symplectic level. Therefore M_X sends L₀ to L₀ because N sends L_e₀ to L_c. Likewise O_X sends L₀ to L₀ because N sends L_span(e₀,E) to L_H₈. In type A, O_Y is monomial because N sends L_E to L_A; in type B use L_span(e₀,E) instead. A Clifford preserving L₀ is monomial. Exact lowering resolves its affine permutation, quadratic phase and absolute scalar phase.
+
+Direct multiplication, without approximation, gives
+
+      O_X (C_H C_c⁻¹) M_X = D,
+      O_Y C_A M_Y          = T_Y,
+      O_Y (C_A C_c⁻¹) M_X = T_Y Q⁻¹.
+
+Thus diag(O_X,O_Y) M diag(M_X,M_Y) is exactly F_A or F_B as claimed. No independently chosen column is credited twice; the wrappers act on the original two independent main inputs and their actual outputs. Helpers remain independent and unchanged by these external main-only wrappers.
+
+The monomial wrappers are explicit finite nonrecursive operations. They must be counted in any subsequent finite-template route/scalar allowance; they are not zero-cost machine instructions. Their degree, coordinate dimension and coefficients are fixed, so they contribute fixed linear per-record work under the native lowering. All their phases have modulus one, so the wrappers do not introduce a growing conditioning loss.
+
+## 4. Inverse transpose and every fiber width
+
+The actual backward source word uses the inverse-transpose logical identity and the corresponding conjugated frame operators. If F=O M N is the forward identity, then
+
+      F⁻ᵀ=O⁻ᵀ M⁻ᵀ N⁻ᵀ.
+
+The inverse transpose of a monomial is monomial. Hence the normalized backward type is exactly F_A⁻ᵀ or F_B⁻ᵀ, rather than an independently guessed orientation. The extra central Q is on physical Y before taking this dual; its exponent changes sign under inverse transpose.
+
+For fiber width f, tensor each ADDRESS-OPERATOR block identity f times. For example, from O_X A_X M_X=D one obtains O_X^(⊗f) A_X^(⊗f) M_X^(⊗f)=D^(⊗f). Apply the same argument separately to the Y diagonal and the off-diagonal coefficient. This preserves the two-field block shape and scalar coefficient 1. It does not tensor the entire 2×2 field matrix, which would create additional field rows. Monomial tensor powers remain explicit monomials, and the chronological arbitrary-input identity at every fiber width follows from the independent free-group-algebra argument below.
+
+## 5. A universal free-group-algebra evaluation proof
+
+The logical endpoint is not inferred by tensoring a numerical one-column field matrix. The retained literal interpreter computes a stronger symbolic identity.
+
+Let F be the free group on 72 named generators g₁,…,g₇₂ and R=Q[F] its group algebra. A row is a finitely supported map from pairs (initial field, reduced group word) to rational coefficients. Initialize each of the 632 persistent fields as its own basis vector. The owned C field is also represented symbolically until it is explicitly cleared. Process every record as follows:
+
+- A native warp with signed operator i multiplies each coefficient on the LEFT by g_|i| or its inverse. The implementation prepends the signed symbol and removes it only when it cancels the adjacent inverse symbol.
+- ADD and SCALE perform exact rational module arithmetic. COPY duplicates the source expression only into permitted owned storage. CLEAR sets only permitted owned storage to zero.
+- A paid frame change is the identity on logical values; its physical conjugating frame operators are accounted separately. Phase and adapter markers do not modify the logical row.
+
+These are precisely module operations in the free R-module on the initial field symbols. Induction on the record index therefore proves that the interpreter's row is the corresponding formal logical expression, before any native operator has been assigned a numerical matrix. In particular, no relation such as commutation, finite order, dimension, a chosen binary G map, or a one-column coincidence is used.
+
+At termination, the checked forward rows are X_i↦X_i, Y_i↦Y_i+X_i and h_j↦h_j; the backward rows are X_i↦X_i−Y_i, Y_i↦Y_i and h_j↦h_j. Every surviving coefficient has the EMPTY group word. The owned C row is zero. The fresh receipt records 632 persistent rows, 744 exact terms and zero nonempty group words in each orientation. Changing one occurrence to a new unshared generator produces a nonzero endpoint difference and is explicitly rejected.
+
+Now take any vector space V over Q or C and assign ANY invertible linear operator T_i∈GL(V) to each shared generator. Send a reduced word to the ordered product of those operators and extend Q-linearly. This is a well-defined algebra homomorphism R→End(V): the only reduction used, g_i g_i⁻¹=1, is valid because T_i is invertible. Extending it componentwise to module rows sends every step of the formal computation to the actual vector-valued operation. Hence the final formal identity proves the same endpoint for arbitrary independent V-valued inputs.
+
+Apply this evaluation independently at every fiber width f, assigning the explicitly constructed shared K_G,f and their inverses. The same operator must be used at every occurrence of its name; this is why the simultaneous shared-map construction in section 1 was required. The 72 new maps satisfy that condition. The backward interpreter uses a separately named set of generators, so the result also applies to the inverse-transpose assignments. This proves the changed word's universal logical all-fiber endpoint directly. The only tensor arguments needed are for individual frame/normalizer operator identities, where tensor powers do preserve composition; no assertion that tensor powers preserve sums is made.
+
+This evaluation theorem is completely separate from a contraction or a complete multiplication algorithm. It proves the arbitrary-input operator identity and does not supply a favorable paid invoice by itself.
+
+## 6. Controller relevance and paid obligations
+
+The type-B identity has a useful exact rewriting:
+
+      diag(1,Q) S_y(Q⁻¹)=S_y(1) diag(1,Q).
+
+Also Q² is monomial. This permits central-parity row gauges that can change whether a query coefficient requires a rank-one Gaussian call. It does not make all queries free: an ADD across different central gauges can itself require a paid rank-one call. A complete controller must charge every such bridge and derive its final central target parities from the actual diagonal operator. The seven-axis target ranks cannot be priced with the old eight-axis invoice.
+
+The receipt intentionally states only a typed local supplier. A full contraction, compiler, native caller and larger κ must be proved using the resulting complete paid and productive profiles.
+
+## Evidence, source status and credit
+
+`repair_shared_warps.py` constructs the repaired 72 shared maps, resynthesizes the word, performs two-interpreter arbitrary-input replay and lowers all actual warp classes in both orientations. Its word payload SHA-256 is `599da9a45213bc4cd98d897d6bd00e5e4bc2af8160e90ec50aec467e0c6236eb`.
+
+`typed_pair_normalizers.py` constructs all 448 monomial wrappers, lowers them with absolute phases and checks all 336 block identities by exact tableaux and exact zero-state vectors. Its normalizer payload SHA-256 is `7617a2893f7cb117beb35c499a02feac3d2b0a6b3e60bdd4aa198a680a26ab54`. The check takes about 18 seconds with CPython 3.12. These are exact finite certificates plus the all-fiber argument above, not Lean verification or an independent human review.
+
+Credit DaysSky for the kernel quotient and helper repadding in #4596/#4629/#4633; Nick Petalas for the quotient family classification in #4627; Ryanson Jonathan for the endpoint-frame audit in #4604; Cinna Davis and the PR #4470 native/helper word; Cao Yifan for the shared-generator interface work in #4610; Dugongue for the transported/arbitrary-frame and native Word RAM work; zxv and Jacob Alan Sussman for retained native and compiler/matching results; and all original source notices. The new contribution here is the explicit shared-map repair, universal free-group-algebra evaluation argument, and exact typed mixed seven-axis normal form, not an assertion that the original quotient already supplied the old operator.
diff --git a/research/typed-primitive-price/inputs/typed-word.json.gz b/research/typed-primitive-price/inputs/typed-word.json.gz
new file mode 100644
index 0000000000..b22174e7a9
Binary files /dev/null and b/research/typed-primitive-price/inputs/typed-word.json.gz differ
diff --git a/research/typed-primitive-price/verify.py b/research/typed-primitive-price/verify.py
new file mode 100644
index 0000000000..5db42ebc2e
--- /dev/null
+++ b/research/typed-primitive-price/verify.py
@@ -0,0 +1,178 @@
+#!/usr/bin/env python3
+"""Source-bound primitive-price comparison. Apache-2.0; Codex assistance."""
+import argparse
+from collections import Counter
+from fractions import Fraction as Q
+from hashlib import sha1, sha256
+import gzip
+import importlib.util
+import json
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def add(*values):
+    return tuple(sum(v[i] for v in values) for i in (0, 1))
+
+
+def authenticate():
+    for row in json.loads((HERE/'SOURCES.json').read_text())['files']:
+        if row['usage'] == 'input':
+            need(sha256((ROOT/row['path']).read_bytes()).hexdigest() == row['sha256'], 'Live interval engine pin')
+    for row in json.loads((HERE/'FROZEN-INPUTS.json').read_text()):
+        raw = (HERE/row['snapshot']).read_bytes()
+        need(sha256(raw).hexdigest() == row['sha256'], 'Frozen source bytes')
+        need(sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == row['git_blob'], 'Frozen Git blob')
+
+
+def engine():
+    path = ROOT/'research/higher-moment-strictification/verify.py'
+    spec = importlib.util.spec_from_file_location('primitive_price_intervals', path)
+    module = importlib.util.module_from_spec(spec)
+    spec.loader.exec_module(module)
+    return module
+
+
+def typed_profiles():
+    word = json.loads(gzip.decompress((HERE/'inputs/typed-word.json.gz').read_bytes()))
+    c = word['canonical']
+    H = Counter()
+    for role in range(224, 632):
+        a, b = (c['frames'][c[key][role]] for key in ('start','final'))
+        def span(basis):
+            s = {0}
+            for x in basis:
+                s |= {v^x for v in tuple(s)}
+            return s
+        need(span(a) <= span(b), 'Nested arbitrary helper interface')
+        H[len(b)-len(a)] += 1
+    profiles = []
+    for direction in ('forward','backward'):
+        P = Counter()
+        for event in word['programs'][direction]:
+            if event[0] in ('climb','center','cache_child'):
+                rank = event[-1]
+                old, new = event[-3:-1]
+                need(rank == abs(len(c['frames'][new])-len(c['frames'][old])), 'Emitted paid rank')
+                P[rank] += 1
+        profiles.append(P)
+    need(profiles[0] == profiles[1], 'Both emitted paid censuses')
+    need(H == {3:2,6:7,7:47,8:139,9:213}, 'Typed helper census')
+    need(profiles[0] == {1:2177,2:424,3:389,4:147,5:50,8:8}, 'Typed paid census')
+    return H, profiles[0]
+
+
+# Exact Laurent polynomials, with commuting symbols D and Q. No finite order.
+def plus(a, b):
+    out = dict(a)
+    for key, value in b.items():
+        out[key] = out.get(key, 0)+value
+    return {k:v for k,v in out.items() if v}
+
+
+def times(a, b):
+    out = {}
+    for (d,q), x in a.items():
+        for (e,r), y in b.items():
+            k = (d+e,q+r)
+            out[k] = out.get(k, 0)+x*y
+    return {k:v for k,v in out.items() if v}
+
+
+def mm(a, b):
+    return [[plus(times(a[i][0],b[0][j]),times(a[i][1],b[1][j])) for j in range(2)] for i in range(2)]
+
+
+def mono(d=0,q=0,c=1):
+    return {(d,q):c}
+
+
+def operator_identities():
+    one, zero, d, dq = mono(), {}, mono(1), mono(1,1)
+    Sy = [[one,zero],[mono(q=-1),one]]
+    A = [[d,zero],[mono(1,-1),d]]
+    B = [[d,zero],[d,dq]]
+    need(mm([[d,zero],[zero,d]], Sy) == A, 'Direct forward type A')
+    need(mm([[one,zero],[one,one]], [[d,zero],[zero,dq]]) == B, 'Direct forward type B')
+    # The direct inverse transposes are literal transposes of inverses.
+    Adual = [[mono(-1),mono(-1,-1,-1)],[zero,mono(-1)]]
+    Bdual = [[mono(-1),mono(-1,-1,-1)],[zero,mono(-1,-1)]]
+    Ax = [[one,mono(q=-1,c=-1)],[zero,one]]
+    Bx = [[one,mono(c=-1)],[zero,one]]
+    need(mm([[mono(-1),zero],[zero,mono(-1)]], Ax) == Adual, 'Direct raw backward type A')
+    need(mm(Bx, [[mono(-1),zero],[zero,mono(-1,-1)]]) == Bdual, 'Direct raw backward type B')
+    # Omitting Q from the B diagonal, or replacing Q^-1 by Q, is false.
+    need(mm([[one,zero],[one,one]], [[d,zero],[zero,d]]) != B, 'B query is actually paid')
+    need(mm([[d,zero],[zero,d]], [[one,zero],[mono(q=1),one]]) != A, 'Q inverse control')
+
+
+def gap(E, H, P, block, saving):
+    t = 1-saving
+    return add(E.moment(P,t), E.scale(E.moment(H,t),-1),
+               E.scale(E.power(block,t),-224), (Q(-112),)*2)
+
+
+def certify():
+    authenticate()
+    E = engine()
+    H, P = typed_profiles()
+    operator_identities()
+    # Normalized derivative lower bounds in PROOF.md retain just rank one.
+    log7, log8 = E.log_bounds(7), E.log_bounds(8)
+    log76 = add(log7,E.scale(E.log_bounds(6),-1))
+    log87 = add(log8,E.scale(log7,-1))
+    need(log7[0]>1 and log8[0]>1 and log76[1]<1 and log87[1]<1, 'Elementary log bounds')
+    need(Q(2065,7)-7 == 288 > 0, 'Typed normalized gap increases for all C')
+    mass = lambda p:sum(r*n for r,n in p.items())
+    need(mass(P)-mass(H)-224*7-112 == 8, 'Every direct helper and central job charged')
+    source = json.loads((HERE/'inputs/round3-arithmetic.json').read_bytes())
+    Ho = {int(k):n for k,n in source['local_helpers'].items()}
+    Po = {int(k):n for k,n in source['local_paid'].items()}
+    need(Ho == {4:28,7:7,8:47,9:326}, 'Round-three helper input')
+    need(Po == {1:2201,2:412,3:510,4:127,5:40,8:8}, 'Round-three paid input')
+    need(Q(2089,8)-7 == Q(2033,8)>0, 'Original normalized gap strictly increases for all C')
+    lo, hi = Q('0.0062073960'), Q('0.0062073961')
+    below, above = gap(E,Ho,Po,8,lo),gap(E,Ho,Po,8,hi)
+    need(below[1]<0 and above[0]>0, 'Unique original discount endpoint')
+    samples = {}
+    for C in (Q(0),Q('0.003'),Q('0.004'),Q('0.006'),Q('0.01')):
+        G = gap(E,H,P,7,C)
+        lower = E.scale(E.power(7,-C),8)
+        need(G[0]>=lower[1] if C else G[0]<=8<=G[1], 'Uniform typed dominance lower bound')
+        samples[str(C)] = {'typed_native_minus_direct':E.display(G),
+                          'original_direct_minus_native':E.display(E.scale(gap(E,Ho,Po,8,C),-1))}
+    # An actually removed centre reverses the integer boundary; this is a false invoice.
+    unpaid = dict(P)
+    unpaid[8] -= 2
+    need(mass(unpaid)-mass(H)-224*7-112 < 0, 'Unpaid owned jobs control')
+    return {'status':'PASS_TYPED_DIRECT_PRIMITIVE_DOMINANCE',
+            'scope':'Exact typed ABI and direct helper normalization; local moment comparison only',
+            'typed_H':H,'typed_P':P,'direct_main_paid':{'1':112,'7':224},
+            'uniform_gap_lower_bound':'8 * 7^(-C), 0<=C<1',
+            'normalized_derivative_lower_bound':'288',
+            'original_discount_endpoint':[str(lo),str(hi)],
+            'original_gap_below':E.display(below),'original_gap_above':E.display(above),
+            'samples':samples,'new_kappa':False}
+
+
+def main():
+    p = argparse.ArgumentParser()
+    p.add_argument('--write',action='store_true')
+    args = p.parse_args()
+    result = json.loads(json.dumps(certify()))
+    if args.write:
+        (HERE/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n')
+    else:
+        need(json.loads((HERE/'RESULT.json').read_text()) == result, 'Committed exact receipt')
+    print(json.dumps(result,sort_keys=True))
+
+
+if __name__ == '__main__':
+    main()