crossingClose: f(sampled crossing point) is close to f(c) -- STATED with two UNDISCHARGED hypotheses

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

Recorded description

For F uniformly continuous on [a,b], delta > 0, e : Nat, a <= c <= b: GIVEN also the two hypotheses hap : a <= samplePt and hpb : samplePt <= b (samplePt being the bucket-index-sampled point a + bucketIndex(...)*delta), and given the two Archimedean slack bounds, then |F(c) - F(samplePt)| <= 1/(e+1). This kernel does NOT discharge hap/hpb for any concrete delta or mesh count -- they are explicit hypotheses of the theorem's own statement, not derived facts -- and a lane proved by arithmetic that the existing generic bucket_index_bound (a +3 clamp) is too lossy to supply them at any mesh fineness. This fact is registered as what the theorem STATES; it should NOT be treated as a usable closed result until hap/hpb are separately discharged.

Formal statement

theorem CReal.crossingClose : ((x0 : ((x0 : CReal) -> CReal)) -> ((x1 : CReal) -> ((x2 : CReal) -> ((x3 : CReal) -> ((x4 : Rat) -> ((x5 : AxNat) -> ((x6 : CReal.UniformlyContinuousOn x0 x1 x2) -> ((x7 : Rat.lt Rat.zero x4) -> ((x8 : CReal.le x1 x3) -> ((x9 : CReal.le x3 x2) -> ((x10 : CReal.le x1 (CReal.add x1 (CReal.mul (CReal.ofNat (CReal.bucketIndex (CReal.mul (CReal.ofRat (Rat.inv x4)) (CReal.add x3 (CReal.neg x1))) AxNat.zero)) (CReal.ofRat x4)))) -> ((x11 : CReal.le (CReal.add x1 (CReal.mul (CReal.ofNat (CReal.bucketIndex (CReal.mul (CReal.ofRat (Rat.inv x4)) (CReal.add x3 (CReal.neg x1))) AxNat.zero)) (CReal.ofRat x4))) x2) -> ((x12 : CReal.le (CReal.add (CReal.ofRat x4) (CReal.mul (CReal.ofRat x4) (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 x6 x5)))) -> ((x13 : CReal.le (CReal.neg (CReal.mul (CReal.ofRat x4) (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 x6 x5)))) -> CReal.le (CReal.abs (CReal.add (x0 x3) (CReal.neg (x0 (CReal.add x1 (CReal.mul (CReal.ofNat (CReal.bucketIndex (CReal.mul (CReal.ofRat (Rat.inv x4)) (CReal.add x3 (CReal.neg x1))) AxNat.zero)) (CReal.ofRat x4))))))) (CReal.ofRat (Rat.natDivSucc (AxNat.succ AxNat.zero) x5))))))))))))))))

Dependencies

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

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

Evidence

kernel-CReal.crossingClose

Kind: kernel-term
Status: checked

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

Evidence notes

The producing prelude admits CReal.crossingClose through the trusted Kernel::add_declaration gate, which re-checks the proof term against the stated type. theorem_dependency_inventory exits non-zero for a named filter matching nothing (a deleted/renamed theorem cannot read as a re-derived one), and grep -c (never -q) both avoids a SIGPIPE-under-pipefail false negative and independently 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.

footprint-CReal.crossingClose

Kind: exhaustive-enumeration
Status: checked

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

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.crossingClose, 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_close)",
  "source": "theorem name, canonical type and direct dependency edges read via theorem_dependency_inventory's own per-name output (cargo run -q --release -p axeyum-lean-kernel --example theorem_dependency_inventory -- <Name>), which prints '<Name>\\t<comma-separated direct deps>'; the canonical type itself was cross-extracted from kernel_declaration_projection's unfiltered TSV dump the same way as the Definition facts in this batch, and confirmed byte-for-byte identical between the two tools' output for every name in this batch. crates/ source was not touched to produce this batch."
}