subdivisionLevels
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not encode non-binary or irregular subdivisions.
- Does not incorporate tempo, beat, or measure definitions.
- Does not extend the hierarchy past the fourth level.
- Does not reference the phi-ladder or J-cost functions.
Lean usage
theorem subdivision_is_binary : subdivisionLevels = [2^0, 2^1, 2^2, 2^3] := by simp [subdivisionLevels]formal statement (Lean)
85def subdivisionLevels : List ℕ := [1, 2, 4, 8]
proof body
Definition body.
86