universal_tonal_categories
plain-language theorem explainer
The theorem states that exactly seven non-tonic tonal assignments exist in the three-dimensional binary space. Music cognition researchers studying cross-cultural universals would cite this to anchor the empirical 5-7 range to the Recognition Science count of 2^3 - 1. The proof is a one-line decision procedure that computes the cardinality of the filtered finite set directly.
Claim. The cardinality of the set of non-tonic tonal assignments equals 7: $ |{ t : TonalAssignment | t ≠ tonic }| = 7 $.
background
The module addresses cross-cultural tonal universals. Studies report 5-7 categories across cultures despite scale variation. Recognition Science predicts the count 7 = 2^3 - 1 as the non-zero elements of the vector space F_2^3, generated by three binary acoustic axes (pitch height, tonal function, tension). The zero vector is the tonic; the remaining seven are flip variants forced by the D=3 lattice.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the cardinality of Finset.univ filtered by IsNonTonic, confirming the result equals 7.
why it matters
This supplies the universal_count field inside TonalUniversalsCert, which also records the total space cardinality and the empirical-range check. It realizes the RS prediction for tonal categories forced by the D=3 lattice (T8) and the eight-tick structure (T7), where the non-trivial assignments number 2^3 - 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.