Relative Initial Profile

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section5.Contracts.initialLayer_from_relative_profiles (β C₀ A Cs : ℝ) (hCs : 0 < Cs) : ∃ (Ci : ℝ) (C₁ : ℝ), Integration.OnA8Instances β C₀ C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (_g : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => have ν := I.kappaSeq κ M (m - 1); have S := √ν * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (θprev t)); Integration.TPositiveJetsContract I m T A S → Integration.ThetaProfileContract I m ν θprev Cs S → Integration.VIncrementContract I m ν T Cs R S → Integration.InitialLayerContract I hΦ m (I.kappaSeq κ M m) θm T Ci S

Exact relative initial layer from the named positive-jet, gradient-profile, and increment contracts. All constants precede the physical family.