tritone
plain-language theorem explainer
The tritone is defined as the real ratio 45/32. Music theorists applying Recognition Science to interval ordering cite this definition when building J-cost hierarchies. It supplies the numerical input for downstream proofs that place the tritone between the fourth and fifth in cost. The declaration is a direct constant assignment with no computation.
Claim. The tritone ratio is the real number $45/32$.
background
The HarmonicModes module supplies concrete real ratios for standard musical intervals so that the J-cost function from the Cost module can be evaluated on them. Superparticular ratios of the form (n+1)/n are noted as the simplest building blocks of just intonation. The tritone sits among sibling definitions for octave, fifth, fourth, and thirds. Upstream results supply the J-cost definition itself via ledger factorization and observer forcing, together with the active-edge count A used in phi-power balance at D=3.
proof idea
One-line definition that directly assigns the constant 45/32.
why it matters
The definition is referenced by the consonance theorems that prove the strict J-cost chain Jcost fourth < Jcost tritone < Jcost fifth and by the explicit evaluation Jcost tritone = 169/2880. It therefore participates in the Recognition framework's application of the Recognition Composition Law to musical intervals and supports the eight-tick octave structure. No open scaffolding is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.