subdivision_is_binary
plain-language theorem explainer
The subdivision levels in rhythmic structures equal the binary powers from 2^0 through 2^3. Recognition Science music theorists cite this to embed rhythmic division inside the eight-tick octave forced by three spatial dimensions. The proof is a direct simplification that unfolds the list definition.
Claim. The subdivision levels equal the sequence $[2^{0}, 2^{1}, 2^{2}, 2^{3}]$.
background
Recognition Science derives an eight-tick octave (period $2^{3}$) from T7 in the unified forcing chain once D equals 3. Subdivision levels record the allowed binary divisions inside each cycle. The module imports the active edge count A from IntegrationGap, where A equals 1 and satisfies the phi-power balance identity at D=3: phi to the (A minus gap) times phi to the gap equals phi. Upstream structures from PhiForcingDerived supply the J-cost and from SpectralEmergence supply the discrete tier count 3 times 2 to the D that yields 24 chiral degrees of freedom.
proof idea
The proof is a one-line wrapper that applies simp to the definition of subdivisionLevels.
why it matters
The result anchors the MusicTheory.Rhythm module inside T7 of the forcing chain and the eight-tick octave. It supplies the binary grid on which tempo definitions and swing asymmetry (phi-like 2:1 displacement) are later built. No downstream theorems are recorded yet, but the declaration closes the rhythmic counterpart to the ledger factorization and continuum bridge already established upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.