MarkovPrinciple
plain-language theorem explainer
Markov's principle: a binary sequence that is not identically false must be true at some index. It is the constructive "known-to-halt unbounded search succeeds" axiom. Anyone relating LPO, WLPO, and search principles in the omniscience hierarchy cites it. The declaration is a pure Prop abbreviation, not a proved assertion.
Claim. Markov's principle is the statement that for every binary sequence $\alpha:\mathbb{N}\to\{\mathrm{false},\mathrm{true}\}$, if $\neg(\forall n,\,\alpha(n)=\mathrm{false})$, then $\exists n,\,\alpha(n)=\mathrm{true}$.
background
The Omniscience module records the classical hierarchy of limited omniscience principles over binary sequences $\alpha:\mathbb{N}\to\mathrm{Bool}$. These principles measure how much non-constructive information is needed to decide $\Sigma^0_1$ and $\Pi^0_1$ statements about sequences.
Markov's principle is the search fragment: from a proof that $\alpha$ is not everywhere false, one may extract a witness where it is true. It is strictly weaker than the Limited Principle of Omniscience (LPO), which decides for every $\alpha$ whether it is identically false or hits true somewhere. The Lesser Limited Principle (LLPO) is weaker still and encodes order dichotomy and exact IVT content.
In Recognition Science this hierarchy sits inside Primitive Recognition Calculus, where certified analytic protocols and real values are built from constructive data; omniscience principles mark exactly which classical leaps are being assumed when one passes from protocols to decided reals.
proof idea
No proof: the declaration is a definitional abbreviation of a Prop. The body is the universal quantification over binary sequences of the implication from non-identity-with-false to existence of a true term. Downstream theorems treat it as a hypothesis or conclusion by unfolding this Prop.
why it matters
The definition is the hinge that pins LPO between weaker principles. Downstream, lpo_imp_markov shows full omniscience implies the known-to-halt search (choice-free). Conversely, wlpo_and_markov_imp_lpo shows that deciding the $\Pi^0_1$ statement together with Markov recovers LPO exactly, again choice-free.
In the Recognition foundation this matters because certified real values and analytic protocols are constructive; any appeal to classical dichotomy or intermediate-value content must be tracked as an omniscience assumption. Markov is the minimal search axiom that turns a negative non-existence proof into a positive witness, which is the constructive content of "unbounded search known to succeed." It does not itself force the eight-tick or $J$-cost structure, but it clarifies the logical strength of any later classical real-analysis step in the calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.