phi_fifth_power
plain-language theorem explainer
The definition sets the real number equal to the golden ratio raised to the fifth power. Researchers deriving the 12-tone scale from Recognition Science constants cite it to connect φ^5 ≈ 11.09 to the emergence of 12 semitones per octave. The construction is a direct assignment from the CPM Constants bundle with no further reduction.
Claim. Define the real number φ^5 where φ satisfies φ = 1 + 1/φ, yielding φ^5 ≈ 11.09; this value is close to 11 and its ceiling is 12.
background
The Aesthetics.MusicalScale module derives the Western 12-tone equal temperament from the golden ratio φ via optimal frequency ratios. Key observations are 12 semitones per octave with ratio 2^(1/12) ≈ 1.0595, the perfect fifth 2^(7/12) ≈ 1.4983 ≈ 3/2, and the connection 12 ≈ round(φ^5 / 2) × 2. The RS mechanism optimizes consonance and closure under φ-scaling, with the circle of fifths closing after 12 steps as (3/2)^12 ≈ 2^7. Upstream the Constants structure bundles CPM parameters (Knet, Cproj, Ceng, Cdisp) with non-negativity on Knet.
proof idea
The definition is a one-line assignment that computes Constants.phi raised to the fifth power in the reals. No lemmas or tactics are applied beyond built-in exponentiation.
why it matters
This definition supplies the numerical bridge φ^5 ≈ 11.09 that links the golden ratio (forced at T6 as self-similar fixed point) to the 12-tone octave division. It fills the step supporting the module prediction that 12 semitones optimize consonance and closure, with the circle of fifths closing after 12 steps. No downstream uses appear in the graph, but the value directly informs sibling constructions such as twelve_from_phi and circle_of_fifths_closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.