WLPO
plain-language theorem explainer
WLPO is the weak limited principle of omniscience: every binary sequence is either identically false, or not. It decides the Π⁰₁ statement without producing a Σ⁰₁ witness. Constructive analysts cite it as the omniscience content short of full LPO. The declaration is a pure Prop definition, not a proved assertion.
Claim. The weak limited principle of omniscience asserts: for every binary sequence $\alpha:\mathbb{N}\to\{0,1\}$, either $\forall n,\,\alpha(n)=0$, or it is not the case that $\forall n,\,\alpha(n)=0$. Equivalently, every $\Pi^0_1$ statement over $\mathbb{N}$ is decidable, without deciding a $\Sigma^0_1$ witness.
background
This module packages the classical omniscience principles used in constructive analysis: LPO, WLPO, LLPO, and Markov's principle. LPO says that for every binary sequence $\alpha$, either $\alpha$ is identically false or some entry is true (every $\Sigma^0_1$ predicate on $\mathbb{N}$ is decidable). Classically trivial, constructively unprovable; it is the omniscience content of real trichotomy.
WLPO weakens the positive disjunct of LPO from an existential witness to a double negation: one still decides whether the sequence is identically false, but without locating a true bit. In arithmetic hierarchy language, WLPO decides the $\Pi^0_1$ statement, not its $\Sigma^0_1$ dual. Markov's principle (defined next in the file) is the dual search axiom: if a sequence is not identically false, then it is true somewhere.
proof idea
No proof: this is a definitional abbreviation of a proposition. The body is the universal quantification over binary sequences of the classical disjunction between the $\Pi^0_1$ statement and its negation. Downstream implication theorems treat the name as a hypothesis or conclusion Prop.
why it matters
WLPO sits in the standard constructive hierarchy between full LPO and weaker fragments. Downstream, lpo_imp_wlpo shows LPO implies WLPO by discarding the witness; wlpo_and_markov_imp_lpo shows that WLPO plus Markov recovers LPO, pinning LPO exactly as the conjunction of deciding the $\Pi^0_1$ statement and unbounded search. LLPO (lesser LPO, the omniscience behind $0\le x\lor x\le 0$ and exact IVT) is a separate weaker principle also implied by LPO.
In the Recognition Science foundation layer this module supplies the constructive baseline against which later forcing and calculus arguments are measured: which real-analytic dichotomies require which omniscience. It does not itself invoke the T0–T8 forcing chain, $\phi$, or the eight-tick octave; those live upstream in UnifiedForcingChain. The value here is a clean, choice-free interface for omniscience hypotheses used by the primitive recognition calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.