LLPO
plain-language theorem explainer
LLPO is the Lesser Limited Principle of Omniscience: for any binary sequence with at most one true entry, either every even index is false or every odd index is false. Constructive analysts cite it as the omniscience content of the real order dichotomy 0 ≤ x ∨ x ≤ 0 and of the exact intermediate-value theorem. It is strictly weaker than LPO. The declaration is a pure Prop definition, not a proved implication.
Claim. The lesser limited principle of omniscience asserts: for every binary sequence $\alpha:\mathbb{N}\to\{0,1\}$ that is true at most once, either $\alpha(2k)=0$ for all $k$, or $\alpha(2k+1)=0$ for all $k$.
background
This module records the classical omniscience hierarchy used in constructive analysis: LPO (limited principle of omniscience), WLPO (its weak form), Markov's principle, and LLPO. LPO says every binary sequence is either identically false or true somewhere; equivalently, every $\Sigma^0_1$ predicate on $\mathbb{N}$ is decidable. WLPO decides only the $\Pi^0_1$ statement "identically false" versus its negation. Markov's principle is the search principle: if a sequence is not identically false, then it is true somewhere.
LLPO sits strictly below LPO. It restricts attention to sequences with at most one true term and asks only for a parity split: all even indices false, or all odd indices false. Classically every such principle is trivial; constructively each is an independent axiom. The module later proves the choice-free implications LPO $\Rightarrow$ LLPO, LPO $\Rightarrow$ Markov, and LPO $\Rightarrow$ WLPO, together with the recovery WLPO + Markov $\Rightarrow$ LPO.
proof idea
There is no proof body: LLPO is introduced as a bare Prop abbreviation. The universal quantifier ranges over binary sequences; the hypothesis encodes "at most one true"; the conclusion is the even/odd disjunction. Downstream theorems such as lpo_imp_llpo inhabit this type by applying LPO and splitting on the parity of the located witness via an omega-produced disjunction $n\bmod 2=0\lor n\bmod 2=1$.
why it matters
LLPO is the precise omniscience content of the constructive order dichotomy $0\le x\lor x\le 0$ and of the exact intermediate-value theorem; both fail in Bishop-style analysis without some form of LLPO. Inside the module it is the target of lpo_imp_llpo and appears in the sibling lattice with Markov's principle and WLPO. The hierarchy calibrates how much non-constructive power is smuggled into later Recognition Calculus arguments that talk about real comparison, zero-finding, or exact IVT-style existence. It does not itself force the Recognition Science landmarks (T5 J-uniqueness, $\phi$, eight-tick octave, $D=3$); it only records the logical strength needed when those arguments touch classical real analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.