CReal.supOn_ub: the upper-bound law -- supOn dominates F at every point of [a, b]

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

Recorded description

For a uniformly continuous F on [a, b] (a <= b) and any x with a <= x <= b, F x <= CReal.supOn F a b. This is the upper-bound half of what characterizes CReal.supOn as a supremum (the other half is CReal.supOn_approx_lub); together they are what makes it a supremum rather than merely the limit of a sequence of mesh maxima. This law is at an ARBITRARY point of [a, b], not just a mesh-sampled one -- the negative control (transposing the second hypothesis to le b x) is rejected by the kernel, since a point beyond b need not be dominated by the supremum over [a, b].

Formal statement

theorem CReal.supOn_ub : ((x0 : ((x0 : CReal) -> CReal)) -> ((x1 : CReal) -> ((x2 : CReal) -> ((x3 : CReal.le x1 x2) -> ((x4 : CReal.UniformlyContinuousOn x0 x1 x2) -> ((x5 : CReal) -> ((x6 : CReal.le x1 x5) -> ((x7 : CReal.le x5 x2) -> CReal.le (x0 x5) (CReal.supOn x0 x1 x2 x3 x4)))))))))

Dependencies

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

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

Evidence

kernel-CReal.supOn_ub

Kind: kernel-term
Status: checked

Supports: CReal.supOn_ub 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_ub 2>/dev/null | grep -cE '^CReal\.supOn_ub[[: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. This theorem shipped under the name CReal.supOn_ub -- ADR-0692's absence probe searched for the guessed name CReal.supOn_upper_bound and found nothing, which is a different, correct observation about a name that never existed; see ADR-0895.

footprint-CReal.supOn_ub

Kind: exhaustive-enumeration
Status: checked

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

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.

unit-CReal.supOn_ub-not-vacuous

Kind: instance-pin
Status: checked

Supports: The stated type is genuinely the ARBITRARY-point upper-bound law and not a weaker variant -- the negative control (transposing le x b to le b x) is rejected.

Checker command

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

Evidence notes

crates/axeyum-lean-kernel/src/creal/sup_laws.rs's own test rebuilds the expected Pi type independently of the declaring function and asserts the kernel accepts the shipped proof term at the ORIGINAL type and REJECTS it at the transposed one -- a small, one-swap negative control, not a whole-subterm transposition (see CLAUDE.md on the unbounded-failing-defeq pathology a large transposed control can trigger).

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_ub)",
  "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."
}