The two-dimensional cofactor-divergence identity for smooth maps.

theorem AVenhance.Infra.Section5.FlowPiolaDivergence.rowCofactor_00 (A : Matrix (Fin 2) (Fin 2) ℝ) : rowCofactor A 0 0 = A 1 1

theorem AVenhance.Infra.Section5.FlowPiolaDivergence.rowCofactor_01 (A : Matrix (Fin 2) (Fin 2) ℝ) : rowCofactor A 0 1 = -A 1 0

theorem AVenhance.Infra.Section5.FlowPiolaDivergence.rowCofactor_10 (A : Matrix (Fin 2) (Fin 2) ℝ) : rowCofactor A 1 0 = -A 0 1

theorem AVenhance.Infra.Section5.FlowPiolaDivergence.rowCofactor_11 (A : Matrix (Fin 2) (Fin 2) ℝ) : rowCofactor A 1 1 = A 0 0

theorem AVenhance.Infra.Section5.FlowPiolaDivergence.gradMatrix_entry_hasFDerivAt_of_contDiff {M : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} (hM : ContDiff ℝ 2 M) (i j : Fin 2) : HasFDerivAt (fun (y : Homogenization.Vec 2) => gradMatrix M y i j) (ContinuousLinearMap.proj j ∘SL (fderiv ℝ (fderiv ℝ M) x).flip (Homogenization.basisVec i)) x

theorem AVenhance.Infra.Section5.rowCofactor_gradMatrix_piolaInputs {M : Homogenization.Vec 2 → Homogenization.Vec 2} (hM : ContDiff ℝ 2 M) (x : Homogenization.Vec 2) : (∀ (i j : Fin 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => rowCofactor (gradMatrix M y) i j) (fderiv ℝ (fun (y : Homogenization.Vec 2) => rowCofactor (gradMatrix M y) i j) x) x) ∧ ∀ (j : Fin 2), ∑ i : Fin 2, (fderiv ℝ (fun (y : Homogenization.Vec 2) => rowCofactor (gradMatrix M y) i j) x) (Homogenization.basisVec i) = 0

The cofactor of the row-Jacobian of a C² map has zero column divergence. This is the coordinate Piola identity; no volume-preservation hypothesis is needed.

theorem AVenhance.Infra.Section5.xFlowInv_cofactor_piolaInputs {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : (∀ (i j : Fin 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => rowCofactor (gradMatrix (I.xFlowInv hΦ m l t) y) i j) (fderiv ℝ (fun (y : Homogenization.Vec 2) => rowCofactor (gradMatrix (I.xFlowInv hΦ m l t) y) i j) x) x) ∧ ∀ (j : Fin 2), ∑ i : Fin 2, (fderiv ℝ (fun (y : Homogenization.Vec 2) => rowCofactor (gradMatrix (I.xFlowInv hΦ m l t) y) i j) x) (Homogenization.basisVec i) = 0

The inverse-flow cofactor has differentiable entries and zero column divergence. The C² inverse-flow slice is supplied by the flow regularity bridge.