leibniz_8_terms
plain-language theorem explainer
leibniz_8_terms supplies the eight-term partial sum of the Leibniz series for π/4. Researchers deriving π from eight-tick discrete geometry cite this truncation to quantify the three-percent error relative to the true value. The definition consists of a single arithmetic expression that adds and subtracts the reciprocals of the first eight odd integers.
Claim. The eight-term truncation of the Leibniz series is $1 - 1/3 + 1/5 - 1/7 + 1/9 - 1/11 + 1/13 - 1/15$.
background
The Mathematics.Pi module targets derivation of π from RS 8-tick geometry, where the circle is discretized into eight phases and π emerges as the continuous limit of this eight-fold symmetry. The Leibniz series is presented as one standard representation: π/4 equals the infinite alternating sum of odd reciprocals. The eight-term truncation is introduced to illustrate the natural cutoff induced by the eight-tick octave.
proof idea
The definition directly encodes the alternating sum of the first eight odd-denominator reciprocals. No lemmas are applied; the body is the explicit finite sum.
why it matters
This partial sum feeds the approximation theorem leibniz_8_approximates in the same module, which anchors the numerical value of π within the eight-tick framework. It illustrates how the T7 eight-tick octave constrains the continuous limit for π in the RS derivation of geometry from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.