IVT's ADR-0603 row 2: an exact root of the plateau family decides the sign of an arbitrary real

Identifier: F:creal-ivt-exact-root-decides-sign
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let v be an arbitrary constructive real and let ivtPlateau v be the family x |-> min x (max (x + (-1)) v) on [0, 1] -- the clamp of v into the unit-width window [x-1, x]. That family satisfies every hypothesis of the classical Intermediate Value Theorem, and each of the three is a kernel theorem rather than an assertion: it is uniformly continuous on [0, 1] (CReal.ivtPlateau_uniformly_continuous), its value at the left endpoint is <= 0 (CReal.ivtPlateau_nonpos_at_zero), and its value at the right endpoint is >= 0 (CReal.ivtPlateau_nonneg_at_one), the last two unconditionally in v. Then: from any c with an EXACT root, Equiv (ivtPlateau v c) zero, it follows that v <= 0 or 0 <= v. Since a decision procedure for classical IVT would supply such a c for every v at once, the classical conclusion is at least as strong as analytic LLPO -- equivalently the total order le_total over CReal, which this kernel demonstrably does not have. This is an UNPROVABILITY witness, not a refutation: analytic LLPO is consistent with Bishop's constructive mathematics, so it is unprovable here rather than false.

Formal statement

theorem CReal.ivt_exact_root_decides_sign : ((x0 : CReal) -> ((x1 : CReal) -> ((x2 : CReal.le CReal.zero x1) -> ((x3 : CReal.le x1 CReal.one) -> ((x4 : CReal.Equiv (CReal.min x1 (CReal.max (CReal.add x1 (CReal.neg CReal.one)) x0)) CReal.zero) -> Or (CReal.le x0 CReal.zero) (CReal.le CReal.zero x0))))))

Dependencies

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

18 direct dependencies 0 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-CReal.ivt_exact_root_decides_sign

Kind: kernel-term
Status: checked

Supports: CReal.ivt_exact_root_decides_sign 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 theorem_dependency_inventory -- CReal.ivt_exact_root_decides_sign 2>/dev/null | /usr/bin/grep -cE '^CReal\.ivt_exact_root_decides_sign[[:space:]]'

Evidence notes

Two independent failure modes, so the exit status depends on the finding rather than on the run completing: theorem_dependency_inventory exits non-zero when a NAMED filter matches nothing, and grep -c exits 1 printing 0 when the anchored line is absent. Anchored with [[:space:]], never \t -- in a scripted (GNU) grep \t is a literal t, and 54 facts in this ledger once matched nowhere but one interactive shell because of it. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. /usr/bin/grep explicitly, because an interactive `grep` here is a ugrep wrapper with different escape semantics. --release is MANDATORY: this tool builds creal/complex/cpoint, which overflow the default debug thread stack.

hypothesis-class-CReal.ivtPlateau

Kind: kernel-term
Status: checked

Supports: The family this reduction is about lies INSIDE classical IVT's hypothesis class, machine-checked: uniformly continuous on [0, 1], value <= 0 at the left endpoint, value >= 0 at the right endpoint. Each is a Theorem in the creal prelude with axiom footprint 0.

Checker command

test "$(cargo run -q --release -p axeyum-lean-kernel --example prelude_theorem_inventory -- --include-constructed 2>/dev/null | /usr/bin/grep -cE '^creal[[:space:]]CReal\.ivtPlateau_(nonpos_at_zero|nonneg_at_one|uniformly_continuous)[[:space:]]0[[:space:]]*$')" = 3

Evidence notes

The count is TESTED, not printed: `test ... = 3` fails if any of the three is absent, if one loses its Theorem kind (the inventory lists theorems only), or if any footprint becomes non-zero, since the pattern anchors the third column at 0. The prelude column is anchored to `creal` because the same declarations appear again under `complex` and `cpoint`, which build on it -- an unanchored pattern returns 9 and would keep returning a plausible number if two of the three vanished. Not theorem_dependency_inventory: that tool consumes only its FIRST name argument and silently ignores the rest, measured 2026-08-29, so a three-name invocation reports 1 and looks fine.

nonvacuity-le-total-absent

Kind: instance-pin
Status: checked

Supports: The principle this reduction derives is ABSENT from the environment under four specific hand-written spellings, so the reduction is a boundary rather than a detour. CReal.le_total / CReal.lt_total (and both camelCase spellings) are not declared; the same lookup finds CReal.lt_cotrans, which is. This is NOT an exhaustive-enumeration claim: the check pins the absence of four named instances, not of every possible name a total-order principle over CReal could be given -- a declaration landed as, say, CReal.le_or_le or CReal.sign_cases would not trip this guard. Re-labeled from exhaustive-enumeration on 2026-08-30 (docs/formalized-math-2026-08/08-ivt-and-evt-measured-against-mathlib.md's audit): the CHECK is sound and does what it claims (kernel.environment() enumeration with a same-kind positive control, `creal_tests::ivt_row_two_derives_a_principle_absent_from_the_environment`), the earlier LABEL overstated it.

Checker command

cargo test -p axeyum-lean-kernel --lib creal::creal_tests::ivt_row_two_derives_a_principle_absent_from_the_environment -- --exact

Evidence notes

A reduction to something the kernel already proves is worth nothing, which is why this is part of the row-2 claim and not a preliminary to it -- the same check evt_attained_max_decides_sign's non-vacuity rests on. The test reads display names from kernel.environment() and matches them EXACTLY, not by substring: Rat.le_total and Nat.le_total both exist and a substring match would wrongly report the principle as present. The negative is paired with a positive control of the same declaration kind found by the identical lookup (CReal.lt_cotrans), so a query that has stopped finding anything fails loudly instead of reporting a strong negative. `cargo test` exits non-zero when the test fails; the suite is NOT feature-gated (creal_tests.rs has no `#![cfg(feature ...)]`), so it cannot compile to zero tests, and `--exact` pins that exactly one test runs.

footprint-CReal.ivt_exact_root_decides_sign

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the creal prelude's trusted surface is empty, which bounds CReal.ivt_exact_root_decides_sign.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example nat_axiom_inventory -- --include-constructed --require-axiom-free creal

Evidence notes

--require-axiom-free exits non-zero when the named prelude's trusted surface (Axiom + Opaque + Quotient) is not empty, and errors rather than silently passing for a prelude the run never built. A declaration cannot depend on a trusted declaration the environment does not contain, so an empty creal surface bounds every declaration in it. The per-declaration figure is the footprint column of kernel_declaration_projection, measured 0 for this row and for all six supporting declarations.

Provenance

{
  "date": "2026-08-29",
  "established_by": "lane 249-ivt-row-two; crates/axeyum-lean-kernel/src/creal/ivt_boundary.rs",
  "source": "Authored. The reduction IVT => LLPO via a plateau family is standard constructive analysis (Bishop; Bridges); the family, the interval, the discharge of all three hypotheses and the two-branch cotransitivity proof are this repository's own, built on the model of CReal.evt_attained_max_decides_sign (creal/extreme_value.rs). formal.statement is the verbatim Kernel::render_lean type from kernel_declaration_projection, not hand-transcribed.",
  "prior_art": [
    {
      "who": "Errett Bishop and Douglas Bridges",
      "what": "That the classical Intermediate Value Theorem implies a limited omniscience principle, exhibited by a piecewise-linear family with a plateau at height v, and is therefore not constructively provable.",
      "where": "Constructive Analysis, Grundlehren der mathematischen Wissenschaften 279, ch. 2; and Bridges & Richman, Varieties of Constructive Mathematics, ch. 1",
      "year": 1985,
      "attribution": "standard textbook attribution; this lane did not consult the primary sources. The specific family used here (min x (max (x-1) v) on [0,1]) is a reparameterisation chosen so that both endpoint conditions fall out of the lattice's universal properties with no case split, and is not claimed to be verbatim any published one."
    }
  ]
}