CReal.supOn_approx_lub: the approximate least-upper-bound law -- supOn is approached to any requested accuracy

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

Recorded description

For a uniformly continuous F on [a, b] (a <= b) and any accuracy index e, there is a point x in [a, b] with CReal.supOn F a b <= F x + 1/(e+1). This is the constructive least-upper-bound half of what characterizes CReal.supOn as a supremum (the other half is CReal.supOn_ub). It must stay approximate: CReal.evt_attained_max_decides_sign proves an EXACT attaining maximiser (supOn F a b = F x for some x, no epsilon) would decide the sign of an arbitrary real, which this development refuses to assume decidable.

Formal statement

theorem CReal.supOn_approx_lub : ((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) (CReal.le (CReal.supOn x0 x1 x2 x3 x4) (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.

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

Evidence

kernel-CReal.supOn_approx_lub

Kind: kernel-term
Status: checked

Supports: CReal.supOn_approx_lub 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.supOn_approx_lub 2>/dev/null | grep -cE '^CReal\.supOn_approx_lub[[: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. ADR-0692 confirmed this exact declaration present under this exact name in its own re-derivation; what was missing was a ledger entry, not the theorem.

footprint-CReal.supOn_approx_lub

Kind: exhaustive-enumeration
Status: checked

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

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'. --release is MANDATORY here.

Provenance

{
  "date": "2026-08-30",
  "established_by": "axeyum-lean-kernel build_creal_prelude (crates/axeyum-lean-kernel/src/creal/sup_laws.rs, declare_sup_on_approx_lub)",
  "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."
}