piSeries
plain-language theorem explainer
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.
Claim. Define 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.