cert
The definition cert packages a certificate asserting that configDim equal to five forces exactly five canonical musical scales. Ethnomusicologists would cite it to connect observed cross-cultural scale types to the phi-ladder counts of five, seven, and twelve notes. The construction is a direct record assembly that inserts the reflexivity equality for the scale count, the norm_num reduction for the diatonic-pentatonic relation, and the unfolding for chromatic positivity.
claimLet cert be the ScaleCountCert structure satisfying canonicalScaleCount = 5, diatonicCount = pentatonicCount + 2, and 0 < chromaticCount.
background
The module treats five canonical scale types (pentatonic, diatonic, hexatonic, octatonic, chromatic) as forced by configDim D = 5, matching the template for other five-element classifications in Recognition Science. Note counts follow the phi-ladder: pentatonic equals 5 (Fibonacci 3+2), diatonic equals 7 (5+2), and chromatic near phi^5/2. ScaleCountCert bundles the three properties: the scale count equality, the diatonic-pentatonic relation, and chromatic positivity.
proof idea
The definition cert is a one-line record construction that populates the three fields of ScaleCountCert by direct substitution of the sibling theorems canonicalScaleCount_eq, diatonic_eq_pentatonic_plus_two, and chromatic_pos.
why it matters in Recognition Science
This definition supplies the concrete witness that five canonical scales are forced by configDim D = 5, completing the ethnomusicology module and aligning with the framework's five-element classification pattern. It packages the phi-ladder predictions without invoking the J-function or Recognition Composition Law directly. The module states its falsifier as any survey finding fewer than five or more than seven canonical types across at least fifty cultures.
scope and limits
- Does not derive scale counts from the J-cost or Recognition Composition Law.
- Does not enumerate hexatonic or octatonic note counts.
- Does not connect configDim to spatial dimensions D = 3.
- Does not address the eight-tick octave in musical contexts.
formal statement (Lean)
61noncomputable def cert : ScaleCountCert where
62 scale_count := canonicalScaleCount_eq
proof body
Definition body.
63 diatonic_eq := diatonic_eq_pentatonic_plus_two
64 chromatic_pos := chromatic_pos
65