cycleLength
plain-language theorem explainer
The definition fixes the recognition cycle length at eight ticks. Researchers deriving mass-to-light ratios from ledger topology or proving uniqueness of discrete conservative systems cite it to set the fixed period of mass accumulation and photon emission phases. It is introduced as a direct constant definition realizing the eight-tick octave from the forcing chain.
Claim. The cycle length is the natural number $8$.
background
The Mass-to-Light module derives the mass-to-light ratio from ledger structure to answer the objection that observed M/L values are external inputs. The eight-tick cycle partitions recognition events between mass accumulation and photon emission phases, so that M/L emerges as a power of phi in the range 100-550. Upstream, Mass is the type of real numbers, while unit lemmas establish the multiplicative identity in LogicInt, LogicRat, Spin, and PhiClosed sets.
proof idea
This is a direct definition that sets the constant to the literal 8 in the natural numbers. No lemmas are invoked and no tactics are applied.
why it matters
It supplies the cycleLength field in the RSLedger structure used by the ledger uniqueness theorem, which asserts that any discrete conservative system has dimension 3, ratio phi, and cycle length 8. It also enters the phase ratio theorem showing that mass and light phases sum to the cycle length. This realizes T7 (eight-tick octave) from the forcing chain and enables the claim that derived M/L lies in the observed phi^10 to phi^13 band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.