Actual frame renewal for the very correction and flow chosen by the geometric packet factories. Center source matching is derived.

The geometric target of the actual forward or joined primary is the activation time of the next parent frame. These factories are the checked SmoothState renewals with the source-selected amplitude and primary; all target matching is proved from their definitions.

noncomputable def EulerParentPacketFrames.SmoothState.forwardTargetRenewal {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) G.initialCoordinate (↑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) (G.lowGeometry hball).targetTime

The next actual frame, using exactly the forward source primary and its target-normalized amplitude.

Equations

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

theorem EulerParentPacketFrames.SmoothState.forwardTargetRenewal_matches {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) G.initialCoordinate (↑t) (S.evolution.inverse.normalized t 0))) (((A.transverseData m hm J support hSupport).normal.field t) (S.evolution.inverse.normalized t 0))‖ ≤ error) : RenewalAtTarget (G.lowGeometry hball) (S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource)

In particular, the new ray and primary are the old source's actual physical ray and primary at the target, not freely chosen frame vectors.

theorem EulerParentPacketFrames.SmoothState.forwardTargetRenewal_shear {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) G.initialCoordinate (↑t) (S.evolution.inverse.normalized t 0))) (((A.transverseData m hm J support hSupport).normal.field t) (S.evolution.inverse.normalized t 0))‖ ≤ error) : (S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).shear = G.hchild

theorem EulerParentPacketFrames.SmoothState.forwardTargetRenewal_constants {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) G.initialCoordinate (↑t) (S.evolution.inverse.normalized t 0))) (((A.transverseData m hm J support hSupport).normal.field t) (S.evolution.inverse.normalized t 0))‖ ≤ error) : (S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).G = K ∧ (S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).error = error

theorem EulerParentPacketFrames.SmoothState.forwardTargetRenewal_remainder {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) G.initialCoordinate (↑t) (S.evolution.inverse.normalized t 0))) (((A.transverseData m hm J support hSupport).normal.field t) (S.evolution.inverse.normalized t 0))‖ ≤ error) (hT : (G.lowGeometry hball).targetTime ≤ N.T) : ‖((N.transverseData mNext hmNext JNext supportNext hSupportNext).M.field ((N.transverseData mNext hmNext JNext supportNext hSupportNext).clamp (G.lowGeometry hball).targetTime)) 0 - (G.lowGeometry hball).M (G.lowGeometry hball).center (G.lowGeometry hball).targetTime - G.hchild • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit ((G.lowGeometry hball).w (G.lowGeometry hball).center (G.lowGeometry hball).targetTime))) (EulerPacketNormalizedPrimary.unit ((G.lowGeometry hball).r (G.lowGeometry hball).center (G.lowGeometry hball).targetTime))‖ ≤ error

theorem EulerParentPacketFrames.SmoothState.forwardTargetRenewal_parameters {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) G.initialCoordinate (↑t) (S.evolution.inverse.normalized t 0))) (((A.transverseData m hm J support hSupport).normal.field t) (S.evolution.inverse.normalized t 0))‖ ≤ error) (hTilt : (G.lowGeometry hball).tiltError ≤ 1 / 2) : (S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).shear = G.hchild ∧ 0 < (S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).a ∧ |(S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).a / P.a - 1| ≤ (G.lowGeometry hball).couplingError ∧ 0 < (S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).sigma ∧ |G.y⁻¹ ^ 2 * (S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).sigma ^ 2 - 1| ≤ (G.lowGeometry hball).tiltError ∧ 1 / 2 ≤ G.y⁻¹ ^ 2 * (S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).sigma ^ 2 ∧ G.y⁻¹ ^ 2 * (S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).sigma ^ 2 ≤ 3 / 2

theorem EulerParentPacketFrames.SmoothState.forwardTargetRenewal_compression {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) G.initialCoordinate (↑t) (S.evolution.inverse.normalized t 0))) (((A.transverseData m hm J support hSupport).normal.field t) (S.evolution.inverse.normalized t 0))‖ ≤ error) (ht : 0 < (G.lowGeometry hball).targetTime) (hT : (G.lowGeometry hball).targetTime < N.T) (hmargin : 3 * ((G.lowGeometry hball).G + (G.lowGeometry hball).d) + error < (G.lowGeometry hball).compressionScale) : inner ℝ ((((N.transverseData mNext hmNext JNext supportNext hSupportNext).M.field ⟨(G.lowGeometry hball).targetTime, ⋯⟩) 0) (EulerPacketNormalizedPrimary.unit ((S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).m (G.lowGeometry hball).targetTime))) (EulerPacketNormalizedPrimary.unit ((S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).m (G.lowGeometry hball).targetTime)) < 0

theorem EulerParentPacketFrames.SmoothState.forwardTargetRenewal_compression_of_error_le_one {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) G.initialCoordinate (↑t) (S.evolution.inverse.normalized t 0))) (((A.transverseData m hm J support hSupport).normal.field t) (S.evolution.inverse.normalized t 0))‖ ≤ error) (hT : (G.lowGeometry hball).targetTime < N.T) (herror : error ≤ 1) : inner ℝ ((((N.transverseData mNext hmNext JNext supportNext hSupportNext).M.field ⟨(G.lowGeometry hball).targetTime, ⋯⟩) 0) (EulerPacketNormalizedPrimary.unit ((S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).m (G.lowGeometry hball).targetTime))) (EulerPacketNormalizedPrimary.unit ((S.forwardTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext G hball CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).m (G.lowGeometry hball).targetTime)) < 0

noncomputable def EulerParentPacketFrames.SmoothState.joinedTargetRenewal {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) (s : ℝ) (hs : 0 < s) (hsT : s < A.T) (H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial s hs ⋯)) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) s} (G : EulerPacketSourceGeometry.Guards hs hsT P H) (hball : 1 / 2 ≤ G.radius) (hcut : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity s hs hsT H (EulerPacketSourceGeometry.Guards.terminal hs hsT P H G) 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) (G.lowGeometry hball).targetTime

The joined renewal retains the activation-selected endpoint and its actual stationary-history initial trace.

Equations

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

theorem EulerParentPacketFrames.SmoothState.joinedTargetRenewal_matches {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) (s : ℝ) (hs : 0 < s) (hsT : s < A.T) (H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial s hs ⋯)) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) s} (G : EulerPacketSourceGeometry.Guards hs hsT P H) (hball : 1 / 2 ≤ G.radius) (hcut : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity s hs hsT H (EulerPacketSourceGeometry.Guards.terminal hs hsT P H G) 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) : RenewalAtTarget (G.lowGeometry hball) (S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource)

theorem EulerParentPacketFrames.SmoothState.joinedTargetRenewal_shear {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) (s : ℝ) (hs : 0 < s) (hsT : s < A.T) (H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial s hs ⋯)) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) s} (G : EulerPacketSourceGeometry.Guards hs hsT P H) (hball : 1 / 2 ≤ G.radius) (hcut : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity s hs hsT H (EulerPacketSourceGeometry.Guards.terminal hs hsT P H G) 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) : (S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).shear = G.hchild

theorem EulerParentPacketFrames.SmoothState.joinedTargetRenewal_constants {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) (s : ℝ) (hs : 0 < s) (hsT : s < A.T) (H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial s hs ⋯)) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) s} (G : EulerPacketSourceGeometry.Guards hs hsT P H) (hball : 1 / 2 ≤ G.radius) (hcut : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity s hs hsT H (EulerPacketSourceGeometry.Guards.terminal hs hsT P H G) 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) : (S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).G = K ∧ (S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).error = error

theorem EulerParentPacketFrames.SmoothState.joinedTargetRenewal_remainder {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) (s : ℝ) (hs : 0 < s) (hsT : s < A.T) (H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial s hs ⋯)) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) s} (G : EulerPacketSourceGeometry.Guards hs hsT P H) (hball : 1 / 2 ≤ G.radius) (hcut : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity s hs hsT H (EulerPacketSourceGeometry.Guards.terminal hs hsT P H G) 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) (hT : (G.lowGeometry hball).targetTime ≤ N.T) : ‖((N.transverseData mNext hmNext JNext supportNext hSupportNext).M.field ((N.transverseData mNext hmNext JNext supportNext hSupportNext).clamp (G.lowGeometry hball).targetTime)) 0 - (G.lowGeometry hball).M (G.lowGeometry hball).center (G.lowGeometry hball).targetTime - G.hchild • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit ((G.lowGeometry hball).w (G.lowGeometry hball).center (G.lowGeometry hball).targetTime))) (EulerPacketNormalizedPrimary.unit ((G.lowGeometry hball).r (G.lowGeometry hball).center (G.lowGeometry hball).targetTime))‖ ≤ error

theorem EulerParentPacketFrames.SmoothState.joinedTargetRenewal_parameters {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) (s : ℝ) (hs : 0 < s) (hsT : s < A.T) (H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial s hs ⋯)) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) s} (G : EulerPacketSourceGeometry.Guards hs hsT P H) (hball : 1 / 2 ≤ G.radius) (hcut : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity s hs hsT H (EulerPacketSourceGeometry.Guards.terminal hs hsT P H G) 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) (hTilt : (G.lowGeometry hball).tiltError ≤ 1 / 2) : (S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).shear = G.hchild ∧ 0 < (S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).a ∧ |(S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).a / P.a - 1| ≤ (G.lowGeometry hball).couplingError ∧ 0 < (S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).sigma ∧ |G.y⁻¹ ^ 2 * (S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).sigma ^ 2 - 1| ≤ (G.lowGeometry hball).tiltError ∧ 1 / 2 ≤ G.y⁻¹ ^ 2 * (S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).sigma ^ 2 ∧ G.y⁻¹ ^ 2 * (S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).sigma ^ 2 ≤ 3 / 2

theorem EulerParentPacketFrames.SmoothState.joinedTargetRenewal_compression {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) (s : ℝ) (hs : 0 < s) (hsT : s < A.T) (H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial s hs ⋯)) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) s} (G : EulerPacketSourceGeometry.Guards hs hsT P H) (hball : 1 / 2 ≤ G.radius) (hcut : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity s hs hsT H (EulerPacketSourceGeometry.Guards.terminal hs hsT P H G) 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) (ht : 0 < (G.lowGeometry hball).targetTime) (hT : (G.lowGeometry hball).targetTime < N.T) (hmargin : 3 * ((G.lowGeometry hball).G + (G.lowGeometry hball).d) + error < (G.lowGeometry hball).compressionScale) : inner ℝ ((((N.transverseData mNext hmNext JNext supportNext hSupportNext).M.field ⟨(G.lowGeometry hball).targetTime, ⋯⟩) 0) (EulerPacketNormalizedPrimary.unit ((S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).m (G.lowGeometry hball).targetTime))) (EulerPacketNormalizedPrimary.unit ((S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).m (G.lowGeometry hball).targetTime)) < 0

theorem EulerParentPacketFrames.SmoothState.joinedTargetRenewal_compression_of_error_le_one {A N : Parent} (S : SmoothState A) (T : SmoothState N) (hTime : N.T = A.T) {U : Type} [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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (mNext : EulerSmoothLimit.Space) (hmNext : ‖mNext‖ = 1) (JNext : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane mNext)) (supportNext : Set EulerSmoothLimit.Space) (hSupportNext : IsCompact supportNext) (s : ℝ) (hs : 0 < s) (hsT : s < A.T) (H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial s hs ⋯)) {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) s} (G : EulerPacketSourceGeometry.Guards hs hsT P H) (hball : 1 / 2 ≤ G.radius) (hcut : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (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 (G.lowGeometry hball).targetTime N.T, ‖A.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc (G.lowGeometry hball).targetTime N.T, ‖A.centerCurvature t‖ ≤ CH) (hδ : 0 < G.δ) (k : ℝ) (hsource : ∀ (t : ↑(Set.Icc 0 A.T)), (G.lowGeometry hball).targetTime ≤ ↑t → ‖fderiv ℝ (S.velocityIncrement T ↑t) 0 - (G.primaryAmplitude hball * deriv (EulerPeriodicProfile.profile G.δ) (k * inner ℝ m (S.evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity s hs hsT H (EulerPacketSourceGeometry.Guards.terminal hs hsT P H G) 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) (hT : (G.lowGeometry hball).targetTime < N.T) (herror : error ≤ 1) : inner ℝ ((((N.transverseData mNext hmNext JNext supportNext hSupportNext).M.field ⟨(G.lowGeometry hball).targetTime, ⋯⟩) 0) (EulerPacketNormalizedPrimary.unit ((S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).m (G.lowGeometry hball).targetTime))) (EulerPacketNormalizedPrimary.unit ((S.joinedTargetRenewal T hTime m hm J support hSupport mNext hmNext JNext supportNext hSupportNext s hs hsT H G hball hcut CM CH K error hCM hK he hMK hHK hM hH hδ k hsource).m (G.lowGeometry hball).targetTime)) < 0

theorem EulerParentPacketFrames.Evolution.centerStrain_bound {A : Parent} (E : Evolution A) (CM : ℝ) (hCM : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (↑t, y)) x‖ ≤ CM) (t : ℝ) : ‖A.centerStrain t‖ ≤ CM

theorem EulerParentPacketFrames.Evolution.centerCurvature_bound {A : Parent} (E : Evolution A) (CH : ℝ) (hCH : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (E.force t) x‖ ≤ CH) (t : ℝ) : ‖A.centerCurvature t‖ ≤ CH

noncomputable def EulerParentPacketFrames.GeometryForwardChoice.renewal {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : GeometryForwardInput U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (CM CH K : ℝ) (hCM0 : 0 ≤ CM) (hK : 1 ≤ K) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) : EulerPacketSourceGeometry.ParentFrame ((parent I S k hk nextEll hnext hnext1 F).transverseData m hm R support hSupport) (I.geometry.lowGeometry ⋯).targetTime

Renewal, constructed using S.forwardTargetRenewal.

Equations

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

theorem EulerParentPacketFrames.GeometryForwardChoice.renewal_matches {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : GeometryForwardInput U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (CM CH K : ℝ) (hCM0 : 0 ≤ CM) (hK : 1 ≤ K) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) : RenewalAtTarget (I.geometry.lowGeometry ⋯) (F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport)

theorem EulerParentPacketFrames.GeometryForwardChoice.renewal_costs {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : GeometryForwardInput U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (CM CH K : ℝ) (hCM0 : 0 ≤ CM) (hK : 1 ≤ K) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) : (F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).G = K ∧ (F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).error = k ^ (-(1 / 4))

theorem EulerParentPacketFrames.GeometryForwardChoice.renewal_parameters {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : GeometryForwardInput U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (CM CH K : ℝ) (hCM0 : 0 ≤ CM) (hK : 1 ≤ K) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (hTilt : (I.geometry.lowGeometry ⋯).tiltError ≤ 1 / 2) : (F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).shear = I.geometry.hchild ∧ 0 < (F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).a ∧ |(F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).a / I.frame.a - 1| ≤ (I.geometry.lowGeometry ⋯).couplingError ∧ 0 < (F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).sigma ∧ |I.geometry.y⁻¹ ^ 2 * (F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).sigma ^ 2 - 1| ≤ (I.geometry.lowGeometry ⋯).tiltError

theorem EulerParentPacketFrames.GeometryForwardChoice.renewal_compression {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : GeometryForwardInput U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (CM CH K : ℝ) (hCM0 : 0 ≤ CM) (hK : 1 ≤ K) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (e : ℝ) (he : e ≤ 1) : inner ℝ (((F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).B (I.geometry.lowGeometry ⋯).targetTime) (EulerPacketNormalizedPrimary.unit ((F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).m (I.geometry.lowGeometry ⋯).targetTime))) (EulerPacketNormalizedPrimary.unit ((F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).m (I.geometry.lowGeometry ⋯).targetTime)) + e < 0

noncomputable def EulerParentPacketFrames.GeometryJoinedChoice.renewal {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : EulerPacketInitial.Input U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryJoinedChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (CM CH K : ℝ) (hCM0 : 0 ≤ CM) (hK : 1 ≤ K) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) : EulerPacketSourceGeometry.ParentFrame ((parent I S k hk nextEll hnext hnext1 F).transverseData m hm R support hSupport) (I.geometry.lowGeometry ⋯).targetTime

Renewal, constructed using S.joinedTargetRenewal.

Equations

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

theorem EulerParentPacketFrames.GeometryJoinedChoice.renewal_matches {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : EulerPacketInitial.Input U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryJoinedChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (CM CH K : ℝ) (hCM0 : 0 ≤ CM) (hK : 1 ≤ K) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) : RenewalAtTarget (I.geometry.lowGeometry ⋯) (F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport)

theorem EulerParentPacketFrames.GeometryJoinedChoice.renewal_costs {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : EulerPacketInitial.Input U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryJoinedChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (CM CH K : ℝ) (hCM0 : 0 ≤ CM) (hK : 1 ≤ K) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) : (F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).G = K ∧ (F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).error = k ^ (-(1 / 4))

theorem EulerParentPacketFrames.GeometryJoinedChoice.renewal_parameters {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : EulerPacketInitial.Input U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryJoinedChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (CM CH K : ℝ) (hCM0 : 0 ≤ CM) (hK : 1 ≤ K) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (hTilt : (I.geometry.lowGeometry ⋯).tiltError ≤ 1 / 2) : (F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).shear = I.geometry.hchild ∧ 0 < (F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).a ∧ |(F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).a / I.frame.a - 1| ≤ (I.geometry.lowGeometry ⋯).couplingError ∧ 0 < (F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).sigma ∧ |I.geometry.y⁻¹ ^ 2 * (F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).sigma ^ 2 - 1| ≤ (I.geometry.lowGeometry ⋯).tiltError

theorem EulerParentPacketFrames.GeometryJoinedChoice.renewal_compression {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : EulerPacketInitial.Input U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryJoinedChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (CM CH K : ℝ) (hCM0 : 0 ≤ CM) (hK : 1 ≤ K) (hMK : CM ≤ K) (hHK : CM ^ 2 + CH ≤ K ^ 2) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (e : ℝ) (he : e ≤ 1) : inner ℝ (((F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).B (I.geometry.lowGeometry ⋯).targetTime) (EulerPacketNormalizedPrimary.unit ((F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).m (I.geometry.lowGeometry ⋯).targetTime))) (EulerPacketNormalizedPrimary.unit ((F.renewal hSym CM CH K hCM0 hK hMK hHK hCM hCH m hm R support hSupport).m (I.geometry.lowGeometry ⋯).targetTime)) + e < 0