lightPhase
plain-language theorem explainer
lightPhase sets the light-emission tick count per cycle to 3. Derivations of mass-to-light ratios from ledger topology cite this value when splitting the cycle into mass and photon phases. The definition is a direct constant assignment that feeds algebraic simplifications in the ratio theorems.
Claim. The light-emission phase occupies 3 ticks inside the 8-tick cycle, yielding the phase ratio $5/3$ when paired with the complementary mass phase.
background
The module derives the mass-to-light ratio from recognition ledger structure instead of external galaxy data. It partitions the 8-tick cycle between mass accumulation and photon emission phases, with the ratio fixed by the phase lengths. Upstream results supply the phase angles $kπ/4$ for $k=0$ to $7$ and the periodic 8-tick structure with period $2π$.
proof idea
The declaration is a direct definition that assigns the constant value 3. Dependent results invoke norm_num on this value together with the mass-phase and cycle-length constants to obtain the ratio $5/3$.
why it matters
The definition supplies the light-phase length required by the two ratio theorems in the same module. It implements the curvature-partition strategy of the module, placing the observed M/L range inside the interval $φ^{10}$ to $φ^{13}$. This step closes part of gap 10 and connects to the eight-tick octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.