CReal.abs_cases_of_order_decision: the absolute value of a real is equivalent to it or to its negation, on an explicit order-decision hypothesis

Identifier: F:creal-abs-cases-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. THE CONCLUSION IS THE STATEMENT creal.rs MARKS AS NOT AVAILABLE. CReal.abs's field documentation says: "abs is one-sided throughout -- Equiv (abs x) x or Equiv (abs x) (neg x) is a decision on the sign of a real and is NOT available." It is now available, on a hypothesis. Like the apartness fact this is a DEPTH-2 node: it consumes F:creal-le-total-of-order-decision at the pair (neg x, x) and then closes each branch with the join's universal property (CReal.max_le against CReal.le_refl, and CReal.le_max_left / CReal.le_max_right for the converses), both finished by CReal.equiv_of_le_le. CReal.abs is a Definition unfolding to max x (neg x), so the conclusion is stated with abs and no bridge lemma is needed -- the kernel's own conversion does it. 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.abs_cases_of_order_decision : ((x0 : ((x0 : CReal) -> ((x1 : CReal) -> Or (CReal.lt x0 x1) (CReal.le x1 x0)))) -> ((x1 : CReal) -> Or (CReal.Equiv (CReal.abs x1) x1) (CReal.Equiv (CReal.abs x1) (CReal.neg x1))))

Dependencies

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

6 direct dependencies 0 direct dependents

Evidence

kernel-CReal.abs_cases_of_order_decision

Kind: kernel-term
Status: checked

Supports: CReal.abs_cases_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.abs_cases_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.abs_cases_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.abs_cases_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 abs_cases_of_order_decision_lands_on_the_sign_decision_with_neg_intact -- --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."
}