Nat.lpo_implies_markov: the limited principle of omniscience yields Markov's principle

Identifier: F:nat-lpo-implies-markov
Proof route: kernel-lean
External status: Not recorded
Axiom footprint: Empty

Recorded description

Written over a Bool-valued sequence f : Nat -> Bool, which is Bishop's formulation: Hits f := exists n, f n = true ("f fires somewhere") and Misses f := forall n, f n = false ("f never fires"). LPO is forall f, Or (Hits f) (Misses f); WLPO is forall f, Or (Misses f) (Not (Misses f)); Markov's principle (MP) is forall f, Not (Misses f) -> Hits f; LLPO is forall f g, Not (And (Hits f) (Hits g)) -> Or (Misses f) (Misses g); EM is forall (P : Prop), Or P (Not P). Markov's principle says a sequence that CANNOT miss everywhere must fire somewhere -- an unbounded search that is guaranteed to terminate but with no bound on when. One Or.elim: the Hits branch is the conclusion, and the Misses branch contradicts the standing hypothesis. Markov's principle is the constructively contentious half of LPO, and the direction that matters over the reals: CReal.Apart's own field documentation records that `Not (Equiv x y) -> Apart x y` IS Markov's principle and is neither proved nor assumed in the constructive development (F:creal-apart-of-not-equiv-of-order-decision proves it, on a hypothesis). THE PRINCIPLE IS A HYPOTHESIS, NOT AN AXIOM. It is spelled out inline in the type -- never behind a Definition -- so a reader of the rendered statement sees the whole assumption and nothing about the conclusion can be smuggled into an abbreviation. That is why axiom_footprint is empty. ADR-1601 (roadmap W0-2) decides this policy and prices it: across the ten theorems of this family the hypothesis route costs 11 binders and 14 argument positions and ZERO proof obligations. WHAT THIS FACT DOES NOT CLAIM: it does not claim the principle in its hypothesis is true, false, or independent. The SEPARATIONS in the standard picture -- LPO is not constructively derivable, LLPO does not give LPO, WLPO does not give LPO, MP does not give WLPO -- are CITED here (Bishop, Constructive Analysis ch. 1) and are not proved: each needs a model of this kernel rather than a term in it, and ADR-1600 records why an internal metatheorem about this kernel is unavailable.

Formal statement

theorem Nat.lpo_implies_markov : ((x0 : ((x0 : ((x0 : AxNat) -> Bool)) -> Or (Exists.{1} AxNat (fun (x1 : AxNat) => Eq.{1} Bool (x0 x1) Bool.true)) (((x1 : AxNat) -> Eq.{1} Bool (x0 x1) Bool.false)))) -> ((x1 : ((x1 : AxNat) -> Bool)) -> ((x2 : Not (((x2 : AxNat) -> Eq.{1} Bool (x1 x2) Bool.false))) -> Exists.{1} AxNat (fun (x3 : AxNat) => Eq.{1} Bool (x1 x3) Bool.true))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

1 direct dependencies 1 direct dependents

Evidence

kernel-Nat.lpo_implies_markov

Kind: kernel-term
Status: checked

Supports: Nat.lpo_implies_markov is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection -- --require-declaration Nat.lpo_implies_markov --require-kind theorem

Evidence notes

--require-declaration exits non-zero when the name is absent from every constructed prelude, and --require-kind exits non-zero when it is present with the wrong kind, so the exit status depends on the finding rather than on the run completing. --release is MANDATORY: this binary builds creal/complex/cpoint, which overflow the default debug thread stack.

footprint-Nat.lpo_implies_markov

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the classical principle enters as a HYPOTHESIS and nothing is assumed. Read from Kernel::axiom_footprint, never from a rendered name.

Checker command

cargo test -q --release -p axeyum-lean-kernel --lib nat_prelude::omniscience -- --test-threads=4 2>&1 | grep -cE '^test result: ok\. 8 passed'

Evidence notes

The suite's own footprint test reads Kernel::axiom_footprint for every declaration in the family and fails on a non-empty result. The grep -c count is what makes the command discriminating: a fabricated or renamed filter makes cargo print a different passed-count and exit 0, and the anchored pattern then matches nothing, so grep -c prints 0 and exits 1. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. Anchored with [[:space:]]-free literals, never \t -- in a scripted (GNU) grep \t is a literal t.

discrimination-Nat.lpo_implies_markov

Kind: instance-pin
Status: checked

Supports: The statement is the one advertised, not a weaker or stronger one: the theorem is applied at GENUINELY FREE variables of the hypothesis type and the inferred conclusion is pinned against an independently rebuilt term, and a negative control in the hypothesis slot is REQUIRED TO BE REJECTED.

Checker command

cargo test -q --release -p axeyum-lean-kernel --lib lpo_implies_markov_lands_on_the_witness_and_rejects_wlpo_in_its_own_slot -- --test-threads=4 2>&1 | grep -cE '^test result: ok\. 1 passed'

Evidence notes

Numerals reduce and hide definitional-equality gaps, so nothing in this test instantiates a sequence or a real concretely. The builders in the test file are a SECOND, independent implementation of every principle: if they called the module's own private helpers, the check would be comparing a term with itself and could not fail.

Provenance

{
  "date": "2026-09-04",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_nat_prelude (crates/axeyum-lean-kernel/src/nat_prelude/omniscience.rs)",
  "source": "formal.statement is the Kernel::render_lean(declaration.ty()) column of `cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection`, verbatim; axiom_footprint is its footprint-size column (0). No type was hand-transcribed. Prose is hand-written."
}