IsNonTonic
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assign concrete acoustic interpretations to the three axes beyond their Boolean labels.
- Does not derive the 5–7 empirical range from data; it only checks membership in that interval.
- Does not extend the construction to axes with more than two states.
- Does not prove that every culture realizes exactly these seven categories.
Lean usage
theorem universal_tonal_categories : (Finset.univ.filter IsNonTonic).card = 7 := by decideformal statement (Lean)
43def IsNonTonic (t : TonalAssignment) : Prop := t ≠ tonic
proof body
Definition body.
44
45instance (t : TonalAssignment) : Decidable (IsNonTonic t) := instDecidableNot
46
47/-- Total tonal assignment space = 2³ = 8. -/