tritoneInterval
plain-language theorem explainer
tritoneInterval packages the tritone ratio with its positivity witness into the MusicalInterval structure. Music theorists working inside Recognition Science cite it when tabulating J-costs for the standard harmonic intervals. The definition is a direct record constructor that pairs the ratio value with the strict positivity proof.
Claim. The tritone interval is the musical interval whose frequency ratio $r$ satisfies $0 < r$, realized as an element of the structure consisting of a positive real ratio together with its positivity witness.
background
MusicalInterval is the structure whose fields are a real ratio and a proof that the ratio is strictly positive; the associated J-cost is obtained by feeding the ratio into the J-cost function. The HarmonicModes module defines a family of such intervals (octave, fifth, fourth, major and minor thirds, tritone) after importing the Cost abstraction and foundational structures that supply the J-cost minimization setting. Upstream results include the convexity of J-cost minimization with its unique global minimum at ratio 1, the ledger factorization of the positive reals, and the discrete phi-tiers for physical quantities.
proof idea
The declaration is a definition that constructs the MusicalInterval record by supplying the tritone ratio and the tritone_pos positivity proof. It is a one-line wrapper that applies the structure constructor to these two components.
why it matters
This definition supplies the tritone as one of the standard intervals whose J-cost can be evaluated inside the music-theory extension of Recognition Science. It supports embedding harmonic intervals into the J-cost minimization framework stated in PhysicsComplexityStructure.of, which records that J-cost is strictly convex. The placement after the sibling interval definitions prepares the ground for the subsequent J-cost section, though the declaration itself has no downstream uses yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.