Verification

What is proven, and what is not

Two machine checkers carry the proof: Lean's kernel and a SymPy necessity harness. Inside the defined formal model, Lean establishes the internal consistency of the Governed conjunction (projection, absence, and joint-sufficiency lemmas per conjunct) and constructive tamper-evidence, including JSON-level tamper, with no collision-resistance axiom; SymPy establishes failure-mode necessity for nine fields, and the remaining fields are carried as design rationale rather than theorems. It does not establish real-world correctness of any decision, the safety of an agent in a dynamic environment, deployment behaviour of a running product, that the formal definitions match the prose specification, or the sufficiency, independence, or irreducibility of the field set. The proof rests on four modelling assumptions: the system commits before it acts, not after; the inputs to reasoning are accessible and expressible; the action has a definable moment of commitment; and the fields are propositions, not quantitative degrees. A verified record shows the chain is intact; whether the decision was right is a separate question.

Verified properties

All ten Lean roots build clean under Lean v4.27.0 at commit 6aa9008 with zero sorry and zero user-declared axioms; SafeVerify replay passed 2026-06-24. Full verification detail and attestation logs: repo README.

Reproduce it yourself

One block, current baseline at commit 6aa9008. Clone, build the ten roots, print the axiom posture, and replay SafeVerify.

git clone https://github.com/repowazdogz-droid/omega-lean-proof
cd omega-lean-proof
git checkout 6aa9008
lake build
# Ten shipped root .olean files under .lake/build/lib/lean/, including:
# Chain integrity:       .lake/build/lib/lean/OmegaP3Semantic.olean
# Chain<->JCS bridge:    .lake/build/lib/lean/OmegaJCSChain.olean
# v1.3 (legacy):         .lake/build/lib/lean/OmegaProof.olean
#
# Record the #print axioms posture for each:
cat > /tmp/axioms.lean <<'EOF'
import OmegaProof
import OmegaV14
import OmegaP3Semantic
import OmegaP1Governance
import FailureProtocol
import OmegaJCSChain
#print axioms p1_necessary
#print axioms OmegaV14.p2_dag_necessary
#print axioms OmegaP3Semantic.canonicalBytes_injective_wf
#print axioms OmegaP3Semantic.tamper_implies_collision
#print axioms OmegaP1Governance.governance_requires_contract
#print axioms retries_exceed_limit_implies_escalation
#print axioms OmegaJCSChain.json_tamper_implies_collision
#print axioms OmegaJCS.canonicalBytesJCS_injective
EOF
lake env lean /tmp/axioms.lean

SafeVerify replay against all ten shipped .olean files (OmegaProof, OmegaV14, OmegaP3Semantic, OmegaP1Governance, FailureProtocol, OmegaHashChain, OmegaGovernance, OmegaJCSChain, OmegaP5Gate, OmegaProvenance) passed on 2026-06-24 on the standard allowlist (SafeVerify main @ Lean v4.27.0). lean4lean v4.29 segfaults on OmegaProof; attestation uses SafeVerify v4.27. VCVio removed from lakefile.lean v1.4.3 (see VCVIO_RECON.md).

Six honest limits.

These failure modes cannot be closed by a pre-execution black-box governance protocol without model weight access, full execution stack verification, or deployment-layer controls as stated. They are documented alongside the formal artefacts so the scope of the model remains explicit.

FOU: Omniscient Deceiver

An agent can present a perfect compliance facade over a misaligned objective, and without model-weight or activation access post-hoc rationalisation is indistinguishable from genuine reasoning, so OMEGA verifies outputs and commitments rather than internal cognitive fidelity.

Closure requires: model weight access or formal verification of goal representations.

FAP: Anchor Poisoning Residual

If the initial anchor metric for the Continuity Protocol is flawed, the protocol preserves the wrong thing. PCF prevents NLP spoofing of the evaluator: it cannot self-validate the appropriateness of the initial metric selection.

Closure requires: meta-governance at anchor definition time: external validation of metric selection independent of the governed system.

FAB: Attestation Base Integrity

A malicious binary approved in the attestation whitelist via supply chain attack produces valid OMEGA records of invalid behaviour. P5E binds the execution payload to an approved hash: it cannot verify the semantic safety of what was approved.

Closure requires: formal verification of binary behaviour: infeasible at scale without weight-equivalent access to the binary's intent.

FPS: Physical Staleness Gap

Physical environment changes between P5 confirmation and physical actuation. OMEGA commits what the system believed before acting. It cannot re-evaluate physical conditions at the moment of actuation: this is a fundamental boundary of pre-execution governance.

Closure requires: real-time safety interlock integration: hardware-level sensor attestation at the moment of physical execution.

FAH: Accountability Horizon

OMEGA's accountability claims hold only for Human-Agent Collectives whose minimum compound autonomy stays below the Accountability Horizon Λ̂* = 1 − 1/|C_min|; above it, Tibebu (arXiv:2604.07778, April 2026) proves no framework can simultaneously satisfy Attributability, Foreseeability Bound, Non-Vacuity, and Completeness.

Closure requires: reducing compound autonomy below Λ̂* at the deployment layer. OMEGA does not measure or constrain compound autonomy; this limit must be enforced outside the protocol.

FAA: Attestation Authority Integrity

P10 requires cryptographic binding of a competence claim to the decision record. The claim is made by an attestation authority. If that authority is compromised: through regulatory capture, credential inflation, social engineering, or collusion: a valid P10 record can accompany an incompetent agent's action. Distinct from FAB (computational attestation base), FAA covers human and institutional authority integrity.

Closure requires: deployment-layer attestation authority diversity, transparency logs for credentialing decisions, and time-bounded competence claims.