discretePhases
plain-language theorem explainer
The discretePhases map sends each index k in the 8-element set to the real value k π /4. Researchers deriving U(1) gauge symmetry from discrete ledger redundancy in Recognition Science cite this assignment as the explicit realization of the eight-tick octave. The definition is a direct functional assignment requiring no lemmas or reductions.
Claim. Let $ϕ : {0,1,…,7} → ℝ$ be given by $ϕ(k) = k π / 4$.
background
Gauge invariance in Recognition Science emerges from ledger redundancy: distinct ledger representations of the same physical state are related by gauge transformations. The eight-tick structure discretizes the circle into equal phase steps, supplying the fundamental discrete approximation to continuous U(1). Upstream structures establish J-cost convexity, spectral emergence of SU(3)×SU(2)×U(1) content, and local 8-tick neighbor updates that together force exactly eight phases at the base level.
proof idea
Direct definition that assigns to each k in Fin 8 the value (k : ℝ) * π / 4. No lemmas or tactics are invoked; the assignment is the literal functional expression.
why it matters
This definition supplies the concrete phase values required by the eight_tick_span theorem in the same module, which confirms the boundary conditions 0 and 7π/4. It realizes the T7 eight-tick octave landmark and supports the module's derivation of gauge invariance from ledger redundancy, the target of the proposed Nature Physics paper on information redundancy. It bridges discrete ticks to the continuous U(1) limit while leaving non-Abelian extensions open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.