Findings · Assurance architecture
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.
Evidence
The tamper-evidence property is proved constructively. Editing a traceable, hash-linked chain and keeping it traceable forces two distinct byte strings to the same hash. A collision. The canonical JSON encoding is injective, so the encoding cannot hide a change; the chain is append-only, so an earlier record cannot be altered without breaking the link that follows it. Collision-resistance is carried as an explicit theorem hypothesis rather than assumed as an axiom, and the hash itself is left opaque: the proof does not claim the function is SHA-256, only that, whatever it is, tampering that survives the check would exhibit a collision in it.
Sample. Universal over records and chains; 0 user-declared axioms, depending only on Lean's standard axioms.
Boundary
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.
Independent reproduction. None known.
Reproduction
git clone https://github.com/repowazdogz-droid/omega-lean-proof && cd omega-lean-proof && lake build && lake env lean probes/AxiomProbe.lean- Toolchain
- Lean 4 leanprover/lean4:v4.27.0, no Mathlib
- Expected output
- Build completed successfully (16 jobs); 0 user-declared axioms
- Claim stated at
- repowazdogz-droid/omega-lean-proof · OmegaP3Semantic.lean:452 (tamper_implies_collision); OmegaHashChain.lean:19 (append-only)
- Verified at
- repowazdogz-droid/omega-lean-proof@2fab5d1 (2026-07-20)
This pass. Re-verified this pass: lake build and the axiom probe were re-run from a fresh public clone at 2fab5d1 (16 jobs, 0 user-declared axioms).
Artifact: repowazdogz-droid/omega-lean-proof