fourth_pos
plain-language theorem explainer
The fourth musical interval ratio is shown positive in the reals. Music theorists embedding harmonic structures in Recognition Science cite this fact when assembling interval objects from rational ratios. The proof is a direct numerical check via the norm_num tactic.
Claim. $0 < 4/3$
background
The HarmonicModes module defines basic musical intervals as real numbers that serve as frequency ratios. The fourth is introduced as the explicit ratio 4/3. Positivity of this value is required to form a valid MusicalInterval record.
proof idea
One-line wrapper that applies the norm_num tactic to verify the concrete inequality 0 < 4/3 by arithmetic normalization.
why it matters
The result is consumed by the fourthInterval definition, which packages the ratio together with its positivity witness. It supplies one of the elementary intervals (alongside octave and fifth) used to explore harmonic modes inside the Recognition Science music-theory layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.