OMEGA

A record structure for a governed decision, authority, evidence, expected outcome, confirmation, traceability, that is sealed at commit time, can be replayed, and whose seal can be rechecked. A Lean 4 model establishes internal consistency of the governance conjunction and constructive tamper-evidence.

That a decision was correct, that a model's internal reasoning is the recorded reasoning, or that the opaque hash function is SHA-256. The Lean model does not establish that its formal definitions match the prose specification.

A canonical-encoding, hash-linked record chain, with a Lean 4 formalisation of the governance conjunction and the tamper-evidence argument, plus a browser recompute of the record's content hash.

The shipped root theorems are machine-checked; a fresh clone builds green and #print axioms reports 0 user-declared axioms. Tampering a sealed record forces a hash collision; the record chain is append-only; the canonical encoding is injective and round-trips.

Lean kernel v4.27.0 and the three standard axioms propext, Classical.choice, Quot.sound. SHA-256 is modelled as an opaque compute_hash with collision-resistance carried as a discharged theorem hypothesis, not an axiom. No Mathlib.

Tamper-evident logging and hash chains (Haber and Stornetta, 1991), the trusted computing base literature, and canonical serialisation (RFC 8785 JCS). The contribution is the record structure and the machine-checked internal-consistency and tamper-evidence properties, not the discovery of hash chaining.

git clone https://github.com/repowazdogz-droid/omega-lean-proof && cd omega-lean-proof && lake build && lake env lean probes/AxiomProbe.lean

Findings drawn from this artifact are on the evidence ledger.