chromatic_pos
plain-language theorem explainer
The theorem establishes that the chromatic scale count is strictly positive. Researchers verifying the five canonical scales in the Recognition Science ethnomusicology model cite it to complete the certification structure. The proof is a one-line wrapper that unfolds the explicit count definition and normalizes the resulting numerical inequality.
Claim. The chromatic scale count satisfies $0 < 12$.
background
The module develops the Recognition Science claim that configDim D = 5 forces exactly five canonical scale types observed cross-culturally: pentatonic, diatonic, hexatonic, octatonic, and chromatic. Note counts follow the phi-ladder, with chromatic assigned 12 as an approximation to phi^5 / 2. The upstream definition fixes the chromatic count at the constant value 12.
proof idea
This is a one-line wrapper. It unfolds the chromatic count definition to the literal value 12 and applies norm_num to confirm the strict inequality 0 < 12 holds.
why it matters
The result supplies the chromatic_pos field inside the ScaleCountCert structure, which certifies canonicalScaleCount = 5 together with the diatonic-pentatonic relation. It supports the module's structural theorem that five scales are forced by configDim D = 5, consistent with the phi-ladder and eight-tick octave. The module doc states the falsifier as any survey finding fewer than five or more than seven common scale types across at least fifty cultures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.