pith. machine review for the scientific record. sign in
def definition def or abbrev high

lightPhase

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 189def lightPhase : ℕ := 3

proof body

Definition body.

 190
 191/-- The phase ratio is determined by ledger topology. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.