The defining modulus-of-continuity property of CReal.HasDerivativeOn

Identifier: F:creal-hasderivativeon-spec
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Unfolds CReal.HasDerivativeOn f f' a b: given the derivative witness and a precision level n, any two points c, d in [a, b] within the stated modulus of each other make the linear-approximation error at c against the tangent at d bounded by 1/n times |c - d|.

Formal statement

theorem CReal.HasDerivativeOn.spec : ((x0 : ((x0 : CReal) -> CReal)) -> ((x1 : ((x1 : CReal) -> CReal)) -> ((x2 : CReal) -> ((x3 : CReal) -> ((x4 : CReal.HasDerivativeOn x0 x1 x2 x3) -> ((x5 : AxNat) -> ((x6 : CReal) -> ((x7 : CReal) -> ((x8 : CReal.le x2 x6) -> ((x9 : CReal.le x6 x3) -> ((x10 : CReal.le x2 x7) -> ((x11 : CReal.le x7 x3) -> ((x12 : CReal.le (CReal.abs (CReal.add x7 (CReal.neg x6))) (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) (CReal.HasDerivativeOn.modulus x0 x1 x2 x3 x4 x5)))) -> CReal.le (CReal.abs (CReal.add (CReal.add (x0 x7) (CReal.neg (x0 x6))) (CReal.neg (CReal.mul (x1 x6) (CReal.add x7 (CReal.neg x6)))))) (CReal.mul (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) x5)) (CReal.abs (CReal.add x7 (CReal.neg x6)))))))))))))))))

Dependencies

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

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

Evidence

kernel-CReal.HasDerivativeOn.spec

Kind: kernel-term
Status: checked

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

Evidence notes

`build_creal_prelude` admits CReal.HasDerivativeOn.spec through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type, so a line in this tool's output for the exact name is a machine-checked proof having been admitted. `theorem_dependency_inventory` builds creal/complex/cpoint in one run; it exits non-zero for a named filter that matches nothing, and `grep -c` (never `-q`) independently asserts the exact tab-anchored line is present. `--release` is MANDATORY: building the constructed carriers recurses deep enough in a debug build to overflow the default thread stack (measured on this tree: release exits 0, debug SIGABRTs at 134).

footprint-CReal.HasDerivativeOn.spec

Kind: exhaustive-enumeration
Status: checked

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

Checker command

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

Evidence notes

`nat_axiom_inventory --include-constructed --require-axiom-free creal` builds the creal environment as its own group and reports `creal: axiom=0 opaque=0 quotient=0 total_trusted=0` (re-measured on this tree), covering Axiom, Opaque AND Quotient, not just Declaration::Axiom -- this bounds every individual creal theorem's footprint by []. `--include-constructed` is REQUIRED: without it the command exits 1 naming `creal` as known but not built this run rather than a silent pass, which is the standing trap of an empty/absent result reading as a strong negative when the tool was never pointed at the subject. `nat_axiom_inventory` now covers `cpoint` directly (re-verified on this tree: `--require-axiom-free cpoint` exits 0 with `cpoint: axiom=0 opaque=0 quotient=0 total_trusted=0`), so the footprint_closure_audit fallback some earlier CPoint facts used is not needed here. `--release` is MANDATORY for the same deep-recursion reason as `theorem_dependency_inventory` (measured on this tree: debug SIGABRTs at 134).

Provenance

{
  "date": "2026-08-25",
  "established_by": "axeyum-lean-kernel build_creal_prelude",
  "source": "theorem name and dependency edges from theorem_dependency_inventory (builds creal/complex/cpoint); canonical type and top-level binder arity read via a standalone probe binary depending on axeyum-lean-kernel by path, calling only its public Kernel API (environment(), display_name(), render_lean(), axiom_footprint(), expr_node()) -- no in-tree example prints Complex/CPoint theorem types; crates/ source was not touched to produce this batch; the probe was built and run in the session scratchpad and deleted after use."
}