piSeries
piSeries enumerates four classical series expansions for π including the Leibniz alternating sum, Wallis product, Machin arctan formula, and Chudnovsky algorithm. Researchers exploring Recognition Science 8-tick geometry cite the list when asking whether these expansions arise from discrete phase structure. The definition is a direct list of string literals with no computation or proof steps.
claimDefine the list of π series representations as the collection containing the Leibniz series $π/4 = ∑ (-1)^n/(2n+1)$, the Wallis product $π/2 = ∏ (2k)^2/((2k-1)(2k+1))$, Machin's formula $π/4 = 4 arctan(1/5) - arctan(1/239)$, and the Chudnovsky algorithm.
background
The module Mathematics.Pi targets deriving the numerical value of π from RS 8-tick geometry, where an 8-tick circle supplies eight discrete phases whose continuous limit yields π = C/d. The fundamental time quantum is the tick τ₀ = 1 from Constants.tick, which also appears in RSNativeUnits. Upstream CirclePhaseLift.and supplies an explicit log-derivative bound M that becomes the angular Lipschitz constant on a circle of radius r via the chain rule.
proof idea
Direct definition that constructs the list by enumerating four string literals describing the Leibniz, Wallis, Machin, and Chudnovsky representations.
why it matters in Recognition Science
The definition supports the MATH-002 target of extracting π from 8-tick geometry by cataloging known series whose eight-term truncations align with the eight-tick octave (T7). It leaves open whether any listed expansion follows from J-uniqueness or the Recognition Composition Law. No downstream theorems are recorded.
scope and limits
- Does not prove any listed series equals π.
- Does not derive the series from 8-tick axioms or J-cost.
- Does not supply numerical error bounds beyond the embedded comment.
- Does not connect the series to the Recognition Composition Law.
formal statement (Lean)
224def piSeries : List String := [
proof body
Definition body.
225 "Leibniz: π/4 = Σ (-1)^n/(2n+1)",
226 "Wallis: π/2 = Π (2k)²/((2k-1)(2k+1))",
227 "Machin: π/4 = 4·arctan(1/5) - arctan(1/239)",
228 "Chudnovsky: Fastest known algorithm"
229]
230
231/-- The Leibniz series and 8-tick:
232
233 π/4 = 1 - 1/3 + 1/5 - 1/7 + ...
234
235 8 terms: 1 - 1/3 + 1/5 - 1/7 + 1/9 - 1/11 + 1/13 - 1/15
236 ≈ 0.7604
237 π/4 ≈ 0.7854
238
239 Error ≈ 3% with 8 terms. The 8-tick gives a natural truncation. -/