CReal.evt_approx_max: the Extreme Value Theorem's honest row 1 -- an approximate maximum

Identifier: F:creal-evt-approx-max
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let F be an arbitrary uniformly continuous real function on [a, b] with a <= b. Then for EVERY accuracy index n, there exists x in [a, b] such that for every y in [a, b], F y <= F x + 1/(n+1) -- an APPROXIMATE maximum, exact structural mirror of CReal.ivt_approx (ADR-0603 row 1 for IVT). Pure composition of CReal.supOn_approx_lub (the witness x, within 1/(n+1) of the supremum) and CReal.supOn_ub (every F y is at most the supremum) through CReal.le_trans -- no new supremum machinery. This is NOT an attained maximum and does not narrow CReal.evt_attained_max_decides_sign at all: the witness x moves with n and is never claimed to converge to a limit. F must still be assumed UniformlyContinuousOn [a,b] with an explicit modulus carried as Sort 1 data, the same restriction CReal.ivt_approx and every rung of the supremum construction carries.

Formal statement

theorem CReal.evt_approx_max : ((x0 : ((x0 : CReal) -> CReal)) -> ((x1 : CReal) -> ((x2 : CReal) -> ((x3 : CReal.le x1 x2) -> ((x4 : CReal.UniformlyContinuousOn x0 x1 x2) -> ((x5 : AxNat) -> Exists.{1} CReal (fun (x6 : CReal) => And (CReal.le x1 x6) (And (CReal.le x6 x2) (((x7 : CReal) -> ((x8 : CReal.le x1 x7) -> ((x9 : CReal.le x7 x2) -> CReal.le (x0 x7) (CReal.add (x0 x6) (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) x5)))))))))))))))

Dependencies

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

4 direct dependencies 0 direct dependents

Evidence

kernel-CReal.evt_approx_max

Kind: kernel-term
Status: checked

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

Evidence notes

theorem_dependency_inventory exits non-zero for a named filter matching nothing, and grep -c (never -q under pipefail) both consumes the pipe and asserts the exact tab-anchored line is present. --release is MANDATORY: this tool also builds creal/complex/cpoint, which overflow the default debug thread stack.

footprint-CReal.evt_approx_max

Kind: exhaustive-enumeration
Status: checked

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

Checker command

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

Evidence notes

Re-measured on this tree: creal: axiom=0 opaque=0 quotient=0 total_trusted=0, exits 0 printing 'ok: creal trusted surface = 0'. --require-axiom-free <name> errors for a prelude never built by this run. --release is MANDATORY here.

coverage-CReal.evt_approx_max

Kind: instance-pin
Status: checked

Supports: The declaration is a Theorem with an empty axiom footprint, checked against the ENVIRONMENT rather than a hand-maintained list.

Checker command

cargo test -q -p axeyum-lean-kernel --lib creal::creal_tests::every_creal_declaration_is_checked_and_axiom_free 2>&1 | grep -c '1 passed'

Evidence notes

creal_tests::every_creal_declaration_is_checked_and_axiom_free enumerates kernel.environment() directly and fails naming any CReal-prefixed declaration absent from every inventory shard -- CReal.evt_approx_max is registered in crates/axeyum-lean-kernel/src/creal/inventory/evt_row1.rs, so this test would fail if that registration were ever dropped, unlike a hand list that cannot notice what is missing from it.

Provenance

{
  "date": "2026-08-30",
  "established_by": "axeyum-lean-kernel build_creal_prelude (crates/axeyum-lean-kernel/src/creal/evt_row1.rs, declare_evt_approx_max)",
  "source": "canonical type read via kernel_declaration_projection's own UNFILTERED emit mode on this lane's own worktree build, filtered to the creal-prelude row for this declaration. No field was hand-transcribed from the Rust source."
}