Four Lean 4 theorem files on the legitimacy of authority, the residues of attestation, the achievability of containment, and the information-theoretic floor of trust — kernel-checkable, no mathlib, no sorry.
Below is the actual Lean 4 source of four theorem files, unedited. No Lean toolchain was available in the environment that built this page, so nothing here was re-run against the Lean kernel to produce this page — there is no "compiles ✓" badge, because that would not be true. What can honestly be said: every line was read, no file contains sorry or an admitted gap, and the syntax uses only Lean 4 core (no mathlib import). Verify it yourself: lean governance.lean, and so on for the other three. Each file ends with its own "Honest scope" note, kept intact below — read those before the theorem, not after.
A locus is legitimate only if it has a distinct legitimate governor. From that one recurrence, three things follow: an ungoverned "top" is never legitimate (the dogmatic horn — authority that answers to nothing is self-asserted, not earned); a locus that only governs itself can't be legitimate either (the cycle horn — reflexive authority fails the distinctness requirement); and if legitimacy is defined as the smallest predicate closed under that recurrence with no base case, it's empty — nothing satisfies it (the regress horn). No structure is both complete and fully legitimate. A companion lemma: an agent that sets its own boundary always weakly prefers to widen it — self-set boundaries are ratchets, not walls.
theorem top_not_legit
{G : Locus → Locus → Prop} {L : Locus → Prop}
(hL : IsLegitimacyPred G L) {T : Locus} (hT : IsTop G T) : ¬ L T := by
intro hLT
obtain ⟨x, _, hGxT, _⟩ := hL T hLT
exact hT x hGxT
theorem no_self_ground
{G : Locus → Locus → Prop} {L : Locus → Prop}
(hL : IsLegitimacyPred G L) {y : Locus}
(hLy : L y) (onlySelf : ∀ x, G x y → x = y) : False := by
obtain ⟨x, hne, hGxy, _⟩ := hL y hLy
exact hne (onlySelf x hGxy)
theorem regress_empty {G : Locus → Locus → Prop} (y : Locus) :
¬ LegitLFP G y := by
intro h; induction h with
| step _ _ _ ih => exact ih
theorem value_monotone
{A : Type} {u : A → Nat} {B B' : A → Prop}
(hsub : ∀ a, B a → B' a)
{aStar : A} (hB : B aStar) (hmax : ∀ a, B a → u a ≤ u aStar) :
∃ b, B' b ∧ ∀ a, B a → u a ≤ u b :=
⟨aStar, hsub aStar hB, hmax⟩
Four loci, each governed by the next. Click one to mark it "the top" (ungoverned). The proof says: whatever you pick, it can't be legitimate.
A sound attestation discharges containment with no requirement that the checker be exterior to the selector — so where does "exterior" actually have to live? Three places, and removing any one collapses the certificate: (i) the spec — if the agent can weaken its own spec, it ratchets to the vacuous predicate True, which every trace satisfies, including violating ones; (ii) the trust root — if the verifier's own soundness is only self-attested, the evaluator's own rule (reject self-attested evidence) blocks acceptance outright; (iii) timing — a verdict computed after an irreversible action never enters the containment predicate, so it can't retroactively make a violating trace contained. Given all three exterior conditions, containment is sufficient — necessity is carried by these three residues.
theorem vacuous_certifies_nothing
{A : Type} (admStrict : A → Prop) (tr : Trace A)
(someViolation : ∃ t, ¬ admStrict (tr t)) :
Contained (fun _ => True) tr ∧ ¬ Contained admStrict tr := by
refine ⟨fun _ => trivial, ?_⟩
obtain ⟨t₀, hv⟩ := someViolation
intro h; exact hv (h t₀)
theorem root_selfattested_fails
{Ev : Type} {AccE selfAttested : Ev → Prop}
(C4 : ∀ e, selfAttested e → ¬ AccE e)
{soundnessClaim : Ev} (hself : selfAttested soundnessClaim) :
¬ AccE soundnessClaim :=
C4 soundnessClaim hself
theorem postaction_insufficient
{A : Type} (adm : A → Prop) (tr : Trace A)
{t₀ : Nat} (violation : ¬ adm (tr t₀)) :
¬ Contained adm tr := by
intro h; exact violation (h t₀)
Given a fixed, exterior-supplied verifier that is sound and complete for a boundary B, and B is adequate (a subset of the target set A*): gating every action through the verifier before it executes puts every executed action in A* — containment, with no exterior information entering per-action. Two side conditions make the gate honest rather than trivial: completeness means it never blocks an admissible action (liveness — no false rejections), and soundness means it genuinely rejects anything outside B (non-vacuity — the gate actually bites).
theorem achiev_correct
{A : Type} (V : A → Bool) (B Astar : A → Prop)
(Vsound : ∀ a, V a = true → B a)
(Badeq : ∀ a, B a → Astar a)
(tr : Trace A) (gated : ∀ t, V (tr t) = true) :
∀ t, Astar (tr t) := by
intro t; exact Badeq _ (Vsound _ (gated t))
theorem achiev_live
{A : Type} (V : A → Bool) (B : A → Prop)
(Vcomplete : ∀ a, B a → V a = true)
{a : A} (hB : B a) : V a = true := Vcomplete a hB
theorem rejects_excluded
{A : Type} (V : A → Bool) (B : A → Prop)
(Vsound : ∀ a, V a = true → B a)
{a : A} (hnotB : ¬ B a) : V a = false := by
cases hva : V a with
| false => rfl
| true => exact absurd (Vsound a hva) hnotB
If the best key-guessing forgery succeeds on at least one key out of the secret's support, and soundness bounds any forgery to at most a 2⁻λ fraction of that support, then the support must have size at least 2^λ — the secret's min-entropy is at least λ bits. A claimed soundness of 2⁻λ is not free: it costs a trust anchor with at least λ bits of uncertainty behind it, or it's impossible.
theorem trust_floor (NK lam fcount : Nat)
(hguess : 1 ≤ fcount)
(hsound : fcount * 2 ^ lam ≤ NK) :
2 ^ lam ≤ NK := by
obtain ⟨f', hf'⟩ : ∃ f', fcount = f' + 1 := ⟨fcount - 1, by omega⟩
have hexp : fcount * 2 ^ lam = f' * 2 ^ lam + 2 ^ lam := by
rw [hf', Nat.add_mul, Nat.one_mul]
omega
theorem short_key_breaks_soundness (NK lam fcount : Nat)
(hguess : 1 ≤ fcount) (hshort : NK < 2 ^ lam) :
¬ (fcount * 2 ^ lam ≤ NK) := by
intro hsound
have := trust_floor NK lam fcount hguess hsound
omega