Consequences of the literal numerical guards for a physical geometry stage.

Actual shear motion, exposed for the compression scale guard.

theorem EulerPacketMovingFrame.physical_shear_motion_bound {B B₁ E : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} {m v : ℝ → EulerSmoothLimit.Space} {c t₀ a ε Θ G d β : ℝ} {S : Set ℝ} (ha : 1 / 2 ≤ a) (hε : 0 < ε) (hΘ : 1 ≤ Θ) (hG : 1 ≤ G) (hd : 0 ≤ d) (hsmall : 16 * (ε * Θ * (4 * G) ^ 2 + d) ≤ 1) (hmap : Set.MapsTo (physicalTime t₀ a ε) (Set.Icc 0 Θ) S) (hBd : ∀ t ∈ S, HasDerivWithinAt B (B₁ t) S t) (hmd : ∀ t ∈ S, HasDerivWithinAt m (-(ContinuousLinearMap.adjoint (B t)) (m t)) S t) (hvd : ∀ t ∈ S, HasDerivWithinAt v (-(B t) (v t) + (2 * inner ℝ (m t) ((B t) (v t)) / ‖m t‖ ^ 2) • m t) S t) (hm0 : ∀ t ∈ S, m t ≠ 0) (hv0 : ∀ t ∈ S, v t ≠ 0) (hmv : ∀ t ∈ S, inner ℝ (m t) (v t) = 0) (hB : ∀ t ∈ S, ‖B t‖ ≤ G) (hB₁ : ∀ t ∈ S, ‖B₁ t‖ ≤ G ^ 2) (hE : ∀ t ∈ S, ‖E t‖ ≤ d) (hb0 : rescaledFrame B m v t₀ a ε 0 0 1 = a) (hk0 : rescaledFrame B m v t₀ a ε 0 2 1 = a * β) (hh0 : rescaledShear c m v t₀ a ε 0 = a / ε ^ 2) : have e := 16 * (ε * Θ * (4 * G) ^ 2 + d); ε ≤ e ∧ ∀ τ ∈ Set.Icc 0 Θ, |ε ^ 2 * rescaledShear c m v t₀ a ε τ / a - 1| ≤ e

theorem EulerPacketMovingFrame.PhysicalGeometryData.a_pos {α : Type u_1} (D : PhysicalGeometryData α) : 0 < D.a

theorem EulerPacketMovingFrame.PhysicalGeometryData.Theta_pos {α : Type u_1} (D : PhysicalGeometryData α) : 0 < D.Θ

theorem EulerPacketMovingFrame.PhysicalGeometryData.error_nonneg {α : Type u_1} (D : PhysicalGeometryData α) : 0 ≤ D.error

theorem EulerPacketMovingFrame.PhysicalGeometryData.target_from_sigma {α : Type u_1} (D : PhysicalGeometryData α) : 1 / D.σ ≤ D.target

theorem EulerPacketMovingFrame.PhysicalGeometryData.target_one {α : Type u_1} (D : PhysicalGeometryData α) : 1 ≤ D.target

theorem EulerPacketMovingFrame.PhysicalGeometryData.target_pos {α : Type u_1} (D : PhysicalGeometryData α) : 0 < D.target

theorem EulerPacketMovingFrame.PhysicalGeometryData.horizon_one {α : Type u_1} (D : PhysicalGeometryData α) : 1 ≤ D.H

theorem EulerPacketMovingFrame.PhysicalGeometryData.horizon_pos {α : Type u_1} (D : PhysicalGeometryData α) : 0 < D.H

theorem EulerPacketMovingFrame.PhysicalGeometryData.target_le_Theta {α : Type u_1} (D : PhysicalGeometryData α) : D.target ≤ D.Θ

theorem EulerPacketMovingFrame.PhysicalGeometryData.sigma_Theta {α : Type u_1} (D : PhysicalGeometryData α) : 1 ≤ D.σ * D.Θ

theorem EulerPacketMovingFrame.PhysicalGeometryData.target_scale {α : Type u_1} (D : PhysicalGeometryData α) : 1 ≤ D.σ ^ 2 * D.target ^ 2

theorem EulerPacketMovingFrame.PhysicalGeometryData.time_mem {α : Type u_1} (D : PhysicalGeometryData α) {τ : ℝ} (hτ : τ ∈ Set.Icc 0 D.H) : D.time τ ∈ D.S

theorem EulerPacketMovingFrame.PhysicalGeometryData.target_time_mem {α : Type u_1} (D : PhysicalGeometryData α) : D.targetTime ∈ D.S

theorem EulerPacketMovingFrame.PhysicalGeometryData.error_le_half {α : Type u_1} (D : PhysicalGeometryData α) : D.error ≤ 1 / 2

theorem EulerPacketMovingFrame.PhysicalGeometryData.error_le_one {α : Type u_1} (D : PhysicalGeometryData α) : D.error ≤ 1

theorem EulerPacketMovingFrame.PhysicalGeometryData.epsilon_le_error {α : Type u_1} (D : PhysicalGeometryData α) : D.ε ≤ D.error

theorem EulerPacketMovingFrame.PhysicalGeometryData.epsilon_le_one {α : Type u_1} (D : PhysicalGeometryData α) : D.ε ≤ 1

theorem EulerPacketMovingFrame.PhysicalGeometryData.ray_error_small {α : Type u_1} (D : PhysicalGeometryData α) : 800 * D.error * D.Θ ^ 5 ≤ 1 / 2

theorem EulerPacketMovingFrame.PhysicalGeometryData.relative_error_small {α : Type u_1} (D : PhysicalGeometryData α) : neighborStabilityConstant * D.error * D.Θ ^ 29 ≤ 1 / 2

theorem EulerPacketMovingFrame.PhysicalGeometryData.scalar_error_small {α : Type u_1} (D : PhysicalGeometryData α) : 4 * Real.exp 6 * (400000000 * D.error * D.Θ ^ 29) ≤ 1

theorem EulerPacketMovingFrame.PhysicalGeometryData.propagator_small {α : Type u_1} (D : PhysicalGeometryData α) : 8000000 * D.error * D.Θ ^ 21 ≤ 1

theorem EulerPacketMovingFrame.PhysicalGeometryData.action_error {α : Type u_1} (D : PhysicalGeometryData α) (ξ : α) {τ : ℝ} (hτ : τ ∈ Set.Icc 0 D.H) (i j : Fin 3) : |scaledAction (D.M ξ (D.time τ)) D.m D.v D.a D.ε (D.time τ) i j - EulerPacketRay.idealVelocityEntry (D.σ ^ 2) i j| ≤ 3 * D.error

theorem EulerPacketMovingFrame.PhysicalGeometryData.target_shear_lower {α : Type u_1} (D : PhysicalGeometryData α) : D.a / (2 * D.ε ^ 2) ≤ D.targetShear

theorem EulerPacketMovingFrame.PhysicalGeometryData.target_shear_pos {α : Type u_1} (D : PhysicalGeometryData α) : 0 < D.targetShear

theorem EulerPacketMovingFrame.PhysicalGeometryData.compression_domination {α : Type u_1} (D : PhysicalGeometryData α) : 30 * (‖D.B D.targetTime‖ + ‖D.E D.center D.targetTime‖) * D.target < D.targetShear * D.ε