Joint source induction for actual higher velocity and gradient jets.

theorem AVenhance.Infra.Section4.amnrSourceJetLevels_advance {β C K : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {cut : ℕ} (hlevels : AmnrSourceJetLevels I Φ K cut) (hK : 1 ≤ K) : ∃ (Knew : ℝ), 1 ≤ Knew ∧ AmnrSourceJetLevels I Φ Knew (cut + 1)

One complete source induction level. The new velocity bound is obtained by actual scale summation; the new gradient bound then uses only lower gradient levels and the just-proved velocity level.

theorem AVenhance.Infra.Section4.amnr_source_jet_levels_exist {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (cut : ℕ) : ∃ (K : ℝ), 1 ≤ K ∧ AmnrSourceJetLevels I Φ K cut

All higher mixed source jets through any finite material cut follow from the stream-regularity estimates and the actual stream construction. No mixed primitive bound is an extra premise. Every level retains its field's weighted source budget.