Verification
The formal artefacts do not prove real-world correctness or safety. They establish properties of a defined formal model and name the limits of that model. Two checkers: the Lean 4 kernel, and a SymPy necessity harness.
What is proven, and what is not
The Lean model establishes internal consistency of the Governed
conjunction, projection, absence and joint-sufficiency lemmas per conjunct,
and constructive tamper-evidence, including at the JSON encoding level, with
collision-resistance carried as an explicit hypothesis rather than an axiom.
A SymPy harness establishes failure-mode necessity for nine schema fields;
the rest are design rationale. The model does not establish real-world
correctness, agent safety, deployment behaviour, or that the formal
definitions match the prose specification.
Verified in the evidence inventory
From a fresh public clone at commit 2fab5d1, on toolchain
leanprover/lean4:v4.27.0 with no Mathlib: lake build
completed successfully (16 jobs), and #print axioms over the root
theorems reported 0 user-declared axioms. Every theorem
depends only on Lean's standard axioms (propext,
Classical.choice, Quot.sound) or on none.
One wording note carried from the repository: the constructive core theorem
tamper_implies_collision is described in the repository README as
"axiom-free", but #print axioms reports it depends on the three
standard Lean axioms. The precise statement is that it uses 0 user
axioms and takes no collision-resistance hypothesis, not that it is free of
Lean's standard axioms.
Main theorems
tamper_implies_collision, tampering a traceable chain forces a hash collision.tamper_detection, under a collision-resistance hypothesis, a tampered chain is no longer traceable.jcsEncode_injective, the canonical JSON encoding is injective.omega_chain_append_only, appending a record leaves prior entries unchanged.
Reproduce
git clone https://github.com/repowazdogz-droid/omega-lean-proof
cd omega-lean-proof
lake build # Build completed successfully (16 jobs)
lake env lean probes/AxiomProbe.lean # 0 user-declared axioms This pass. Re-verified this pass:
lake build and the axiom probe were re-run from a fresh public clone
at 2fab5d1 (16 jobs green; the axiom listing reproduced), not only read from
source.
Honest limits
The repository names structurally unclosable limits, among them: the model cannot distinguish genuine reasoning from a perfect post-hoc rationalisation (it does not access model internals); the external anchor can be poisoned by an actor who rewrites the whole chain; a physical staleness gap remains between the sealed record and the world; and accountability for an emergent, multi-actor failure is not located by a factual record alone. Each is stated with what its closure would require.