/- Cycling behaviour of Polyak's Heavy-Ball method - formal verification (Lean 4 + Mathlib). Single self-contained file (only `import Mathlib`). Contents: A.2 `HeavyBallKeyIdentity` - the Key Identity bridging the DFT cycling function to GTD's cycling quadratic h. Sorry-free. A.3 `HBTheorem1` - the trigonometric core of Theorem 1 (primitive R-o-U feasibility): residual system <-> angle bound, in binding / tangent / arctangent forms. Sorry-free. B `NonAcc1D` - 1D non-acceleration. The full internal geometric construction (`proj_slopes_in_range`, `cycle_exists_of_feasible`, `nonacceleration_1D`) with NO `sorry`. `proj_slopes_in_range` depends only on the standard Mathlib axioms; `nonacceleration_1D` rests on exactly two named external axioms, both standard published results the paper cites (neither in Mathlib): * `interp_exists` - 1D smooth strongly-convex interpolation (THG); * `accel_implies_feasible` - GTD's acceleration-region containment. i.e. `#print axioms nonacceleration_1D` = [propext, Classical.choice, Quot.sound, interp_exists, accel_implies_feasible] (no `sorryAx`). Headline: 1D non-acceleration of Heavy-Ball is formally verified modulo the interpolation theorem and GTD's containment; the geometric argument between them is machine-checked. Verified under Lean v4.30.0 + Mathlib. -/ import Mathlib open Real /- =========================================================================== A.2 Key Identity =========================================================================== φ(α, α) = (1 - cos α)/(κ · η^2) · h(x, cos α), the algebraic bridge from the DFT cycling function φ to GTD's cycling quadratic h. In the paper it is a three-step coefficient match; checked numerically by `paper/verify.py`. Here it is proven as an exact identity over ℝ. Notation: x = μγ, κ = μ/L, η = (1-κ)x/κ, u = 1 - cos α, s2 = sin^2α = u(2-u). Faithfulness note. φ(α,α) is *even* in sin α: its definition φ(α,α) = C·(cos α - 1) + B·sin α, C = A - A^2 - B^2, A = ((1+β)u - x)/η, B = (1-β) sin α / η, contains sin α only through B^2 = (1-β)^2 s2 / η^2 and B·sin α = (1-β) s2 / η, so substituting s2 = sin^2α loses nothing: the statement is the genuine φ(α,α). -/ namespace HeavyBallKeyIdentity /-- η = (1-κ)x/κ. -/ noncomputable def eta (x κ : ℝ) : ℝ := (1 - κ) * x / κ /-- A(α) with u = 1 - cos α. -/ noncomputable def Aval (x β κ u : ℝ) : ℝ := ((1 + β) * u - x) / eta x κ /-- φ(α, α), with `s2` standing for sin^2α. `B^2 = (1-β)^2 s2 / η^2` and `B·sin α = (1-β) s2 / η`, and `cos α - 1 = -u`. -/ noncomputable def phiDiag (x β κ u s2 : ℝ) : ℝ := let e := eta x κ let A := Aval x β κ u (A - A ^ 2 - (1 - β) ^ 2 * s2 / e ^ 2) * (-u) + (1 - β) * s2 / e /-- GTD cycling quadratic h(x, c) evaluated at c = 1 - u, i.e. h(x, cos α). -/ def hquad (x β κ u : ℝ) : ℝ := let c := 1 - u x ^ 2 - 2 * (β - c + κ * (1 - β * c)) * x + 2 * κ * (1 - c) * (1 + β ^ 2 - 2 * β * c) /-- **Key Identity (division-free form).** `κ · η^2 · φ(α,α) = u · h(x, cos α)`, equivalently `φ(α,α) = (1 - cos α)/(κ η^2) · h(x, cos α)` after dividing by `κ η^2 ≠ 0`. Hypotheses are exactly the convergence-region facts used in the paper: `κ ≠ 0`, `1 - κ ≠ 0` (since κ = μ/L < 1), `x = μγ ≠ 0`, and the Pythagorean relation `s2 = u(2-u)` for `sin^2α`. -/ theorem key_identity {x β κ u s2 : ℝ} (hκ : κ ≠ 0) (h1κ : (1 : ℝ) - κ ≠ 0) (hx : x ≠ 0) (hs2 : s2 = u * (2 - u)) : κ * (eta x κ) ^ 2 * phiDiag x β κ u s2 = u * hquad x β κ u := by subst hs2 simp only [phiDiag, Aval, hquad, eta] field_simp ring /-- **Sign corollary**, as used downstream: `sign φ(α,α) = sign h(x, cos α)`, via the strictly positive prefactor `(1 - cos α)/(κ η^2) = u/(κ η^2) > 0` on the convergence region (`u > 0`, `κ > 0`, `η ≠ 0`). Stated here as the equivalence `0 ≤ φ ↔ 0 ≤ h`; the strict/`<` versions are identical. -/ theorem phi_nonneg_iff_h_nonneg {x β κ u s2 : ℝ} (hκ : 0 < κ) (h1κ : (1 : ℝ) - κ ≠ 0) (hx : x ≠ 0) (hu : 0 < u) (hs2 : s2 = u * (2 - u)) : 0 ≤ phiDiag x β κ u s2 ↔ 0 ≤ hquad x β κ u := by -- positive prefactor κ·η^2 have heta : eta x κ ≠ 0 := div_ne_zero (mul_ne_zero h1κ hx) (ne_of_gt hκ) have hsq : 0 < (eta x κ) ^ 2 := (sq_nonneg _).lt_of_ne (Ne.symm (pow_ne_zero 2 heta)) have hpre : 0 < κ * (eta x κ) ^ 2 := mul_pos hκ hsq -- rewrite φ via the Key Identity, then peel off the two positive factors have key := key_identity (β := β) (ne_of_gt hκ) h1κ hx hs2 have hphi : phiDiag x β κ u s2 = u * hquad x β κ u / (κ * (eta x κ) ^ 2) := by rw [eq_div_iff (ne_of_gt hpre)]; linear_combination key rw [hphi, le_div_iff₀ hpre, zero_mul] exact mul_nonneg_iff_of_pos_left hu end HeavyBallKeyIdentity /- =========================================================================== A.3 Trigonometric core of Theorem 1 (primitive R-o-U feasibility) =========================================================================== Fix K ≥ 3 and a mode with operator M = p - i q, q > 0 (the case 1 ≤ m ≤ (K-1)/2). Write C := p(1-p) - q^2 and, for the grid index j (angle j·2π/K), φ(j) := C (cos(j·2π/K) - 1) + q sin(j·2π/K). We prove: * resid_factored : φ(j) = 2 sin(jπ/K) · (q cos(jπ/K) - C sin(jπ/K)); * feasible_iff_binding : (∀ j ∈ {1,...,K-1}, φ(j) ≤ 0) ↔ q cos(π/K) ≤ C sin(π/K); * feasible_iff_tan : (∀ j ∈ {1,...,K-1}, φ(j) ≤ 0) ↔ q ≤ C tan(π/K) (ii); * binding_iff_angle : q ≤ C tan(π/K) ↔ arctan(q/p)+arctan(q/(1-p)) ≤ π/K (iii); * Cc_pos_of_binding : the binding inequality forces C > 0. The smallest grid angle is 2π/K (index j = 1), which after the coprimality permutation Δ -> mΔ mod K corresponds to the binding slice Δ_m = m^-1. -/ namespace HBTheorem1 /-- `C = p(1-p) - q^2`, the quantity `p(1-p) - q^2` appearing in the residual. -/ def Cc (p q : ℝ) : ℝ := p * (1 - p) - q ^ 2 /-- The interpolation residual at grid index `j`: angle `j·2π/K`. -/ noncomputable def resid (K : ℕ) (p q : ℝ) (j : ℕ) : ℝ := Cc p q * (Real.cos ((j : ℝ) * (2 * π / (K : ℝ))) - 1) + q * Real.sin ((j : ℝ) * (2 * π / (K : ℝ))) /-- Half-angle factorization of the residual. -/ lemma resid_factored (K : ℕ) (p q : ℝ) (j : ℕ) : resid K p q j = 2 * Real.sin ((j : ℝ) * π / (K : ℝ)) * (q * Real.cos ((j : ℝ) * π / (K : ℝ)) - Cc p q * Real.sin ((j : ℝ) * π / (K : ℝ))) := by unfold resid have hsplit : (j : ℝ) * (2 * π / (K : ℝ)) = 2 * ((j : ℝ) * π / (K : ℝ)) := by ring rw [hsplit, Real.cos_two_mul, Real.sin_two_mul] have hpyth := Real.sin_sq_add_cos_sq ((j : ℝ) * π / (K : ℝ)) linear_combination (2 * Cc p q) * hpyth /-- Basic positivity facts about the angle `π/K` for `K ≥ 3`. -/ lemma piK_facts (K : ℕ) (hK : 3 ≤ K) : 0 < π / (K : ℝ) ∧ π / (K : ℝ) < π ∧ 0 < Real.cos (π / (K : ℝ)) ∧ 0 < Real.sin (π / (K : ℝ)) := by have hKr : (3 : ℝ) ≤ (K : ℝ) := by exact_mod_cast hK have hKpos : 0 < (K : ℝ) := by linarith have h1 : 0 < π / (K : ℝ) := by positivity have hle3 : π / (K : ℝ) ≤ π / 3 := by gcongr have hlt2 : π / (K : ℝ) < π / 2 := lt_of_le_of_lt hle3 (by nlinarith [Real.pi_pos]) have hltpi : π / (K : ℝ) < π := by nlinarith [Real.pi_pos, hlt2] have hcos : 0 < Real.cos (π / (K : ℝ)) := Real.cos_pos_of_mem_Ioo ⟨by linarith [h1, Real.pi_pos], hlt2⟩ have hsin : 0 < Real.sin (π / (K : ℝ)) := Real.sin_pos_of_pos_of_lt_pi h1 hltpi exact ⟨h1, hltpi, hcos, hsin⟩ /-- The single residual at `j = 1` is non-positive iff the binding inequality holds. -/ lemma resid1_iff_bind (K : ℕ) (p q : ℝ) (hK : 3 ≤ K) : resid K p q 1 ≤ 0 ↔ q * Real.cos (π / (K : ℝ)) ≤ Cc p q * Real.sin (π / (K : ℝ)) := by obtain ⟨_, _, _, hsin⟩ := piK_facts K hK rw [resid_factored] simp only [Nat.cast_one, one_mul] constructor · intro h; nlinarith [h, hsin] · intro h; nlinarith [h, hsin] /-- The geometric heart: the binding inequality at the smallest angle forces every grid residual to be non-positive. -/ lemma bind_imp_factor (K : ℕ) (p q : ℝ) (hK : 3 ≤ K) (hq : 0 < q) (hbind : q * Real.cos (π / (K : ℝ)) ≤ Cc p q * Real.sin (π / (K : ℝ))) (j : ℕ) (hj1 : 1 ≤ j) (hj2 : j ≤ K - 1) : resid K p q j ≤ 0 := by obtain ⟨ha_pos, _, _, hsin_a⟩ := piK_facts K hK have hKr : (3 : ℝ) ≤ (K : ℝ) := by exact_mod_cast hK have hKpos : 0 < (K : ℝ) := by linarith have hKne : (K : ℝ) ≠ 0 := ne_of_gt hKpos have hj1r : (1 : ℝ) ≤ (j : ℝ) := by exact_mod_cast hj1 have hjK : (j : ℝ) < (K : ℝ) := by have : j < K := by omega exact_mod_cast this -- rewrite bj = j·(π/K) have hbj_eq : (j : ℝ) * π / (K : ℝ) = (j : ℝ) * (π / (K : ℝ)) := by ring have hKmul : (K : ℝ) * (π / (K : ℝ)) = π := by field_simp have hbj_pos : 0 < (j : ℝ) * π / (K : ℝ) := by rw [hbj_eq]; exact mul_pos (by linarith [hj1r]) ha_pos have hbj_lt : (j : ℝ) * π / (K : ℝ) < π := by rw [hbj_eq] calc (j : ℝ) * (π / (K : ℝ)) < (K : ℝ) * (π / (K : ℝ)) := mul_lt_mul_of_pos_right hjK ha_pos _ = π := hKmul have hsin_bj : 0 < Real.sin ((j : ℝ) * π / (K : ℝ)) := Real.sin_pos_of_pos_of_lt_pi hbj_pos hbj_lt -- a ≤ bj have hab : π / (K : ℝ) ≤ (j : ℝ) * π / (K : ℝ) := by rw [hbj_eq]; nlinarith [mul_le_mul_of_nonneg_right hj1r ha_pos.le] -- 0 ≤ sin(bj - a), expanded by the subtraction formula have hsub_nonneg : 0 ≤ (j : ℝ) * π / (K : ℝ) - π / (K : ℝ) := by linarith [hab] have hsub_le_pi : (j : ℝ) * π / (K : ℝ) - π / (K : ℝ) ≤ π := by linarith [hbj_lt, ha_pos] have hsin_diff : 0 ≤ Real.sin ((j : ℝ) * π / (K : ℝ) - π / (K : ℝ)) := Real.sin_nonneg_of_nonneg_of_le_pi hsub_nonneg hsub_le_pi rw [Real.sin_sub] at hsin_diff -- hsin_diff : 0 ≤ sin bj * cos a - cos bj * sin a -- combine with the binding inequality have t1 : 0 ≤ Real.sin ((j : ℝ) * π / (K : ℝ)) * (Cc p q * Real.sin (π / (K : ℝ)) - q * Real.cos (π / (K : ℝ))) := mul_nonneg hsin_bj.le (by linarith [hbind]) have t2 : 0 ≤ q * (Real.sin ((j : ℝ) * π / (K : ℝ)) * Real.cos (π / (K : ℝ)) - Real.cos ((j : ℝ) * π / (K : ℝ)) * Real.sin (π / (K : ℝ))) := mul_nonneg hq.le hsin_diff have hfac : q * Real.cos ((j : ℝ) * π / (K : ℝ)) ≤ Cc p q * Real.sin ((j : ℝ) * π / (K : ℝ)) := by nlinarith [t1, t2, hsin_a] rw [resid_factored] nlinarith [hfac, hsin_bj] /-- **Feasibility of the residual system equals the single binding inequality.** -/ theorem feasible_iff_binding (K : ℕ) (p q : ℝ) (hK : 3 ≤ K) (hq : 0 < q) : (∀ j : ℕ, 1 ≤ j → j ≤ K - 1 → resid K p q j ≤ 0) ↔ q * Real.cos (π / (K : ℝ)) ≤ Cc p q * Real.sin (π / (K : ℝ)) := by constructor · intro hf exact (resid1_iff_bind K p q hK).mp (hf 1 le_rfl (by omega)) · intro hb j hj1 hj2 exact bind_imp_factor K p q hK hq hb j hj1 hj2 /-- Conversion of the binding inequality to the tangent form `q ≤ C tan(π/K)`. -/ lemma binding_iff_tan (K : ℕ) (p q : ℝ) (hK : 3 ≤ K) : q * Real.cos (π / (K : ℝ)) ≤ Cc p q * Real.sin (π / (K : ℝ)) ↔ q ≤ Cc p q * Real.tan (π / (K : ℝ)) := by obtain ⟨_, _, hcos, _⟩ := piK_facts K hK rw [Real.tan_eq_sin_div_cos, ← mul_div_assoc, le_div_iff₀ hcos] /-- **Theorem 1 (trig core), tangent form.** The residual system is feasible iff `q ≤ C·tan(π/K)`, i.e. condition (ii) of the report. -/ theorem feasible_iff_tan (K : ℕ) (p q : ℝ) (hK : 3 ≤ K) (hq : 0 < q) : (∀ j : ℕ, 1 ≤ j → j ≤ K - 1 → resid K p q j ≤ 0) ↔ q ≤ Cc p q * Real.tan (π / (K : ℝ)) := (feasible_iff_binding K p q hK hq).trans (binding_iff_tan K p q hK) /-- Feasibility forces `C = p(1-p) - q^2 > 0`. -/ lemma Cc_pos_of_binding (K : ℕ) (p q : ℝ) (hK : 3 ≤ K) (hq : 0 < q) (hbind : q * Real.cos (π / (K : ℝ)) ≤ Cc p q * Real.sin (π / (K : ℝ))) : 0 < Cc p q := by obtain ⟨_, _, hcos, hsin⟩ := piK_facts K hK nlinarith [hbind, hq, hcos, hsin, mul_pos hq hcos] /-- **The angle-bound form (iii).** With `M = p - i q`, `|arg M| = arctan(q/p)` and `arg(1-M) = arctan(q/(1-p))`; the tangent condition is the angle bound `|arg M| + arg(1-M) ≤ π/K`. Requires `0 < p < 1` and `C > 0` (both implied by feasibility, cf. `Cc_pos_of_binding`). -/ lemma binding_iff_angle (K : ℕ) (p q : ℝ) (hK : 3 ≤ K) (hq : 0 < q) (hp0 : 0 < p) (hp1 : p < 1) (hC : 0 < Cc p q) : q ≤ Cc p q * Real.tan (π / (K : ℝ)) ↔ Real.arctan (q / p) + Real.arctan (q / (1 - p)) ≤ π / (K : ℝ) := by obtain ⟨hpiK_pos, _, _, _⟩ := piK_facts K hK have hKr : (3 : ℝ) ≤ (K : ℝ) := by exact_mod_cast hK have hlt2 : π / (K : ℝ) < π / 2 := by have h3 : π / (K : ℝ) ≤ π / 3 := by gcongr nlinarith [Real.pi_pos, h3] have h1p : (0 : ℝ) < 1 - p := by linarith have hp0' : p ≠ 0 := ne_of_gt hp0 have h1p' : (1 : ℝ) - p ≠ 0 := ne_of_gt h1p have hCne : p * (1 - p) - q ^ 2 ≠ 0 := by have h := hC; rw [Cc] at h; exact ne_of_gt h -- product of the two tangents is < 1 (this is exactly C > 0) have hprod : (q / p) * (q / (1 - p)) < 1 := by rw [div_mul_div_comm, div_lt_one (mul_pos hp0 h1p)] have hCeq : Cc p q = p * (1 - p) - q ^ 2 := rfl nlinarith [hC, hCeq] -- arctan addition formula collapses the two angles to arctan(q/C) have hadd : Real.arctan (q / p) + Real.arctan (q / (1 - p)) = Real.arctan (q / Cc p q) := by rw [Real.arctan_add hprod] congr 1 rw [Cc]; field_simp; ring -- arctan(tan(π/K)) = π/K have htan : Real.arctan (Real.tan (π / (K : ℝ))) = π / (K : ℝ) := Real.arctan_tan (by linarith [hpiK_pos, Real.pi_pos]) hlt2 rw [hadd] conv_rhs => rw [← htan] rw [Real.arctan_le_arctan_iff, div_le_iff₀ hC, mul_comm (Cc p q) (Real.tan (π / (K : ℝ)))] end HBTheorem1 -- Axiom audit (verified): the top-level results depend only on the three standard -- Mathlib axioms `[propext, Classical.choice, Quot.sound]` and contain no `sorry`. -- Uncomment to re-check: -- #print axioms HeavyBallKeyIdentity.key_identity -- #print axioms HBTheorem1.feasible_iff_tan -- #print axioms HBTheorem1.binding_iff_angle namespace NonAcc1D /-! ### Definitions -/ /-- The one-dimensional class `F_{μ,L}`: differentiable, with all secant slopes of the derivative in `[μ,L]`. This is the standard characterization of "μ-strongly-convex ∧ L-smooth" in dimension one. -/ def IsFmuL (μ L : ℝ) (f : ℝ → ℝ) : Prop := Differentiable ℝ f ∧ ∀ x y : ℝ, x ≠ y → μ ≤ (deriv f x - deriv f y) / (x - y) ∧ (deriv f x - deriv f y) / (x - y) ≤ L /-- The gradient Heavy-Ball forces at a cycle point with neighbours `yPrev, yNext`. -/ noncomputable def hbGrad (γ β yPrev yCur yNext : ℝ) : ℝ := ((1 + β) * yCur - yNext - β * yPrev) / γ /-- Heavy-Ball cycles over the `K` points `y : ZMod K → ℝ` (not all equal). -/ def HBCycles (γ β : ℝ) (f : ℝ → ℝ) {K : ℕ} (y : ZMod K → ℝ) : Prop := (∃ s t, y s ≠ y t) ∧ ∀ t : ZMod K, deriv f (y t) = hbGrad γ β (y (t - 1)) (y t) (y (t + 1)) /-! ### The interpolation input (external, not in Mathlib) 1D smooth strongly-convex interpolation (Taylor-Hendrickx-Glineur). If the prescribed (point, gradient) data is a `[μ,L]`-monotone *relation* - every secant slope `(g s - g t)/(y s - y t)` between distinct points lies in `[μ,L]` (`hslope`), and the data is single-valued, i.e. coinciding points carry equal gradients (`hwd`) - then an interpolating `f ∈ F_{μ,L}` exists. Standard result; stated as an axiom (the 1D construction integrates a clamped-slope interpolant, not formalized here). The `hwd` clause is the well-definedness half of the monotone-relation condition; it is essential - without it the hypotheses would be vacuously satisfiable for inconsistent data (two equal points with different gradients). -/ axiom interp_exists (μ L : ℝ) (hμ : 0 < μ) (hμL : μ < L) {K : ℕ} (y g : ZMod K → ℝ) (hslope : ∀ s t : ZMod K, y s ≠ y t → μ ≤ (g s - g t) / (y s - y t) ∧ (g s - g t) / (y s - y t) ≤ L) (hwd : ∀ s t : ZMod K, y s = y t → g s = g t) : ∃ f : ℝ → ℝ, IsFmuL μ L f ∧ ∀ t, deriv f (y t) = g t /-! ### The Heavy-Ball operator and the feasibility region -/ /-- `θ_K = 2π/K`. -/ noncomputable def thetaK (K : ℕ) : ℝ := 2 * π / (K : ℝ) /-- Real part `p_m` of the normalized HB operator `M_m = p_m - i q_m`. -/ noncomputable def Mp (μ L γ β : ℝ) (m K : ℕ) : ℝ := ((1 + β - μ * γ) - (1 + β) * Real.cos ((m : ℝ) * thetaK K)) / ((L - μ) * γ) /-- (Negative) imaginary part `q_m`. -/ noncomputable def Mq (μ L γ β : ℝ) (m K : ℕ) : ℝ := ((1 - β) * Real.sin ((m : ℝ) * thetaK K)) / ((L - μ) * γ) /-- The feasibility (cycling) condition for mode `(m,K)`: the trig-core tangent bound `q ≤ C·tan(π/K)` with `C = p(1-p) - q^2`. By `HeavyBall.feasible_iff_tan` this is exactly primitive R-o-U feasibility. -/ def Feasible (μ L γ β : ℝ) (m K : ℕ) : Prop := Mq μ L γ β m K ≤ (Mp μ L γ β m K * (1 - Mp μ L γ β m K) - (Mq μ L γ β m K) ^ 2) * Real.tan (π / (K : ℝ)) /-! ### The projection construction (Theorem 2) The explicit 1D cycle: rotate the m-jump roots-of-unity cycle by the phase `φ* = -1/2 arg((1-M)M) - π/(2K)` and project onto ℝ. -/ /-- `a = |arg M| = arctan(Mq/Mp)` (when `Mp > 0`). -/ noncomputable def aVal (μ L γ β : ℝ) (m K : ℕ) : ℝ := Real.arctan (Mq μ L γ β m K / Mp μ L γ β m K) /-- `b = arg(1-M) = arctan(Mq/(1-Mp))` (when `Mp < 1`). -/ noncomputable def bVal (μ L γ β : ℝ) (m K : ℕ) : ℝ := Real.arctan (Mq μ L γ β m K / (1 - Mp μ L γ β m K)) /-- The explicit phase `φ* = 1/2(a-b) - π/(2K)`. This equals the paper's `-1/2 arg((1-M)M) - π/(2K)`, but is written via `arctan` to avoid `Complex.arg` branch-cut reasoning. -/ noncomputable def phiStar (μ L γ β : ℝ) (m K : ℕ) : ℝ := (1 / 2) * (aVal μ L γ β m K - bVal μ L γ β m K) - π / (2 * (K : ℝ)) /-- The projected 1D cycle points `y_t = 2r cos(m t θ_K + φ*)`. -/ noncomputable def cyclePts (μ L γ β r : ℝ) (m K : ℕ) (t : ZMod K) : ℝ := 2 * r * Real.cos ((m : ℝ) * (t.val : ℝ) * thetaK K + phiStar μ L γ β m K) /-! ### Bridge identities (PROVED): HB recurrence -> the operator `M = Mp - i·Mq` The two load-bearing algebraic facts of Theorem 2. With `y(φ) = 2r cos φ` and the HB gradient `g(φ) = ((1+β)y(φ) - y(φ+α) - β y(φ-α))/γ` at angle separation `α = m θ_K`, the HB three-term recurrence collapses onto `Re(M e^{iφ})` and `Re((1-M) e^{iφ})`: g(φ) - μ·y(φ) = 2r(L-μ)·(Mp cos φ + Mq sin φ) [= 2r(L-μ)·Re(M e^{iφ})], L·y(φ) - g(φ) = 2r(L-μ)·((1-Mp) cos φ - Mq sin φ) [= 2r(L-μ)·Re((1-M) e^{iφ})]. These are exact and machine-checked. -/ /-- Bridge identity (I): `g(φ) - μ y(φ) = 2r(L-μ)(Mp cos φ + Mq sin φ)`. -/ lemma grad_sub_mu (μ L γ β r α φ : ℝ) (hγ : γ ≠ 0) (hLμ : L - μ ≠ 0) : (((1 + β) * (2 * r * Real.cos φ) - 2 * r * Real.cos (φ + α) - β * (2 * r * Real.cos (φ - α))) / γ) - μ * (2 * r * Real.cos φ) = 2 * r * (L - μ) * ((((1 + β - μ * γ) - (1 + β) * Real.cos α) / ((L - μ) * γ)) * Real.cos φ + ((1 - β) * Real.sin α / ((L - μ) * γ)) * Real.sin φ) := by rw [Real.cos_add, Real.cos_sub]; field_simp; ring /-- Bridge identity (II): `L y(φ) - g(φ) = 2r(L-μ)((1-Mp) cos φ - Mq sin φ)`. -/ lemma L_sub_grad (μ L γ β r α φ : ℝ) (hγ : γ ≠ 0) (hLμ : L - μ ≠ 0) : L * (2 * r * Real.cos φ) - (((1 + β) * (2 * r * Real.cos φ) - 2 * r * Real.cos (φ + α) - β * (2 * r * Real.cos (φ - α))) / γ) = 2 * r * (L - μ) * ((1 - (((1 + β - μ * γ) - (1 + β) * Real.cos α) / ((L - μ) * γ))) * Real.cos φ - ((1 - β) * Real.sin α / ((L - μ) * γ)) * Real.sin φ) := by rw [Real.cos_add, Real.cos_sub]; field_simp; ring /-- **Slope-cone reduction (PROVED).** Between two cycle angles `φs, φt`, the secant slope of the HB cycle data lies in `[μ,L]` as soon as the two real "cone" sign conditions on `Δc = cos φs - cos φt` hold: `(Mp·Δc + Mq·Δs)·Δc ≥ 0` and `((1-Mp)·Δc - Mq·Δs)·Δc ≥ 0`. This is the per-pair heart of Theorem 2; it follows from the two bridge identities by writing `slope - μ = (L-μ)·(Mp Δc + Mq Δs)·Δc / Δc^2`. -/ lemma slope_mem_of_cone (μ L γ β r α φs φt : ℝ) (hγ : γ ≠ 0) (hLμ : 0 < L - μ) (hr : 0 < r) (hΔ : Real.cos φs ≠ Real.cos φt) (hc1 : 0 ≤ ((((1 + β - μ * γ) - (1 + β) * Real.cos α) / ((L - μ) * γ)) * (Real.cos φs - Real.cos φt) + ((1 - β) * Real.sin α / ((L - μ) * γ)) * (Real.sin φs - Real.sin φt)) * (Real.cos φs - Real.cos φt)) (hc2 : 0 ≤ ((1 - (((1 + β - μ * γ) - (1 + β) * Real.cos α) / ((L - μ) * γ))) * (Real.cos φs - Real.cos φt) - ((1 - β) * Real.sin α / ((L - μ) * γ)) * (Real.sin φs - Real.sin φt)) * (Real.cos φs - Real.cos φt)) : μ ≤ (((1 + β) * (2 * r * Real.cos φs) - 2 * r * Real.cos (φs + α) - β * (2 * r * Real.cos (φs - α))) / γ - ((1 + β) * (2 * r * Real.cos φt) - 2 * r * Real.cos (φt + α) - β * (2 * r * Real.cos (φt - α))) / γ) / (2 * r * Real.cos φs - 2 * r * Real.cos φt) ∧ (((1 + β) * (2 * r * Real.cos φs) - 2 * r * Real.cos (φs + α) - β * (2 * r * Real.cos (φs - α))) / γ - ((1 + β) * (2 * r * Real.cos φt) - 2 * r * Real.cos (φt + α) - β * (2 * r * Real.cos (φt - α))) / γ) / (2 * r * Real.cos φs - 2 * r * Real.cos φt) ≤ L := by have hΔsq : 0 < (Real.cos φs - Real.cos φt) ^ 2 := by positivity set S := (((1 + β) * (2 * r * Real.cos φs) - 2 * r * Real.cos (φs + α) - β * (2 * r * Real.cos (φs - α))) / γ - ((1 + β) * (2 * r * Real.cos φt) - 2 * r * Real.cos (φt + α) - β * (2 * r * Real.cos (φt - α))) / γ) / (2 * r * Real.cos φs - 2 * r * Real.cos φt) with hS have hsubμ : S - μ = (L - μ) * (((((1 + β - μ * γ) - (1 + β) * Real.cos α) / ((L - μ) * γ)) * (Real.cos φs - Real.cos φt) + ((1 - β) * Real.sin α / ((L - μ) * γ)) * (Real.sin φs - Real.sin φt)) * (Real.cos φs - Real.cos φt)) / (Real.cos φs - Real.cos φt) ^ 2 := by rw [hS]; simp only [Real.cos_add, Real.cos_sub]; field_simp; ring have hLsub : L - S = (L - μ) * (((1 - (((1 + β - μ * γ) - (1 + β) * Real.cos α) / ((L - μ) * γ))) * (Real.cos φs - Real.cos φt) - ((1 - β) * Real.sin α / ((L - μ) * γ)) * (Real.sin φs - Real.sin φt)) * (Real.cos φs - Real.cos φt)) / (Real.cos φs - Real.cos φt) ^ 2 := by rw [hS]; simp only [Real.cos_add, Real.cos_sub]; field_simp; ring refine ⟨by nlinarith [div_nonneg (mul_nonneg (le_of_lt hLμ) hc1) (le_of_lt hΔsq), hsubμ], by nlinarith [div_nonneg (mul_nonneg (le_of_lt hLμ) hc2) (le_of_lt hΔsq), hLsub]⟩ /-- **Cone-at-grid (PROVED) - the analytic replacement for the sort-order lemma.** For the valid phase `φ ∈ [a-π/K, -b]` (nonempty exactly when the angle bound `a+b ≤ π/K` holds), at every grid position `j ∈ {0,...,K-1}` both `σ`-form cone products are `≥ 0`, where `σ = jπ/K + φ`: `sin(σ-a)·sin σ ≥ 0` and `sin(σ+b)·sin σ ≥ 0`. Since every pairwise `σ` of the projected cycle reduces (mod π) to such a grid position, this discharges the cone conditions for ALL pairs at once - no explicit sorting permutation or transitivity is needed. Proof is the bounded casework `j = 0` vs `1 ≤ j ≤ K-1`. -/ lemma cone_at_grid (K : ℕ) (hK : 3 ≤ K) (a b φ : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a + b ≤ π / (K : ℝ)) (hφl : a - π / (K : ℝ) ≤ φ) (hφr : φ ≤ -b) (j : ℕ) (hj : j ≤ K - 1) : 0 ≤ Real.sin (((j : ℝ) * π / K + φ) - a) * Real.sin ((j : ℝ) * π / K + φ) ∧ 0 ≤ Real.sin (((j : ℝ) * π / K + φ) + b) * Real.sin ((j : ℝ) * π / K + φ) := by have hKr : (3 : ℝ) ≤ K := by exact_mod_cast hK have hKpos : 0 < (K : ℝ) := by linarith have hπpos := Real.pi_pos have hπK_pos : 0 < π / (K : ℝ) := by positivity have hπK_le3 : π / (K : ℝ) ≤ π / 3 := by gcongr have hπK_ltπ : π / (K : ℝ) < π := by nlinarith [hπK_le3, hπpos] have sin_nonpos : ∀ x : ℝ, -π ≤ x → x ≤ 0 → Real.sin x ≤ 0 := by intro x h1 h2 have h := Real.sin_nonneg_of_nonneg_of_le_pi (x := -x) (by linarith) (by linarith) rw [Real.sin_neg] at h; linarith have mul_npnp : ∀ x y : ℝ, x ≤ 0 → y ≤ 0 → 0 ≤ x * y := by intro x y hx hy have := mul_nonneg (neg_nonneg.2 hx) (neg_nonneg.2 hy); simpa using this rcases Nat.eq_zero_or_pos j with hj0 | hjpos · subst hj0 simp only [Nat.cast_zero, zero_mul, zero_div, zero_add] have hsφ : Real.sin φ ≤ 0 := sin_nonpos φ (by linarith) (by linarith) have hsφa : Real.sin (φ - a) ≤ 0 := sin_nonpos (φ - a) (by linarith) (by linarith) have hsφb : Real.sin (φ + b) ≤ 0 := sin_nonpos (φ + b) (by linarith) (by linarith) exact ⟨mul_npnp _ _ hsφa hsφ, mul_npnp _ _ hsφb hsφ⟩ · have hj1 : (1 : ℝ) ≤ (j : ℝ) := by exact_mod_cast hjpos have hjK : (j : ℝ) ≤ (K : ℝ) - 1 := by have h : (j : ℝ) ≤ ((K - 1 : ℕ) : ℝ) := by exact_mod_cast hj rwa [Nat.cast_sub (by omega), Nat.cast_one] at h have hKne : (K : ℝ) ≠ 0 := hKpos.ne' have hmul1 : (1 : ℝ) * (π / (K : ℝ)) ≤ (j : ℝ) * (π / (K : ℝ)) := mul_le_mul_of_nonneg_right hj1 hπK_pos.le have hmul2 : (j : ℝ) * (π / (K : ℝ)) ≤ ((K : ℝ) - 1) * (π / (K : ℝ)) := mul_le_mul_of_nonneg_right hjK hπK_pos.le have hKfrac : ((K : ℝ) - 1) * (π / (K : ℝ)) = π - π / (K : ℝ) := by field_simp have heq : (j : ℝ) * π / (K : ℝ) = (j : ℝ) * (π / (K : ℝ)) := by ring have hj_ge : π / (K : ℝ) ≤ (j : ℝ) * (π / (K : ℝ)) := by calc π / (K : ℝ) = 1 * (π / (K : ℝ)) := by ring _ ≤ (j : ℝ) * (π / (K : ℝ)) := hmul1 have hj_le : (j : ℝ) * (π / (K : ℝ)) ≤ π - π / (K : ℝ) := by rw [← hKfrac]; exact hmul2 have hlo : a ≤ (j : ℝ) * π / K + φ := by rw [heq]; linarith [hj_ge, hφl] have hhi : (j : ℝ) * π / K + φ ≤ π - π / (K : ℝ) - b := by rw [heq]; linarith [hj_le, hφr] have hσpos : 0 < (j : ℝ) * π / K + φ := by linarith have hσltπ : (j : ℝ) * π / K + φ < π := by linarith have hsσ : 0 < Real.sin ((j : ℝ) * π / K + φ) := Real.sin_pos_of_pos_of_lt_pi hσpos hσltπ have hsσa : 0 ≤ Real.sin (((j : ℝ) * π / K + φ) - a) := Real.sin_nonneg_of_nonneg_of_le_pi (by linarith) (by linarith) have hsσb : 0 ≤ Real.sin (((j : ℝ) * π / K + φ) + b) := Real.sin_nonneg_of_nonneg_of_le_pi (by linarith) (by linarith) exact ⟨mul_nonneg hsσa (le_of_lt hsσ), mul_nonneg hsσb (le_of_lt hsσ)⟩ /-- **Sum-to-product for cone 1 (PROVED).** With `φs = σ+δ`, `φt = σ-δ`, the cone-1 expression factors as `4 sin^2δ · sinσ · (Mp sinσ - Mq cosσ)`. Combined with `(Mp sinσ - Mq cosσ) = |M| sin(σ-a)` this is what feeds `cone_at_grid`. -/ lemma cone1_stp (Mp Mq σ δ : ℝ) : (Mp * (Real.cos (σ + δ) - Real.cos (σ - δ)) + Mq * (Real.sin (σ + δ) - Real.sin (σ - δ))) * (Real.cos (σ + δ) - Real.cos (σ - δ)) = 4 * Real.sin δ ^ 2 * Real.sin σ * (Mp * Real.sin σ - Mq * Real.cos σ) := by simp only [Real.cos_add, Real.cos_sub, Real.sin_add, Real.sin_sub]; ring /-- **Sum-to-product for cone 2 (PROVED).** Likewise the cone-2 expression factors as `4 sin^2δ · sinσ · ((1-Mp) sinσ + Mq cosσ)`, with `((1-Mp) sinσ + Mq cosσ) = |1-M| sin(σ+b)`. -/ lemma cone2_stp (Mp Mq σ δ : ℝ) : ((1 - Mp) * (Real.cos (σ + δ) - Real.cos (σ - δ)) - Mq * (Real.sin (σ + δ) - Real.sin (σ - δ))) * (Real.cos (σ + δ) - Real.cos (σ - δ)) = 4 * Real.sin δ ^ 2 * Real.sin σ * ((1 - Mp) * Real.sin σ + Mq * Real.cos σ) := by simp only [Real.cos_add, Real.cos_sub, Real.sin_add, Real.sin_sub]; ring /-- **R-sin form, cone 1 (PROVED).** `Mp sinσ - Mq cosσ = |M| sin(σ - a)` with `a = arctan(Mq/Mp)`, `|M| = sqrt (Mp^2+Mq^2)`, for `Mp > 0`. This is the link that turns `cone1_stp`'s factor into the `sin(σ-a)` form handled by `cone_at_grid`. -/ lemma cone1_arg (Mp Mq σ : ℝ) (hMp : 0 < Mp) : Mp * Real.sin σ - Mq * Real.cos σ = Real.sqrt (Mp ^ 2 + Mq ^ 2) * Real.sin (σ - Real.arctan (Mq / Mp)) := by have hRcos : Real.sqrt (Mp ^ 2 + Mq ^ 2) * Real.cos (Real.arctan (Mq / Mp)) = Mp := by rw [Real.cos_arctan, show (1 : ℝ) + (Mq / Mp) ^ 2 = (Mp ^ 2 + Mq ^ 2) / Mp ^ 2 by field_simp, Real.sqrt_div (by positivity), Real.sqrt_sq hMp.le] field_simp have hRsin : Real.sqrt (Mp ^ 2 + Mq ^ 2) * Real.sin (Real.arctan (Mq / Mp)) = Mq := by rw [Real.sin_arctan, show (1 : ℝ) + (Mq / Mp) ^ 2 = (Mp ^ 2 + Mq ^ 2) / Mp ^ 2 by field_simp, Real.sqrt_div (by positivity), Real.sqrt_sq hMp.le] field_simp rw [Real.sin_sub] linear_combination (-Real.sin σ) * hRcos + (Real.cos σ) * hRsin /-- **R-sin form, cone 2 (PROVED).** `(1-Mp) sinσ + Mq cosσ = |1-M| sin(σ + b)` with `b = arctan(Mq/(1-Mp))`, `|1-M| = sqrt ((1-Mp)^2+Mq^2)`, for `Mp < 1`. -/ lemma cone2_arg (Mp Mq σ : ℝ) (hMp : Mp < 1) : (1 - Mp) * Real.sin σ + Mq * Real.cos σ = Real.sqrt ((1 - Mp) ^ 2 + Mq ^ 2) * Real.sin (σ + Real.arctan (Mq / (1 - Mp))) := by have h1 : 0 < 1 - Mp := by linarith have hRcos : Real.sqrt ((1 - Mp) ^ 2 + Mq ^ 2) * Real.cos (Real.arctan (Mq / (1 - Mp))) = 1 - Mp := by rw [Real.cos_arctan, show (1 : ℝ) + (Mq / (1 - Mp)) ^ 2 = ((1 - Mp) ^ 2 + Mq ^ 2) / (1 - Mp) ^ 2 by field_simp, Real.sqrt_div (by positivity), Real.sqrt_sq h1.le] field_simp have hRsin : Real.sqrt ((1 - Mp) ^ 2 + Mq ^ 2) * Real.sin (Real.arctan (Mq / (1 - Mp))) = Mq := by rw [Real.sin_arctan, show (1 : ℝ) + (Mq / (1 - Mp)) ^ 2 = ((1 - Mp) ^ 2 + Mq ^ 2) / (1 - Mp) ^ 2 by field_simp, Real.sqrt_div (by positivity), Real.sqrt_sq h1.le] field_simp rw [Real.sin_add] linear_combination (-Real.sin σ) * hRcos + (-Real.cos σ) * hRsin /-- **π-periodicity of the cone product (PROVED).** Shifting `σ` by an integer multiple of `π` leaves `sin(σ+c)·sin σ` unchanged (`c = -a` for cone 1, `c = b` for cone 2). This is what lets a pair's `σ` be replaced by its grid representative without changing the cone sign. -/ lemma sin_shift_periodic (c x : ℝ) (n : ℤ) : Real.sin ((x + (n : ℝ) * π) + c) * Real.sin (x + (n : ℝ) * π) = Real.sin (x + c) * Real.sin x := by rw [show x + (n : ℝ) * π + c = (x + c) + (n : ℝ) * π by ring, Real.sin_add_int_mul_pi, Real.sin_add_int_mul_pi] have h2 : (-1 : ℝ) ^ n * (-1) ^ n = 1 := by rw [← mul_zpow]; norm_num linear_combination (Real.sin (x + c) * Real.sin x) * h2 /-- **Grid reduction (PROVED).** `M·π/K = (M mod K)·π/K + (M div K)·π`. So a pair's angle `M·π/K` (with `M = m(s+t)`) sits at the grid position `(M mod K)·π/K` up to an integer multiple of `π` - feeding `sin_shift_periodic` and then `cone_at_grid` at the grid index `j = M mod K ∈ {0,...,K-1}`. -/ lemma grid_reduce (M K : ℕ) (hK : 0 < K) : (M : ℝ) * π / K = ((M % K : ℕ) : ℝ) * π / K + ((M / K : ℕ) : ℝ) * π := by have hdm : M % K + K * (M / K) = M := by rw [Nat.add_comm]; exact Nat.div_add_mod M K have h : (M : ℝ) = ((M % K : ℕ) : ℝ) + (K : ℝ) * ((M / K : ℕ) : ℝ) := by exact_mod_cast hdm.symm have hKne : (K : ℝ) ≠ 0 := by exact_mod_cast hK.ne' rw [h]; field_simp /-- **ZMod neighbor periodicity (PROVED).** The cycle angle at the successor `t+1` equals the angle at `t.val+1` (no wraparound) up to an integer multiple of `2π`, hence the same cosine. This is the wrapping fact needed so the bridge identity (stated for `cos(φ +- mθ)`) applies to the actual `hbGrad` on `cyclePts`. -/ lemma cos_succ_periodic (m K : ℕ) (hK : 1 < K) (φ : ℝ) (t : ZMod K) : Real.cos ((m : ℝ) * (((t + 1).val : ℕ) : ℝ) * (2 * π / (K : ℝ)) + φ) = Real.cos ((m : ℝ) * (((t.val : ℕ) : ℝ) + 1) * (2 * π / (K : ℝ)) + φ) := by haveI : NeZero K := ⟨by omega⟩ haveI : Fact (1 < K) := ⟨hK⟩ have hval : (t + 1).val = (t.val + 1) % K := by rw [ZMod.val_add, ZMod.val_one] have hc : t.val + 1 = (t + 1).val + K * ((t.val + 1) / K) := by rw [hval]; exact (Nat.mod_add_div (t.val + 1) K).symm have hKne : (K : ℝ) ≠ 0 := by exact_mod_cast (by omega : K ≠ 0) have hcr : ((t.val : ℝ) + 1) = (((t + 1).val : ℕ) : ℝ) + (K : ℝ) * (((t.val + 1) / K : ℕ) : ℝ) := by exact_mod_cast hc have key : (m : ℝ) * (((t.val : ℕ) : ℝ) + 1) * (2 * π / (K : ℝ)) + φ = ((m : ℝ) * (((t + 1).val : ℕ) : ℝ) * (2 * π / (K : ℝ)) + φ) + ((m * ((t.val + 1) / K) : ℕ) : ℝ) * (2 * π) := by rw [hcr]; push_cast; field_simp; ring rw [key, Real.cos_add_nat_mul_two_pi] /-- **ZMod predecessor wrapping (PROVED).** Mirror of `cos_succ_periodic` for `t-1`: the angle at `t-1` matches the no-wraparound `t.val-1` up to `2π·ℤ`. -/ lemma cos_pred_periodic (m K : ℕ) (hK : 1 < K) (φ : ℝ) (t : ZMod K) : Real.cos ((m : ℝ) * (((t - 1).val : ℕ) : ℝ) * (2 * π / (K : ℝ)) + φ) = Real.cos ((m : ℝ) * (((t.val : ℕ) : ℝ) - 1) * (2 * π / (K : ℝ)) + φ) := by haveI : NeZero K := ⟨by omega⟩ have hsub : t - 1 = t + ((K - 1 : ℕ) : ZMod K) := by rw [Nat.cast_sub (by omega : 1 ≤ K), Nat.cast_one, ZMod.natCast_self]; ring have hval : (t - 1).val = (t.val + (K - 1)) % K := by rw [hsub, ZMod.val_add, ZMod.val_natCast, Nat.mod_eq_of_lt (by omega : K - 1 < K)] obtain ⟨q, hq'⟩ : ∃ q : ℕ, (t - 1).val + K * q = t.val + (K - 1) := ⟨(t.val + (K - 1)) / K, by rw [hval]; exact Nat.mod_add_div _ _⟩ have hKne : (K : ℝ) ≠ 0 := by exact_mod_cast (by omega : K ≠ 0) have hmodR : ((t - 1).val : ℝ) + (K : ℝ) * (q : ℝ) = (t.val : ℝ) + ((K : ℝ) - 1) := by have h2 : (((t - 1).val + K * q : ℕ) : ℝ) = ((t.val + (K - 1) : ℕ) : ℝ) := by exact_mod_cast hq' push_cast [Nat.cast_sub (by omega : 1 ≤ K)] at h2 linarith [h2] have hq : ((t - 1).val : ℝ) = (t.val : ℝ) + ((K : ℝ) - 1) - (K : ℝ) * (q : ℝ) := by linarith [hmodR] have key : (m : ℝ) * (((t - 1).val : ℕ) : ℝ) * (2 * π / (K : ℝ)) + φ = ((m : ℝ) * (((t.val : ℕ) : ℝ) - 1) * (2 * π / (K : ℝ)) + φ) + (((m : ℤ) * (1 - (q : ℤ))) : ℤ) * (2 * π) := by rw [hq]; push_cast; field_simp; ring rw [key, Real.cos_add_int_mul_two_pi] /-- Helper: the cone sin-product at angle `Msum·π/K + φ` equals its value at the grid position `(Msum mod K)·π/K + φ` (π-periodicity + grid reduction). -/ lemma sin_prod_grid (c φ : ℝ) (K Msum : ℕ) (hK : 0 < K) : Real.sin (((Msum : ℝ) * π / K + φ) + c) * Real.sin ((Msum : ℝ) * π / K + φ) = Real.sin ((((Msum % K : ℕ) : ℝ) * π / K + φ) + c) * Real.sin (((Msum % K : ℕ) : ℝ) * π / K + φ) := by have hgrid := grid_reduce Msum K hK have hx : (Msum : ℝ) * π / K + φ = (((Msum % K : ℕ) : ℝ) * π / K + φ) + (((Msum / K : ℕ) : ℤ) : ℝ) * π := by rw [hgrid, Int.cast_natCast]; ring rw [hx] exact sin_shift_periodic c (((Msum % K : ℕ) : ℝ) * π / K + φ) ((Msum / K : ℕ) : ℤ) /-- **Master cone condition 1 (PROVED).** At an interior-feasible operator the first cone sign condition holds for the projected pair at angle `σ = Msum·π/K + φ*`. -/ lemma cone1_holds (Mp Mq φ σ δ : ℝ) (K Msum : ℕ) (hK : 3 ≤ K) (hMp0 : 0 < Mp) (hMp1 : Mp < 1) (hMq : 0 < Mq) (hab : Real.arctan (Mq / Mp) + Real.arctan (Mq / (1 - Mp)) ≤ π / (K : ℝ)) (hφ : φ = (1 / 2) * (Real.arctan (Mq / Mp) - Real.arctan (Mq / (1 - Mp))) - π / (2 * (K : ℝ))) (hσ : σ = (Msum : ℝ) * π / (K : ℝ) + φ) : 0 ≤ (Mp * (Real.cos (σ + δ) - Real.cos (σ - δ)) + Mq * (Real.sin (σ + δ) - Real.sin (σ - δ))) * (Real.cos (σ + δ) - Real.cos (σ - δ)) := by have h1mp : 0 < 1 - Mp := by linarith have hKr : (0 : ℝ) < K := by exact_mod_cast (by omega : 0 < K) rw [cone1_stp, cone1_arg Mp Mq σ hMp0] set a := Real.arctan (Mq / Mp) with ha set b := Real.arctan (Mq / (1 - Mp)) with hb have ha_pos : 0 < a := Real.arctan_pos.mpr (by positivity) have hb_pos : 0 < b := Real.arctan_pos.mpr (by positivity) have hrel : π / (K : ℝ) = 2 * (π / (2 * (K : ℝ))) := by field_simp have hφl : a - π / (K : ℝ) ≤ φ := by rw [hφ]; nlinarith [hab, hrel] have hφr : φ ≤ -b := by rw [hφ]; nlinarith [hab, hrel] have hjlt : Msum % K ≤ K - 1 := by have := Nat.mod_lt Msum (show 0 < K by omega); omega have hcone := (cone_at_grid K hK a b φ ha_pos hb_pos hab hφl hφr (Msum % K) hjlt).1 have hsp : Real.sin (σ - a) * Real.sin σ = Real.sin ((((Msum % K : ℕ) : ℝ) * π / K + φ) - a) * Real.sin (((Msum % K : ℕ) : ℝ) * π / K + φ) := by rw [hσ, show (Msum : ℝ) * π / K + φ - a = ((Msum : ℝ) * π / K + φ) + (-a) by ring, show (((Msum % K : ℕ) : ℝ) * π / K + φ) - a = (((Msum % K : ℕ) : ℝ) * π / K + φ) + (-a) by ring] exact sin_prod_grid (-a) φ K Msum (by omega) have hsp' : 0 ≤ Real.sin (σ - a) * Real.sin σ := by rw [hsp]; exact hcone have h4 : (0 : ℝ) ≤ 4 * Real.sin δ ^ 2 := by positivity have hsqrt : (0 : ℝ) ≤ Real.sqrt (Mp ^ 2 + Mq ^ 2) := Real.sqrt_nonneg _ nlinarith [mul_nonneg (mul_nonneg h4 hsqrt) hsp'] /-- **Master cone condition 2 (PROVED).** Likewise for the second cone sign. -/ lemma cone2_holds (Mp Mq φ σ δ : ℝ) (K Msum : ℕ) (hK : 3 ≤ K) (hMp0 : 0 < Mp) (hMp1 : Mp < 1) (hMq : 0 < Mq) (hab : Real.arctan (Mq / Mp) + Real.arctan (Mq / (1 - Mp)) ≤ π / (K : ℝ)) (hφ : φ = (1 / 2) * (Real.arctan (Mq / Mp) - Real.arctan (Mq / (1 - Mp))) - π / (2 * (K : ℝ))) (hσ : σ = (Msum : ℝ) * π / (K : ℝ) + φ) : 0 ≤ ((1 - Mp) * (Real.cos (σ + δ) - Real.cos (σ - δ)) - Mq * (Real.sin (σ + δ) - Real.sin (σ - δ))) * (Real.cos (σ + δ) - Real.cos (σ - δ)) := by have h1mp : 0 < 1 - Mp := by linarith have hKr : (0 : ℝ) < K := by exact_mod_cast (by omega : 0 < K) rw [cone2_stp, cone2_arg Mp Mq σ hMp1] set a := Real.arctan (Mq / Mp) with ha set b := Real.arctan (Mq / (1 - Mp)) with hb have ha_pos : 0 < a := Real.arctan_pos.mpr (by positivity) have hb_pos : 0 < b := Real.arctan_pos.mpr (by positivity) have hrel : π / (K : ℝ) = 2 * (π / (2 * (K : ℝ))) := by field_simp have hφl : a - π / (K : ℝ) ≤ φ := by rw [hφ]; nlinarith [hab, hrel] have hφr : φ ≤ -b := by rw [hφ]; nlinarith [hab, hrel] have hjlt : Msum % K ≤ K - 1 := by have := Nat.mod_lt Msum (show 0 < K by omega); omega have hcone := (cone_at_grid K hK a b φ ha_pos hb_pos hab hφl hφr (Msum % K) hjlt).2 have hsp : Real.sin (σ + b) * Real.sin σ = Real.sin ((((Msum % K : ℕ) : ℝ) * π / K + φ) + b) * Real.sin (((Msum % K : ℕ) : ℝ) * π / K + φ) := by rw [hσ]; exact sin_prod_grid b φ K Msum (by omega) have hsp' : 0 ≤ Real.sin (σ + b) * Real.sin σ := by rw [hsp]; exact hcone have h4 : (0 : ℝ) ≤ 4 * Real.sin δ ^ 2 := by positivity have hsqrt : (0 : ℝ) ≤ Real.sqrt ((1 - Mp) ^ 2 + Mq ^ 2) := Real.sqrt_nonneg _ nlinarith [mul_nonneg (mul_nonneg h4 hsqrt) hsp'] /-! ### The geometric core (FULLY PROVED) At an interior-feasible parameter the projected cycle data has all pairwise secant slopes in `[μ,L]`. The proof: `slope_mem_of_cone` turns "slope ∈ [μ,L]" into the two real cone signs; `cone1_holds`/`cone2_holds` discharge those signs for every pair (via `cone*_stp → cone*_arg → grid_reduce + sin_shift_periodic → cone_at_grid`); the `ZMod` neighbor wrappings (`cos_succ_periodic`, `cos_pred_periodic`) put `hbGrad` into the bridge form; and the operator facts (`0 0 have hα0 : 0 < (m : ℝ) * thetaK K := by rw [thetaK]; positivity have hαπ : (m : ℝ) * thetaK K < π := by rw [thetaK, show (m : ℝ) * (2 * π / (K : ℝ)) = (m : ℝ) * 2 * π / (K : ℝ) by ring, div_lt_iff₀ hKr] nlinarith [Real.pi_pos, h2mK] have hsinpos : 0 < Real.sin ((m : ℝ) * thetaK K) := Real.sin_pos_of_pos_of_lt_pi hα0 hαπ -- operator positivity from feasibility have hMqpos : 0 < Mq μ L γ β m K := by rw [Mq]; exact div_pos (mul_pos (by linarith) hsinpos) hη have hbind : Mq μ L γ β m K * Real.cos (π / (K : ℝ)) ≤ HBTheorem1.Cc (Mp μ L γ β m K) (Mq μ L γ β m K) * Real.sin (π / (K : ℝ)) := (HBTheorem1.binding_iff_tan K (Mp μ L γ β m K) (Mq μ L γ β m K) hK).mpr hfeas have hCpos' : 0 < Mp μ L γ β m K * (1 - Mp μ L γ β m K) - (Mq μ L γ β m K) ^ 2 := by have := HBTheorem1.Cc_pos_of_binding K (Mp μ L γ β m K) (Mq μ L γ β m K) hK hMqpos hbind rwa [HBTheorem1.Cc] at this have hMp0 : 0 < Mp μ L γ β m K := by nlinarith [hCpos', sq_nonneg (Mq μ L γ β m K), sq_nonneg (Mp μ L γ β m K)] have hMp1 : Mp μ L γ β m K < 1 := by nlinarith [hCpos', sq_nonneg (Mq μ L γ β m K), sq_nonneg (1 - Mp μ L γ β m K)] have hab : Real.arctan (Mq μ L γ β m K / Mp μ L γ β m K) + Real.arctan (Mq μ L γ β m K / (1 - Mp μ L γ β m K)) ≤ π / (K : ℝ) := by have hCc : 0 < HBTheorem1.Cc (Mp μ L γ β m K) (Mq μ L γ β m K) := by rw [HBTheorem1.Cc]; exact hCpos' exact (HBTheorem1.binding_iff_angle K (Mp μ L γ β m K) (Mq μ L γ β m K) hK hMqpos hMp0 hMp1 hCc).mp hfeas have hφeq : phiStar μ L γ β m K = (1 / 2) * (Real.arctan (Mq μ L γ β m K / Mp μ L γ β m K) - Real.arctan (Mq μ L γ β m K / (1 - Mp μ L γ β m K))) - π / (2 * (K : ℝ)) := by rw [phiStar, aVal, bVal] intro s t hst set α := (m : ℝ) * thetaK K with hαdef set φ_s := (m : ℝ) * (s.val : ℝ) * thetaK K + phiStar μ L γ β m K with hφs_def set φ_t := (m : ℝ) * (t.val : ℝ) * thetaK K + phiStar μ L γ β m K with hφt_def have hcs : cyclePts μ L γ β r m K s = 2 * r * Real.cos φ_s := by unfold cyclePts; rw [← hφs_def] have hct : cyclePts μ L γ β r m K t = 2 * r * Real.cos φ_t := by unfold cyclePts; rw [← hφt_def] have hcs1 : cyclePts μ L γ β r m K (s + 1) = 2 * r * Real.cos (φ_s + α) := by rw [show φ_s + α = (m : ℝ) * ((s.val : ℝ) + 1) * (2 * π / (K : ℝ)) + phiStar μ L γ β m K by rw [hφs_def, hαdef]; simp only [thetaK]; ring] unfold cyclePts; simp only [thetaK] rw [cos_succ_periodic m K (by omega) (phiStar μ L γ β m K) s] have hcsm1 : cyclePts μ L γ β r m K (s - 1) = 2 * r * Real.cos (φ_s - α) := by rw [show φ_s - α = (m : ℝ) * ((s.val : ℝ) - 1) * (2 * π / (K : ℝ)) + phiStar μ L γ β m K by rw [hφs_def, hαdef]; simp only [thetaK]; ring] unfold cyclePts; simp only [thetaK] rw [cos_pred_periodic m K (by omega) (phiStar μ L γ β m K) s] have hct1 : cyclePts μ L γ β r m K (t + 1) = 2 * r * Real.cos (φ_t + α) := by rw [show φ_t + α = (m : ℝ) * ((t.val : ℝ) + 1) * (2 * π / (K : ℝ)) + phiStar μ L γ β m K by rw [hφt_def, hαdef]; simp only [thetaK]; ring] unfold cyclePts; simp only [thetaK] rw [cos_succ_periodic m K (by omega) (phiStar μ L γ β m K) t] have hctm1 : cyclePts μ L γ β r m K (t - 1) = 2 * r * Real.cos (φ_t - α) := by rw [show φ_t - α = (m : ℝ) * ((t.val : ℝ) - 1) * (2 * π / (K : ℝ)) + phiStar μ L γ β m K by rw [hφt_def, hαdef]; simp only [thetaK]; ring] unfold cyclePts; simp only [thetaK] rw [cos_pred_periodic m K (by omega) (phiStar μ L γ β m K) t] have hΔ : Real.cos φ_s ≠ Real.cos φ_t := fun h => hst (by rw [hcs, hct, h]) have hσeq : (φ_s + φ_t) / 2 = ((m * (s.val + t.val) : ℕ) : ℝ) * π / (K : ℝ) + phiStar μ L γ β m K := by rw [hφs_def, hφt_def]; simp only [thetaK]; push_cast; ring have hc1 := cone1_holds (Mp μ L γ β m K) (Mq μ L γ β m K) (phiStar μ L γ β m K) ((φ_s + φ_t) / 2) ((φ_s - φ_t) / 2) K (m * (s.val + t.val)) hK hMp0 hMp1 hMqpos hab hφeq hσeq have hc2 := cone2_holds (Mp μ L γ β m K) (Mq μ L γ β m K) (phiStar μ L γ β m K) ((φ_s + φ_t) / 2) ((φ_s - φ_t) / 2) K (m * (s.val + t.val)) hK hMp0 hMp1 hMqpos hab hφeq hσeq rw [show (φ_s + φ_t) / 2 + (φ_s - φ_t) / 2 = φ_s by ring, show (φ_s + φ_t) / 2 - (φ_s - φ_t) / 2 = φ_t by ring] at hc1 hc2 rw [hcs, hct, hcs1, hcsm1, hct1, hctm1] unfold hbGrad exact slope_mem_of_cone μ L γ β r α φ_s φ_t (ne_of_gt hγ) hLμ hr hΔ hc1 hc2 /-- **Well-definedness of the forced gradient (PROVED).** Under feasibility, whenever two projected cycle points coincide, the Heavy-Ball-forced gradients there agree - so the prescribed (point, gradient) data is single-valued, discharging the `hwd` hypothesis of `interp_exists`. A coincidence `cos φ_s = cos φ_t` is either the alignment `φ_s = φ_t (mod 2π)` or the reflection `φ_s = -φ_t (mod 2π)`. The reflection is impossible here: it would force `a - b` to be an odd multiple of `π/K`, but `a,b > 0` with `a + b ≤ π/K` pins `|a - b| < π/K`. The alignment shifts both neighbours `φ +- α` equally, so all three arguments of `hbGrad` agree. (No coprimality of `m,K` is needed.) -/ theorem cyclePts_grad_welldef (μ L γ β r : ℝ) (m K : ℕ) (hμ : 0 < μ) (hμL : μ < L) (hK : 3 ≤ K) (hr : 0 < r) (hγ : 0 < γ) (hβ : β < 1) (hm1 : 1 ≤ m) (hm2 : 2 * m < K) (hfeas : Feasible μ L γ β m K) : ∀ s t : ZMod K, cyclePts μ L γ β r m K s = cyclePts μ L γ β r m K t → hbGrad γ β (cyclePts μ L γ β r m K (s - 1)) (cyclePts μ L γ β r m K s) (cyclePts μ L γ β r m K (s + 1)) = hbGrad γ β (cyclePts μ L γ β r m K (t - 1)) (cyclePts μ L γ β r m K t) (cyclePts μ L γ β r m K (t + 1)) := by have hKr : (0 : ℝ) < K := by exact_mod_cast (by omega : 0 < K) have hKne : (K : ℝ) ≠ 0 := ne_of_gt hKr have hLμ : 0 < L - μ := by linarith have hη : 0 < (L - μ) * γ := mul_pos hLμ hγ have h2mK : (2 : ℝ) * (m : ℝ) < (K : ℝ) := by exact_mod_cast hm2 have hα0 : 0 < (m : ℝ) * thetaK K := by rw [thetaK]; positivity have hαπ : (m : ℝ) * thetaK K < π := by rw [thetaK, show (m : ℝ) * (2 * π / (K : ℝ)) = (m : ℝ) * 2 * π / (K : ℝ) by ring, div_lt_iff₀ hKr] nlinarith [Real.pi_pos, h2mK] have hsinpos : 0 < Real.sin ((m : ℝ) * thetaK K) := Real.sin_pos_of_pos_of_lt_pi hα0 hαπ have hMqpos : 0 < Mq μ L γ β m K := by rw [Mq]; exact div_pos (mul_pos (by linarith) hsinpos) hη have hbind : Mq μ L γ β m K * Real.cos (π / (K : ℝ)) ≤ HBTheorem1.Cc (Mp μ L γ β m K) (Mq μ L γ β m K) * Real.sin (π / (K : ℝ)) := (HBTheorem1.binding_iff_tan K (Mp μ L γ β m K) (Mq μ L γ β m K) hK).mpr hfeas have hCpos' : 0 < Mp μ L γ β m K * (1 - Mp μ L γ β m K) - (Mq μ L γ β m K) ^ 2 := by have := HBTheorem1.Cc_pos_of_binding K (Mp μ L γ β m K) (Mq μ L γ β m K) hK hMqpos hbind rwa [HBTheorem1.Cc] at this have hMp0 : 0 < Mp μ L γ β m K := by nlinarith [hCpos', sq_nonneg (Mq μ L γ β m K), sq_nonneg (Mp μ L γ β m K)] have hMp1 : Mp μ L γ β m K < 1 := by nlinarith [hCpos', sq_nonneg (Mq μ L γ β m K), sq_nonneg (1 - Mp μ L γ β m K)] set A := Real.arctan (Mq μ L γ β m K / Mp μ L γ β m K) with hA set B := Real.arctan (Mq μ L γ β m K / (1 - Mp μ L γ β m K)) with hB have hab : A + B ≤ π / (K : ℝ) := by have hCc : 0 < HBTheorem1.Cc (Mp μ L γ β m K) (Mq μ L γ β m K) := by rw [HBTheorem1.Cc]; exact hCpos' exact (HBTheorem1.binding_iff_angle K (Mp μ L γ β m K) (Mq μ L γ β m K) hK hMqpos hMp0 hMp1 hCc).mp hfeas have ha_pos : 0 < A := Real.arctan_pos.mpr (div_pos hMqpos hMp0) have hb_pos : 0 < B := Real.arctan_pos.mpr (div_pos hMqpos (by linarith)) have hπK : 0 < π / (K : ℝ) := div_pos Real.pi_pos hKr have hrange : |A - B| < π / (K : ℝ) := by rw [abs_lt]; constructor <;> linarith have hps : phiStar μ L γ β m K = (1 / 2) * (A - B) - π / (2 * (K : ℝ)) := by rw [phiStar, aVal, bVal, ← hA, ← hB] intro s t hst set α := (m : ℝ) * thetaK K with hαdef set φ_s := (m : ℝ) * (s.val : ℝ) * thetaK K + phiStar μ L γ β m K with hφs_def set φ_t := (m : ℝ) * (t.val : ℝ) * thetaK K + phiStar μ L γ β m K with hφt_def have hcs : cyclePts μ L γ β r m K s = 2 * r * Real.cos φ_s := by unfold cyclePts; rw [← hφs_def] have hct : cyclePts μ L γ β r m K t = 2 * r * Real.cos φ_t := by unfold cyclePts; rw [← hφt_def] have hcs1 : cyclePts μ L γ β r m K (s + 1) = 2 * r * Real.cos (φ_s + α) := by rw [show φ_s + α = (m : ℝ) * ((s.val : ℝ) + 1) * (2 * π / (K : ℝ)) + phiStar μ L γ β m K by rw [hφs_def, hαdef]; simp only [thetaK]; ring] unfold cyclePts; simp only [thetaK] rw [cos_succ_periodic m K (by omega) (phiStar μ L γ β m K) s] have hcsm1 : cyclePts μ L γ β r m K (s - 1) = 2 * r * Real.cos (φ_s - α) := by rw [show φ_s - α = (m : ℝ) * ((s.val : ℝ) - 1) * (2 * π / (K : ℝ)) + phiStar μ L γ β m K by rw [hφs_def, hαdef]; simp only [thetaK]; ring] unfold cyclePts; simp only [thetaK] rw [cos_pred_periodic m K (by omega) (phiStar μ L γ β m K) s] have hct1 : cyclePts μ L γ β r m K (t + 1) = 2 * r * Real.cos (φ_t + α) := by rw [show φ_t + α = (m : ℝ) * ((t.val : ℝ) + 1) * (2 * π / (K : ℝ)) + phiStar μ L γ β m K by rw [hφt_def, hαdef]; simp only [thetaK]; ring] unfold cyclePts; simp only [thetaK] rw [cos_succ_periodic m K (by omega) (phiStar μ L γ β m K) t] have hctm1 : cyclePts μ L γ β r m K (t - 1) = 2 * r * Real.cos (φ_t - α) := by rw [show φ_t - α = (m : ℝ) * ((t.val : ℝ) - 1) * (2 * π / (K : ℝ)) + phiStar μ L γ β m K by rw [hφt_def, hαdef]; simp only [thetaK]; ring] unfold cyclePts; simp only [thetaK] rw [cos_pred_periodic m K (by omega) (phiStar μ L γ β m K) t] have hcoseq : Real.cos φ_s = Real.cos φ_t := by have h := hst; rw [hcs, hct] at h exact mul_left_cancel₀ (by positivity : (2 * r : ℝ) ≠ 0) h have hzero : Real.sin ((φ_s + φ_t) / 2) = 0 ∨ Real.sin ((φ_s - φ_t) / 2) = 0 := by have hcsc := Real.cos_sub_cos φ_s φ_t rw [hcoseq, sub_self] at hcsc rcases mul_eq_zero.mp hcsc.symm with h | h · rcases mul_eq_zero.mp h with h' | h' · exact absurd h' (by norm_num) · exact Or.inl h' · exact Or.inr h rcases hzero with hσ0 | hδ0 · -- reflection alignment: impossible exfalso obtain ⟨n, hn⟩ := Real.sin_eq_zero_iff.mp hσ0 have hσeq : (φ_s + φ_t) / 2 = ((m * (s.val + t.val) : ℕ) : ℝ) * π / (K : ℝ) + phiStar μ L γ β m K := by rw [hφs_def, hφt_def]; simp only [thetaK]; push_cast; ring rw [hσeq, hps] at hn set N : ℕ := m * (s.val + t.val) with hNdef have hkey : A - B = (π / (K : ℝ)) * (2 * (n : ℝ) * (K : ℝ) - 2 * (N : ℝ) + 1) := by field_simp at hn ⊢ ring_nf at hn ⊢ linarith [hn] rw [hkey, abs_mul, abs_of_pos hπK] at hrange have hlt1 : |2 * (n : ℝ) * (K : ℝ) - 2 * (N : ℝ) + 1| < 1 := lt_of_mul_lt_mul_left (by rw [mul_one]; exact hrange) (le_of_lt hπK) have hcast : ((2 * n * (K : ℤ) - 2 * (N : ℤ) + 1 : ℤ) : ℝ) = 2 * (n : ℝ) * (K : ℝ) - 2 * (N : ℝ) + 1 := by push_cast; ring rw [← hcast, ← Int.cast_abs] at hlt1 have hJlt : |2 * n * (K : ℤ) - 2 * (N : ℤ) + 1| < 1 := by exact_mod_cast hlt1 obtain ⟨h1, h2⟩ := abs_lt.mp hJlt have e : 2 * n * (K : ℤ) - 2 * (N : ℤ) + 1 = 2 * (n * (K : ℤ)) - 2 * (N : ℤ) + 1 := by ring rw [e] at h1 h2 generalize n * (K : ℤ) = Q at h1 h2 omega · -- alignment: φ_s = φ_t (mod 2π); propagate to both neighbours obtain ⟨n, hn⟩ := Real.sin_eq_zero_iff.mp hδ0 have hphis : φ_s = φ_t + (n : ℝ) * (2 * π) := by linear_combination (-2 : ℝ) * hn have hshift : ∀ c : ℝ, Real.cos (φ_s + c) = Real.cos (φ_t + c) := by intro c rw [hphis, show φ_t + (n : ℝ) * (2 * π) + c = (φ_t + c) + (n : ℝ) * (2 * π) by ring] exact Real.cos_add_int_mul_two_pi (φ_t + c) n have kα : Real.cos (φ_s + α) = Real.cos (φ_t + α) := hshift α have kmα : Real.cos (φ_s - α) = Real.cos (φ_t - α) := by have h := hshift (-α) rwa [show φ_s + (-α) = φ_s - α by ring, show φ_t + (-α) = φ_t - α by ring] at h unfold hbGrad rw [hcs, hct, hcs1, hct1, hcsm1, hctm1, hcoseq, kα, kmα] /-! ### Cycle existence at feasible parameters (the inverse direction) -/ /-- **Cycle existence.** At an interior-feasible parameter, Heavy-Ball cycles on a nontrivial set of `K` points for some `f ∈ F_{μ,L}`. PROVED modulo `interp_exists` (external); `proj_slopes_in_range` is sorry-free. -/ theorem cycle_exists_of_feasible (μ L γ β r : ℝ) (m K : ℕ) (hμ : 0 < μ) (hμL : μ < L) (hK : 3 ≤ K) (hr : 0 < r) (hγ : 0 < γ) (hβ : β < 1) (hm1 : 1 ≤ m) (hm2 : 2 * m < K) (hfeas : Feasible μ L γ β m K) (hnontriv : ∃ s t : ZMod K, cyclePts μ L γ β r m K s ≠ cyclePts μ L γ β r m K t) : ∃ (f : ℝ → ℝ) (y : ZMod K → ℝ), IsFmuL μ L f ∧ HBCycles γ β f y := by -- gradient data forced by HB on the projected points set y : ZMod K → ℝ := cyclePts μ L γ β r m K with hy set g : ZMod K → ℝ := fun t => hbGrad γ β (y (t - 1)) (y t) (y (t + 1)) with hg -- the projected slopes lie in [μ,L] have hslope := proj_slopes_in_range μ L γ β r m K hμ hμL hK hr hγ hβ hm1 hm2 hfeas -- the data is single-valued: coinciding points carry equal forced gradients have hwd : ∀ s t : ZMod K, y s = y t → g s = g t := fun s t hyst => cyclePts_grad_welldef μ L γ β r m K hμ hμL hK hr hγ hβ hm1 hm2 hfeas s t hyst -- interpolate obtain ⟨f, hf, hgrad⟩ := interp_exists μ L hμ hμL y g hslope hwd refine ⟨f, y, hf, hnontriv, ?_⟩ intro t rw [hgrad t] /-! ### Non-acceleration We define the candidate-acceleration regime **concretely** via the worst-case quadratic convergence rate, then state GTD's containment about it (no opaque placeholder). On the 1D quadratic with curvature `lam`, HB is the linear recurrence `x_{t+1} = (1+β-γ lam) x_t - β x_{t-1}`, whose asymptotic rate is the spectral radius of its companion matrix, i.e. the larger-modulus root of `z^2 - (1+β-γ lam)z + β`. -/ /-- Asymptotic contraction rate of `HB_{γ,β}` on the 1D quadratic with curvature `lam` (larger-modulus root of `z^2 - (1+β-γ lam)z + β`; complex-conjugate case gives `sqrt β`). -/ noncomputable def hbRate (γ β lam : ℝ) : ℝ := let a := 1 + β - γ * lam if a ^ 2 - 4 * β < 0 then Real.sqrt β else max |(a + Real.sqrt (a ^ 2 - 4 * β)) / 2| |(a - Real.sqrt (a ^ 2 - 4 * β)) / 2| /-- Worst-case quadratic rate of `HB_{γ,β}` over the class `Q_{μ,L}` (curvatures in `[μ,L]`). -/ noncomputable def hbWorstRate (μ L γ β : ℝ) : ℝ := ⨆ lam ∈ Set.Icc μ L, hbRate γ β lam /-- **The candidate-acceleration regime (concrete).** `HB_{γ,β}` attains an accelerated worst-case quadratic rate on `Q_{μ,L}`: `hbWorstRate ≤ (1-Cκ)/(1+Cκ)`, `κ = μ/L`. This matches the rate threshold of GTD's non-acceleration corollary. -/ def AccelRegime (C μ L γ β : ℝ) : Prop := hbWorstRate μ L γ β ≤ (1 - C * (μ / L)) / (1 + C * (μ / L)) /-- **GTD containment** (`[GTD25]`): with the absolute constant `C > 50/3`, every parameter attaining the accelerated rate (in the convergence region, so `0 < γ`, `β < 1`) cycles for some mode `(m,K)` with `1 ≤ m`, `2m < K`. External result. -/ axiom accel_implies_feasible (C μ L γ β : ℝ) (hμ : 0 < μ) (hμL : μ < L) (hγ : 0 < γ) (hβ : β < 1) (hC : 50 / 3 < C) (hacc : AccelRegime C μ L γ β) : ∃ (m K : ℕ) (r : ℝ), 3 ≤ K ∧ 0 < r ∧ 1 ≤ m ∧ 2 * m < K ∧ Feasible μ L γ β m K ∧ (∃ s t : ZMod K, cyclePts μ L γ β r m K s ≠ cyclePts μ L γ β r m K t) /-- **1D non-acceleration.** For every parameter that attains the accelerated worst-case quadratic rate (`AccelRegime`, `C > 50/3`) there is an `f ∈ F_{μ,L}(ℝ)` on which Heavy-Ball cycles - hence it does not converge, so the accelerated rate is not actually attained. PROVED modulo the two external axioms (`interp_exists`, `accel_implies_feasible`); the internal geometric argument is fully closed, and `AccelRegime` is now a concrete definition (no opaque placeholder). -/ theorem nonacceleration_1D (C μ L γ β : ℝ) (hμ : 0 < μ) (hμL : μ < L) (hγ : 0 < γ) (hβ : β < 1) (hC : 50 / 3 < C) (hacc : AccelRegime C μ L γ β) : ∃ (K : ℕ) (f : ℝ → ℝ) (y : ZMod K → ℝ), IsFmuL μ L f ∧ HBCycles γ β f y := by obtain ⟨m, K, r, hK, hr, hm1, hm2, hfeas, hnontriv⟩ := accel_implies_feasible C μ L γ β hμ hμL hγ hβ hC hacc obtain ⟨f, y, hf, hcyc⟩ := cycle_exists_of_feasible μ L γ β r m K hμ hμL hK hr hγ hβ hm1 hm2 hfeas hnontriv exact ⟨K, f, y, hf, hcyc⟩ end NonAcc1D