theorem proved term proof

`subdivision_is_binary`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  87theorem subdivision_is_binary :
  88    subdivisionLevels = [2^0, 2^1, 2^2, 2^3] := by

proof body

Term-mode proof.

  89  simp [subdivisionLevels]
  90
  91/-! ## Swing as Asymmetry
  92
  93"Swing" in jazz/blues displaces the second note of each pair.
  94A 2:1 swing ratio means the first eighth note lasts twice as long
  95as the second — introducing a φ-like asymmetry into the rhythm. -/
  96

depends on (10)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
subdivisionLevels in IndisputableMonolith.MusicTheory.Rhythm decl_use