lpo_imp_markov
plain-language theorem explainer
Full Limited Principle of Omniscience implies Markov's principle: a binary sequence known not to be identically false must hit true somewhere. Constructive analysts and anyone mapping the omniscience lattice in Primitive Recognition Calculus cite this implication. The argument is a direct case split on the LPO disjunction, killing the all-false branch by absurdity. Choice-free throughout.
Claim. Assume the Limited Principle of Omniscience: for every $\alpha:\mathbb{N}\to\mathrm{Bool}$, either $\forall n,\,\alpha(n)=\mathsf{false}$ or $\exists n,\,\alpha(n)=\mathsf{true}$. Then Markov's principle holds: for every such $\alpha$, $\neg(\forall n,\,\alpha(n)=\mathsf{false})$ implies $\exists n,\,\alpha(n)=\mathsf{true}$.
background
The module collects classical omniscience principles as pure propositions over binary sequences, without assuming classical logic globally. LPO (Limited Principle of Omniscience) asserts that every $\alpha:\mathbb{N}\to\mathrm{Bool}$ is either identically false or true at some index; 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.
Markov's principle is the weaker search axiom: if $\alpha$ is not identically false, then a true entry exists. It is the constructive reading of "an unbounded search known to succeed does succeed." Sibling principles in the same file include WLPO (decide the $\Pi^0_1$ negation without a witness) and LLPO (parity split under an at-most-one-true hypothesis), the latter tied to order dichotomy and exact IVT.
The local setting is the Primitive Recognition Calculus foundation: these principles calibrate how much global decision power is smuggled into recognition or trace reasoning. The implication here is the standard lattice edge LPO $\Rightarrow$ Markov.
proof idea
Term/tactic hybrid, essentially a one-step case analysis. Introduce the sequence $\alpha$ and the hypothesis that it is not identically false. Apply the LPO assumption to $\alpha$, obtaining the disjunction "all false or exists true." The all-false branch contradicts the negation hypothesis via absurd. The existential branch is exactly the Markov conclusion. No auxiliary lemmas, no choice, no classical even_or_odd.
why it matters
Places Markov inside the LPO cone of the omniscience hierarchy developed in Foundation.PrimitiveRecognitionCalculus.Omniscience. Sibling edges in the same module are LPO $\Rightarrow$ WLPO, LPO $\Rightarrow$ LLPO, and the converse reconstruction WLPO $\wedge$ Markov $\Rightarrow$ LPO, so this theorem is one strut of the lattice that identifies full omniscience with the conjunction of weak omniscience and known-to-halt search.
In Recognition Science terms, LPO is the decision content behind real trichotomy; Markov is the minimal search needed once non-existence of a null sequence is already known. Keeping the implication choice-free matters for later constructive readings of recognition traces and defect calculus, where classical case splits would silently import more omniscience than the forcing chain (T0--T8) licenses. No downstream consumers are wired yet; the result stands as a proved lattice edge ready for any argument that assumes LPO and needs a witness from a negated universal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.