Structural identities for the Section 2 construction flow.

theorem AVenhance.Infra.Construction.Section2FlowIdentities.linearMap_apply_two (A : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (v : Homogenization.Vec 2) (i : Fin 2) : A v i = A (Homogenization.basisVec 0) i * v 0 + A (Homogenization.basisVec 1) i * v 1

theorem AVenhance.Infra.Construction.Section2FlowIdentities.continuousLinearMap_det_two (J : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) : J.det = J (Homogenization.basisVec 0) 0 * J (Homogenization.basisVec 1) 1 - J (Homogenization.basisVec 1) 0 * J (Homogenization.basisVec 0) 1

theorem AVenhance.Infra.Construction.left_inverse_entries_of_det_one {A B : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hcomp : A ∘SL B = ContinuousLinearMap.id ℝ (Homogenization.Vec 2)) (hdet : B.det = 1) : A (Homogenization.basisVec 0) 0 = B (Homogenization.basisVec 1) 1 ∧ A (Homogenization.basisVec 1) 0 = -B (Homogenization.basisVec 1) 0 ∧ A (Homogenization.basisVec 0) 1 = -B (Homogenization.basisVec 0) 1 ∧ A (Homogenization.basisVec 1) 1 = B (Homogenization.basisVec 0) 0

In two dimensions, a left inverse of a determinant-one map is its cofactor transpose. The four coordinate equalities are the form used in c.material.DX.Xinv.

theorem AVenhance.Infra.Construction.spatialDivergence_eq_vecDiv {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) (t : ℝ) (x : Homogenization.Vec 2) : Flow.spatialDivergence b t x = vecDiv (b t) x

The spatial derivative trace used in Liouville's formula is the classical divergence of a smooth spatial slice.

theorem AVenhance.Infra.Construction.streamVel_spatialDivergence_eq_zero {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (t : ℝ) (x : Homogenization.Vec 2) : Flow.spatialDivergence (streamVel φ) t x = 0

The velocity from any admissible stream function is classically divergence-free.

theorem AVenhance.Infra.Construction.constructionFlowInvJacobian_det_eq_one {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (s r : ℝ) (x : Homogenization.Vec 2) : (constructionFlowInvJacobian hseq m r s x).det = 1

The inverse-flow spatial derivative also has determinant one.

theorem AVenhance.Infra.Construction.constructionComposedJacobian_comp_inverse_eq_id {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (s r : ℝ) (x : Homogenization.Vec 2) : constructionComposedFlowJacobian hseq m s r x ∘SL constructionFlowInvJacobian hseq m r s x = ContinuousLinearMap.id ℝ (Homogenization.Vec 2)

The forward and inverse variational maps at a fixed pair of times are compositional inverses.

theorem AVenhance.Infra.Construction.constructionComposedJacobian_cofactor_entries {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (s r : ℝ) (x : Homogenization.Vec 2) : (constructionComposedFlowJacobian hseq m s r x) (Homogenization.basisVec 0) 0 = (constructionFlowInvJacobian hseq m r s x) (Homogenization.basisVec 1) 1 ∧ (constructionComposedFlowJacobian hseq m s r x) (Homogenization.basisVec 1) 0 = -(constructionFlowInvJacobian hseq m r s x) (Homogenization.basisVec 1) 0 ∧ (constructionComposedFlowJacobian hseq m s r x) (Homogenization.basisVec 0) 1 = -(constructionFlowInvJacobian hseq m r s x) (Homogenization.basisVec 0) 1 ∧ (constructionComposedFlowJacobian hseq m s r x) (Homogenization.basisVec 1) 1 = (constructionFlowInvJacobian hseq m r s x) (Homogenization.basisVec 0) 0

The c.material.DX.Xinv cofactor identity: in two dimensions the composed forward Jacobian is the cofactor transpose of the inverse Jacobian. This identity is pointwise; quantitative derivative bounds are separate.