Nat.lpo_implies_wlpo: the limited principle of omniscience yields its weak form

Identifier: F:nat-lpo-implies-wlpo
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). LPO returns a WITNESS when the sequence fires; WLPO returns only a DECISION about whether it never fires. This edge is the forgetful direction, and it is the cheap one: the Hits branch refutes Misses pointwise at the witness through Bool.false_ne_true. The interesting content is that the converse is NOT this edge reversed -- see F:nat-wlpo-and-markov-imply-lpo, where recovering LPO from WLPO needs Markov's principle as a second 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_wlpo : ((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)) -> Or (((x2 : AxNat) -> Eq.{1} Bool (x1 x2) Bool.false)) (Not (((x2 : AxNat) -> Eq.{1} Bool (x1 x2) Bool.false)))))

Dependencies

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

2 direct dependencies 1 direct dependents

Evidence

kernel-Nat.lpo_implies_wlpo

Kind: kernel-term
Status: checked

Supports: Nat.lpo_implies_wlpo 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_wlpo --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_wlpo

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_wlpo

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_wlpo_lands_on_the_decision_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."
}