A shared mid-anchor sample index turns two independent closeness bounds into one, with the index left free

Identifier: F:creal-riemannsum-sharedaccuracyclose-at
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For x, y1, y2 : CReal, rate functions bound1, bound2 : Nat -> Rat, and a shared mid-anchor index l: if x-y1 is Within bound1(i) at every sample index i, and x-y2 is Within bound2(i) at every sample index i, then for ANY sample indices oi, oj, jj1, jj2, y1-y2 (sampled at oi and oj respectively) is Within an explicit combined bound built from bound1(jj1), bound2(jj2) and l. Unlike the derived CRealPrelude::riemann_sum_shared_accuracy_close (which picks l and the two closeness hypotheses internally from a common Cauchy-modulus refinement), l and the two hypotheses h1/h2 here are genuinely free Pi-bound parameters -- this is the level-of-generality upgrade this batch's kernel exposes, letting a caller supply its own mid-anchor and its own per-side bound functions directly.

Formal statement

theorem CReal.riemannSum_sharedAccuracyClose_at : ((x0 : CReal) -> ((x1 : CReal) -> ((x2 : CReal) -> ((x3 : ((x3 : AxNat) -> Rat)) -> ((x4 : ((x4 : AxNat) -> Rat)) -> ((x5 : AxNat) -> ((x6 : ((x6 : AxNat) -> CReal.Within (CReal.seq (CReal.add x0 (CReal.neg x1)) x6) (x3 x6))) -> ((x7 : ((x7 : AxNat) -> CReal.Within (CReal.seq (CReal.add x0 (CReal.neg x2)) x7) (x4 x7))) -> ((x8 : AxNat) -> ((x9 : AxNat) -> ((x10 : AxNat) -> ((x11 : AxNat) -> CReal.Within (Rat.sub (CReal.seq x1 x8) (CReal.seq x2 x9)) (Rat.add (Rat.add (Rat.add (Rat.add (Rat.natDivSucc (AxNat.succ AxNat.zero) x5) (Rat.natDivSucc (AxNat.succ AxNat.zero) (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x10)))) (x3 x10)) (Rat.add (Rat.natDivSucc (AxNat.succ AxNat.zero) (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x10))) (Rat.natDivSucc (AxNat.succ AxNat.zero) x8))) (Rat.add (Rat.add (Rat.add (Rat.natDivSucc (AxNat.succ AxNat.zero) x5) (Rat.natDivSucc (AxNat.succ AxNat.zero) (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x11)))) (x4 x11)) (Rat.add (Rat.natDivSucc (AxNat.succ AxNat.zero) (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x11))) (Rat.natDivSucc (AxNat.succ AxNat.zero) x9))))))))))))))))

Dependencies

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

5 direct dependencies 0 direct dependents

Evidence

kernel-CReal.riemannSum_sharedAccuracyClose_at

Kind: kernel-term
Status: checked

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

Evidence notes

build_creal_prelude admits CReal.riemannSum_sharedAccuracyClose_at 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. Verified with /usr/bin/grep directly (not the ugrep-backed interactive `grep` function) against a freshly built --release binary on this tree, returning count 1. --release is MANDATORY: this tool also builds creal/complex/cpoint, which overflow the default debug thread stack.

footprint-CReal.riemannSum_sharedAccuracyClose_at

Kind: exhaustive-enumeration
Status: checked

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

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.riemannSum_sharedAccuracyClose_at, 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/integral.rs, declare_riemann_sum_shared_accuracy_close_at)",
  "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()). That output was piped to a scratchpad file and the exact row for this declaration's creal prelude row 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 (second-to-last field) and matched against the ledger's own registered facts (by parsing each candidate fact's formal.statement for its declared theorem/def name) to populate depends_on. No new probe binary was written for this batch; crates/ source was not touched to produce this batch."
}