TonalAssignment
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assign numerical frequencies or interval sizes to the categories.
- Does not depend on any particular musical scale or tuning system.
- Does not include the tonic baseline in the universal count of seven.
- Does not encode cultural or historical variation beyond the binary axes.
formal statement (Lean)
33structure TonalAssignment where
34 pitchHeight : Bool -- false = low, true = high
35 tonalFunction : Bool -- false = stable, true = unstable
36 tension : Bool -- false = consonant, true = dissonant
37 deriving DecidableEq, BEq, Repr, Fintype
38
39/-- The tonic (baseline): (0,0,0). -/