Fundamental theorem of calculus, part I, for a uniformly continuous integrand

Identifier: F:creal-hasderivative-antiderivative-of-uc
Proof route: kernel-lean
External status: Not recorded
Axiom footprint: Empty

Recorded description

THE FUNDAMENTAL THEOREM OF CALCULUS, PART I, in the form a textbook states it. For F uniformly continuous on the closed interval [a, b] of the constructive reals, the function G(x) = the integral of F from a to the clamped x has derivative F on [a, b], in Bishop's UNIFORM sense: CReal.HasDerivativeOn carries an explicit modulus as a data field, not an existential, and the modulus here is E |-> (modulus of uniform continuity of F)(2E + 1) -- two halves of 1/(2E+2) summing to the 1/(E+1) the specification asks for. NO side condition beyond uniform continuity: the (kb : Nat) and BoundedOn F a b kb that CReal.hasDerivative_antiderivative demands of its caller are discharged here from the uniform-continuity witness, because CReal.bounded_of_uniformly_continuous COMPUTES such a kb (one Nat expression in F, a, b, u) with no Exists-elimination. Nothing about the estimate is re-proved: the proof term IS that theorem applied.

Formal statement

theorem CReal.hasDerivative_antiderivative_of_uc : ((x0 : ((x0 : CReal) -> CReal)) -> ((x1 : CReal) -> ((x2 : CReal) -> ((x3 : CReal.le x1 x2) -> ((x4 : CReal.UniformlyContinuousOn x0 x1 x2) -> CReal.HasDerivativeOn (CReal.antiderivative x0 x1 x2 x3 x4) x0 x1 x2)))))

Dependencies

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

2 direct dependencies 0 direct dependents

Evidence

kernel-CReal.hasDerivative_antiderivative_of_uc

Kind: kernel-term
Status: checked

Supports: CReal.hasDerivative_antiderivative_of_uc 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.hasDerivative_antiderivative_of_uc 2>/dev/null | grep -cE '^CReal\.hasDerivative_antiderivative_of_uc[[: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 a backslash-t -- in a scripted (GNU) grep that 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.

footprint-CReal.hasDerivative_antiderivative_of_uc

Kind: exhaustive-enumeration
Status: checked

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

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. Measured 2026-09-04: 'ok: creal trusted surface = 0'. The per-declaration figure is the footprint column of kernel_declaration_projection, measured 0 for this row the same day.

test-CReal.hasDerivative_antiderivative_of_uc-no-bound

Kind: instance-pin
Status: checked

Supports: The theorem applies at fully symbolic F, a, b, hab, u with NO BoundedOn witness anywhere in the local context -- which is the entire content of this fact over CReal.hasDerivative_antiderivative.

Checker command

RUST_MIN_STACK=1073741824 cargo test --release -p axeyum-lean-kernel --lib -- ftc_of_uc --test-threads=4 2>&1 | grep -cE '^test result: ok[.] 1 passed'

Evidence notes

Mutation-verified 2026-09-04 against the full creal:: suite (230 tests). Mutant M1 restores the (kb : Nat) + BoundedOn binders to this declaration: 229 passed, 1 failed, and the one failure is this test. Nothing else in the suite moves, so this test is the only guard on the fact's content. The test also carries a negative control -- the derivative replaced by CReal.neg, a Const against an FVar so def_eq fails immediately -- which the kernel must reject.

Provenance

{
  "date": "2026-09-04",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_creal_prelude, step integral::declare_ftc_of_uc (crates/axeyum-lean-kernel/src/creal/integral.rs)",
  "source": "Hand-written by lane ftc (roadmap W1-2, ADR-1597). formal.statement is the final field of this declaration's row in the unfiltered emit of `cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection`, transcribed verbatim; axiom_footprint is that row's footprint column, cross-checked by the whole-prelude nat_axiom_inventory run in the second evidence row. The prose in `statement` and `notes` is authored, not generated."
}