Fundamental theorem of calculus, part II (evaluation rule), for a uniformly continuous integrand

Identifier: F:creal-integral-eq-antideriv-diff-of-uc
Proof route: kernel-lean
External status: Not recorded
Axiom footprint: Empty

Recorded description

THE FUNDAMENTAL THEOREM OF CALCULUS, PART II -- THE EVALUATION RULE -- in the form a textbook states it: if G has derivative F on [a, b] (uniformly, in Bishop's sense) and F is uniformly continuous there, then the integral of F over [a, b] is equivalent to G(b) - G(a). The conclusion is CReal.Equiv, the Bishop-setoid equality on regular sequences, not Eq. G is ANY antiderivative, not the canonical CReal.antiderivative. NO side condition beyond uniform continuity: the (kb : Nat) and BoundedOn F a b kb that CReal.integral_eq_antideriv_diff demands of its caller are discharged from the uniform-continuity witness via CReal.bounded_of_uniformly_continuous, whose kb is COMPUTED, not obtained by Exists-elimination.

Formal statement

theorem CReal.integral_eq_antideriv_diff_of_uc : ((x0 : ((x0 : CReal) -> CReal)) -> ((x1 : ((x1 : CReal) -> CReal)) -> ((x2 : CReal) -> ((x3 : CReal) -> ((x4 : CReal.le x2 x3) -> ((x5 : CReal.UniformlyContinuousOn x0 x2 x3) -> ((x6 : CReal.HasDerivativeOn x1 x0 x2 x3) -> CReal.Equiv (CReal.integral x0 x2 x3 x4 x5) (CReal.add (x1 x3) (CReal.neg (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.integral_eq_antideriv_diff_of_uc

Kind: kernel-term
Status: checked

Supports: CReal.integral_eq_antideriv_diff_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.integral_eq_antideriv_diff_of_uc 2>/dev/null | grep -cE '^CReal\.integral_eq_antideriv_diff_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.integral_eq_antideriv_diff_of_uc

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the creal prelude's trusted surface is empty, which bounds CReal.integral_eq_antideriv_diff_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.integral_eq_antideriv_diff_of_uc-no-bound

Kind: instance-pin
Status: checked

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

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 M2 restores the (kb : Nat) + BoundedOn binders to this declaration: 229 passed, 1 failed, and the one failure is this test. The test's negative control for this direction states the evaluation term as G a - G b instead of G b - G a, which at F := id on [0, 1] asserts 1/2 = -1/2; the kernel must reject it.

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."
}