Public statement.

theorem AVenhance.Ingredients.qMNR_char {β : ℝ} (I : Ingredients β) (κ : ℝ) (hκ : 0 < κ) (m : ℕ) (hm : 1 ≤ m) (n : ℕ) : (∀ (t : ℝ), I.qMNR κ m n 0 t = I.jMN κ m n t - timeAvgMat (I.jMN κ m n)) ∧ (∀ (r : ℕ), Function.Periodic (I.qMNR κ m n r) (4 * tau β I.Λ m)) ∧ (∀ (r : ℕ), 1 ≤ r → timeAvgMat (I.qMNR κ m n r) = 0) ∧ (∀ (r : ℕ) (t : ℝ) (i j : Fin 2), HasDerivAt (fun (s : ℝ) => I.qMNR κ m n (r + 1) s i j) (-I.qMNR κ m n r t i j) t) ∧ ∀ (q' : ℕ → ℝ → Matrix (Fin 2) (Fin 2) ℝ), (∀ (t : ℝ), q' 0 t = I.jMN κ m n t - timeAvgMat (I.jMN κ m n)) → (∀ (r : ℕ), Function.Periodic (q' r) (4 * tau β I.Λ m)) → (∀ (r : ℕ), 1 ≤ r → timeAvgMat (q' r) = 0) → (∀ (r : ℕ) (t : ℝ) (i j : Fin 2), HasDerivAt (fun (s : ℝ) => q' (r + 1) s i j) (-q' r t i j) t) → ∀ (r : ℕ), q' r = I.qMNR κ m n r

qMNR is the family characterized in e.q.mnr.def (existence and uniqueness), with the period corrected to 4τ_m. Required before FILE 19 lands (source-characterized rule).