pythagoreanComma
plain-language theorem explainer
The Pythagorean comma is defined as the real number (3/2)^12 divided by 2^7, which measures the residual mismatch after twelve perfect fifths return near one octave. Music theorists and acousticians studying just intonation cite this quantity when quantifying closure error in the circle of fifths. The definition is a direct arithmetic expression with no lemmas or tactic steps.
Claim. The Pythagorean comma is the real number $(3/2)^{12} / 2^7$.
background
In the Aesthetics.MusicalScale module the 12-tone scale is constructed from optimal frequency ratios tied to the golden ratio φ. The perfect fifth is the ratio 3/2 and twelve such steps should close near the octave 2/1; the comma records the small excess. The module states that 12 emerges as round(φ^5 / 2) and that the circle of fifths satisfies (3/2)^12 ≈ 2^7.
proof idea
The definition is a direct arithmetic expression; no lemmas are applied and no tactics are invoked.
why it matters
This definition supplies the numerical value used by the downstream theorem comma_small, which proves the comma is less than 1.02. It fills the AE-001 claim that the Western scale arises from φ-scaling and circle-of-fifths closure. Within the Recognition framework the construction supports the eight-tick octave and the prediction that 12 semitones optimize consonance under phi-ladder constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.