IsNonTonic
plain-language theorem explainer
IsNonTonic marks any tonal assignment that differs from the zero element in at least one of the three binary acoustic axes. Music theorists working on cross-cultural universals would cite it when isolating the seven non-trivial categories inside the F₂³ space. The definition is a direct inequality that immediately supplies a Decidable instance via the standard negation rule.
Claim. Let $t$ be a tonal assignment with components for pitch height, tonal function, and tension. Then IsNonTonic$(t)$ holds if and only if $t$ is not the tonic baseline $⟨false, false, false⟩$.
background
The module models cross-cultural tonal universals as the non-trivial elements of the vector space F₂³. TonalAssignment is the structure whose three Bool fields encode the binary choices along pitch height (low/high), tonal function (stable/unstable), and tension (consonant/dissonant). The tonic is defined as the zero vector ⟨false, false, false⟩. The module states that the seven flip variants are forced by the D=3 lattice and are independent of cultural scale conventions.
proof idea
The declaration is a one-line definition that expands to the inequality t ≠ tonic. The accompanying instance supplies decidability by reducing to instDecidableNot on the equality instance already derived for TonalAssignment.
why it matters
IsNonTonic supplies the predicate that universal_tonal_categories and TonalUniversalsCert use to certify the count (Finset.univ.filter IsNonTonic).card = 7. This implements the Recognition Science claim that the canonical tonal category count equals 2³ - 1, the number of non-zero vectors in the D=3 lattice, and places the result inside the empirical 5–7 range reported by Brown 2017 and Mehr 2019.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.