Extraction of pointwise primitive spatial bounds from the source seminorm.

theorem AVenhance.Infra.Section4.amnr_partial_norm_le_of_barNorm (f : Homogenization.Vec 2 → ℝ) (n : ℕ) (hf : ContDiff ℝ (↑n) f) {R B : ℝ} (hR : 0 < R) (hB : 0 ≤ B) (hb : barNorm n R f ≤ ENNReal.ofReal B) (x : Homogenization.Vec 2) (J : Fin n → Fin 2) : ‖(iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (J j)‖ ≤ B * ↑n.factorial * R ^ n / (↑n + 1) ^ 2

The source seminorm bounds each actual ordered coordinate derivative. The factorial and radius factors are retained exactly.

theorem AVenhance.Infra.Section4.amnr_stream_hessian_le_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (x : Homogenization.Vec 2) (J : Fin 2 → Fin 2) : ‖(iteratedFDeriv ℝ 2 (Φ m t) x) fun (j : Fin 2) => Homogenization.basisVec (J j)‖ ≤ 2 ^ 19 * a β I.Λ m

The precise second-order stream-regularity seminorm gives a universal Hessian bound on an actual stream. This conditional helper consumes the stream-regularity data.