TonalAssignment
plain-language theorem explainer
TonalAssignment encodes the three binary acoustic axes that label the seven non-tonic tonal categories forced by the D=3 lattice. Music cognition researchers would cite the structure when counting universal categories independent of scale conventions. The definition is a direct structure declaration that equips the type with decidable equality and finite cardinality.
Claim. A tonal assignment is a triple of booleans $(p, f, t)$ where $p$ records pitch height (low or high), $f$ records tonal function (stable or unstable), and $t$ records tension (consonant or dissonant).
background
The module formalizes the claim that cross-cultural studies recover 5–7 tonal categories. Recognition Science derives the exact count 7 = 2^3 - 1 from the three-dimensional binary lattice F_2^3. The three axes are pitch height, tonal function, and tension; their non-zero assignments label the seven flip variants of the tonic baseline.
proof idea
Structure definition that derives DecidableEq, BEq, Repr, and Fintype instances automatically.
why it matters
TonalAssignment supplies the carrier set for TonalUniversalsCert, which records the space cardinality 8 and the universal count 7 together with the empirical range check. It realizes the D = 3 lattice prediction that appears in the module header and connects to the eight-tick octave structure elsewhere in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.