  31theorem gap45_from_lcm : Nat.lcm 8 45 = 360 := by native_decide
  32
  33/-- 360 = 8 × 45. -/
  34theorem sync_factorization : 360 = 8 * 45 := by norm_num
  35
  36/-- 8 divides 360. -/
  37theorem eight_divides_sync : 8 ∣ 360 := ⟨45, by norm_num⟩
  38
  39/-- 45 divides 360. -/
  40theorem fortyfive_divides_sync : 45 ∣ 360 := ⟨8, by norm_num⟩
  41
  42/-- The landscape flatness parameter: inversely proportional to sync period. -/
  43noncomputable def landscapeFlatness (sync : ℕ) : ℝ := 1 / (sync : ℝ)
  44
  45/-- Flatness at 360 is small. -/
  46theorem flatness_at_360 : landscapeFlatness 360 = 1 / 360 := by
  47  simp [landscapeFlatness]
  48
  49/-- Flatness is positive for positive sync period. -/
  50theorem flatness_pos (sync : ℕ) (h : 0 < sync) : 0 < landscapeFlatness sync := by
  51  simp [landscapeFlatness]; positivity
  52
  53/-- **Gap-45 creates flat landscape**: The sync period of 360 creates a J-cost
  54    landscape where attractor energy differences are at most 1/360. -/
  55theorem gap45_creates_flat_landscape :
  56    landscapeFlatness 360 ≤ 1 / 100 := by
  57  simp [landscapeFlatness]
  58  norm_num
  59
  60/-- The gap region gets flatter with larger sync periods. -/
  61theorem larger_sync_flatter (s1 s2 : ℕ) (h1 : 0 < s1) (h2 : 0 < s2) (h : s1 < s2) :
  62    landscapeFlatness s2 < landscapeFlatness s1 := by
  63  simp [landscapeFlatness]
  64  exact div_lt_div_of_pos_left one_pos (by positivity) (by exact_mod_cast h)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.