## Tracker: Wave-12c Merkle Replay Safety Formal proofs for: 1. **Merkle aggregation determinism** — same inputs always yield same root 2. **Receipt replay impossibility** — distinct windows have distinct window counters ### Deliverables - `docs/phd/theorems/igla/MerkleReplaySafety.v` with all theorems ending `Qed.` - `docs/phd/artifacts/coq_citation_map.json` updated with new mappings ### Anchor φ² + φ⁻² = 3 ### License Apache-2.0
Tracker: Wave-12c Merkle Replay Safety
Formal proofs for:
Deliverables
docs/phd/theorems/igla/MerkleReplaySafety.vwith all theorems endingQed.docs/phd/artifacts/coq_citation_map.jsonupdated with new mappingsAnchor
φ² + φ⁻² = 3
License
Apache-2.0