proofs(coq): reconnect obliterate_not_injective after #57 closes (admit #3 of 3 from #55)

[hyperpolymath]

Background

PR #55 introduced 3 documented admits. This is the dependent one — closure is mechanical once #57 (overwrite_pass_equalizes_storage) lands.

Admit

proofs/coq/rmo_operations.v:531 — obliterate_not_injective

Closure path

Once overwrite_pass_equalizes_storage is sound (issue #57 above), this theorem follows by:

1. Two storages that differ only in unmapped blocks both produce the same obliterate output.
2. Therefore obliterate is not injective.

The proof skeleton already exists in rmo_operations.v:531-ish; just re-wire to call the (newly-sound) overwrite_pass_equalizes_storage lemma in place of the admit.

Marketing claim impact

obliterate_not_injective is the formal grounding for valence-shell's "mathematically irreversible secure deletion" marketing claim (per #42 foundation pack #5). Currently the claim rests on an Admitted. — closing this restores soundness of the README claim.

Echo-types alignment

Per #51, this is exactly EchoLossTaxonomy.const-fibre-↔-domain — could potentially be lifted directly from echo-types rather than reconstructed locally.

Blocked by

• proofs(coq): strengthen Hgeom or weaken overwrite_pass_equalizes_storage (admit #2 of 3 from #55) #57 (overwrite_pass_equalizes_storage)

Refs

• PR proofs(coq): close build-oracle cascade + re-enable verify-proofs (closes #49) #55 (closes proofs(coq): re-enable verify-proofs CI job (oracle); fix 5 cascading build errors #49)
• proofs/coq/rmo_operations.v:531
• Proof inventory — 478 candidate theorems + 8-theorem foundation pack #42 foundation pack chore(deps): bump the actions group across 1 directory with 9 updates #5 (secureDeleteIrreversible / obliterate_not_injective)
• [Integration] Ground L3 (reversibility + equivalence + loss) theorems in echo-types LAYER3 module #51 echo-types integration audit

🤖 Filed from PR #55 closure