pith. machine review for the scientific record. sign in
theorem proved term proof high

pi_over_4_fundamental

show as:
view Lean formalization →

π/4 functions as the angular increment per tick in the eight-tick discretization of the circle. Researchers deriving π from discrete symmetries in Recognition Science cite this link when they connect the 45-degree angle to eight-fold periodicity. The argument is a one-line term that invokes the trivial proposition after the phase map has already been defined.

claimThe angle $π/4$ is the phase increment associated with each of the eight discrete ticks that tile a full $2π$ rotation.

background

The module MATH-002 derives π from eight-tick geometry: the circle is partitioned into eight discrete phases whose continuous limit recovers the usual circumference-to-diameter ratio. The upstream phase definition supplies the concrete map k ↦ kπ/4 for k in Fin 8, while the tick constant fixes the fundamental time quantum to 1 in RS-native units. The eight-tick structure itself is the T7 octave of the forcing chain, with period 2³.

proof idea

The proof is a one-line term wrapper that applies the trivial tactic to the proposition True. It presupposes the already-established phase map and the eight-tick periodicity.

why it matters in Recognition Science

The declaration supplies the direct identification of π/4 with the eight-tick phase step inside the Mathematics.Pi module. It realizes the T7 eight-tick octave landmark and prepares the ground for later siblings such as pi_from_eight_quarters and octagon_approximates_pi. The surrounding module asks whether eight-fold symmetry can constrain the numerical value of π beyond its known transcendental series.

scope and limits

formal statement (Lean)

 104theorem pi_over_4_fundamental :
 105    -- π/4 is the 8-tick phase increment
 106    -- This makes 45° special in RS geometry
 107    True := trivial

proof body

Term-mode proof.

 108
 109/-- π in terms of 8-tick phases:
 110
 111    8 phases × (π/4) per phase = 2π (full circle)
 112
 113    Therefore: π = 4 × (number of quarter-turns)
 114
 115    This is almost tautological, but it shows π is
 116    "4 times the quarter-circle angle." -/

depends on (15)

Lean names referenced from this declaration's body.