modes_from_dimension
plain-language theorem explainer
The declaration proves that the number of modes per octave equals eight, matching the eight-tick period required by the forcing chain. Researchers linking harmonic structures to Recognition Science would cite it when aligning musical octave counts with T7. The proof is a one-line simplification that unfolds the constant definition of modesPerOctave to reach the numerical identity.
Claim. The number of harmonic modes per octave equals $2^3$.
background
In the HarmonicModes module the definition modesPerOctave fixes the count of modes per octave at the natural number 8. This choice encodes the eight-tick octave from the unified forcing chain, where T7 requires a period of $2^3$. The theorem therefore equates the explicit definition to the power-of-two expression demanded by the dimensional forcing that yields three spatial dimensions.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of modesPerOctave, reducing the equality directly to the trivial numerical identity 8 = 8.
why it matters
This result anchors the musical octave count to the eight-tick structure in the Recognition Science framework at T7 of the forcing chain. It supplies the base count used by sibling interval definitions such as fifth and fourth inside the same module. The alignment supports the self-similar fixed point phi and the overall derivation of constants from the single functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.