The Weierstrass M-test: a uniform series bound gives uniform convergence

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

Recorded description

If f : Nat -> CReal -> CReal is a series of functions and mseq : Nat -> CReal dominates it uniformly on [a,b] (|f j pt| <= mseq j for every j and every pt in [a,b]), and the partial sums of mseq are themselves Cauchy at a stated rational rate, then the partial sums of f converge UNIFORMLY on [a,b] to the pointwise limit built at each point. This is Spivak's Weierstrass M-test, and it needs two hypotheses beyond the textbook statement, both mathematically forced by this development's own foundations rather than proof-engineering artifacts: (1) f must respect CReal's Equiv congruence (∀ j p q, Equiv p q -> Equiv (f j p) (f j q)) -- CReal is a Bishop SETOID here (ADR-0512), not a literal quotient, so an arbitrary CReal -> CReal term need not be well-defined on equivalence classes, and without this hypothesis nothing relates f j pt to f j pt' once pt ~ pt' is shown; (2) the limit function G is built at the CLAMPED point max a (min pt b) rather than at pt directly, because CReal.le is not decidable in this development (the standing rule: never branch on it), so there is no way to conjure the domain-membership proof (a <= pt, pt <= b) that the pointwise domination hypothesis needs for an arbitrary symbolic pt. Clamping first is unconditional (max_le + min_le_right give the upper bound from a <= b alone, le_max_left gives the lower bound outright, no case split, no decidability), so G is total by construction; the M-test's conclusion is then transported from the clamped point back to the original one via the Equiv congruence hypothesis.

Formal statement

theorem CReal.weierstrassMTest : ((x0 : ((x0 : AxNat) -> ((x1 : CReal) -> CReal))) -> ((x1 : ((x1 : AxNat) -> CReal)) -> ((x2 : CReal) -> ((x3 : CReal) -> ((x4 : CReal.le x2 x3) -> ((x5 : ((x5 : AxNat) -> ((x6 : CReal) -> ((x7 : CReal) -> ((x8 : CReal.Equiv x6 x7) -> CReal.Equiv (x0 x5 x6) (x0 x5 x7)))))) -> ((x6 : AxNat) -> ((x7 : ((x7 : AxNat) -> ((x8 : CReal) -> ((x9 : CReal.le x2 x8) -> ((x10 : CReal.le x8 x3) -> CReal.le (CReal.abs (x0 x7 x8)) (x1 x7)))))) -> ((x8 : ((x8 : AxNat) -> ((x9 : AxNat) -> CReal.Within (Rat.sub (CReal.seq (CReal.sumRange x1 x8) x8) (CReal.seq (CReal.sumRange x1 x9) x9)) (Rat.add (Rat.natDivSucc x6 x8) (Rat.natDivSucc x6 x9))))) -> CReal.UniformConvergesOn (fun (x9 : AxNat) => fun (x10 : CReal) => CReal.sumRange (fun (x11 : AxNat) => x0 x11 x10) x9) (fun (x9 : CReal) => CReal.mk (CReal.speedup (fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => x0 x11 (CReal.max x2 (CReal.min x9 x3))) x10) x10) (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) (CReal.regular_of_kregular (fun (x10 : AxNat) => CReal.seq (CReal.sumRange (fun (x11 : AxNat) => x0 x11 (CReal.max x2 (CReal.min x9 x3))) x10) x10) (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) (fun (x10 : AxNat) => fun (x11 : AxNat) => And.intro (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) x11))) (Rat.sub ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x10) ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x11))) (Rat.le (Rat.sub ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x10) ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x11)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) x11))) (Rat.le_trans (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) x11))) (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11))) (Rat.sub ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x10) ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x11)) (Rat.neg_le_neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) x11)) (Rat.add_le_add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) x11) (Rat.natDivSucc_le_add_left (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) (AxNat.succ AxNat.zero) x10) (Rat.natDivSucc_le_add_left (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) (AxNat.succ AxNat.zero) x11))) (And.rec.{0} (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11))) (Rat.sub ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x10) ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x11))) (Rat.le (Rat.sub ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x10) ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x11)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11))) (fun (x12 : And (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11))) (Rat.sub ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x10) ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x11))) (Rat.le (Rat.sub ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x10) ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x11)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11)))) => Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11))) (Rat.sub ((fun (x13 : AxNat) => CReal.seq (CReal.sumRange (fun (x14 : AxNat) => x0 x14 (CReal.max x2 (CReal.min x9 x3))) x13) x13) x10) ((fun (x13 : AxNat) => CReal.seq (CReal.sumRange (fun (x14 : AxNat) => x0 x14 (CReal.max x2 (CReal.min x9 x3))) x13) x13) x11))) (fun (x12 : Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11))) (Rat.sub ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x10) ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x11))) => fun (x13 : Rat.le (Rat.sub ((fun (x13 : AxNat) => CReal.seq (CReal.sumRange (fun (x14 : AxNat) => x0 x14 (CReal.max x2 (CReal.min x9 x3))) x13) x13) x10) ((fun (x13 : AxNat) => CReal.seq (CReal.sumRange (fun (x14 : AxNat) => x0 x14 (CReal.max x2 (CReal.min x9 x3))) x13) x13) x11)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11))) => x12) ((fun (x12 : AxNat) => fun (x13 : AxNat) => Or.rec (AxNat.le x12 x13) (AxNat.le x13 x12) (fun (x14 : Or (AxNat.le x12 x13) (AxNat.le x13 x12)) => CReal.Within (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13))) (fun (x14 : AxNat.le x12 x13) => Eq.rec.{0, 1} Rat (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12)) (fun (x15 : Rat) => fun (x16 : Eq.{1} Rat (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12)) x15) => CReal.Within (Rat.sub (CReal.seq (CReal.sumRange (fun (x17 : AxNat) => x0 x17 (CReal.max x2 (CReal.min x9 x3))) x12) x12) (CReal.seq (CReal.sumRange (fun (x17 : AxNat) => x0 x17 (CReal.max x2 (CReal.min x9 x3))) x13) x13)) x15) (Eq.rec.{0, 1} Rat (Rat.neg (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) (fun (x15 : Rat) => fun (x16 : Eq.{1} Rat (Rat.neg (Rat.sub (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) x15) => CReal.Within x15 (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.bounds_neg (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12)) (And.rec.{0} (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (fun (x15 : And (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12)))) => Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) (fun (x15 : Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) => fun (x16 : Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) => x15) (CReal.sumRange_cauchy_dominated_ordered_normalized (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x1 x6 x12 x13 (fun (x15 : AxNat) => x7 x15 (CReal.max x2 (CReal.min x9 x3)) (CReal.le_max_left x2 (CReal.min x9 x3)) (CReal.max_le x2 (CReal.min x9 x3) x3 x4 (CReal.min_le_right x9 x3))) x8 x14)) (And.rec.{0} (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (fun (x15 : And (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12)))) => Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (fun (x15 : Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) => fun (x16 : Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) => x16) (CReal.sumRange_cauchy_dominated_ordered_normalized (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x1 x6 x12 x13 (fun (x15 : AxNat) => x7 x15 (CReal.max x2 (CReal.min x9 x3)) (CReal.le_max_left x2 (CReal.min x9 x3)) (CReal.max_le x2 (CReal.min x9 x3) x3 x4 (CReal.min_le_right x9 x3))) x8 x14))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13)) (Rat.neg_sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13)) (Rat.add_comm (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (fun (x14 : AxNat.le x13 x12) => CReal.sumRange_cauchy_dominated_ordered_normalized (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x1 x6 x13 x12 (fun (x15 : AxNat) => x7 x15 (CReal.max x2 (CReal.min x9 x3)) (CReal.le_max_left x2 (CReal.min x9 x3)) (CReal.max_le x2 (CReal.min x9 x3) x3 x4 (CReal.min_le_right x9 x3))) x8 x14) (AxNat.le_total x12 x13)) x10 x11))) (Rat.le_trans (Rat.sub ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x10) ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x11)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) x11)) (And.rec.{0} (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11))) (Rat.sub ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x10) ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x11))) (Rat.le (Rat.sub ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x10) ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x11)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11))) (fun (x12 : And (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11))) (Rat.sub ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x10) ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x11))) (Rat.le (Rat.sub ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x10) ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x11)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11)))) => Rat.le (Rat.sub ((fun (x13 : AxNat) => CReal.seq (CReal.sumRange (fun (x14 : AxNat) => x0 x14 (CReal.max x2 (CReal.min x9 x3))) x13) x13) x10) ((fun (x13 : AxNat) => CReal.seq (CReal.sumRange (fun (x14 : AxNat) => x0 x14 (CReal.max x2 (CReal.min x9 x3))) x13) x13) x11)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11))) (fun (x12 : Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11))) (Rat.sub ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x10) ((fun (x12 : AxNat) => CReal.seq (CReal.sumRange (fun (x13 : AxNat) => x0 x13 (CReal.max x2 (CReal.min x9 x3))) x12) x12) x11))) => fun (x13 : Rat.le (Rat.sub ((fun (x13 : AxNat) => CReal.seq (CReal.sumRange (fun (x14 : AxNat) => x0 x14 (CReal.max x2 (CReal.min x9 x3))) x13) x13) x10) ((fun (x13 : AxNat) => CReal.seq (CReal.sumRange (fun (x14 : AxNat) => x0 x14 (CReal.max x2 (CReal.min x9 x3))) x13) x13) x11)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11))) => x13) ((fun (x12 : AxNat) => fun (x13 : AxNat) => Or.rec (AxNat.le x12 x13) (AxNat.le x13 x12) (fun (x14 : Or (AxNat.le x12 x13) (AxNat.le x13 x12)) => CReal.Within (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13))) (fun (x14 : AxNat.le x12 x13) => Eq.rec.{0, 1} Rat (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12)) (fun (x15 : Rat) => fun (x16 : Eq.{1} Rat (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12)) x15) => CReal.Within (Rat.sub (CReal.seq (CReal.sumRange (fun (x17 : AxNat) => x0 x17 (CReal.max x2 (CReal.min x9 x3))) x12) x12) (CReal.seq (CReal.sumRange (fun (x17 : AxNat) => x0 x17 (CReal.max x2 (CReal.min x9 x3))) x13) x13)) x15) (Eq.rec.{0, 1} Rat (Rat.neg (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) (fun (x15 : Rat) => fun (x16 : Eq.{1} Rat (Rat.neg (Rat.sub (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) x15) => CReal.Within x15 (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.bounds_neg (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12)) (And.rec.{0} (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (fun (x15 : And (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12)))) => Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) (fun (x15 : Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) => fun (x16 : Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) => x15) (CReal.sumRange_cauchy_dominated_ordered_normalized (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x1 x6 x12 x13 (fun (x15 : AxNat) => x7 x15 (CReal.max x2 (CReal.min x9 x3)) (CReal.le_max_left x2 (CReal.min x9 x3)) (CReal.max_le x2 (CReal.min x9 x3) x3 x4 (CReal.min_le_right x9 x3))) x8 x14)) (And.rec.{0} (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (fun (x15 : And (Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) (Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12)))) => Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (fun (x15 : Rat.le (Rat.neg (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) => fun (x16 : Rat.le (Rat.sub (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x16 : AxNat) => x0 x16 (CReal.max x2 (CReal.min x9 x3))) x12) x12)) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) => x16) (CReal.sumRange_cauchy_dominated_ordered_normalized (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x1 x6 x12 x13 (fun (x15 : AxNat) => x7 x15 (CReal.max x2 (CReal.min x9 x3)) (CReal.le_max_left x2 (CReal.min x9 x3)) (CReal.max_le x2 (CReal.min x9 x3) x3 x4 (CReal.min_le_right x9 x3))) x8 x14))) (Rat.sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13)) (Rat.neg_sub (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x13) x13) (CReal.seq (CReal.sumRange (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x12) x12))) (Rat.add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13)) (Rat.add_comm (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x13) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x12))) (fun (x14 : AxNat.le x13 x12) => CReal.sumRange_cauchy_dominated_ordered_normalized (fun (x15 : AxNat) => x0 x15 (CReal.max x2 (CReal.min x9 x3))) x1 x6 x13 x12 (fun (x15 : AxNat) => x7 x15 (CReal.max x2 (CReal.min x9 x3)) (CReal.le_max_left x2 (CReal.min x9 x3)) (CReal.max_le x2 (CReal.min x9 x3) x3 x4 (CReal.min_le_right x9 x3))) x8 x14) (AxNat.le_total x12 x13)) x10 x11)) (Rat.add_le_add (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) x10) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) x11) (Rat.natDivSucc (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6))))))))) x11) (Rat.natDivSucc_le_add_left (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) (AxNat.succ AxNat.zero) x10) (Rat.natDivSucc_le_add_left (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ x6)))))))) (AxNat.succ AxNat.zero) x11)))))) x2 x3)))))))))

Dependencies

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

40 direct dependencies 5 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-CReal.weierstrassMTest

Kind: kernel-term
Status: checked

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

Evidence notes

build_creal_prelude admits CReal.weierstrassMTest 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.weierstrassMTest

Kind: exhaustive-enumeration
Status: checked

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

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.weierstrassMTest, 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/uniform_convergence.rs, declare_weierstrass_m_test)",
  "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."
}