cert_inhabited
plain-language theorem explainer
The declaration establishes that the certificate structure for canonical musical scale counts is inhabited, confirming existence of a witness for five scales in the Recognition Science ethnomusicology model. Cross-cultural music theorists would cite it to anchor the phi-ladder predictions for pentatonic, diatonic, and chromatic lengths. The proof is a direct term construction supplying the prior cert term as the witness for nonemptiness.
Claim. The structure of certificates for scale counts is inhabited: there exists a witness such that the canonical scale count equals 5, the diatonic count equals the pentatonic count plus 2, and the chromatic count is positive.
background
The Ethnomusicology module derives the count of canonical musical scales from configDim D = 5, matching the five scale types observed across cultures: pentatonic, diatonic, hexatonic, octatonic, and chromatic. ScaleCountCert packages three properties: canonicalScaleCount equals 5, diatonicCount equals pentatonicCount plus 2, and chromaticCount is positive. These rest on the phi-ladder where note counts follow Fibonacci relations, with chromatic near phi^5 / 2.
proof idea
The proof is a one-line term wrapper that applies the constructor of Nonempty to the term cert, which already satisfies the three properties of the certificate structure.
why it matters
This result completes the structural theorem of the module by witnessing the certificate, supporting the Recognition Science prediction that five scale types are forced by the same configDim template as other five-element classifications. It ties into the phi-ladder and eight-tick octave landmarks without downstream dependencies recorded. The module falsifier is any survey showing 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.