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

sync_exceeds_both

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)

  50theorem sync_exceeds_both :
  51    gap45.sync_period > gap45.recognition_period ∧
  52    gap45.sync_period > gap45.phase_period := by

proof body

Term-mode proof.

  53  constructor <;> simp [gap45, Gap45Frustration.sync_period,
  54    Gap45Frustration.recognition_period, Gap45Frustration.phase_period,
  55    syncPeriod_3]
  56  all_goals norm_num
  57
  58/-! ## The Perpetual Complexity Theorem -/
  59
  60/-- At every 360-tick boundary, there exist voxels where the recognition
  61    and phase cadences are misaligned. These voxels have positive local
  62    J-cost (they are not at x=1) and constitute structured excitations. -/

depends on (11)

Lean names referenced from this declaration's body.