The finite noncommuting word induction is identified with the source material iterates and packaged as p.material.goal.

theorem AVenhance.Infra.Construction.MaterialGoalAllOrders.material_aux_pure_material_word_eq {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {F : ℝ → Homogenization.Vec 2 → ℝ} (hb : ContDiff ℝ (↑⊤) (constructionJointVector b)) (hF : ContDiff ℝ (↑⊤) (constructionJointScalar F)) (ell : ℕ) : Section4.amnrWord (constructionJointVector b) (List.replicate ell none) (constructionJointScalar F) = constructionJointScalar (constructionMaterialIterate b ell F)

theorem AVenhance.Infra.Construction.MaterialGoalAllOrders.material_aux_mixed_velocity_word_eq {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m ell : ℕ) (i : Fin 2) (α : List (Fin 2)) : (Section4.amnrWord (fun (z : Section4.AmnrSpace) => streamVel (Φ m) z.1 z.2) (Section4.amnrMixedWord α ell) fun (z : Section4.AmnrSpace) => streamVel (Φ m) z.1 z.2 i) = fun (z : Section4.AmnrSpace) => Section4.amnrSpaceWord α (fun (y : Homogenization.Vec 2) => constructionMaterialIterate (streamVel (Φ m)) ell (fun (r : ℝ) (x : Homogenization.Vec 2) => streamVel (Φ m) r x i) z.1 y) z.2

theorem AVenhance.Infra.Construction.MaterialGoalAllOrders.material_aux_fderiv_component {f : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec 2) (i j : Fin 2) : (fderiv ℝ (fun (y : Homogenization.Vec 2) => f y i) x) (Homogenization.basisVec j) = (fderiv ℝ f x) (Homogenization.basisVec j) i

theorem AVenhance.Infra.Construction.MaterialGoalAllOrders.material_aux_gradient_iterate_eq {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : ContDiff ℝ (↑⊤) (constructionJointVector b)) (ell : ℕ) (i j : Fin 2) : (constructionMaterialIterate b ell fun (r : ℝ) (x : Homogenization.Vec 2) => (fderiv ℝ (fun (y : Homogenization.Vec 2) => b r y i) x) (Homogenization.basisVec j)) = materialIterateGradientEntry b ell b i j

theorem AVenhance.Infra.Construction.MaterialGoalAllOrders.material_aux_mixed_gradient_word_eq {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m ell : ℕ) (i j : Fin 2) (α : List (Fin 2)) : Section4.amnrWord (fun (z : Section4.AmnrSpace) => streamVel (Φ m) z.1 z.2) (Section4.amnrMixedWord α ell) (Section4.amnrVelocityGradient (fun (z : Section4.AmnrSpace) => streamVel (Φ m) z.1 z.2) i j) = fun (z : Section4.AmnrSpace) => Section4.amnrSpaceWord α (fun (y : Homogenization.Vec 2) => materialIterateGradientEntry (streamVel (Φ m)) ell (streamVel (Φ m)) i j z.1 y) z.2

theorem AVenhance.Infra.Construction.MaterialGoalAllOrders.material_aux_iteratedFDeriv_component {f : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : Homogenization.Vec 2) (J : Fin n → Fin 2) (i : Fin 2) : ((iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => f y i) x) fun (k : Fin n) => Homogenization.basisVec (J k)) = (iteratedFDeriv ℝ n f x) (fun (k : Fin n) => Homogenization.basisVec (J k)) i

theorem AVenhance.Infra.Construction.MaterialGoalAllOrders.p_material_goal_source_with_levels {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {K : ℝ} (hK : 1 ≤ K) (hlevels : MaterialAuxJetLevels I Φ (2 * Nstar β + 1) K (Nstar β)) (m : ℕ) : PMaterialGoalSourceData I Φ K m

All source-form p.material.goal bounds follow from the spatial stream-regularity estimates and the differentiated recursion. The material cutoff is exactly Nstar; the larger AMNR word budget is only an auxiliary combinatorial allowance.