Actual classical witnesses for every temperature iterate.
theorem
AVenhance.Infra.Section4.amnr_tIterates_classical_family
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
{κm κprev : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(i : ℕ)
(hi : i ≤ Nstar β)
:
∃ (F : ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel (Φ (m - 1))) κprev F θ₀ (T i)
The starting unforced temperature and the iterate construction supply every classical witness; no energy or differentiated equation is assumed.