pith. machine review for the scientific record. sign in
theorem proved term proof

perpetual_complexity

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  99theorem perpetual_complexity
 100    (omega_lambda_pos : (0 : ℝ) < 11 / 16)
 101    (gap45_coprime : Nat.Coprime 8 45) :
 102    ∀ t : ℕ, t % 360 ≠ 0 → (t % 8 ≠ 0 ∨ t % 45 ≠ 0) := by

proof body

Term-mode proof.

 103  intro t ht
 104  exact misalignment_exists t ht
 105
 106/-- **COROLLARY**: Heat death is impossible.
 107    In a hypothetical heat death state, every voxel has x = 1 (zero defect)
 108    and both cadences are synchronized. But gcd(8,45) = 1 means at least
 109    one cadence is always misaligned at 359 out of every 360 ticks. -/

depends on (20)

Lean names referenced from this declaration's body.