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

[cryptskii]

PR C1 — the D4 correction, landed as item-8 verification machinery before the cutover (2c-D §11's boundary note: item 8 "adds the last verifier, and stops"). No behaviour change: verify_published_receipt has no live caller.

Why D4 needed correcting

D4 sourced the device post_root from "the already validated successor/economic-admission path". Checked at source, that path never produces one:

C_T^+      relationship_chain_tip_v2(...) 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
child_r_a  discarded by the route; never published
device SMT a bounded cache with no validity replay

The only independently validated root is R_T^+, and the settle write set already commits the receipt's facts under it as EconomicSettlementReceiptState. The owner's correction is recorded verbatim in 2c-C4 §9, after the D4 block rather than replacing it; 2c-D §11 item 8 is amended to match.

The fold is the correspondence check

The leaf is rebuilt from the receipt's facts, keyed from the proven identity and the settlement being verified, and folded under R_T^+. One altered field → a different root. There is no second copy of the facts to compare against, so nothing to drift. The fixture tree comes from the real settle write set.

One check deliberately removed — the signature

Its payload covers the receipt's own post_root, so keeping it would feed the retired device root back in. What it attested is now established by inclusion under a lineage-validated root. the_legacy_device_fields_carry_no_weight_either_way pins the removal as a decision. If you want it back, it is a few lines — but it would reintroduce the device root into the verifier.

Controls

the_receipts_own_device_path_is_not_evidence	the correction as a test: the device path proves its leaf under its own root, and here proves nothing
a_self_rooted_receipt_is_refused_though_the_legacy_verifier_accepts_it	inflated output; legacy verifier says OK, Req 21.16 refuses
an_altered_amount_asset_or_sequence_is_refused	each field alone lands the fold elsewhere
facts_committed_by_another_trader_do_not_verify_for_this_one	key/position from the proven identity

Mutation controls, executed, restored from byte copies:

• M1 delete the fold comparison → 6 named tests red
• M2 delete the identity check → a_receipt_naming_another_trader_is_refused red (the fold keys on the proven identity, so it can't catch this alone)

Lean owes nothing (no theorem encodes the device-root rule); no TLA+ spec models the trader fence.

Flagged, not fixed here: ccb-object-registry.md ~line 2110 still says 2c-D's adopting change "is NOT started" — stale since #841. Different fact, different PR.

Verification

dlv::published_receipt               14/14
make lint                            exit 0
ci/production_safety_checks.sh       exit 0

Next: PR C2, the cutover.