octave
plain-language theorem explainer
The octave is defined as the real number 2, serving as the base frequency doubling interval. Researchers deriving 12-tone scales from φ would cite it when closing the circle of fifths or building octave-homomorphisms. The definition is a direct constant assignment with no computation or lemmas.
Claim. The octave frequency ratio equals the real number $2$.
background
The Aesthetics.MusicalScale module derives the Western 12-tone equal temperament from φ, noting that 12 semitones per octave satisfy 2^(1/12) ≈ 1.0595 and that the circle of fifths closes after 12 steps via (3/2)^12 ≈ 2^7. The module doc-comment states that 12 emerges from optimizing consonance, closure, and φ-scaling with the relation 12 ≈ φ^5 / log(3/2).
proof idea
The definition is a direct assignment of the constant 2. No lemmas or tactics are invoked; it is a primitive real constant in this module.
why it matters
This supplies the base interval for downstream uses including OctaveAlgHom in RecognitionCategory and OctaveLoop in CoherenceTechnology. It instantiates the eight-tick octave period from forcing chain T7 and the frequency-ratio form appearing in UniversalForcing.Strict.Music. The module doc-comment ties it to the prediction that 12 semitones is optimal for Western harmony.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.