Closeness at an arbitrary shared index implies closeness at the canonical Cauchy index

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

Recorded description

If two CReal values x, y are Equiv-witnessed by a bound function e (x - y is Within (e n) at every index n), then for ANY three indices m1, m2, m3, the raw samples x[m1] and y[m2] are within the canonical CReal.Cauchy bound built from m3 and e(m3). This is the general representative-index bridge Chapter 13's common-refinement construction needs: arbitrary shared-index closeness implies own-canonical-index closeness, stated generically in the two sequences and the bound function rather than specifically for riemannSum.

Formal statement

theorem CReal.sharedIndexToCanonical : ((x0 : CReal) -> ((x1 : CReal) -> ((x2 : ((x2 : AxNat) -> Rat)) -> ((x3 : ((x3 : AxNat) -> CReal.Within (CReal.seq (CReal.add x0 (CReal.neg x1)) x3) (x2 x3))) -> ((x4 : AxNat) -> ((x5 : AxNat) -> ((x6 : AxNat) -> CReal.Within (Rat.sub (CReal.seq x0 x4) (CReal.seq x1 x5)) (Rat.add (Rat.add (Rat.add (Rat.natDivSucc (AxNat.succ AxNat.zero) x4) (Rat.natDivSucc (AxNat.succ AxNat.zero) (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x6)))) (x2 x6)) (Rat.add (Rat.natDivSucc (AxNat.succ AxNat.zero) (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x6))) (Rat.natDivSucc (AxNat.succ AxNat.zero) x5))))))))))

Dependencies

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

3 direct dependencies 8 direct dependents

Evidence

kernel-CReal.sharedIndexToCanonical

Kind: kernel-term
Status: checked

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

Evidence notes

build_creal_prelude admits CReal.sharedIndexToCanonical through the trusted Kernel::add_declaration gate. theorem_dependency_inventory exits non-zero for a named filter matching nothing; grep -c (never -q) asserts the exact tab-anchored line. Mutation-tested on an isolated /data0 snapshot: renaming the display string from "sharedIndexToCanonical" to "sharedIndexToCanonical_MUTATED" at crates/axeyum-lean-kernel/src/creal.rs:4380 makes this exact grep return 0 matches (exit 1) in the rebuilt binary, while unrelated control names (CReal.integral_const, CReal.integral_add) in the SAME rebuild still matched. --release is MANDATORY: this tool also builds creal/complex/cpoint, which overflow the default debug thread stack.

footprint-CReal.sharedIndexToCanonical

Kind: exhaustive-enumeration
Status: checked

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

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'. --require-axiom-free <name> errors for a prelude never built by this run rather than silently passing on zero rows. --release is MANDATORY: --include-constructed builds creal/complex/cpoint and this example has no deep-stack worker.

Provenance

{
  "date": "2026-08-27",
  "established_by": "axeyum-lean-kernel build_creal_prelude (crates/axeyum-lean-kernel/src/creal/integral.rs, declare_shared_index_to_canonical)",
  "source": "theorem name and canonical type read via a standalone probe binary depending on axeyum-lean-kernel by path, calling only its public Kernel API -- no in-tree example prints this theorem's own type. Direct dependency edges cross-checked against theorem_dependency_inventory's own output on the same tree. The probe was built and run in the session scratchpad and deleted after use; crates/ source was not touched to produce this batch."
}