The crossing-close bound restated at an ordinary Riemann-sum sample point

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

Recorded description

CReal.crossingCloseClamped (this batch) specialized at c := ptI, where ptI := a + ofNat(i)*stepAb is an ORDINARY Riemann-sum sample point (stepAb an arbitrary CReal, not necessarily riemannSum's own mesh step): given F uniformly continuous on [a,b], 0 < deltaAc, a <= ptI <= b, and the two crossing slacks already within the continuity modulus, |F(ptI) - F(clampedPt)| <= 1/e, clampedPt at c := ptI, delta := deltaAc. This is integral.rs's SEVENTH 2026-08-27 module-doc-proposed term-pairing lemma, RESTRICTED to the one case that type-checks against this file's existing machinery: crossingIndex (hence crossingCloseClamped) takes its step as a Rat, not a CReal, so this theorem is only usable when the caller already has a rational deltaAc in hand (e.g. c := a + ofRat q for some Rat q), not for a fully general CReal split point c -- extending to that general case needs a CReal-level inverse construction this prelude does not yet wire up (see the field doc for the exact obstruction: crossing.rs's internal recipe is hard-wired to Rat.inv).

Formal statement

theorem CReal.riemannSampleCrossingClose : ((x0 : ((x0 : CReal) -> CReal)) -> ((x1 : CReal) -> ((x2 : CReal) -> ((x3 : CReal.UniformlyContinuousOn x0 x1 x2) -> ((x4 : CReal) -> ((x5 : AxNat) -> ((x6 : Rat) -> ((x7 : AxNat) -> ((x8 : Rat.lt Rat.zero x6) -> ((x9 : CReal.le x1 (CReal.add x1 (CReal.mul (CReal.ofNat x5) x4))) -> ((x10 : CReal.le (CReal.add x1 (CReal.mul (CReal.ofNat x5) x4)) x2) -> ((x11 : CReal.le (CReal.add (CReal.ofRat x6) (CReal.mul (CReal.ofRat x6) (CReal.ofRat (Rat.natDivSucc (AxNat.succ (AxNat.succ AxNat.zero)) (AxNat.mul (AxNat.succ AxNat.zero) (AxNat.succ AxNat.zero)))))) (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) (CReal.UniformlyContinuousOn.modulus x0 x1 x2 x3 x7)))) -> ((x12 : CReal.le (CReal.neg (CReal.mul (CReal.ofRat x6) (CReal.ofRat (Rat.neg (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.mul (AxNat.succ AxNat.zero) (AxNat.succ AxNat.zero))))))) (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) (CReal.UniformlyContinuousOn.modulus x0 x1 x2 x3 x7)))) -> CReal.le (CReal.abs (CReal.add (x0 (CReal.add x1 (CReal.mul (CReal.ofNat x5) x4))) (CReal.neg (x0 (CReal.min (CReal.add x1 (CReal.mul (CReal.ofNat (CReal.bucketIndex (CReal.mul (CReal.ofRat (Rat.inv x6)) (CReal.add (CReal.add x1 (CReal.mul (CReal.ofNat x5) x4)) (CReal.neg x1))) AxNat.zero)) (CReal.ofRat x6))) x2))))) (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) x7)))))))))))))))

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

kernel-CReal.riemannSampleCrossingClose

Kind: kernel-term
Status: checked

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

Evidence notes

build_creal_prelude admits CReal.riemannSampleCrossingClose through the trusted Kernel::add_declaration gate. theorem_dependency_inventory exits non-zero for a named filter matching nothing; grep -c asserts the exact tab-anchored line. --release is MANDATORY: this tool also builds creal/complex/cpoint, which overflow the default debug thread stack.

footprint-CReal.riemannSampleCrossingClose

Kind: exhaustive-enumeration
Status: checked

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

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'. That bounds every declaration in the creal environment, including CReal.riemannSampleCrossingClose, since a declaration cannot depend on a trusted declaration the environment does not contain. --require-axiom-free <name> errors for a prelude never built by this run rather than silently passing on zero rows. --release is MANDATORY here.

Provenance

{
  "date": "2026-08-27",
  "established_by": "axeyum-lean-kernel build_creal_prelude (crates/axeyum-lean-kernel/src/creal/crossing.rs, declare_crossing_sample_pairing_close)",
  "source": "canonical type read via kernel_declaration_projection's own UNFILTERED emit mode (cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection, no --require-declaration flag), which prints, per constructed prelude, one TSV row per declaration whose last field is kernel.render_lean(declaration.ty()) -- the same Kernel::render_lean canonical form nat_theorem_inventory prints, just not filtered to Declaration::Theorem. That output was piped to a scratchpad file and the exact row for this declaration's own prelude label was extracted and injected here programmatically (a Python script reading the TSV, never hand-transcribed); direct theorem dependencies were cross-read from the same run's direct_theorems column (field 6) and matched against the ledger's own registered kernel_theorem/formal.statement names to populate depends_on. No new probe binary was written for this batch; crates/ source was not touched to produce this batch."
}