CReal.evt_attained_max_decides_sign: an attained maximiser for a linear family decides the sign of an arbitrary real

Identifier: F:creal-evt-attained-max-decides-sign
Proof route: kernel-lean
External status: Not recorded
Axiom footprint: Empty

Recorded description

CReal.evt_attained_max_decides_sign is the Extreme Value Theorem's ADR-0603 row 2, mirroring CReal.ivt_exact_root_decides_sign. Let v be an arbitrary real and consider the family CReal.evtLinear v := fun t => mul t v on [0, 1]. If some c in [0, 1] attains the maximum of this family over [0, 1] (mul t v <= mul c v for every t in [0, 1]), then v <= 0 or 0 <= v -- again analytic LLPO. So an operator that produces an ATTAINING maximiser for every uniformly continuous function on a closed interval -- the classical Extreme Value Theorem's conclusion -- is at least as strong as a principle this kernel's order does not have; the conclusion is UNPROVABLE here, not refuted, since it is consistent with Bishop's constructive mathematics. Non-vacuity, in both senses IVT's row 2 checks for, is now evidenced IN THIS LEDGER (2026-08-31, lane evt-row2-nonvacuity, closing docs/formalized-math-2026-08/08-ivt-and-evt-measured-against-mathlib.md's item-3 gap): (1) the maximality hypothesis is non-vacuously satisfiable -- exhibited at TWO structurally different witnesses, (v,c) = (1,1) and (v,c) = (0,0), each a genuine kernel proof term the theorem accepts (evidence id hypothesis-class-satisfiable-evt; also see creal_tests::evt_linear_endpoint_values_reduce_and_flip_with_the_sign_of_v, which shows by reduction that evtLinear's two endpoint values swap dominance as the sign of v flips, so the maximiser genuinely moves); (2) the classical conclusion this theorem reduces to -- analytic LLPO -- is itself absent from the environment under the same four names CReal.ivt_exact_root_decides_sign's fact checks, now asserted against THIS declaration by its own dedicated test rather than only by citation (evidence id nonvacuity-le-total-absent-evt, creal_tests::evt_row_two_derives_a_principle_absent_from_the_environment). What this fact still does NOT supply, and this is the substantive remaining gap: ANY positive constructive substitute for EVT's classical conclusion (an attaining maximiser). Unlike IVT's exact-root theorem, no operator here PRODUCES an attaining c; F:creal-evt-approx-max supplies the approximate row-1 substitute (an epsilon-maximiser for every n), which is the honest positive content available, not an attaining one. This fact remains a refutation of the classical conclusion; it is evidence that the refutation is non-vacuous, not evidence that EVT's classical conclusion has been given a constructive treatment here.

Formal statement

theorem CReal.evt_attained_max_decides_sign : ((x0 : CReal) -> ((x1 : CReal) -> ((x2 : CReal.le CReal.zero x1) -> ((x3 : CReal.le x1 CReal.one) -> ((x4 : ((x4 : CReal) -> ((x5 : CReal.le CReal.zero x4) -> ((x6 : CReal.le x4 CReal.one) -> CReal.le (CReal.mul x4 x0) (CReal.mul x1 x0))))) -> 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.

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

Evidence

kernel-CReal.evt_attained_max_decides_sign

Kind: kernel-term
Status: checked

Supports: CReal.evt_attained_max_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.evt_attained_max_decides_sign 2>/dev/null | grep -cE '^CReal\.evt_attained_max_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. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. --release is MANDATORY: this tool builds creal/complex/cpoint, which overflow the default debug thread stack.

nonvacuity-le-total-absent-evt

Kind: instance-pin
Status: checked

Supports: The principle this reduction derives -- analytic LLPO, `Or (le v zero) (le zero v)` for an arbitrary v -- is ABSENT from the environment under four 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 closes the gap docs/formalized-math-2026-08/08-ivt-and-evt-measured-against-mathlib.md flagged: the check `CReal.ivt_exact_root_decides_sign`'s own fact carries (`F:creal-ivt-exact-root-decides-sign`'s `nonvacuity-le-total-absent` evidence row) applies mathematically to this theorem too -- the two theorems render an IDENTICAL conclusion type -- but until this row was added nothing in this fact's own evidence asserted it against `CReal.evt_attained_max_decides_sign` by name. `creal_tests::evt_row_two_derives_a_principle_absent_from_the_environment` is a dedicated mirror of the IVT test rather than a bare citation, so it independently re-derives the Theorem-kind and empty-axiom-footprint guards for THIS declaration as well.

Checker command

cargo test -p axeyum-lean-kernel --lib creal::creal_tests::evt_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 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. BREAK/RESTORE proof, done in a scripts/lane-snapshot.sh scratch copy, never in the tracked file: mutating one of the four `absent` names to `CReal.lt_cotrans` (a declaration certainly present) makes the run FAIL with exit 101 and the exact panic message naming the mutated string, confirming the exit status depends on the finding rather than on the run completing; reverting restores the clean pass.

hypothesis-class-satisfiable-evt

Kind: instance-pin
Status: checked

Supports: The maximality hypothesis `forall t, le zero t -> le t one -> le (mul t v) (mul c v)` is non-vacuously satisfiable, exhibited by two structurally different concrete witnesses rather than one, so the check cannot be passing merely because it found one degenerate corner: (v, c) = (1, 1), the genuine argmax when v >= 0 (t = 1 strictly dominates every other t in [0,1]); and (v, c) = (0, 0), where the maximiser is non-unique (every t attains the maximum of the constant-zero family) and c = 1 from the first case would NOT satisfy the hypothesis. Both tests build a real kernel proof term for the discharged hypothesis (via mul_one / mul_zero / le_congr, not an assumption or an axiom) and require `Kernel::infer` to accept CReal.evt_attained_max_decides_sign applied to it, then pin the resulting conclusion type VERBATIM against an independently constructed `Or (le v zero) (le zero v)` at that v -- so a theorem that concluded some other disjunction, or that silently accepted an ill-typed hypothesis, cannot pass. This is the specific gap the fact's own `statement` field named before this evidence row existed: the discharge was checked in creal_tests.rs (also see evt_linear_endpoint_values_reduce_and_flip_with_the_sign_of_v, which shows by kernel REDUCTION -- not proof-term construction -- that evtLinear's two endpoint values swap dominance as the sign of v flips, i.e. that the maximiser genuinely MOVES and the row-2 theorem is deciding something real) but no evidence entry here cited it.

Checker command

test "$(cargo test -p axeyum-lean-kernel --lib creal::creal_tests::evt_attained_max_hypothesis_is_satisfiable 2>&1 | /usr/bin/grep -cE '^test result: ok\. 2 passed; 0 failed')" -ge 1

Evidence notes

The filter `creal::creal_tests::evt_attained_max_hypothesis_is_satisfiable` matches exactly two test names in the tree (evt_attained_max_hypothesis_is_satisfiable_at_v_one_c_one, _at_v_zero_c_zero; confirmed by grep before this checker was written) and no others, so it cannot silently run zero or a smaller subset -- the pinned `2 passed; 0 failed` in the grep pattern is what guards against the `cargo test --lib` zero-tests-matched trap this ledger has been burned by before (a typo'd or renamed filter prints `test result: ok. 0 passed; 0 failed` and exits 0; the pinned count fails to match that string, so `test ... -ge 1` fails). Verified against a deliberately misspelled filter (`..._satisfiable_WRONG_NAME`): `running 0 tests`, `0 passed; 0 failed`, exit 0 from cargo itself, but this checker's grep count is 0 and the `test -ge 1` wrapper exits 1. BREAK/RESTORE proof, done in a scratch snapshot: swapping the (hc0, hc1) argument order in the v=1,c=1 instance -- so the term passed for `le zero c` is actually a proof of `le c one` and vice versa -- makes `Kernel::infer` return a `TypeMismatch` and the test's `.unwrap_or_else` panic fires, exit 101; reverting restores the clean 2-passed run. This also answers the two questions CLAUDE.md requires for a non-vacuity check: not vacuous (the mutation above makes it fail, so it is not a control that always passes), and not inverted (the witness genuinely discharges the theorem's actual hypothesis type, checked by the kernel's own type checker rather than asserted).

footprint-CReal.evt_attained_max_decides_sign

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the creal prelude's trusted surface is empty, which bounds CReal.evt_attained_max_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, including CReal.evt_attained_max_decides_sign. This is a whole-prelude bound, not a per-declaration measurement; the per-declaration figure is the footprint column of kernel_declaration_projection, measured 0 for this row.

Provenance

{
  "date": "2026-08-27",
  "curation": "curated",
  "generated_by": "scripts/gen-kernel-facts.py",
  "established_by": "axeyum-lean-kernel build_creal_prelude (crates/axeyum-lean-kernel/src/creal/)",
  "source": "Derived mechanically from the unfiltered emit of `cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection`, which prints one TSV row per declaration whose fields are (prelude, kind, display name, axiom-footprint size, direct type declarations, direct declarations, direct theorems, Kernel::render_lean(declaration.ty())). formal.statement is that last field verbatim; depends_on is the direct-theorem column intersected with this ledger's registered facts; axiom_footprint is the footprint-size column, cross-checked by the whole-prelude nat_axiom_inventory run recorded in the second evidence row. No field was hand-transcribed and no prose was authored."
}