tonal_space_card
plain-language theorem explainer
The theorem establishes that the finite set of tonal assignments, each a triple of boolean values on three acoustic axes, has cardinality exactly 8. Cognitive scientists and music theorists studying cross-cultural universals would cite this to anchor the prediction of seven non-tonic categories. The proof is a one-line decide tactic that evaluates the derived Fintype instance on the structure.
Claim. Let $T$ be the set of all assignments specified by three boolean coordinates (pitch height, tonal function, tension). Then $|T| = 8$.
background
TonalAssignment is the structure with three boolean fields: pitchHeight (low/high), tonalFunction (stable/unstable), and tension (consonant/dissonant). The module situates this construction in cross-cultural data from Brown 2017 and Mehr 2019, which report 5–7 universal tonal categories. RS derives the count 7 = 2³ − 1 as the non-zero elements of the vector space F₂³, with the zero vector reserved for the tonic baseline.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds because TonalAssignment derives Fintype, DecidableEq, and Repr from its three boolean components, allowing direct computation of the cardinality as 2³.
why it matters
This supplies the space_card field inside the TonalUniversalsCert definition, which bundles the total assignment count with the universal count and empirical-range check. It implements the RS claim that the seven non-trivial assignments arise from the D=3 lattice, matching the eight-tick octave period 2³ and the spatial dimension count in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.