Delta Kernel Ledger Lpo Left

The posit ledger

A ledger, in this framework, is a discrete record of which assumptions a derivation consumed. The declaration lpo_left establishes a bookkeeping fact: if one side of a union carries the limited principle of omniscience, then the combined record carries it too. The limited principle of omniscience, in its arithmetical form, says that if a property is decidable point by point, then either there exists a witness or the property fails everywhere; it is a classical omniscience principle, not a constructively available one.

The theorem is a monotonicity statement about the union operation on ledgers. If ledger a has the LPO flag set to true, then a.union b also has that flag true, regardless of what b contains. The proof is a case split over the Boolean fields, and the machine-checked library records it as a theorem with no axioms beyond the ambient type theory. The same pattern holds for the other posit flags, em and mp, and for the tier marker indFull.

What this declaration does not claim is more interesting than what it does. It does not say that the limited principle of omniscience is true, or that any derivation actually used it. It does not say that a ledger containing LPO is forced in the sense of the forcing-spectrum accounting; the isForced predicate returns false for any ledger with LPO set, and the theorem ofLPO_isForced records exactly that. The declaration is purely structural: it governs how flags propagate through unions, not which flags appear in the first place.

The practical payoff is decidability of bookkeeping. Because the ledger is a record of Booleans, the union operation and the question of whether a ledger is empty are decidable structural facts, not list bookkeeping. A proof that combines two derivations can check, by computation, whether the combined ledger is forced or conditional. The lpo_left theorem is one small gear in that machinery: it lets the library simplify expressions of the form (a.union b).lpo when a.lpo is known to be true, which keeps the accounting transparent as proofs grow.

theorem lpo_left {a b : Ledger} (h : a.lpo = true) : (a.union b).lpo = true := by
  simp [union, h]

@[simp] theorem ofLPO_isForced : ofLPO.isForced = false := rfl

/-- The posit-and-tier ledger. Fields `em`, `lpo`, `mp` are POSITS (named
classical/omniscience principles consumed). Field `indFull` is a TIER marker:
the derivation used induction on a formula with quantifiers. Extending the
posit alphabet = adding a field. -/
structure Ledger where
  /-- Full excluded middle schema `φ ∨ ¬φ`. -/
  em : Bool
  /-- Limited principle of omniscience (arithmetical form):
  pointwise decidability of `φ` yields `(∃x φ) ∨ (∀x ¬φ)`. -/
  lpo : Bool
  /-- Markov's principle for quantifier-free matrices:
  `¬¬(∃x φ) → ∃x φ`. -/
  mp : Bool
  /-- TIER (not a posit): induction was used on a non-quantifier-free
  formula. `FORCED @ FULL-IND` vs `FORCED @ QF-IND`. -/
  indFull : Bool

What this page does not claim

The limited principle of omniscience is true or constructively valid. A ledger containing LPO is forced in the forcing-spectrum sense. The declaration says anything about which derivations use LPO, only how flags propagate.

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: