Geometric renewal between two actual Euler states. Their spatial regularity, particle velocity laws and fixed origin are supplied by the states themselves; only the quantitative packet expansion is an input.

The literal primary terms in source (20) initialize the next geometric parent frame. The forward coordinate is prescribed; the joined coordinate is the genuine stationary history trace and is proved nonzero.

The next source's center expansion follows from the actual physical velocity update. Odd particle displacements fix the origin, and the two literal velocity laws identify the source matrices there.

theorem EulerParentPacketFrames.Parent.position_zero_of_odd (G : Parent) (hodd : ∀ (t : ↑(Set.Icc 0 G.T)), Function.Odd ⇑(G.displacement.field t)) (t : ↑(Set.Icc 0 G.T)) : G.position t 0 = 0

theorem EulerParentPacketFrames.Parent.center_update_of_odd (G N : Parent) (hTime : N.T = G.T) (u w : ℝ → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (u ↑t) x) (hw : ∀ (t : ↑(Set.Icc 0 N.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (w ↑t) x) (hGvelocity : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.velocity.field t) x = u (↑t) (G.position t x)) (hNvelocity : ∀ (t : ↑(Set.Icc 0 N.T)) (x : EulerSmoothLimit.Space), (N.velocity.field t) x = u (↑t) (N.position t x) + w (↑t) (N.position t x)) (hGodd : ∀ (t : ↑(Set.Icc 0 G.T)), Function.Odd ⇑(G.displacement.field t)) (hNodd : ∀ (t : ↑(Set.Icc 0 N.T)), Function.Odd ⇑(N.displacement.field t)) (t : ↑(Set.Icc 0 N.T)) : (N.strain.field t) 0 = G.centerStrain ↑t + fderiv ℝ (w ↑t) 0

noncomputable def EulerParentPacketFrames.Parent.geometryFrameOfPhysicalUpdate (G N : Parent) (hTime : N.T = G.T) (u w : ℝ → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (u ↑t) x) (hw : ∀ (t : ↑(Set.Icc 0 N.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (w ↑t) x) (hGvelocity : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.velocity.field t) x = u (↑t) (G.position t x)) (hNvelocity : ∀ (t : ↑(Set.Icc 0 N.T)) (x : EulerSmoothLimit.Space), (N.velocity.field t) x = u (↑t) (N.position t x) + w (↑t) (N.position t x)) (hGodd : ∀ (t : ↑(Set.Icc 0 G.T)), Function.Odd ⇑(G.displacement.field t)) (hNodd : ∀ (t : ↑(Set.Icc 0 N.T)), Function.Odd ⇑(N.displacement.field t)) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNew : EulerSmoothLimit.Space) (hmNew : ‖mNew‖ = 1) (RNew : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNew)) (SNew : Set EulerSmoothLimit.Space) (hSNew : IsCompact SNew) (τ : ℝ) (hτ : 0 ≤ τ) (η : U) (hη : η ≠ 0) (c CM CH K error : ℝ) (hCM : 0 ≤ CM) (hK : 1 ≤ K) (he : 0 ≤ error) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hM : ∀ t ∈ Set.Icc τ N.T, ‖G.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc τ N.T, ‖G.centerCurvature t‖ ≤ CH) (hpacket : ∀ t ∈ Set.Icc τ N.T, ‖fderiv ℝ (w t) 0 - c • ((InnerProductSpace.rankOne ℝ) (G.sourceVelocity m hm R S hS η t)) (G.sourceNormal m t)‖ ≤ error) : EulerPacketSourceGeometry.ParentFrame (N.transverseData mNew hmNew RNew SNew hSNew) τ

Concrete old/new-parent factory. The source matrix split is derived from the two physical velocity identities. The remaining quantitative inputs are the preceding packet's center shear error and parent low norm bounds, as used by the geometric induction.

Equations

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

theorem EulerParentPacketFrames.Parent.forward_primary_center_term (G : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (η : U) (δ : ℝ) (hδ : 0 < δ) (α k : ℝ) (t : ↑(Set.Icc 0 G.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hY : Y 0 = 0) : (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ m (Y 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity (G.transverseData m hm R S hS) η (↑t) (Y 0))) (((G.transverseData m hm R S hS).normal.field t) (Y 0)) = (α / δ) • ((InnerProductSpace.rankOne ℝ) (G.sourceVelocity m hm R S hS η ↑t)) (G.sourceNormal m ↑t)

theorem EulerParentPacketFrames.Parent.joined_primary_center_term (G : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (s : ℝ) (hs : 0 < s) (hsT : s < G.T) (B : EulerTransversePacketProvider.HistoryData ((G.transverseData m hm R S hS).initial s hs ⋯)) (ξ : U) (hcut : tsupport EulerSpatialCutoffs.innerCutoff ⊆ S) (δ : ℝ) (hδ : 0 < δ) (α k : ℝ) (t : ↑(Set.Icc 0 G.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hY : Y 0 = 0) : (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ m (Y 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity s hs hsT B ξ hcut (↑t) (Y 0))) (((G.transverseData m hm R S hS).normal.field t) (Y 0)) = (α / δ) • ((InnerProductSpace.rankOne ℝ) (G.sourceVelocity m hm R S hS (((B.coefficients.labelCoordinate 0) ξ) ⟨0, ⋯⟩) ↑t)) (G.sourceNormal m ↑t)

noncomputable def EulerParentPacketFrames.Parent.forwardGeometryFrame (G : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (N : Parent) (hTime : N.T = G.T) (u w : ℝ → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (u ↑t) x) (hw : ∀ (t : ↑(Set.Icc 0 N.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (w ↑t) x) (hGvelocity : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.velocity.field t) x = u (↑t) (G.position t x)) (hNvelocity : ∀ (t : ↑(Set.Icc 0 N.T)) (x : EulerSmoothLimit.Space), (N.velocity.field t) x = u (↑t) (N.position t x) + w (↑t) (N.position t x)) (hGodd : ∀ (t : ↑(Set.Icc 0 G.T)), Function.Odd ⇑(G.displacement.field t)) (hNodd : ∀ (t : ↑(Set.Icc 0 N.T)), Function.Odd ⇑(N.displacement.field t)) {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNew : EulerSmoothLimit.Space) (hmNew : ‖mNew‖ = 1) (RNew : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNew)) (SNew : Set EulerSmoothLimit.Space) (hSNew : IsCompact SNew) (τ : ℝ) (hτ : 0 ≤ τ) (CM CH K error : ℝ) (hCM : 0 ≤ CM) (hK : 1 ≤ K) (he : 0 ≤ error) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hM : ∀ t ∈ Set.Icc τ N.T, ‖G.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc τ N.T, ‖G.centerCurvature t‖ ≤ CH) (Y : ↑(Set.Icc 0 G.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hY : ∀ (t : ↑(Set.Icc 0 G.T)), Y t 0 = 0) (δ : ℝ) (hδ : 0 < δ) (α k : ℝ) (η : U) (hη : η ≠ 0) (hsource20 : ∀ (t : ↑(Set.Icc 0 G.T)), τ ≤ ↑t → ‖fderiv ℝ (w ↑t) 0 - (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ m (Y t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity (G.transverseData m hm R S hS) η (↑t) (Y t 0))) (((G.transverseData m hm R S hS).normal.field t) (Y t 0))‖ ≤ error) : EulerPacketSourceGeometry.ParentFrame (N.transverseData mNew hmNew RNew SNew hSNew) τ

Forward geometry frame as an element of ParentFrame (N.transverseData mNew hmNew RNew SNew hSNew) τ.

Equations

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

noncomputable def EulerParentPacketFrames.Parent.joinedGeometryFrame (G : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (N : Parent) (hTime : N.T = G.T) (u w : ℝ → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (u ↑t) x) (hw : ∀ (t : ↑(Set.Icc 0 N.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (w ↑t) x) (hGvelocity : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.velocity.field t) x = u (↑t) (G.position t x)) (hNvelocity : ∀ (t : ↑(Set.Icc 0 N.T)) (x : EulerSmoothLimit.Space), (N.velocity.field t) x = u (↑t) (N.position t x) + w (↑t) (N.position t x)) (hGodd : ∀ (t : ↑(Set.Icc 0 G.T)), Function.Odd ⇑(G.displacement.field t)) (hNodd : ∀ (t : ↑(Set.Icc 0 N.T)), Function.Odd ⇑(N.displacement.field t)) {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNew : EulerSmoothLimit.Space) (hmNew : ‖mNew‖ = 1) (RNew : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNew)) (SNew : Set EulerSmoothLimit.Space) (hSNew : IsCompact SNew) (τ : ℝ) (hτ : 0 ≤ τ) (CM CH K error : ℝ) (hCM : 0 ≤ CM) (hK : 1 ≤ K) (he : 0 ≤ error) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hM : ∀ t ∈ Set.Icc τ N.T, ‖G.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc τ N.T, ‖G.centerCurvature t‖ ≤ CH) (Y : ↑(Set.Icc 0 G.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hY : ∀ (t : ↑(Set.Icc 0 G.T)), Y t 0 = 0) (δ : ℝ) (hδ : 0 < δ) (α k s : ℝ) (hs : 0 < s) (hsT : s < G.T) (B : EulerTransversePacketProvider.HistoryData ((G.transverseData m hm R S hS).initial s hs ⋯)) (ξ : U) (hξ : ξ ≠ 0) (hcut : tsupport EulerSpatialCutoffs.innerCutoff ⊆ S) (hsource20 : ∀ (t : ↑(Set.Icc 0 G.T)), τ ≤ ↑t → ‖fderiv ℝ (w ↑t) 0 - (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ m (Y t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity s hs hsT B ξ hcut (↑t) (Y t 0))) (((G.transverseData m hm R S hS).normal.field t) (Y t 0))‖ ≤ error) : EulerPacketSourceGeometry.ParentFrame (N.transverseData mNew hmNew RNew SNew hSNew) τ

Joined geometry frame as an element of ParentFrame (N.transverseData mNew hmNew RNew SNew hSNew) τ.

Equations

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

def EulerParentPacketFrames.SmoothState.velocityIncrement {A N : Parent} (S : SmoothState A) (T : SmoothState N) (t : ℝ) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Velocity increment, given by T.evolution.velocity (t,x)-S.evolution.velocity (t,x).

Equations

• S.velocityIncrement T t x = T.evolution.velocity (t, x) - S.evolution.velocity (t, x)

theorem EulerParentPacketFrames.SmoothState.velocityIncrement_smooth {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) (t : ↑(Set.Icc 0 N.T)) : ContDiff ℝ (↑⊤) (S.velocityIncrement T ↑t)

theorem EulerParentPacketFrames.SmoothState.next_velocity {A N : Parent} (S : SmoothState A) (T : SmoothState N) (t : ↑(Set.Icc 0 N.T)) (x : EulerSmoothLimit.Space) : (N.velocity.field t) x = S.evolution.velocity (↑t, N.position t x) + S.velocityIncrement T (↑t) (N.position t x)

theorem EulerParentPacketFrames.SmoothState.normalized_inverse_zero {A : Parent} (S : SmoothState A) (t : ↑(Set.Icc 0 A.T)) : S.evolution.inverse.normalized t 0 = 0

noncomputable def EulerParentPacketFrames.SmoothState.forwardRenewal {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) (τ : ℝ) (hτ : 0 ≤ τ) (CM CH K error : ℝ) (hCM : 0 ≤ CM) (hK : 1 ≤ K) (he : 0 ≤ error) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hM : ∀ t ∈ Set.Icc τ N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc τ N.T, ‖A.centerCurvature t‖ ≤ CH) (δ : ℝ) (hδ : 0 < δ) (α k : ℝ) (ξ : U) (hξ : ξ ≠ 0) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), τ ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) ξ (↑t) (S.evolution.inverse.normalized t 0))) (((A.transverseData m hm J support hSupport).normal.field t) (S.evolution.inverse.normalized t 0))‖ ≤ error) : EulerPacketSourceGeometry.ParentFrame (N.transverseData mNext hmNext JNext supportNext hSupportNext) τ

Forward renewal, constructed using A.forwardGeometryFrame.

Equations

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

noncomputable def EulerParentPacketFrames.SmoothState.joinedRenewal {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) (τ : ℝ) (hτ : 0 ≤ τ) (CM CH K error : ℝ) (hCM : 0 ≤ CM) (hK : 1 ≤ K) (he : 0 ≤ error) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hM : ∀ t ∈ Set.Icc τ N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc τ N.T, ‖A.centerCurvature t‖ ≤ CH) (δ : ℝ) (hδ : 0 < δ) (α k s : ℝ) (hs : 0 < s) (hsT : s < A.T) (H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial s hs ⋯)) (ξ : U) (hξ : ξ ≠ 0) (hcut : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), τ ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity s hs hsT H ξ hcut (↑t) (S.evolution.inverse.normalized t 0))) (((A.transverseData m hm J support hSupport).normal.field t) (S.evolution.inverse.normalized t 0))‖ ≤ error) : EulerPacketSourceGeometry.ParentFrame (N.transverseData mNext hmNext JNext supportNext hSupportNext) τ

Joined renewal, constructed using A.joinedGeometryFrame.

Equations

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