fix(2c-D): Req 21.16 proves the receipt's facts under the validated R_T^+, not a device root

docs/papers/amendment-2c-c4-accepted-successor-closure.md

@@ -527,11 +527,12 @@ Req 21.15 half-completion — THE WITHHOLD HALF, owed here: bind, withhold the
 Req 21.16 receipt-verifier — OWED BY 2c-D in full: no TA_B can be parsed here.
     When it lands it must establish, from the published receipt set alone: retrieve
     and verify TA_B; prove the commitment carries the exact bundled trader
-    parent/successor; verify sigma_dsm directly over it; verify the receipt leaf's
-    inclusion proof under the INDEPENDENTLY DERIVED/AUTHENTICATED TRADER `post_root`
-    (see the disambiguation below); match (b, X); and reproduce the DLV reserve
-    deltas — with removal or substitution of TA_B, C_dsm+, sigma_dsm or the
-    inclusion proof each failing closed.
+    parent/successor; verify sigma_dsm directly over it; verify the receipt's
+    facts as the EconomicSettlementReceiptState leaf the settle write set
+    committed, included under the INDEPENDENTLY VALIDATED economic root R_T^+
+    (see the disambiguation below, as CORRECTED 2026-09-11); match (b, X); and
+    reproduce the DLV reserve deltas — with removal or substitution of TA_B,
+    C_dsm+, sigma_dsm or the inclusion proof each failing closed.
 ```
 
 ### Which root — a normative clarification (owner ruling, 2026-09-10)
@@ -608,6 +609,131 @@ establish that the exact bundle was economically accepted; Req 21.16 then establ
 that the published receipt corresponds to the authenticated device post-state rather
 than being a plausible standalone object.
 
+### Corrected 2026-09-11 — the root D4 names has no independent source (owner ruling)
+
+**D4 is corrected, not reversed.** Its invariant stands exactly: *the verifier must anchor
+to a root established independently of the receipt being verified.* What was wrong is
+*which* root. Implementing PR C exposed that the source D4 names — *"obtained from the
+already validated successor/economic-admission path"* — never produces a DEVICE root:
+
+```text
+C_T^+     = relationship_chain_tip_v2(rel_key, embedded_parent, counterparty_devid,
+                                      operation_bytes, entropy, encapsulated_entropy)
+            -> commits no root at all
+sigma_dsm   signs H(G ‖ DevID ‖ C_dsm+ ‖ operation_digest)       -> no root
+0x0031      the settle's admission substrate                     -> no root
+AdvanceOutcome.child_r_a                    discarded by the route; never published
+device SMT  a bounded cache with NO validity replay
+```
+
+A root carried by the receipt is self-authenticating, and a trader signature over a
+device root would establish *provenance* but never *validity* — the device SMT has no
+replay that could make it so. That is the gap Rev 15 spec:971-976 names: *a Merkle proof
+authenticates membership relative to a root; it does not authenticate the provenance of
+that root.* The Rev 15 conformance delta (2026-08-21, §5) had already recorded the same
+divergence: Rev 15 requires `C_T^+` to commit the post-advance root, and this
+implementation's does not.
+
+The one independently VALIDATED root on the settle path is `R_T^+`, and the settle write
+set already commits the receipt's facts under it as an `EconomicSettlementReceiptState`
+leaf. So Req 21.16 anchors there:
+
+> ```text
+> RULING — D4 / Req 21.16 root correction
+>
+> Choose Option 1.
+>
+> Amend D4.
+>
+> The previous requirement that Req 21.16 verify the legacy device-SMT
+> receipt leaf under an independently established DEVICE post_root is not
+> implementable under the current protocol:
+>
+>     * the device SMT has no validity replay;
+>     * no independently validated device post_root exists on the settle path;
+>     * a root carried by the receipt is self-authenticating and therefore
+>       insufficient;
+>     * a trader signature over such a root establishes provenance only,
+>       not validity.
+>
+> Do NOT add a signed-device-root artifact merely to satisfy the wording.
+>
+> Req 21.16 instead verifies the published receipt's economically relevant
+> facts against the existing EconomicSettlementReceiptState leaf committed
+> by the settle write set under the independently validated economic root
+> R_T^+.
+>
+> Required chain:
+>
+>     authenticated / validated settle
+>         -> deterministic economic write set
+>         -> EconomicSettlementReceiptState
+>         -> inclusion under independently validated R_T^+
+>         -> receipt correspondence
+>         -> VerifiedReceipt
+>
+> The verifier MUST:
+>
+> 1. Take R_T^+ from the already validated economic advancement path.
+>    It MUST NOT accept a root supplied by the receipt itself.
+>
+> 2. Reconstruct the expected EconomicSettlementReceiptState from the
+>    authenticated settlement facts / exact receipt facts required by
+>    Def 14.2.
+>
+> 3. Derive its canonical economic-SMT key independently.
+>
+> 4. Verify the ordered inclusion path under R_T^+.
+>
+> 5. Require exact correspondence between the published receipt and the
+>    authenticated economic receipt state for every realization-relevant
+>    field.
+>
+> 6. Reject altered settlement identity, operation identity, amounts,
+>    assets, parties, key/position, path, or any other field covered by
+>    the economic receipt state.
+>
+> 7. Return a typed verified-receipt fact only after the inclusion and
+>    correspondence checks succeed.
+>
+> The existing DEVICE-SMT receipt leaf remains legacy state/cache material.
+> It is NOT realization evidence and MUST NOT be used to certify value
+> movement.
+>
+> This is a correction to D4, not a substitution of an arbitrary economic
+> root for a device root. R_T^+ is appropriate because the receipt facts
+> being certified are already represented by the economic receipt leaf
+> inside the validated economic state transition.
+>
+> Do not change relationship_chain_tip_v2.
+> Do not add a new signed-device-root artifact.
+> Do not defer Req 21.16 from realization.
+> ```
+
+The three rejected options are recorded with their reasons, because each will be proposed
+again. **A signed device-root artifact** repairs the wording and not the defect: it proves
+who signed a root, never that the root is the state a valid transition produced.
+**Deferring Req 21.16** would weaken the cutover for no reason once a validated
+representation of the receipt's facts is known to exist. **Making `C_T^+` commit the root**
+is the Rev 15 literal and rewrites a foundational DSM commitment — every chain tip — to
+accommodate one verifier.
+
+```text
+wrong               receipt -> the receipt's claimed device root -> "verified"
+insufficient        receipt -> a trader-signed device root -> provenance, not validity
+right               validated economic transition -> R_T^+
+                        -> committed EconomicSettlementReceiptState
+                        <- exact correspondence -> published receipt
+```
+
+**What the correction does NOT do.** It does not put the receipt leaf into the economic
+SMT: the settle write set already writes `EconomicSettlementReceiptState` there, and did
+before D4 was taken. It does not collapse the two trees §7 and Req 21.16 read — they now
+read two different leaves (`0x0032` and the settlement receipt) under ONE validated root,
+which is the honest statement of what the settle path actually authenticates. And the
+device-SMT receipt leaf is not deleted: it remains the trader's local state, carries no
+evidential weight, and nothing may read it as evidence that value moved.
+
 ## Mutation controls
 
 Each disabled in turn, with a **named** test going red by performing the forbidden action, then

docs/papers/amendment-2c-d-bundle-acceptance-and-realization.md

@@ -650,10 +650,12 @@ cannot proceed without.
    encoder, never the production encoder under test.
 
 8  Req 21.15's realize half and Req 21.16 in full. Req 21.16 verifies the
-   published Receipt under the INDEPENDENTLY DERIVED TRADER `post_root` (the
-   device SMT), never under `R_T^+` (the economic SMT) and never under a root
-   the Receipt itself carries — see 2c-C4 §9's root disambiguation. The two
-   roots authenticate different claims and neither substitutes for the other.
+   published Receipt's facts as the EconomicSettlementReceiptState leaf the
+   settle write set committed, included under the INDEPENDENTLY VALIDATED
+   economic root `R_T^+` — never under a root the Receipt itself carries, and
+   never under the legacy device-SMT `post_root`, which has no independent
+   source (2c-C4 §9, D4 as corrected 2026-09-11). §7 and Req 21.16 read two
+   different leaves under one validated root.
 
 9  the fifteenth Lean module's successor, or an extension of
    DSMAcceptedSuccessorWalk, discharging §7's ordering and the two-conjunct

dsm_client/deterministic_state_machine/dsm/src/dlv/mod.rs

@@ -12,7 +12,7 @@ pub mod controller_rotation;
 pub mod market_evidence; // 2c-B G1-G4 — the validity half of market successor evidence
 pub mod market_producer; // 5c-2 Step 2 — the genuine market bundle producer; nothing invented
 pub mod pair_identity;
-pub mod published_receipt; // Req 21.16 — a receipt proven under an INDEPENDENT post_root
+pub mod published_receipt; // Req 21.16 — a receipt's facts proven under the VALIDATED R_T^+
 pub mod quorum_bind; // Def 6.21 — Class K sans-IO quorum-binding decision engine
 pub mod route_commit;
 pub mod settlement_bundle; // Def 6.14 — the canonical immutable SettlementBundle + K(B)