IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Omniscience
Defines the classical omniscience principles used in constructive analysis: LPO, WLPO, LLPO, and Markov's principle, together with the standard implication lattice among them. Anyone tracking decidability assumptions behind real trichotomy or forced discrete gaps cites this module. The body is definitional plus short implication proofs; nothing here asserts that LPO holds constructively.
claimThe module packages four omniscience axioms over binary sequences $\alpha:\mathbb{N}\to\{0,1\}$: LPO (either $\alpha$ is identically $0$, or $\alpha(n)=1$ for some $n$), WLPO, LLPO, and Markov's principle, plus the classical implications $\mathrm{LPO}\Rightarrow\mathrm{WLPO}$, $\mathrm{LPO}\Rightarrow\mathrm{Markov}$, $\mathrm{LPO}\Rightarrow\mathrm{LLPO}$, and $\mathrm{WLPO}\wedge\mathrm{Markov}\Rightarrow\mathrm{LPO}$.
background
In constructive mathematics, quantification over infinite binary sequences is not automatically decidable. The Limited Principle of Omniscience (LPO) asserts that every such sequence is either identically false or true at some index; equivalently, every $\Sigma^0_1$ predicate on $\mathbb{N}$ is decidable. Classically this is trivial (law of excluded middle); constructively it is an extra axiom.
Weaker siblings sit below LPO: WLPO decides only the "all false" side, LLPO is a disjunctive half-principle, and Markov's principle recovers existence from double-negated existence for decidable predicates. The module doc ties LPO to the omniscience content of real-number trichotomy: deciding $x<0$, $x=0$, or $x>0$ for arbitrary reals requires essentially this strength.
The surrounding Primitive Recognition Calculus uses these named hypotheses when a discrete forcing or gap argument would otherwise smuggle classical case splits on infinite data.
proof idea
This is primarily a definition module. Each principle is introduced as a Prop over binary sequences (or equivalent $\Sigma^0_1$ form). The four implication lemmas are short constructive proofs: LPO specializes to WLPO, Markov, and LLPO by discarding disjuncts or rewriting quantifiers; the converse direction shows WLPO plus Markov recover full LPO by using Markov to extract a witness once WLPO rules out the all-false case. No attempt is made to prove any principle from pure intuitionistic logic.
why it matters in Recognition Science
DeltaForced imports this module, so every downstream forcing or discreteness argument that needs a named omniscience hypothesis draws its vocabulary here rather than inlining classical excluded-middle. In the Recognition foundation stack, primitive recognition calculus must track exactly which discrete decisions about sequences or reals are assumed when deriving forced gaps, ticks, or dimensional constraints; packaging LPO and its weakenings keeps those assumptions auditable.
The module does not itself advance the T0–T8 forcing chain, but it supplies the constructive hygiene layer those later steps rely on whenever a proof would otherwise treat "exists a hit in the sequence" as decidable without comment.
scope and limits
- Does not prove LPO, WLPO, LLPO, or Markov from pure constructive logic.
- Does not derive real trichotomy; only records that LPO is its omniscience content.
- Does not connect omniscience principles to phi, J-cost, or eight-tick structure.
- Does not quantify computational cost or oracle strength beyond the named Props.
- Does not address choice principles outside this small implication lattice.