perfectFourth
plain-language theorem explainer
This definition supplies the just-intonation perfect fourth as the positive real 4/3 inside the positive frequency ratio subtype. Researchers building strict musical realizations in the Recognition framework would cite it for rational interval generators. The definition packages the value directly with an automated check for positivity.
Claim. The perfect fourth frequency ratio equals $4/3$.
background
The module develops a musical realization over positive frequency ratios, using equality as the cost function in this strict version. The positive frequency ratio subtype collects positive real numbers for interval comparisons. This definition selects the rational value 4/3. It draws on the octave definitions from the aesthetics and constants modules, where the octave serves as the fundamental stacking unit, and on the canonical arithmetic object that supplies realization-independent Peano structure.
proof idea
This is a direct definition that applies the subtype constructor to 4/3 and uses norm_num to confirm the positivity condition.
why it matters
This declaration supplies the rational generator for the perfect fourth interval in the strict music setting. It is used by the perfect fourth definition in the aesthetics musical scale module. Within the framework it supports octave stacking as the canonical generator and provides the just-intonation counterpart to equal-tempered approximations, consistent with the eight-tick octave period. The module notes that richer psychoacoustic costs may refine the comparison later.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.