cert
plain-language theorem explainer
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.
Claim. Let 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.