Source indexing bridges between the finite A/q sums and H_{m,r} and endpoint definitions.

theorem AVenhance.Infra.Section5.FrozenHmSourceIdentity.vecDot_spaceGrad_eq_fderiv {f : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (v : Homogenization.Vec 2) : Homogenization.vecDot v (spaceGrad f x) = (fderiv ℝ f x) v

theorem AVenhance.Infra.Section5.amnrPairFluxSum_eq_nested {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m N : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (z : ST) : amnrPairFluxSum I hΦ m N κ T r z = fun (i : Fin 2) => ∑ n ∈ Finset.range N, ∑ j : Fin 2, ∑ k : Fin 2, I.Amnr hΦ m κ n T r z.1 z.2 i j k * I.qMNR κ m n (r + 1) z.1 j k

theorem AVenhance.Infra.Section5.amnrPairEndpointFluxSum_eq_nested {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m N : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (z : ST) : amnrPairEndpointFluxSum I hΦ m N κ T r z = fun (i : Fin 2) => ∑ n ∈ Finset.range N, ∑ j : Fin 2, ∑ k : Fin 2, I.Amnr hΦ m κ n T r z.1 z.2 i j k * I.qMNR κ m n r z.1 j k

theorem AVenhance.Infra.Section5.frozen_Hmr_eq_stDiv_pairFluxSum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (t : ℝ) (x : Homogenization.Vec 2) (hF : DifferentiableAt ℝ (amnrPairFluxSum I hΦ m (Nstar β) κ T r) (t, x)) : I.Hmr hΦ m κ T r t x = stDiv (amnrPairFluxSum I hΦ m (Nstar β) κ T r) (t, x)

Hmr is the spacetime divergence of its finite A_r q_{r+1} flux. This is the exact source-indexing bridge, with only differentiability needed to identify slice derivatives with spacetime derivatives.

theorem AVenhance.Infra.Section5.frozen_hmEndpoint_eq_stDiv_pairEndpointFluxSum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (t : ℝ) (x : Homogenization.Vec 2) (hF : DifferentiableAt ℝ (amnrPairEndpointFluxSum I hΦ m (Nstar β) κ T r) (t, x)) : hmEndpoint I hΦ m κ T r t x = stDiv (amnrPairEndpointFluxSum I hΦ m (Nstar β) κ T r) (t, x)

The finite endpoint divergence is the corresponding spacetime divergence of the A_r q_r flux.

theorem AVenhance.Infra.Section5.frozen_Hmr_material_step {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (t : ℝ) (x : Homogenization.Vec 2) (ht : 0 < t) (hb : ContDiff ℝ 2 fun (z : ST) => streamVel (Φ (m - 1)) z.1 z.2) (hdiv : ∀ (z : ST), stDiv (fun (w : ST) => streamVel (Φ (m - 1)) w.1 w.2) z = 0) (hA : ∀ (n : ℕ) (i j k : Fin 2) (z : ST), 0 < z.1 → DifferentiableAt ℝ (fun (w : ST) => I.Amnr hΦ m κ n T r w.1 w.2 i j k) z) (hPair : ∀ (a : AmnrPairIndex) (z : ST), 0 < z.1 → DifferentiableAt ℝ (amnrPairFlux I hΦ m κ T r a) z) (hFlux : ContDiffAt ℝ 2 (amnrPairFluxSum I hΦ m (Nstar β) κ T r) (t, x)) (hEndNext : DifferentiableAt ℝ (amnrPairEndpointFluxSum I hΦ m (Nstar β) κ T (r + 1)) (t, x)) (hEnd : DifferentiableAt ℝ (amnrPairEndpointFluxSum I hΦ m (Nstar β) κ T r) (t, x)) : deriv (fun (s : ℝ) => I.Hmr hΦ m κ T r s x) t + (fderiv ℝ (I.Hmr hΦ m κ T r t) x) (streamVel (Φ (m - 1)) t x) = hmEndpoint I hΦ m κ T (r + 1) t x - hmEndpoint I hΦ m κ T r t x

The finite step is exactly the Hmr material equation. The assumptions are regularity of the finite source fluxes and endpoint fluxes; the proof uses the per-index recurrence and divergence-free transport proved above.