theorem landscape_structure (e : NSectorEconomy N) (n : Fin N)
    (hKeff : 0 < sectorEffectiveCurvature e n) :
    -- The sector-n component of the landscape is strictly convex
    -- on 1⊥ when K_eff_n > 0 (sub-critical regime).
    -- We state the algebraic consequence: the relaxation rate is
    -- strictly positive, ensuring convergence to equilibrium.
    0 < sectorRelaxRate e n := by
  simp only [sectorRelaxRate]
  apply mul_pos
  · apply mul_pos (e.hℓ n) (abs_pos.mpr _)
    simp only [logCesEigenvaluePerp]
    apply div_ne_zero
    · simp only [neg_ne_zero]; linarith [e.hρ n]
    · exact mul_ne_zero (Nat.cast_ne_zero.mpr (by have := e.hJ n; omega))
        (pow_ne_zero 2 (ne_of_gt (e.hc n)))
  · -- (1 - T/T*)⁺ > 0 from K_eff > 0
    simp only [sectorEffectiveCurvature, effectiveCurvatureKeff] at hKeff
    have hK : 0 < curvatureK (e.J n) (e.ρ n) := curvatureK_pos (e.hJ n) (e.hρ n)
    have hmax : 0 < max 0 (1 - e.T n / sectorCriticalFriction e n) := by
      by_contra h; push_neg at h
      have := le_antisymm h (le_max_left 0 _)
      rw [this, mul_zero] at hKeff; linarith
    exact hmax

theorem eigenstructure_bridge (e : NSectorEconomy N) (n : Fin N) :
    -- For the block-diagonal (sector-decoupled) case, the eigenvalue of
    -- the dynamics matrix M = W · ∇²V at sector n equals the sector
    -- relaxation rate: μ_n = ℓ_n · |λ_⊥(n)| · (1 - T_n/T*_n)⁺.
    -- This is exactly sectorRelaxRate, proving that the eigenstructure
    -- bridge is definitionally built into the relaxation spectrum.
    sectorRelaxRate e n =
    e.ℓ n * |logCesEigenvaluePerp (e.J n) (e.ρ n) (e.c n)| *
      max 0 (1 - e.T n / sectorCriticalFriction e n) := rfl

theorem decay_factor_in_unit (M : ℝ) (hM : 1 < M) :
    0 < 1 - 1 / M ∧ 1 - 1 / M < 1 := by
  constructor
  · rw [sub_pos, div_lt_one (by linarith)]; linarith
  · linarith [div_pos one_pos (by linarith : (0 : ℝ) < M)]

theorem steady_state_variance (M sig_new : ℝ) (hM : 1 < M) :
    varianceRecurrence (M * sig_new) M sig_new = M * sig_new := by
  simp only [varianceRecurrence]
  have hMne : M ≠ 0 := ne_of_gt (by linarith)
  field_simp
  ring