lpo_imp_llpo
plain-language theorem explainer
The Limited Principle of Omniscience implies the Lesser Limited Principle of Omniscience: any binary sequence with at most one true bit has either all even indices false or all odd indices false. Constructive analysts tracking the strength of order dichotomy and the exact intermediate-value theorem cite this implication. The proof applies LPO, then splits on the omega-derived parity of any located witness and uses uniqueness to kill the opposite parity class.
Claim. Assume that for every $\alpha:\mathbb{N}\to\mathrm{Bool}$, either $\forall n,\,\alpha(n)=\mathrm{false}$ or $\exists n,\,\alpha(n)=\mathrm{true}$. Then for every $\alpha$ with at most one true term (i.e. $\alpha(m)=\alpha(n)=\mathrm{true}$ forces $m=n$), either $\forall k,\,\alpha(2k)=\mathrm{false}$ or $\forall k,\,\alpha(2k+1)=\mathrm{false}$.
background
This module records the classical omniscience hierarchy used as background for the Primitive Recognition Calculus. LPO (Limited Principle of Omniscience) asserts that every binary sequence is either identically false or true somewhere; equivalently, every $\Sigma^0_1$ predicate on $\mathbb{N}$ is decidable. It is constructively unprovable and classically trivial, and is the omniscience content of real trichotomy.
LLPO (Lesser Limited Principle of Omniscience) is strictly weaker: given a binary sequence with at most one true term, either the even subsequence is identically false or the odd subsequence is. It is the omniscience content of the order dichotomy $0\le x\lor x\le 0$ and of the exact intermediate-value theorem. WLPO sits between them in the usual lattice (deciding the $\Pi^0_1$ statement without producing a witness).
The local goal is a choice-free map of implications among these principles, so later recognition and cost arguments can cite exactly which fragment of classical omniscience they consume.
proof idea
Tactic proof. Introduce the sequence $\alpha$ and the uniqueness hypothesis (at most one true). Apply LPO to $\alpha$.
- If $\alpha$ is identically false, the even-index claim is immediate (restrict to $2k$).
- If a witness $n$ with $\alpha(n)=\mathrm{true}$ is returned, split on the constructive disjunction $n\bmod 2=0\lor n\bmod 2=1$ (via
omega, avoiding classicalNat.even_or_odd).- Even witness: claim all odd indices false. If some $\alpha(2k+1)$ were true, uniqueness would force $n=2k+1$, contradicting parity;
omegacloses. - Odd witness: symmetrically, all even indices are false.
- Even witness: claim all odd indices false. If some $\alpha(2k+1)$ were true, uniqueness would force $n=2k+1$, contradicting parity;
No choice, no classical excluded middle beyond the omega parity split.
why it matters
Pins one edge of the constructive omniscience lattice inside the Foundation layer of Recognition Science: LPO is strong enough to recover LLPO, hence strong enough for the order dichotomy and exact IVT content that LLPO packages. Sibling results in the same module place LPO above WLPO and Markov, and show that WLPO plus Markov recovers LPO, so LPO sits exactly between those weaker principles and full classical omniscience.
No downstream consumers are wired yet (used_by empty). The lemma is infrastructure for later arguments that must declare, rather than hide, any appeal to non-constructive sequence decisions when building recognition cost, ladder, or continuum structure. It does not itself invoke J-cost, phi, or the T0–T8 forcing chain; it only clears the logical ground those developments may later stand on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.