phase_ratio_from_topology
plain-language theorem explainer
The mass-accumulation phase of length 5 and light-emission phase of length 3 sum to the full eight-tick cycle length. Workers deriving mass-to-light ratios from ledger topology cite this result to establish that the ratio follows from phase partitioning in the recognition ledger. The proof is a one-line term reduction that evaluates the constant definitions directly.
Claim. In the eight-tick ledger cycle the mass-accumulation phase length plus the light-emission phase length equals the cycle length: $5 + 3 = 8$.
background
The module derives the mass-to-light ratio from ledger topology rather than external galaxy-cluster data. The eight-tick cycle partitions into five mass-accumulation ticks and three light-emission ticks, with cycleLength defined as 8. These constants appear in the three derivation strategies listed in the module: recognition-cost weighting, ledger-budget constraint, and curvature partition. Upstream, the phase structure inherits from the eight-tick octave in Foundation.EightTick, where phases are multiples of π/4.
proof idea
The proof is a one-line term proof that applies norm_num to the definitions of massPhase, lightPhase, and cycleLength, confirming the arithmetic identity.
why it matters
This declaration supplies the phase-fraction identity required by the curvature-partition strategy in the mass-to-light derivation. It shows that M/L inherits its φ-power structure from the ledger topology, matching the observed range φ^10 to φ^13. The result sits inside the eight-tick octave (T7) of the forcing chain and supports the claim that all dimensionless ratios in Recognition Science are algebraic in φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.