major_third_skew_pos
plain-language theorem explainer
The declaration shows that the ledger skew for the major third interval is strictly positive. Researchers analyzing harmonic valence or scale stability in the Recognition Science music theory module would reference it. The proof reduces the claim to a numerical verification after substituting the pre-established skew value of 9/20.
Claim. $0 < 5/4 - (5/4)^{-1}$
background
In the Valence module, ledger skew of a ratio r is defined as r minus its reciprocal. The major third is defined as the just ratio 5/4. A companion theorem establishes that this skew equals 9/20 exactly. The module imports HarmonicModes, which supplies an equivalent definition of the major third. This setup allows direct computation of skew signs for common intervals. Upstream results include the equal-tempered major third 2^{4/12} from Aesthetics, but the valence treatment uses the just value for exact skew calculation.
proof idea
The proof rewrites the target inequality using the major_third_skew theorem, which equates the ledger skew of the major third to 9/20. It then invokes norm_num to confirm that 9/20 is positive.
why it matters
This theorem contributes to the valence analysis in music theory by establishing the sign of the major third's skew. It has no immediate parent theorems in the used_by list, indicating it serves as a basic positivity fact for further scale comparisons. Within Recognition Science, it exemplifies interval ratio analysis but remains isolated from the T0-T8 forcing chain, RCL, phi-ladder, and physical constants such as alpha or G.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.