pythagorean_comma_positive
plain-language theorem explainer
The theorem asserts that twelve stacked perfect fifths exceed seven octaves by a positive factor. Music theorists and Recognition Science researchers cite it when building the circle of fifths or sizing commas in interval lattices. The proof is a one-line wrapper that invokes numerical normalization to confirm the inequality.
Claim. The inequality $(3/2)^{12}/2^{7} > 1$ holds.
background
The CircleOfFifths module models musical intervals via rational ratios, with the octave fixed at 2 and the fifth at 3/2, drawing on basic interval definitions from the HarmonicModes import. The Pythagorean comma is the excess factor obtained by comparing twelve fifths against seven octaves. This theorem supplies the strict positivity of that factor as a foundational numerical fact for the module's interval constructions.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to evaluate the concrete rational inequality directly.
why it matters
This result anchors the circle of fifths construction and supports sibling results on comma size and interval closure within the MusicTheory domain. It aligns with the eight-tick octave structure in the Recognition Science forcing chain by confirming the positive discrepancy that arises in rational approximations to the octave. No open questions are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.