Foundation Primitive Recognition Calculus Omniscience Lpo Imp Llpo

The implication

In mathematics, an infinite binary sequence is a list of true-or-false values that goes on forever, such as the digits of a number or the answers to a yes-or-no question posed for every whole number. Three classical principles describe how much a mathematician may know about such a sequence. The Limited Principle of Omniscience (LPO) says that for any sequence, either every entry is false or at least one entry is true. The Lesser Limited Principle of Omniscience (LLPO) applies only to sequences with at most one true entry, and says that either all even-indexed entries are false or all odd-indexed entries are false. The theorem lpo_imp_llpo proves that LPO implies LLPO: if you can always locate a true entry, then you can decide which parity contains it.

The proof is short and instructive. Given a sequence with at most one true entry, LPO finds the unique true position. That position has a parity: it is either even or odd. If the true entry sits at an even index, then all odd-indexed entries must be false, because the sequence has no second truth. The other case is symmetric. The argument uses only the fact that every natural number is either even or odd, a fact the framework derives constructively from the definition of the natural numbers, not from the classical law of excluded middle. The theorem is recorded in the framework's machine-checked library of formal theorems, where every step is verified by the computer.

The implication matters because it orders the principles by strength. LPO is the stronger claim, and LLPO is strictly weaker: there are constructive settings where LLPO holds but LPO does not. The framework also proves the converse direction in a precise sense: LPO is exactly the conjunction of the weaker Weak Limited Principle of Omniscience (WLPO), which decides whether a sequence is all false, and Markov's Principle, which says a known-to-terminate search does terminate. That exact location, LPO if and only if WLPO and Markov, is a separate theorem in the same file. Together these results map the constructive territory of omniscience principles without relying on classical axioms.

In Recognition Science, this theorem is part of the foundation layer that studies what a discrete ledger of events can and cannot know. The framework treats the cost of recognition as forced, and these omniscience principles describe the limits of that recognition: what a process can decide about an infinite stream of observations. The implication itself does not assert that any physical process actually possesses LPO or LLPO. It only records a logical relationship: if one kind of omniscience were available, another would follow automatically, and the proof shows exactly why, with no appeal to excluded middle.

/-- `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

/-- `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

The theorem does not assert that any physical process possesses LPO or LLPO. It does not prove LLPO implies LPO, only the one-way implication. It does not rely on the law of excluded middle or any choice principle.

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: