modesPerOctave
plain-language theorem explainer
The modes per octave count is defined as the natural number eight. Researchers tracing the eight-tick period through the forcing chain would cite this when mapping harmonic structure to the T7 step. The declaration is a direct constant assignment with no lemmas or computational steps.
Claim. The number of modes per octave is defined to be the natural number $8$.
background
The HarmonicModes module defines interval constants such as octave, fifth, fourth, majorThird and minorThird via superparticular ratios. It imports the Cost module to access the J-cost function that underlies the Recognition Composition Law. This places the modes count inside the discrete octave period that aligns with the self-similar fixed point.
proof idea
The declaration is a direct definition that binds the modes per octave count to the value 8. No lemmas or tactics are invoked.
why it matters
The modes per octave definition supplies the constant used in the downstream theorem that equates it to two to the power three. It realizes the eight-tick octave landmark in the T7 step of the forcing chain T0 to T8, where the period 2^3 follows from J-uniqueness and the phi fixed point. The placement bridges the abstract chain to concrete harmonic intervals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.