PROVEN
Finding · replay
Changing a sealed record after the fact is provably as hard as breaking the hash it is sealed with.
§ 1
The record
FINDING · tamper-of-a-sealed-record-forces-a-collisionreplay
Changing a sealed record after the fact is provably as hard as breaking the hash it is sealed with.
- Claim
- Tampering with a sealed, hash-linked decision record forces a hash collision: the canonical encoding is injective, the chain is append-only, and detection follows in Lean without a collision-resistance axiom.
- Status
- PROVEN Follows from stated premises inside a named frame.
- Subject
- A Lean 4 model of the OMEGA record chain (model). built for the study
- Frame
- Opaque hash; collision-resistance as a discharged hypothesis, not an axiom.
- Method
- Injective canonical encoding, append-only chain, detection theorem.
- Oracle
- The Lean 4 kernel; #print axioms reports 0 user axioms.
- Negative control
- Present The axiom probe is committed; a browser recompute of the content hash goes red on a one-byte change.
- Limitation
- That the opaque hash function is SHA-256, that the recorded decision was correct, or that the formal definitions match the prose specification. It is tamper-evidence at the model level, not a claim about any deployed system.
- Source
- repowazdogz-droid/omega-lean-proof @ 2fab5d1
- Reproduce
git clone https://github.com/repowazdogz-droid/omega-lean-proof && cd omega-lean-proof && lake build && lake env lean probes/AxiomProbe.lean
- Independent reproduction
- None known.
§ 2
Where this sits
This finding answers Replayable is not independently established and supports the REPLAY stage of the operating method.