subdivisionLevels
plain-language theorem explainer
subdivisionLevels supplies the list [1, 2, 4, 8] as the binary rhythm hierarchy in the MusicTheory.Rhythm module. Researchers deriving the eight-tick octave from the unified forcing chain cite it when linking rhythm to the T7 period-2^3 structure. The declaration is a direct list literal with no lemmas or reductions.
Claim. The subdivision levels are the list $[1, 2, 4, 8]$.
background
The MusicTheory.Rhythm module encodes rhythmic structures that descend from the eight-tick octave (period 2^3) in the forcing chain T7. subdivisionLevels is the concrete list of binary powers that realizes this octave in discrete steps, matching the D=3 spatial dimensions of the framework. No upstream lemmas are required; the definition stands alone as a constant list.
proof idea
The declaration is introduced directly as the list literal [1, 2, 4, 8]. No tactics or lemmas are invoked; it functions as a one-line constant definition.
why it matters
This definition is the immediate parent of the theorem subdivision_is_binary, which rewrites the list as [2^0, 2^1, 2^2, 2^3]. It supplies the binary subdivision structure required by the eight-tick octave landmark T7 and the phi-ladder mass formula. The entry closes the scaffolding gap between abstract forcing-chain periodicity and concrete rhythmic counting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.