Family producer for the Piola source rate

hmPiolaSourceRate_onA7 proves the spacetime L² rate HmPiolaSourceRate of the divergence of the regular Piola flux Σ_l ξ̂_l F_lᵀ (𝒥 - K) F_l ∇T, unconditionally on the big-bound premise block. It combines

• the pointwise product-rule bound |Piola| ≤ 32 A · hmPiolaQ (hmPiola_vecDiv_tsum_abs_le), A bounding the entries of 𝒥 - K;
• the flux coefficient rate hm_flux_coefficient_rate_onA7 for A;
• the L² rate of the majorant hmPiolaQ (hmPiolaQ_eLpNorm_rate_onA7);
• the measurability of the actual Piola source on the time cube (hm_actual_pairing_field_measurability).

theorem AVenhance.Infra.Section5.Contracts.hmPiolaSourceRate_onA7 (β C₀ : ℝ) : ∃ (Creg : ℝ) (C₁ : ℝ), Integration.OnA7Instances β C₀ C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => HmPiolaSourceRate I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T Creg √(l2NormSq θ₀)

The Piola source rate, produced on the big-bound premise block.