Quadratic vector algebra for actual material forcing energies.

theorem AVenhance.Infra.Section4.iterate_matrix_vector_sq_bound (Q : Matrix (Fin 2) (Fin 2) ℝ) (u : Homogenization.Vec 2) {D : ℝ} (hQ : ∀ (i j : Fin 2), |Q i j| ≤ D) : Homogenization.vecNormSq (Q.mulVec u) ≤ 4 * D ^ 2 * Homogenization.vecNormSq u

Entrywise matrix control costs four in the actual Euclidean vector square.

theorem AVenhance.Infra.Section4.iterate_vecNormSq_sub_le (u v : Homogenization.Vec 2) : Homogenization.vecNormSq (u - v) ≤ 2 * (Homogenization.vecNormSq u + Homogenization.vecNormSq v)

Subtracting two actual vectors costs at most twice their squared energies.

theorem AVenhance.Infra.Section4.iterate_material_vector_sq_bound (κ : ℝ) (a f e : Homogenization.Vec 2) : Homogenization.vecNormSq (κ • a + f - e) ≤ 2 * κ ^ 2 * Homogenization.vecNormSq a + 4 * Homogenization.vecNormSq f + 4 * Homogenization.vecNormSq e

The three actual terms in a material-gradient equation have a uniform quadratic energy allocation.