pythagorean_comma_small
plain-language theorem explainer
The inequality bounds the Pythagorean comma by showing that twelve fifths exceed seven octaves by a factor below 1.02. Music theorists and Recognition Science modelers cite it when embedding the circle of fifths into the eight-tick octave structure. The proof is a one-line wrapper that applies norm_num to evaluate the real expression directly.
Claim. $ (3/2)^{12} / 2^{7} < 1.02 $
background
The CircleOfFifths module constructs intervals from the fifth ratio 3/2 and octave ratio 2, with sibling definitions fixing semitonesPerOctave at 12 and rsModesPerOctave at 8. The Pythagorean comma is the residual factor after twelve fifths, which must close near seven octaves. Upstream results supply collision-free empirical programs and algebraic tautologies that treat these interval products as well-defined operations inside the Recognition framework.
proof idea
The proof is a one-line wrapper that invokes norm_num to compute the decimal value of (3/2)^12 * 2^(-7) and confirm the strict inequality against 1.02.
why it matters
The bound supports embedding the circle of fifths into the Recognition Science eight-tick octave (T7) by keeping the comma small enough for harmonic modes to fit without large defects. It prepares comparisons such as twelve_fifths_overshoot and fifth_cost_lt_octave_cost that appear among sibling declarations. The result closes a numerical step in the music-theory layer without touching the phi-ladder or J-uniqueness directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.