comma_small
plain-language theorem explainer
The declaration shows that the Pythagorean comma, given by (3/2)^12 divided by 2^7, satisfies the strict inequality less than 1.02. Music theorists comparing just intonation to equal temperament cite this bound to quantify the closure error after twelve fifths. The proof unfolds the definition then applies numerical evaluation of the explicit powers to discharge the inequality.
Claim. Let $C = (3/2)^{12} / 2^7$. Then $C < 1.02$.
background
The module derives the Western 12-tone scale from the golden ratio φ by optimizing consonance and closure under frequency ratios. The key definition is the Pythagorean comma $C = (3/2)^{12} / 2^7$, which measures the mismatch after stacking twelve perfect fifths against seven octaves. The module notes that 12 emerges as round(φ^5 / 2) and that the circle of fifths closes because (3/2)^12 ≈ 2^7. Upstream results supply the explicit definition of the comma and the φ-forcing structures that motivate the exponent 12.
proof idea
The tactic proof first simplifies the definition of the comma. It then introduces two auxiliary facts that evaluate (3/2)^12 = 531441/4096 and 2^7 = 128 by direct computation. Substitution followed by a final numerical check confirms the target inequality holds.
why it matters
This bound supports the module claim that the 12-tone scale arises from φ-optimized closure of the circle of fifths. It directly instantiates the RS mechanism that 12 ≈ φ^5 / log(3/2) and that the comma remains small enough for practical consonance. No downstream theorems depend on it yet, but it closes a numerical verification step inside the aesthetics development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.