The first amplification stage starts at time zero. Its primary is the actual homogeneous forward solution with a fixed initial coordinate; no stationary-history solve is used in this stage.

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

Forward error, given by P.error+‖D.M.derivative.field‖*radius.

Equations

• P.forwardError radius = P.error + ‖D.M.derivative.field‖ * radius

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

Forward guards data, collecting radius, y, δ, hchild, radius_nonneg, delta_nonneg and their compatibility conditions.

• radius : ℝ

  Radius of ForwardGuards, of type ℝ.

• y : ℝ

  Y of ForwardGuards, of type ℝ.

• δ : ℝ

  Δ of ForwardGuards, of type ℝ.

• hchild : ℝ

  Hchild of ForwardGuards, of type ℝ.

• 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
• 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.forwardError self.radius)) * P.horizon ^ 40 ≤ 1
• compression_guard : 60 * (P.G + P.forwardError self.radius) * (self.y⁻¹ / P.sigma) * P.epsilon < P.a
• initial_frame (x : EulerSmoothLimit.Space) : (D.F.field ⟨0, ⋯⟩) x = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space
• normal_choice : D.m₀ = EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (P.m 0)) (EulerPacketNormalizedPrimary.unit (P.v 0))

theorem EulerPacketSourceGeometry.ForwardGuards.a_pos {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) : 0 < P.a

theorem EulerPacketSourceGeometry.ForwardGuards.epsilon_pos {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) : 0 < P.epsilon

theorem EulerPacketSourceGeometry.ForwardGuards.error_nonneg {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) : 0 ≤ P.forwardError G.radius

noncomputable def EulerPacketSourceGeometry.ForwardGuards.initialCoordinate {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) : U

Initial coordinate, constructed using D.R.symm.

Equations

• G.initialCoordinate = D.R.symm ⟨EulerPacketNormalizedPrimary.unit (P.v 0), ⋯⟩

theorem EulerPacketSourceGeometry.ForwardGuards.initialCoordinate_map {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) : ↑(D.R G.initialCoordinate) = EulerPacketNormalizedPrimary.unit (P.v 0)

theorem EulerPacketSourceGeometry.ForwardGuards.initialCoordinate_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) : ‖G.initialCoordinate‖ = 1

theorem EulerPacketSourceGeometry.ForwardGuards.initialCoordinate_ne_zero {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) : G.initialCoordinate ≠ 0

theorem EulerPacketSourceGeometry.ForwardGuards.initial_inverse {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (x : EulerSmoothLimit.Space) : (D.FInv.field ⟨0, ⋯⟩) x = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space

theorem EulerPacketSourceGeometry.ForwardGuards.initial_normal {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (x : EulerSmoothLimit.Space) : sourceRay D x 0 = EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (P.m 0)) (EulerPacketNormalizedPrimary.unit (P.v 0))

noncomputable def EulerPacketSourceGeometry.ForwardGuards.sourceVelocity {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) [CompleteSpace U] (x : EulerSmoothLimit.Space) (t : ℝ) : EulerSmoothLimit.Space

Source velocity, given by EulerPacketForwardFactorization.uncutVelocity D G.initialCoordinate t x.

Equations

• G.sourceVelocity x t = EulerPacketForwardFactorization.uncutVelocity D G.initialCoordinate t x

theorem EulerPacketSourceGeometry.ForwardGuards.initial_velocity {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) [CompleteSpace U] (x : EulerSmoothLimit.Space) : G.sourceVelocity x 0 = EulerPacketNormalizedPrimary.unit (P.v 0)

theorem EulerPacketSourceGeometry.ForwardGuards.sourceVelocity_equation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) [CompleteSpace U] (x : EulerSmoothLimit.Space) (t : ℝ) (ht : t ∈ Set.Icc 0 D.T) : HasDerivWithinAt (G.sourceVelocity x) (-(sourceMatrix D x t) (G.sourceVelocity x t) + (2 * inner ℝ (sourceRay D x t) ((sourceMatrix D x t) (G.sourceVelocity x t)) / ‖sourceRay D x t‖ ^ 2) • sourceRay D x t) (Set.Icc 0 D.T) t

theorem EulerPacketSourceGeometry.ForwardGuards.sourceRay_equation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} (x : EulerSmoothLimit.Space) (t : ℝ) (ht : t ∈ Set.Icc 0 D.T) : HasDerivWithinAt (sourceRay D x) (-(ContinuousLinearMap.adjoint (sourceMatrix D x t)) (sourceRay D x t)) (Set.Icc 0 D.T) t

theorem EulerPacketSourceGeometry.ForwardGuards.initial_tangent {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) [CompleteSpace U] (x : EulerSmoothLimit.Space) : inner ℝ (sourceRay D x 0) (G.sourceVelocity x 0) = 0

theorem EulerPacketSourceGeometry.ForwardGuards.scaled_ray_initial {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (x : EulerSmoothLimit.Space) : EulerPacketMovingFrame.scaledRay P.m P.v (sourceRay D x) 1 0 P.a P.epsilon 0 = ![0, 0, 1]

theorem EulerPacketSourceGeometry.ForwardGuards.scaled_velocity_initial {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) [CompleteSpace U] (x : EulerSmoothLimit.Space) : EulerPacketMovingFrame.scaledVelocity P.m P.v (G.sourceVelocity x) 0 P.a P.epsilon 0 0 = 0 ∧ EulerPacketMovingFrame.scaledVelocity P.m P.v (G.sourceVelocity x) 0 P.a P.epsilon 0 1 = 1

theorem EulerPacketSourceGeometry.ForwardGuards.sourceError_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (x : EulerSmoothLimit.Space) (hx : ‖x‖ ≤ G.radius) (t : ℝ) (ht : t ∈ Set.Icc 0 D.T) : ‖ParentFrame.sourceError x t‖ ≤ P.forwardError G.radius