Quantitative parameters at a genuine geometric target. The matching certificate below is proved for the actual state renewal constructors in ParentTargetRenewal; it records equality of the physical matrix and the two physical vectors, rather than postulating their scalar estimates.

noncomputable def EulerPacketMovingFrame.PhysicalGeometryData.couplingError {ι : Type u_1} (G : PhysicalGeometryData ι) : ℝ

Coupling error, given by G.y^4+G.σ^2*G.y^2+8*G.σ*G.y^3 + 30000000*neighborStabilityConstant*G.error*G.Θ^40.

Equations

• G.couplingError = G.y ^ 4 + G.σ ^ 2 * G.y ^ 2 + 8 * G.σ * G.y ^ 3 + 30000000 * EulerPacketMovingFrame.neighborStabilityConstant * G.error * G.Θ ^ 40

noncomputable def EulerPacketMovingFrame.PhysicalGeometryData.tiltError {ι : Type u_1} (G : PhysicalGeometryData ι) : ℝ

Tilt error, given by 1500*G.σ+30000000*neighborStabilityConstant*G.error*G.Θ^40.

Equations

• G.tiltError = 1500 * G.σ + 30000000 * EulerPacketMovingFrame.neighborStabilityConstant * G.error * G.Θ ^ 40

noncomputable def EulerPacketMovingFrame.PhysicalGeometryData.compressionScale {ι : Type u_1} (G : PhysicalGeometryData ι) : ℝ

A lower bound for the magnitude of the leading compressive term.

Equations

• G.compressionScale = G.a / (20 * G.ε * G.target)

theorem EulerPacketMovingFrame.PhysicalGeometryData.start_lt_targetTime {ι : Type u_1} (G : PhysicalGeometryData ι) : G.t₀ < G.targetTime

theorem EulerPacketMovingFrame.PhysicalGeometryData.targetTime_pos {ι : Type u_1} (G : PhysicalGeometryData ι) (hstart : 0 ≤ G.t₀) : 0 < G.targetTime

theorem EulerPacketMovingFrame.PhysicalGeometryData.nextCoupling_pos {ι : Type u_1} (G : PhysicalGeometryData ι) : 0 < G.nextCoupling

theorem EulerPacketMovingFrame.PhysicalGeometryData.nextCoupling_error {ι : Type u_1} (G : PhysicalGeometryData ι) : |G.nextCoupling / G.a - 1| ≤ G.couplingError

theorem EulerPacketMovingFrame.PhysicalGeometryData.nextTilt_error {ι : Type u_1} (G : PhysicalGeometryData ι) : |G.y⁻¹ ^ 2 * G.nextTilt - 1| ≤ G.tiltError

theorem EulerPacketMovingFrame.PhysicalGeometryData.nextTilt_pos {ι : Type u_1} (G : PhysicalGeometryData ι) (herror : G.tiltError ≤ 1 / 2) : 0 < G.nextTilt

theorem EulerPacketMovingFrame.PhysicalGeometryData.compressionScale_pos {ι : Type u_1} (G : PhysicalGeometryData ι) : 0 < G.compressionScale

theorem EulerPacketMovingFrame.PhysicalGeometryData.compression_margin {ι : Type u_1} (G : PhysicalGeometryData ι) {e : ℝ} (he : e ≤ 1) : 3 * (G.G + G.d) + e < G.compressionScale

The existing geometric smallness guard leaves enough compression margin for any subsequent center remainder of size at most one.

theorem EulerPacketMovingFrame.PhysicalGeometryData.nextCompression_le {ι : Type u_1} (G : PhysicalGeometryData ι) : G.nextCompression ≤ -G.compressionScale + 3 * (G.G + G.d)

theorem EulerPacketMovingFrame.PhysicalGeometryData.target_shear_normalization {ι : Type u_1} (G : PhysicalGeometryData ι) (hδ : 0 < G.δ) : G.amplitude / G.δ * G.targetSize = G.hchild

structure EulerParentPacketFrames.RenewalAtTarget {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} (G : EulerPacketMovingFrame.PhysicalGeometryData ι) (P : EulerPacketSourceGeometry.ParentFrame D G.targetTime) : Prop

Exact target matching, supplied by the actual forward or joined SmoothState renewal. In particular the primary is not renormalized.

• matrix_eq : P.B G.targetTime = G.M G.center G.targetTime
• ray_eq : P.m G.targetTime = G.r G.center G.targetTime
• velocity_eq : P.v G.targetTime = G.w G.center G.targetTime
• coefficient_eq : P.c = G.amplitude / G.δ

theorem EulerParentPacketFrames.RenewalAtTarget.a_eq {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) : P.a = G.nextCoupling

theorem EulerParentPacketFrames.RenewalAtTarget.sigma_eq {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) : P.sigma = √G.nextTilt

theorem EulerParentPacketFrames.RenewalAtTarget.shear_eq {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) (hδ : 0 < G.δ) : P.shear = G.hchild

theorem EulerParentPacketFrames.RenewalAtTarget.epsilon_eq {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) (hδ : 0 < G.δ) : P.epsilon = √(P.a / G.hchild)

theorem EulerParentPacketFrames.RenewalAtTarget.normalized_ray_eq {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) : EulerPacketNormalizedPrimary.unit (P.m G.targetTime) = EulerPacketNormalizedPrimary.unit (G.r G.center G.targetTime)

theorem EulerParentPacketFrames.RenewalAtTarget.normalized_velocity_eq {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) : EulerPacketNormalizedPrimary.unit (P.v G.targetTime) = EulerPacketNormalizedPrimary.unit (G.w G.center G.targetTime)

theorem EulerParentPacketFrames.RenewalAtTarget.target_remainder {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) (hδ : 0 < G.δ) (hT : G.targetTime ≤ D.T) : ‖(D.M.field (D.clamp G.targetTime)) 0 - G.M G.center G.targetTime - G.hchild • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit (G.w G.center G.targetTime))) (EulerPacketNormalizedPrimary.unit (G.r G.center G.targetTime))‖ ≤ P.error

The actual next source matrix has the prescribed target shear and the original packet's center error.

theorem EulerParentPacketFrames.RenewalAtTarget.coupling_pos {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) : 0 < P.a

theorem EulerParentPacketFrames.RenewalAtTarget.coupling_error {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) : |P.a / G.a - 1| ≤ G.couplingError

theorem EulerParentPacketFrames.RenewalAtTarget.coupling_interval {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) : (1 - G.couplingError) * G.a ≤ P.a ∧ P.a ≤ (1 + G.couplingError) * G.a

theorem EulerParentPacketFrames.RenewalAtTarget.coupling_absolute_error {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) : |P.a - G.a| ≤ G.a * G.couplingError

theorem EulerParentPacketFrames.RenewalAtTarget.sigma_sq {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) (herror : G.tiltError ≤ 1 / 2) : P.sigma ^ 2 = G.nextTilt

theorem EulerParentPacketFrames.RenewalAtTarget.sigma_pos {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) (herror : G.tiltError ≤ 1 / 2) : 0 < P.sigma

theorem EulerParentPacketFrames.RenewalAtTarget.tilt_error {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) (herror : G.tiltError ≤ 1 / 2) : |G.y⁻¹ ^ 2 * P.sigma ^ 2 - 1| ≤ G.tiltError

theorem EulerParentPacketFrames.RenewalAtTarget.tilt_interval {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) (herror : G.tiltError ≤ 1 / 2) : 1 / 2 ≤ G.y⁻¹ ^ 2 * P.sigma ^ 2 ∧ G.y⁻¹ ^ 2 * P.sigma ^ 2 ≤ 3 / 2

theorem EulerParentPacketFrames.RenewalAtTarget.sigma_small {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) (herror : G.tiltError ≤ 1 / 2) (hy : G.y ≤ 1 / 8) : P.sigma ≤ 1 / 4

theorem EulerParentPacketFrames.RenewalAtTarget.background_compression_eq {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) : inner ℝ ((P.B G.targetTime) (EulerPacketNormalizedPrimary.unit (P.m G.targetTime))) (EulerPacketNormalizedPrimary.unit (P.m G.targetTime)) = G.nextCompression

theorem EulerParentPacketFrames.RenewalAtTarget.activation_normal_le {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) (ht : 0 < G.targetTime) (hT : G.targetTime < D.T) : inner ℝ (((D.M.field ⟨G.targetTime, ⋯⟩) 0) (EulerPacketNormalizedPrimary.unit (P.m G.targetTime))) (EulerPacketNormalizedPrimary.unit (P.m G.targetTime)) ≤ -G.compressionScale + 3 * (G.G + G.d) + P.error

The new packet error is retained in the compression margin.

theorem EulerParentPacketFrames.RenewalAtTarget.activation_compression {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) (ht : 0 < G.targetTime) (hT : G.targetTime < D.T) (hmargin : 3 * (G.G + G.d) + P.error < G.compressionScale) : inner ℝ (((D.M.field ⟨G.targetTime, ⋯⟩) 0) (EulerPacketNormalizedPrimary.unit (P.m G.targetTime))) (EulerPacketNormalizedPrimary.unit (P.m G.targetTime)) < 0

theorem EulerParentPacketFrames.RenewalAtTarget.activation_compression_of_error_le_one {ι : Type u_1} {V : Type} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {D : EulerTransversePacketProvider.Data V} {G : EulerPacketMovingFrame.PhysicalGeometryData ι} {P : EulerPacketSourceGeometry.ParentFrame D G.targetTime} (J : RenewalAtTarget G P) (ht : 0 < G.targetTime) (hT : G.targetTime < D.T) (he : P.error ≤ 1) : inner ℝ (((D.M.field ⟨G.targetTime, ⋯⟩) 0) (EulerPacketNormalizedPrimary.unit (P.m G.targetTime))) (EulerPacketNormalizedPrimary.unit (P.m G.targetTime)) < 0