Orthogonality of gradients of functions sharing one scalar coordinate.

theorem AVenhance.Infra.Section5.composed_gradients_sigma_orthogonal {η : Homogenization.Vec 2 → ℝ} {f g : ℝ → ℝ} {x : Homogenization.Vec 2} {L : Homogenization.Vec 2 →L[ℝ] ℝ} {f' g' : ℝ} (hη : HasFDerivAt η L x) (hf : HasDerivAt f f' (η x)) (hg : HasDerivAt g g' (η x)) : Homogenization.vecDot (spaceGrad (fun (y : Homogenization.Vec 2) => f (η y)) x) (sigmaMat.mulVec (spaceGrad (fun (y : Homogenization.Vec 2) => g (η y)) x)) = 0

If two scalar fields are both functions of one scalar coordinate, their gradients are parallel; the rotated gradient pairing therefore vanishes.