CReal.trichotomy_of_order_decision: trichotomy on the constructed reals, on an explicit order-decision hypothesis

Identifier: F:creal-trichotomy-of-order-decision
Proof route: kernel-lean
External status: Not recorded
Axiom footprint: Empty

Recorded description

The hypothesis is the ORDER DECISION on the constructed reals, OrderDecision := forall (x y : CReal), Or (CReal.lt x y) (CReal.le y x), spelled out inline in the type rather than behind a Definition. It is written strict-on-the-left deliberately: Or (le x y) (le y x) is only LLPO-strength, while the strict form is LPO-strength (applied to 0 and the real coded by a Bool sequence it decides whether the sequence ever fires), and F:creal-le-total-of-order-decision measures exactly that gap. Trichotomy -- for all x y, either x < y, or x is equivalent to y, or y < x -- is available over Q (Rat.lt_trichotomy) precisely because Q's order is decidable, and is ABSENT over CReal for precisely the reason this hypothesis supplies. Two Or.elims and one CReal.equiv_of_le_le: no arithmetic, no subtraction, no estimate. The hypothesis is consumed TWICE, once at (x, y) and once at (y, x), which is the smallest honest measurement of what carrying a classical hypothesis costs -- one extra argument at each of two use sites, and nothing else. 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 CReal.trichotomy_of_order_decision : ((x0 : ((x0 : CReal) -> ((x1 : CReal) -> Or (CReal.lt x0 x1) (CReal.le x1 x0)))) -> ((x1 : CReal) -> ((x2 : CReal) -> Or (CReal.lt x1 x2) (Or (CReal.Equiv x1 x2) (CReal.lt x2 x1)))))

Dependencies

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

1 direct dependencies 1 direct dependents

Evidence

kernel-CReal.trichotomy_of_order_decision

Kind: kernel-term
Status: checked

Supports: CReal.trichotomy_of_order_decision 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 CReal.trichotomy_of_order_decision --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-CReal.trichotomy_of_order_decision

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 creal::omniscience -- --test-threads=4 2>&1 | grep -cE '^test result: ok\. 6 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-CReal.trichotomy_of_order_decision

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 trichotomy_of_order_decision_lands_on_trichotomy_and_needs_the_strict_decision -- --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_creal_prelude (crates/axeyum-lean-kernel/src/creal/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."
}