Foundation Primitive Recognition Calculus Omniscience Llpo

The Lesser Limited Principle

In mathematics, the Lesser Limited Principle of Omniscience (LLPO) is a statement about binary sequences, which are infinite lists where each entry is either true or false. The principle concerns sequences with a special property: at most one entry in the entire infinite list is true. LLPO asserts that for any such sequence, either every entry in the even positions (2nd, 4th, 6th, and so on) is false, or every entry in the odd positions (1st, 3rd, 5th, and so on) is false. In other words, if there is at most one true entry, you can always identify a parity, even or odd, that contains no true entry at all.

This statement is a classical theorem in ordinary mathematics, where it is trivially true. Its significance emerges in constructive mathematics, where a proof must provide a method for finding the answer. LLPO is not constructively provable because there is no general algorithm that can examine an infinite sequence and decide which parity is all-false. It is a weaker cousin of the Limited Principle of Omniscience (LPO), which asserts that for any binary sequence, either it is all false or it has a true entry somewhere. The framework's machine-checked library of formal theorems proves that LPO implies LLPO, and that LLPO is strictly weaker than LPO. The library also proves an exact equivalence: LPO holds if and only if both the Weak Limited Principle of Omniscience (WLPO) and Markov's Principle hold. WLPO decides whether a sequence is all false, while Markov's Principle states that a sequence known not to be all false must have a true entry. Together, these two weaker principles exactly capture the full strength of LPO.

Within Recognition Science, this principle appears in the foundation of its primitive recognition calculus, which models how a discrete ledger of events can be processed. The framework does not use LLPO as an axiom or a theorem about physics. Instead, the declaration in its library is a formal definition of a known mathematical statement, along with proofs of its relationships to other omniscience principles. The library shows, for instance, that LLPO is the omniscience content behind the order dichotomy for real numbers, where for any real number x, either 0 ≤ x or x ≤ 0. This connection is a formal fact about logic, not a claim about how recognition events behave in the physical world.

What LLPO does not claim is just as important as what it does. It does not claim that a search through an infinite sequence can always find a true entry; that is the stronger LPO. It does not claim that the even or odd parity can be identified by a finite procedure; it only asserts the disjunction exists. And importantly, the declaration in the framework's library does not claim that the physical universe is governed by this principle. It is a formal tool, a precise statement about the limits of constructive reasoning, placed in the foundation for logical completeness, not as a physical law.

/-- **LLPO**, the Lesser Limited Principle of Omniscience. For a binary sequence with
at most one `true` term, either all even-indexed terms are `false`, or all
odd-indexed terms are `false`. This is the omniscience content of the order dichotomy
`0 ≤ x ∨ x ≤ 0` and of the (exact) intermediate value theorem. Strictly weaker than
`LPO`. -/
def LLPO : Prop :=
  ∀ α : ℕ → Bool,
    (∀ m n, α m = true → α n = true → m = n) →
    ((∀ k, α (2 * k) = false) ∨ (∀ k, α (2 * k + 1) = false))

/-- `LPO ⇒ LLPO`. Given the witness located by `LPO` and the at-most-one-true
hypothesis, every index of the other parity must be `false`. The parity split is the
omega-produced disjunction `n % 2 = 0 ∨ n % 2 = 1`, so the proof avoids the classical
`Nat.even_or_odd` and stays choice-free. -/
theorem lpo_imp_llpo (h : LPO) : LLPO := by
  intro α hone
  rcases h α with hall | ⟨n, hn⟩
  · exact Or.inl (fun k => hall (2 * k))
  · have hmod : n % 2 = 0 ∨ n % 2 = 1 := by omega
    rcases hmod with hpar | hpar
    · refine Or.inr (fun k => ?_)
      cases hb : α (2 * k + 1) with
      | false => rfl
      | true => exfalso; have := hone n (2 * k + 1) hn hb; omega
    · refine Or.inl (fun k => ?_)
      cases hb : α (2 * k) with
      | false => rfl
      | true => exfalso; have := hone n (2 * k) hn hb; omega

/-- **The exact location of LPO**: `LPO ⇔ WLPO ∧ Markov`. The two coordinates
are the global bit (WLPO) and the terminating search (Markov); full omniscience
is exactly their conjunction. Choice-free. -/
theorem lpo_iff_wlpo_and_markov : LPO ↔ (WLPO ∧ MarkovPrinciple) :=
  ⟨fun h => ⟨lpo_imp_wlpo h, lpo_imp_markov h⟩,
   fun ⟨hw, hm⟩ => wlpo_and_markov_imp_lpo hw hm⟩

What this page does not claim

LLPO does not claim that a finite procedure can find the true entry in a sequence. The declaration does not assert that the physical universe obeys LLPO. The framework does not use LLPO as a physical axiom.

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/Foundation/PrimitiveRecognitionCalculus/Omniscience.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: