massPhase
plain-language theorem explainer
The definition fixes the mass-accumulation ticks per recognition cycle at the integer 5. Derivations of galaxy mass-to-light ratios from ledger topology cite this value to recover the ratio 5/3. The assignment is a direct constant with no reduction steps.
Claim. Let $m$ be the number of mass-accumulation ticks in one cycle. Then $m = 5$.
background
The module derives the mass-to-light ratio from the ledger structure rather than treating it as an external parameter. Recognition cost weighting and curvature partition over the eight-tick cycle produce M/L as a power of phi, with observed values falling between phi^10 and phi^13. The upstream one lemmas supply the unit elements in LogicInt, LogicRat, Spin, and the phi-closed field that underwrite the integer constants used here.
proof idea
Direct constant definition assigning the numeral 5.
why it matters
The constant supplies the numerator in the phase-ratio theorems ml_from_phase_ratio and phase_ratio_from_topology, which close the curvature-partition argument for the M/L ratio. It realizes the T7 eight-tick octave inside the Gap-10 derivation and aligns the mass phase with the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.