Construction of geometric source data from the actual parent strain, normal and stationary primary. Only the older homogeneous frame, parent center remainder, low source bounds and numerical guards are inputs.

structure EulerPacketSourceGeometry.ParentFrame {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (τ : ℝ) : Type

The older frame at the fixed center, together with the actual parent strain's center remainder. It contains no new ray, new velocity or amplification assertion.

• B : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

  Bound parameter of ParentFrame, of type ℝ → Space →L[ℝ] Space.

• B₁ : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

  B₁ of ParentFrame, of type ℝ → Space →L[ℝ] Space.

• m : ℝ → EulerSmoothLimit.Space

  M of ParentFrame, of type ℝ → Space.

• v : ℝ → EulerSmoothLimit.Space

  V of ParentFrame, of type ℝ → Space.

• c : ℝ

  C of ParentFrame, of type ℝ.

• G : ℝ

  Geometric data of ParentFrame, of type ℝ.

• error : ℝ

  Error of ParentFrame, of type ℝ.

• G_lower : 1 ≤ self.G
• error_nonneg : 0 ≤ self.error
• B_derivative (t : ℝ) : t ∈ Set.Icc τ D.T → HasDerivWithinAt self.B (self.B₁ t) (Set.Icc τ D.T) t
• ray_equation (t : ℝ) : t ∈ Set.Icc τ D.T → HasDerivWithinAt self.m (-(ContinuousLinearMap.adjoint (self.B t)) (self.m t)) (Set.Icc τ D.T) t
• velocity_equation (t : ℝ) : t ∈ Set.Icc τ D.T → HasDerivWithinAt self.v (-(self.B t) (self.v t) + (2 * inner ℝ (self.m t) ((self.B t) (self.v t)) / ‖self.m t‖ ^ 2) • self.m t) (Set.Icc τ D.T) t
• ray_nonzero (t : ℝ) : t ∈ Set.Icc τ D.T → self.m t ≠ 0
• velocity_nonzero (t : ℝ) : t ∈ Set.Icc τ D.T → self.v t ≠ 0
• tangent (t : ℝ) : t ∈ Set.Icc τ D.T → inner ℝ (self.m t) (self.v t) = 0
• B_bound (t : ℝ) : t ∈ Set.Icc τ D.T → ‖self.B t‖ ≤ self.G
• B₁_bound (t : ℝ) : t ∈ Set.Icc τ D.T → ‖self.B₁ t‖ ≤ self.G ^ 2
• remainder_bound (t : ℝ) : t ∈ Set.Icc τ D.T → ‖(D.M.field (D.clamp t)) 0 - self.B t - EulerPacketMovingFrame.primaryShear self.c self.m self.v t • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit (self.v t))) (EulerPacketNormalizedPrimary.unit (self.m t))‖ ≤ self.error

noncomputable def EulerPacketSourceGeometry.ParentFrame.a {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (P : ParentFrame D τ) : ℝ

A, given by normalizedCoupling (P.B τ) (P.m τ) (P.v τ).

Equations

• P.a = EulerPacketMovingFrame.normalizedCoupling (P.B τ) (P.m τ) (P.v τ)

noncomputable def EulerPacketSourceGeometry.ParentFrame.sigma {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (P : ParentFrame D τ) : ℝ

Sigma, given by Real.sqrt (normalizedTilt (P.B τ) (P.m τ) (P.v τ)).

Equations

• P.sigma = √(EulerPacketMovingFrame.normalizedTilt (P.B τ) (P.m τ) (P.v τ))

noncomputable def EulerPacketSourceGeometry.ParentFrame.shear {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (P : ParentFrame D τ) : ℝ

Shear, given by primaryShear P.c P.m P.v τ.

Equations

• P.shear = EulerPacketMovingFrame.primaryShear P.c P.m P.v τ

noncomputable def EulerPacketSourceGeometry.ParentFrame.epsilon {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (P : ParentFrame D τ) : ℝ

Epsilon, given by Real.sqrt (P.a/P.shear).

Equations

• P.epsilon = √(P.a / P.shear)

noncomputable def EulerPacketSourceGeometry.ParentFrame.horizon {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (P : ParentFrame D τ) : ℝ

Horizon, given by P.a*(D.T-τ)/P.epsilon.

Equations

• P.horizon = P.a * (D.T - τ) / P.epsilon

noncomputable def EulerPacketSourceGeometry.ParentFrame.rayScale {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (P : ParentFrame D τ) (hτ : 0 < τ) (hτT : τ < D.T) : ℝ

Ray scale, given by activationRayScale (D.deformationEquiv ⟨τ,hτ.le,hτT.le⟩ 0) (cross (unit (P.m τ)) (unit (P.v τ))).

Equations

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

noncomputable def EulerPacketSourceGeometry.ParentFrame.terminalBound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (P : ParentFrame D τ) (CM CH : ℝ) : ℝ

Terminal bound, given by 8*(activationConstant CM CH+1)*D.inverseBound/P.shear.

Equations

• P.terminalBound CM CH = 8 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) * D.inverseBound / P.shear

noncomputable def EulerPacketSourceGeometry.ParentFrame.neighborCost {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (P : ParentFrame D τ) (hτ : 0 < τ) (hτT : τ < D.T) (H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (CM CH : ℝ) : ℝ

Neighbor cost as an element of ℝ.

Equations

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

noncomputable def EulerPacketSourceGeometry.ParentFrame.totalError {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (P : ParentFrame D τ) (hτ : 0 < τ) (hτT : τ < D.T) (H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (CM CH ρ : ℝ) : ℝ

Total error, given by P.error+P.neighborCost hτ hτT H CM CH*ρ.

Equations

• P.totalError hτ hτT H CM CH ρ = P.error + P.neighborCost hτ hτT H CM CH * ρ

structure EulerPacketSourceGeometry.Guards {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (hτ : 0 < τ) (hτT : τ < D.T) (P : ParentFrame D τ) (H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) : Type

Source and scalar guards, all stated before the new primary is constructed. The neighbor cost is the explicit coefficient expression.

• CM : ℝ

  CM of Guards, of type ℝ.

• CH : ℝ

  CH of Guards, of type ℝ.

• ζ : ℝ

  Ζ of Guards, of type ℝ.

• radius : ℝ

  Radius of Guards, of type ℝ.

• y : ℝ

  Y of Guards, of type ℝ.

• δ : ℝ

  Δ of Guards, of type ℝ.

• hchild : ℝ

  Hchild of Guards, of type ℝ.

• CM_nonneg : 0 ≤ self.CM
• CH_nonneg : 0 ≤ self.CH
• zeta_nonneg : 0 ≤ self.ζ
• radius_nonneg : 0 ≤ self.radius
• delta_nonneg : 0 ≤ self.δ
• child_nonneg : 0 ≤ self.hchild
• coupling_lower : 1 / 2 ≤ P.a
• shear_pos : 0 < P.shear
• sigma_pos : 0 < P.sigma
• sigma_small : P.sigma ≤ 1 / 4
• epsilon_small : P.epsilon ≤ 1
• y_pos : 0 < self.y
• y_small : self.y ≤ 1 / 2
• target_le_horizon : self.y⁻¹ / P.sigma ≤ P.horizon
• horizon_lower : 1 ≤ P.horizon
• short_extension : P.horizon - self.y⁻¹ / P.sigma ≤ 1
• small : 1000000 * EulerPacketMovingFrame.neighborStabilityConstant * (16 * (P.epsilon * P.horizon * (4 * P.G) ^ 2 + P.totalError hτ hτT H self.CM self.CH self.radius)) * P.horizon ^ 40 ≤ 1
• compression_guard : 60 * (P.G + P.totalError hτ hτT H self.CM self.CH self.radius) * (self.y⁻¹ / P.sigma) * P.epsilon < P.a
• normal_choice : D.m₀ = EulerPacketMovingFrame.activationDirection (D.deformationEquiv ⟨τ, ⋯⟩ 0) (EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (P.m τ)) (EulerPacketNormalizedPrimary.unit (P.v τ)))
• history_symmetric (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) : (↑((H.H.field t) 0)).IsSymmetric
• history_layer : 1 ≤ P.shear * τ
• history_strain (t : ↑(Set.Icc 0 τ)) : ‖((D.initial τ hτ ⋯).M.field t) 0‖ ≤ self.CM * P.shear
• history_hessian : ‖H.coefficients.labelHessian 0‖ ≤ self.CH * P.shear ^ 2
• activation_small : 16 * (EulerTransverseActivationSelection.activationConstant self.CM self.CH + 1) * self.ζ ≤ 1
• activation_error : P.G + P.error ≤ self.ζ * P.shear
• activation_compression : inner ℝ (((D.M.field ⟨τ, ⋯⟩) 0) (EulerPacketNormalizedPrimary.unit (P.m τ))) (EulerPacketNormalizedPrimary.unit (P.m τ)) < 0

theorem EulerPacketSourceGeometry.Guards.a_pos {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (hτ : 0 < τ) (hτT : τ < D.T) (P : ParentFrame D τ) (H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (A : Guards hτ hτT P H) : 0 < P.a

theorem EulerPacketSourceGeometry.Guards.epsilon_pos {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (hτ : 0 < τ) (hτT : τ < D.T) (P : ParentFrame D τ) (H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (A : Guards hτ hτT P H) : 0 < P.epsilon

theorem EulerPacketSourceGeometry.Guards.rayScale_pos {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (hτ : 0 < τ) (hτT : τ < D.T) (P : ParentFrame D τ) : 0 < P.rayScale hτ hτT

theorem EulerPacketSourceGeometry.Guards.terminalBound_nonneg {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (hτ : 0 < τ) (hτT : τ < D.T) (P : ParentFrame D τ) (H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (A : Guards hτ hτT P H) : 0 ≤ P.terminalBound A.CM A.CH

theorem EulerPacketSourceGeometry.Guards.neighborCost_nonneg {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (hτ : 0 < τ) (hτT : τ < D.T) (P : ParentFrame D τ) (H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (A : Guards hτ hτT P H) : 0 ≤ P.neighborCost hτ hτT H A.CM A.CH

theorem EulerPacketSourceGeometry.Guards.totalError_nonneg {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (hτ : 0 < τ) (hτT : τ < D.T) (P : ParentFrame D τ) (H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (A : Guards hτ hτT P H) : 0 ≤ P.totalError hτ hτT H A.CM A.CH A.radius

theorem EulerPacketSourceGeometry.Guards.activation_perturbation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (hτ : 0 < τ) (hτT : τ < D.T) (P : ParentFrame D τ) (H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (A : Guards hτ hτT P H) : ‖(D.M.field ⟨τ, ⋯⟩) 0 - P.shear • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit (P.v τ))) (EulerPacketNormalizedPrimary.unit (P.m τ))‖ ≤ A.ζ * P.shear

theorem EulerPacketSourceGeometry.Guards.selection {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} [CompleteSpace U] (hτ : 0 < τ) (hτT : τ < D.T) (P : ParentFrame D τ) (H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (A : Guards hτ hτT P H) : 0 < P.rayScale hτ hτT ∧ EulerPacketMovingFrame.scaledRay P.m P.v (fun (s : ℝ) => (D.normal.field (D.clamp s)) 0) (P.rayScale hτ hτT) τ P.a P.epsilon 0 = ![0, 0, 1] ∧ ∃ (ξ : U) (lam : ℝ), ξ ≠ 0 ∧ 0 ≤ lam ∧ lam ≤ 8 * (EulerTransverseActivationSelection.activationConstant A.CM A.CH + 1) / P.epsilon ∧ ‖ξ‖ ≤ P.terminalBound A.CM A.CH ∧ EulerPacketMovingFrame.scaledVelocity P.m P.v (fun (s : ℝ) => EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT H ξ s 0) τ P.a P.epsilon 0 0 = -lam ∧ EulerPacketMovingFrame.scaledVelocity P.m P.v (fun (s : ℝ) => EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT H ξ s 0) τ P.a P.epsilon 0 1 = 1

noncomputable def EulerPacketSourceGeometry.Guards.terminal {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} [CompleteSpace U] (hτ : 0 < τ) (hτT : τ < D.T) (P : ParentFrame D τ) (H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (A : Guards hτ hτT P H) : U

Terminal, given by A.selection.2.2.choose.

Equations

• EulerPacketSourceGeometry.Guards.terminal hτ hτT P H A = ⋯.choose

noncomputable def EulerPacketSourceGeometry.Guards.slope {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} [CompleteSpace U] (hτ : 0 < τ) (hτT : τ < D.T) (P : ParentFrame D τ) (H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (A : Guards hτ hτT P H) : ℝ

Slope, given by A.selection.2.2.choose_spec.choose.

Equations

• EulerPacketSourceGeometry.Guards.slope hτ hτT P H A = ⋯.choose

theorem EulerPacketSourceGeometry.Guards.terminal_properties {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} [CompleteSpace U] (hτ : 0 < τ) (hτT : τ < D.T) (P : ParentFrame D τ) (H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (A : Guards hτ hτT P H) : terminal hτ hτT P H A ≠ 0 ∧ 0 ≤ slope hτ hτT P H A ∧ slope hτ hτT P H A ≤ 8 * (EulerTransverseActivationSelection.activationConstant A.CM A.CH + 1) / P.epsilon ∧ ‖terminal hτ hτT P H A‖ ≤ P.terminalBound A.CM A.CH ∧ EulerPacketMovingFrame.scaledVelocity P.m P.v (fun (s : ℝ) => EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT H (terminal hτ hτT P H A) s 0) τ P.a P.epsilon 0 0 = -slope hτ hτT P H A ∧ EulerPacketMovingFrame.scaledVelocity P.m P.v (fun (s : ℝ) => EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT H (terminal hτ hτT P H A) s 0) τ P.a P.epsilon 0 1 = 1