pentatonicSize
plain-language theorem explainer
pentatonicSize fixes the pentatonic scale at five notes inside the φ-derived musical structure. Workers on scale sizes in Recognition Science aesthetics reference this constant when proving Fibonacci relations among 5, 7 and 12. The declaration is a direct constant assignment with no further steps.
Claim. The pentatonic scale size equals $5$.
background
The module derives 12-tone equal temperament from φ through optimal frequency ratios and circle-of-fifths closure. It explicitly lists other φ-related sizes (5, 7, 19, 31) as predictions. The upstream scale definition supplies the map $k ↦ φ^k$ used for rung counting; the has class records spectral peaks at those same φ-powers.
proof idea
Direct definition that assigns the natural number 5.
why it matters
Supplies the note count required by the sibling theorems pentatonic_diatonic_fib and scale_fibonacci, which establish the relation 5 + 7 = 12 and the Fibonacci-like sequence 5, 7, 12. This supports the module prediction that scale sizes 5, 7, 19, 31 carry φ structure, consistent with the eight-tick octave and φ^5 forcing step in the Recognition chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.