A Machine-Checked Necessity Result for Accountable Delegated Authority
For thirty years the logic of delegated authority rested on pen and paper. I ran it through a machine.
New paper, machine checked in Lean 4. A six condition predicate for accountable delegated authority: cryptographic binding, identity, mandate, scope, revocation dominance, and appointment. Single governor result derived from an explicit hypothesis on the signature predicate, not assumed. Necessity direction, converse disclaimed. Zero sorry. Sealed and timestamped on the public blockchain.
Block 964554, transaction 78f1c12071618375df1f23410075da604c171583009fe4eb69300c0717923172
Block 964600, transaction 457d89db25e656defc38137eec928517dfb32e778629687bb359dd54827d32fd
A5O.lean exists in three versions, each labeled and independently checkable.
v2 — SHA-256 c219cb0e0c0e8b3948fb0d04060afaaef9da705cfc06aef732376cce47c44ec6, 696 lines. This is the file the sealed paper describes, reproduced in the report of 25 August 2026 and referenced by the paper's §12 and cover page. Attested at Bitcoin blocks 965627, 965642, and 965689.
v3 — SHA-256 2fde9ccbf3ff8d851e1bbf6dcb0de6809d67cf8d2be2fbf440da8387cc13de2a, 736 lines. This is A5O.lean at tag paper-sealed-2026-08-29 — v2 plus a RevocationConsequences section, making revocation dominance load-bearing. Attested at Bitcoin blocks 965627, 965642, and 965689.
v4 — SHA-256 0e5ebe3f5113727ae0cd41ec4399661a352fcc4fb522fcfe7ef7be3318f6b452, 792 lines. This is the 2026-09-07 repair: the nine axioms in v2 and v3 are restated as explicit hypothesis parameters on the theorems that consume them, and all 33 theorems in the file report no axiom dependency. Submitted to OpenTimestamps on 2026-09-07T08:44:33Z; attested at Bitcoin blocks 965908 and 965933.
v2 and v3 carry the nine axioms later found individually inconsistent as stated — each was generalized by Lean over every predicate of its declared type rather than the one predicate the file reasons about, so each derives False when instantiated at a pathological predicate. The sealed paper (.tex/.pdf) is unrevised by this finding.
Two signed corrections address defects found after the paper was sealed. Neither edits the sealed paper; both are issued separately, per standing practice.
Correction to Executive Provenance Record AOB-PROV-2026-08-31-0001, §5.3 (Ref: AOB-CORR-2026-09-06-0001) — corrects §5.3's citation of tag paper-sealed-2026-08-29: that tag resolves to v3, not v2, while the paper's §12 and cover describe v2. Dated 2026-09-06, envelope f94f3dab-3fec-4a18-894b-33373ef268ff. Hash of the signed instrument: 8d446af28d95efe6e6b122e3d6819c7a42f2739b796c91457615e30aba69faf7, attested at Bitcoin block 965717 (verified directly on that instrument's own proof, not inferred; two of three calendars remain pending). The signed PDF itself is not published; its source text is, at hash ae9ed913ca7361628b004ba0e191c7c9a3b97c90542bf0bc515e9f893d44b21c, same block. Directly: artifacts.agentobo.ai/a5o/CORRECTION-2026-09-06-provenance-5.3.md
Correction: all nine axioms were individually inconsistent (no reference number was assigned to this correction) — corrects the paper's §Axioms, §Uniqueness, and each of the five prior-art sections, which described the nine axioms as reasonable, independently-justified assumptions; each was in fact individually inconsistent as stated, and v4 is the repair. Dated 2026-09-07, envelope fa7e9727-b043-4764-a679-58df8d24147e, signed 2026-09-07T08:33:39Z. Hash of the signed instrument: dc15cb164d8f2d41516de6b4661db8535736847a8facfd02b2dd0d126d756d6e. Submitted to OpenTimestamps on 2026-09-07T08:51:43Z; attested at Bitcoin blocks 965908 and 965933. Directly: artifacts.agentobo.ai/a5o/corrections/2026-09-07/Correction to the paper_ all nine axioms were individually inconsistent - Signed.pdf
Three further developments extend the proof beyond A5O.lean. Each is signed, committed, and Bitcoin-anchored; each directory carries its own Check.lean and axioms.txt.
v4/hops — the delegation-chain lineage and its companion. Multi-hop delegation formalized as single-hop appointment iterated: the appointer of one receipt is the agent of an earlier one, and revocation cascades downstream. Fifty-two theorems, no axiom dependency. Seven signed instruments; proofs attested at Bitcoin blocks 967682, 967703, and 967720. Directly: artifacts.agentobo.ai/a5o/v4/closure/hops-companion-closure-2026-09-19.md
v5 — the live gate's deployment closure. The production ledger of theapertures.app exported as a signed trace, consumed by a Lean adapter, and proved to satisfy the gate's own checkers, with the two hypotheses Lean cannot discharge carried as signed operator attestations. Attested at Bitcoin block 966664. Directly: artifacts.agentobo.ai/a5o/v5/README.md
v4/clock — the Clock Standard, Giza, and DataCenter, 19 September 2026. The A⁵O Clock Standard (17.5 ns, 400/7 MHz) fixed as the time axis of the proof: strict precedence, one state per tick, revocation dominance on the clock, and an exposure bound of one tick under a single stated hypothesis. Two exploratory files carry the same constant into arithmetic on the royal cubit and into the physical placement of a ledger relative to its gate, with overlay labeled as such. Six signed instruments, both versions of each file; proofs attested at Bitcoin blocks 967720, 967728, 967736, and 967784. Directly: artifacts.agentobo.ai/a5o/v4/clock/proof-record-2026-09-19.md
Full index, all versions, both corrections, and the three developments above: artifacts.agentobo.ai/a5o/README.md
Re-check with Lean 4.14.0 for v2, v3, and v4, and Lean 4.33.1 for v4/hops, v4/clock, and v5: lean A5O.lean, then lean Check.lean, and compare the output to axioms.txt. Each directory carries its own Check.lean and axioms.txt. Verified, not ratified.
