circle_of_fifths_closure
plain-language theorem explainer
Twelve perfect fifths exceed seven octaves but remain below seven octaves scaled by 1.02. Music theorists analyzing just intonation and the Pythagorean comma cite this bound to confirm near-closure after twelve steps. The proof splits the conjunction and evaluates the exact powers 531441 and 4096 to verify both sides numerically.
Claim. $ (3/2)^{12} > 2^{7} $ and $ (3/2)^{12} < 1.02 2^{7} $
background
The module derives the Western 12-tone scale from the golden ratio φ by optimizing consonance and closure. A perfect fifth carries frequency ratio 3/2 while an octave carries ratio 2; twelve fifths therefore produce the product (3/2)^12 that must be compared with an integer power of 2. The module notes that 12 emerges as round(φ^5 / 2) and that the circle of fifths returns near the starting pitch after this number of steps.
proof idea
Constructor splits the conjunction into independent inequalities. Each half rewrites the left side as the quotient 531441/4096, substitutes the integer powers via norm_num, and reduces the comparison 129.746 > 128 (respectively < 130.56) by a final norm_num.
why it matters
The bound supplies the concrete numerical anchor for the module's claim that twelve semitones optimize consonance and φ-scaling. It quantifies the Pythagorean comma at approximately 1.0136 and illustrates how the octave (period 2) interacts with rational ratios to generate discrete aesthetic scales. In the Recognition framework this result supports the emergence of integer structure from self-similar fixed points without invoking external tuning conventions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.