Delta Kernel Ledger Of Lpo Ne Empty

The ledger entry

A ledger, in this framework, is a discrete record of which classical principles a derivation consumed. The declaration ofLPO_ne_empty proves one small fact: the ledger that records the use of LPO, the limited principle of omniscience, is not the empty ledger. LPO is a classical principle that says, for arithmetic statements, if you can decide each instance, then you can decide whether an example exists or none does. The proof is a theorem in the machine-checked library of formal theorems, and it is proved by the decide tactic, which means it follows directly from the definitions by computation.

To see why this matters, consider what the ledger is for. The framework's kernel records every judgment as a pair: the named posits, or classical principles, that the derivation consumed, and the induction tier it used. The base rules post nothing; each posit rule posts its name. A ledger with all fields false is the empty ledger, and it means the derivation was forced, with no classical principles consumed. The theorem ofLPO_ne_empty says that if you use LPO, you cannot claim the empty ledger. The trace is real, and it is decidable: the ledger is a record of Booleans, so checking whether it is empty is a structural fact, not a matter of list bookkeeping.

The theorem is one of a family. The ledger for EM, the full excluded middle schema, is also not empty, and so is the ledger for MP, Markov's principle. The union of two ledgers is empty if and only if both are empty. These facts are proved in the same library, and they compose: if you combine a derivation that used LPO with one that used nothing, the union still shows the LPO trace. The theorem does not claim that LPO is true or false, nor that it is consistent or inconsistent with the framework. It claims only that using it leaves a mark, and the mark is not nothing.

theorem ofLPO_ne_empty : ofLPO ≠ empty := by decide

theorem ofEM_ne_empty : ofEM ≠ empty := by decide

theorem ofMP_ne_empty : ofMP ≠ empty := by decide

/-- A union is empty iff both parts are: the FORCED verdict is inherited by
every sub-derivation. -/
theorem union_eq_empty {a b : Ledger} :
    a.union b = empty ↔ a = empty ∧ b = empty := by
  cases a; cases b
  simp only [union, empty, Ledger.mk.injEq, Bool.or_eq_false_iff]
  constructor
  · rintro ⟨⟨h1, h2⟩, ⟨h3, h4⟩, ⟨h5, h6⟩, ⟨h7, h8⟩⟩
    exact ⟨⟨h1, h3, h5, h7⟩, ⟨h2, h4, h6, h8⟩⟩
  · rintro ⟨⟨h1, h3, h5, h7⟩, ⟨h2, h4, h6, h8⟩⟩
    exact ⟨⟨h1, h2⟩, ⟨h3, h4⟩, ⟨h5, h6⟩, ⟨h7, h8⟩⟩

What this page does not claim

The theorem does not assert that LPO is true, false, consistent, or inconsistent. It does not claim that using LPO is forbidden, only that it is recorded. It does not establish that any particular derivation actually uses LPO.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/DeltaKernel/Ledger.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: