fifth_pos
plain-language theorem explainer
The positivity of the perfect fifth ratio, fixed at three halves, is recorded as a theorem. Researchers constructing harmonic intervals in Recognition Science cite this when building interval objects from the 12/8 bridge. The proof reduces to a direct numerical check that the constant exceeds zero.
Claim. $0 < 3/2$
background
In the HarmonicModes module the perfect fifth is introduced as the constant ratio 3/2. The same definition appears in CircleOfFifths, accompanied by the remark that the ratio of twelve semitones to eight Recognition Science modes equals 3/2 and forms the central bridge between musical scales and the framework. This supplies the numerical value used throughout the harmonic-mode constructions.
proof idea
The proof is a one-line wrapper that invokes the norm_num tactic to verify the inequality for the explicit rational constant 3/2.
why it matters
The result is consumed by the fifthInterval definition, which packages the ratio together with its positivity to form a MusicalInterval. It therefore supports the extension of Recognition Science into music theory, where the 12/8 identification links directly to the eight-tick octave (T7) and the self-similar structure of the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.