The endpoint difference uses the left-Jacobian Piola base flux and the d_m vector source.

noncomputable def AVenhance.Infra.Section4.hmFrozenTerminalFlux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The terminal endpoint flux at the index, before taking divergence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section4.hmFrozenBaseFlux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The actual base Piola flux at the zero endpoint.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section4.hmFrozenDFirstFlux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The first (nonterminal) summand of the d_m field.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section4.hmFrozenRegularFlux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The Piola flux left after subtracting the first summand of d_m from the zero-endpoint base flux.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section4.hmFrozenRegularSource {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The previous source pairing, retained for downstream migration. It is no longer the scalar source in the endpoint identity.

Equations

• AVenhance.Infra.Section4.hmFrozenRegularSource I hΦ m κ T t x = AVenhance.Infra.Section5.frob (I.flux κ m t - I.Kmat κ m t) (AVenhance.gradMatrix (AVenhance.Infra.Section5.Gbar I hΦ m T t) x)

noncomputable def AVenhance.Infra.Section4.hmFrozenPiolaSource {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The actual regular scalar in the endpoint split, the divergence of the remaining Piola flux.

Equations

• AVenhance.Infra.Section4.hmFrozenPiolaSource I hΦ m κ T t x = AVenhance.vecDiv (AVenhance.Infra.Section4.hmFrozenRegularFlux I hΦ m κ T t) x

theorem AVenhance.Infra.Section4.HmSourcePairing.hmFrozenBaseFlux_eq_dFirst_add_regular {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : hmFrozenBaseFlux I hΦ m κ T t x = hmFrozenDFirstFlux I hΦ m κ T t x + hmFrozenRegularFlux I hΦ m κ T t x

theorem AVenhance.Infra.Section4.HmSourcePairing.hmFrozenSourceErrorD_eq_dFirst_add_tail {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) : Section5.sourceErrorD I hΦ m κ T t = fun (x : Homogenization.Vec 2) => hmFrozenDFirstFlux I hΦ m κ T t x + hmFrozenTerminalFlux I hΦ m κ T t x

theorem AVenhance.Infra.Section4.HmSourcePairing.hmFrozenPulledFlux_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hT : ContDiff ℝ (↑⊤) (T t)) : ContDiff ℝ (↑⊤) (hmFrozenRegularFlux I hΦ m κ T t)

theorem AVenhance.Infra.Section4.HmSourcePairing.hmSource_vecDiv_add_of_differentiableAt {V W : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} (hV : DifferentiableAt ℝ V x) (hW : DifferentiableAt ℝ W x) : vecDiv (fun (y : Homogenization.Vec 2) => V y + W y) x = vecDiv V x + vecDiv W x

theorem AVenhance.Infra.Section4.hm_frozen_terminal_endpoint_eq_div {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Section5.hmEndpoint I hΦ m κ T (Jcut β) t x = vecDiv (hmFrozenTerminalFlux I hΦ m κ T t) x

The exact terminal endpoint is divergence of the terminal Aq tail.

theorem AVenhance.Infra.Section4.hm_frozen_endpoint_difference_source_split {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} {x : Homogenization.Vec 2} (hT : ContDiff ℝ (↑⊤) (T t)) (hTail : DifferentiableAt ℝ (hmFrozenTerminalFlux I hΦ m κ T t) x) : Section5.hmEndpoint I hΦ m κ T (Jcut β) t x - Section5.hmEndpoint I hΦ m κ T 0 t x = hmFrozenPiolaSource I hΦ m κ T t x + vecDiv (Section5.sourceErrorD I hΦ m κ T t) x

The finite endpoint difference is the divergence of the Piola regular source and the new d_m vector field. This uses the actual zero-endpoint base flux, with each F_l on both sides of the matrix gap.