eight_tick_breaks_uniformity

formal source

 241  · exact ⟨i, h0i⟩
 242
 243/-- The 8-tick dynamics creates an entry different from the ground state. -/
 244theorem eight_tick_breaks_uniformity :
 245    ∀ v : ℝ, ¬ cycle_nondegenerate (fun _ : Fin 8 => v) :=
 246  uniform_cycle_degenerate
 247
 248/-! ## Part VII: Perturbation Cost Bounds -/
 249
 250theorem perturbation_cost_quadratic (ε : ℝ) (hε : |ε| ≤ 1 / 2) :
 251    ∃ c : ℝ, Jcost (1 + ε) = ε ^ 2 / 2 + c * ε ^ 3 ∧ |c| ≤ 2 :=
 252  Jcost_one_plus_eps_quadratic ε hε
 253
 254theorem perturbation_cost_positive (ε : ℝ) (hε : ε ≠ 0) (hε_pos : 0 < 1 + ε) :
 255    0 < Jcost (1 + ε) := by
 256  exact Jcost_pos_of_ne_one (1 + ε) hε_pos (by intro h; exact hε (by linarith))
 257
 258theorem perturbation_cost_small_bound (ε : ℝ) (hε : |ε| ≤ 1 / 10) :
 259    |Jcost (1 + ε) - ε ^ 2 / 2| ≤ ε ^ 2 / 10 :=
 260  Jcost_small_strain_bound ε hε
 261
 262/-! ## Part VIII: The d'Alembert Cascade -/
 263
 264theorem dalembert_cascade (a b : ℤ) :
 265    Jcost (PhiForcing.φ ^ a * PhiForcing.φ ^ b) +
 266    Jcost (PhiForcing.φ ^ a / PhiForcing.φ ^ b) =
 267    2 * Jcost (PhiForcing.φ ^ a) + 2 * Jcost (PhiForcing.φ ^ b) +
 268    2 * Jcost (PhiForcing.φ ^ a) * Jcost (PhiForcing.φ ^ b) :=
 269  dalembert_identity (zpow_pos PhiForcing.phi_pos a) (zpow_pos PhiForcing.phi_pos b)
 270
 271theorem phi_power_compose (a b : ℤ) :
 272    PhiForcing.φ ^ a * PhiForcing.φ ^ b = PhiForcing.φ ^ (a + b) :=
 273  (zpow_add₀ PhiForcing.phi_pos.ne' a b).symm
 274