One geometric stage: actual neighboring physical fields, the constructed common scalar reference, and the source amplitude choice. All hypotheses are the literal physical data and explicit scale guards in the data record.

Tangency is preserved by the actual ray and projected velocity ODEs.

theorem EulerPacketMovingFrame.tangentPairing_hasDerivWithinAt (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) {r w : ℝ → EulerSmoothLimit.Space} {t : ℝ} {S : Set ℝ} (hr : HasDerivWithinAt r (-(ContinuousLinearMap.adjoint M) (r t)) S t) (hw : HasDerivWithinAt w (-M (w t) + (2 * inner ℝ (r t) (M (w t)) / ‖r t‖ ^ 2) • r t) S t) (hr0 : r t ≠ 0) : HasDerivWithinAt (fun (s : ℝ) => inner ℝ (r s) (w s)) 0 S t

theorem EulerPacketMovingFrame.rescaled_tangentPairing_zero (M : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) {r w : ℝ → EulerSmoothLimit.Space} {t₀ a ε T : ℝ} {S : Set ℝ} (hmap : Set.MapsTo (physicalTime t₀ a ε) (Set.Icc 0 T) S) (hr : ∀ t ∈ S, HasDerivWithinAt r (-(ContinuousLinearMap.adjoint (M t)) (r t)) S t) (hw : ∀ t ∈ S, HasDerivWithinAt w (-(M t) (w t) + (2 * inner ℝ (r t) ((M t) (w t)) / ‖r t‖ ^ 2) • r t) S t) (hr0 : ∀ τ ∈ Set.Icc 0 T, r (physicalTime t₀ a ε τ) ≠ 0) (h0 : inner ℝ (r t₀) (w t₀) = 0) (τ : ℝ) : τ ∈ Set.Icc 0 T → inner ℝ (r (physicalTime t₀ a ε τ)) (w (physicalTime t₀ a ε τ)) = 0

Continuity of the actual rescaled moving-frame matrices.

theorem EulerPacketMovingFrame.rescaledFrame_continuousOn (B D : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) {m v : ℝ → EulerSmoothLimit.Space} {S U : Set ℝ} {t₀ a ε : ℝ} (hmap : Set.MapsTo (physicalTime t₀ a ε) U S) (hDc : ContinuousOn D S) (hm : ∀ t ∈ S, HasDerivWithinAt m (-(ContinuousLinearMap.adjoint (B t)) (m t)) S t) (hv : ∀ 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) (i j : Fin 3) : ContinuousOn (fun (τ : ℝ) => rescaledFrame D m v t₀ a ε τ i j) U

theorem EulerPacketMovingFrame.frameSkew_continuousOn {B : ℝ → Fin 3 → Fin 3 → ℝ} {U : Set ℝ} (hB : ∀ (i j : Fin 3), ContinuousOn (fun (τ : ℝ) => B τ i j) U) (i j : Fin 3) : ContinuousOn (fun (τ : ℝ) => EulerPacketRay.frameSkew (B τ) i j) U

theorem EulerPacketMovingFrame.scaledRayEntry_continuousOn {M S : ℝ → Fin 3 → Fin 3 → ℝ} {U : Set ℝ} (a ε : ℝ) (hM : ∀ (i j : Fin 3), ContinuousOn (fun (τ : ℝ) => M τ i j) U) (hS : ∀ (i j : Fin 3), ContinuousOn (fun (τ : ℝ) => S τ i j) U) (i j : Fin 3) : ContinuousOn (fun (τ : ℝ) => EulerPacketRay.scaledRayEntry a ε (M τ) (S τ) i j) U

theorem EulerPacketMovingFrame.scaledVelocityEntry_continuousOn {M : ℝ → Fin 3 → Fin 3 → ℝ} {U : Set ℝ} (a ε : ℝ) (hM : ∀ (i j : Fin 3), ContinuousOn (fun (τ : ℝ) => M τ i j) U) (i j : Fin 3) : ContinuousOn (fun (τ : ℝ) => EulerPacketRay.scaledVelocityEntry a ε (M τ) i j) U

Uniform neighboring amplification and before-target size control from the actual physical equations. The scalar reference is shared by uniqueness, so its choice is independent of the physical label.

Actual neighboring physical primaries satisfy the amplification estimate with their genuine initial discrepancy. The source moving frame is the center frame. Its neighboring matrix perturbation is part of the actual parent error; all scaled coefficient and ray bounds are derived here.

theorem EulerPacketMovingFrame.physical_neighbor_stage_references {B B₁ M E : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} {m v r w : ℝ → EulerSmoothLimit.Space} {c s₀ t₀ a ε σ Θ T G d lam : ℝ} {S : Set ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hT0 : 0 < T) (hT : T ≤ Θ) (ha : 1 / 2 ≤ a) (hε : 0 < ε) (hΘ : 1 ≤ Θ) (hG : 1 ≤ G) (hd : 0 ≤ d) (hs₀ : s₀ ≠ 0) (hlam : 0 ≤ lam) (hsmall : 1000000 * neighborStabilityConstant * (16 * (ε * Θ * (4 * G) ^ 2 + d)) * Θ ^ 40 ≤ 1) (hmap : Set.MapsTo (physicalTime t₀ a ε) (Set.Icc 0 Θ) S) (hMc : ContinuousOn M 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) (hrd : ∀ t ∈ S, HasDerivWithinAt r (-(ContinuousLinearMap.adjoint (M t)) (r t)) S t) (hwd : ∀ t ∈ S, HasDerivWithinAt w (-(M t) (w t) + (2 * inner ℝ (r t) ((M t) (w t)) / ‖r t‖ ^ 2) • r t) S t) (hm0 : ∀ t ∈ S, m t ≠ 0) (hv0 : ∀ t ∈ S, v t ≠ 0) (hmv : ∀ t ∈ S, inner ℝ (m t) (v t) = 0) (hrw0 : inner ℝ (r t₀) (w t₀) = 0) (hB : ∀ t ∈ S, ‖B t‖ ≤ G) (hB₁ : ∀ t ∈ S, ‖B₁ t‖ ≤ G ^ 2) (hE : ∀ t ∈ S, ‖E t‖ ≤ d) (hparent : ∀ t ∈ S, M t = B t + primaryShear c m v t • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit (v t))) (EulerPacketNormalizedPrimary.unit (m t)) + E t) (hb0 : rescaledFrame B m v t₀ a ε 0 0 1 = a) (hk0 : rescaledFrame B m v t₀ a ε 0 2 1 = a * σ ^ 2) (hh0 : rescaledShear c m v t₀ a ε 0 = a / ε ^ 2) (hrInitial : EulerPacketRay.norm3 (scaledRay m v r s₀ t₀ a ε 0 0) (scaledRay m v r s₀ t₀ a ε 0 1) (scaledRay m v r s₀ t₀ a ε 0 2 - 1) ≤ 16 * (ε * Θ * (4 * G) ^ 2 + d)) (hvelocityInitial : |scaledVelocity m v w t₀ a ε 0 1 - 1| + |scaledVelocity m v w t₀ a ε 0 0 + lam| ≤ 16 * (ε * Θ * (4 * G) ^ 2 + d)) : have e := 16 * (ε * Θ * (4 * G) ^ 2 + d); have U := fun (τ : ℝ) => scaledVelocity m v w t₀ a ε τ 0; have V := fun (τ : ℝ) => scaledVelocity m v w t₀ a ε τ 1; (∀ τ ∈ Set.Icc 0 T, EulerPacketRay.norm3 (scaledRay m v r s₀ t₀ a ε τ 0 - σ ^ 2 * τ ^ 2) (scaledRay m v r s₀ t₀ a ε τ 1 + 2 * σ ^ 2 * τ) (scaledRay m v r s₀ t₀ a ε τ 2 - 1) ≤ 800 * e * Θ ^ 5 ∧ 1 / 2 ≤ scaledRay m v r s₀ t₀ a ε τ 2 ∧ inner ℝ (r (physicalTime t₀ a ε τ)) (w (physicalTime t₀ a ε τ)) = 0) ∧ ∃ (F : ℝ → ℝ) (F₁ : ℝ → ℝ) (Z : ℝ → ℝ) (Z₁ : ℝ → ℝ), F 0 = 1 ∧ F₁ 0 = 0 ∧ Z 0 = 1 ∧ Z₁ 0 = lam ∧ (∀ (t : ℝ), HasDerivAt F (F₁ t) t) ∧ (∀ (t : ℝ), HasDerivAt Z (Z₁ t) t) ∧ (∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * F₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * F t) t) ∧ (∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) ∧ (∀ t ∈ Set.Icc 0 T, |V t - Z t| + |U t + Z₁ t| ≤ 400000000 * e * Θ ^ 29 * (1 + lam) * F t) ∧ ∀ t ∈ Set.Icc 1 T, 0 < V t ∧ |V t / Z t - 1| ≤ neighborStabilityConstant * e * Θ ^ 29 ∧ |U t / V t + Z₁ t / Z t| ≤ 10 * (neighborStabilityConstant * e * Θ ^ 29)

Uniqueness of the actual scalar comparison equation, including its state.

theorem EulerPacketMovingFrame.equation30_state_eq_of_initial {σ : ℝ} {Z Z₁ W W₁ : ℝ → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt Z (Z₁ t) t) (hW : ∀ (t : ℝ), 0 ≤ t → HasDerivAt W (W₁ t) t) (hfluxZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (hfluxW : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * W₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * W t) t) (hi : Z 0 = W 0) (hi₁ : Z₁ 0 = W₁ 0) (t : ℝ) : 0 ≤ t → Z t = W t ∧ Z₁ t = W₁ t

The scalar equation and its initial state determine both state components on the forward half-line. This lets independently constructed neighbor comparisons use one common reference.

theorem EulerPacketMovingFrame.physical_family_amplification_and_size {α : Type u_1} (center : α) {B B₁ : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} {M E : α → ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} {m v : ℝ → EulerSmoothLimit.Space} {r w : α → ℝ → EulerSmoothLimit.Space} {c s₀ t₀ a ε σ Θ T G d lam : ℝ} {S : Set ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hT0 : 1 ≤ T) (hT : T ≤ Θ) (ha : 1 / 2 ≤ a) (hε : 0 < ε) (hΘ : 1 ≤ Θ) (hG : 1 ≤ G) (hd : 0 ≤ d) (hs₀ : 0 < s₀) (hlam : 0 ≤ lam) (hsmall : 1000000 * neighborStabilityConstant * (16 * (ε * Θ * (4 * G) ^ 2 + d)) * Θ ^ 40 ≤ 1) (hmap : Set.MapsTo (physicalTime t₀ a ε) (Set.Icc 0 Θ) S) (hMc : ∀ (ξ : α), ContinuousOn (M ξ) 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) (hrd : ∀ (ξ : α), ∀ t ∈ S, HasDerivWithinAt (r ξ) (-(ContinuousLinearMap.adjoint (M ξ t)) (r ξ t)) S t) (hwd : ∀ (ξ : α), ∀ t ∈ S, HasDerivWithinAt (w ξ) (-(M ξ t) (w ξ t) + (2 * inner ℝ (r ξ t) ((M ξ t) (w ξ t)) / ‖r ξ t‖ ^ 2) • r ξ t) S t) (hm0 : ∀ t ∈ S, m t ≠ 0) (hv0 : ∀ t ∈ S, v t ≠ 0) (hmv : ∀ t ∈ S, inner ℝ (m t) (v t) = 0) (hrw0 : ∀ (ξ : α), inner ℝ (r ξ t₀) (w ξ t₀) = 0) (hB : ∀ t ∈ S, ‖B t‖ ≤ G) (hB₁ : ∀ t ∈ S, ‖B₁ t‖ ≤ G ^ 2) (hE : ∀ (ξ : α), ∀ t ∈ S, ‖E ξ t‖ ≤ d) (hparent : ∀ (ξ : α), ∀ t ∈ S, M ξ t = B t + primaryShear c m v t • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit (v t))) (EulerPacketNormalizedPrimary.unit (m t)) + E ξ t) (hb0 : rescaledFrame B m v t₀ a ε 0 0 1 = a) (hk0 : rescaledFrame B m v t₀ a ε 0 2 1 = a * σ ^ 2) (hh0 : rescaledShear c m v t₀ a ε 0 = a / ε ^ 2) (hrInitial : ∀ (ξ : α), EulerPacketRay.norm3 (scaledRay m v (r ξ) s₀ t₀ a ε 0 0) (scaledRay m v (r ξ) s₀ t₀ a ε 0 1) (scaledRay m v (r ξ) s₀ t₀ a ε 0 2 - 1) ≤ 16 * (ε * Θ * (4 * G) ^ 2 + d)) (hvelocityInitial : ∀ (ξ : α), |scaledVelocity m v (w ξ) t₀ a ε 0 1 - 1| + |scaledVelocity m v (w ξ) t₀ a ε 0 0 + lam| ≤ 16 * (ε * Θ * (4 * G) ^ 2 + d)) : have e := 16 * (ε * Θ * (4 * G) ^ 2 + d); ∃ (F : ℝ → ℝ) (F₁ : ℝ → ℝ) (Z : ℝ → ℝ) (Z₁ : ℝ → ℝ), F 0 = 1 ∧ F₁ 0 = 0 ∧ Z 0 = 1 ∧ Z₁ 0 = lam ∧ (∀ (t : ℝ), HasDerivAt F (F₁ t) t) ∧ (∀ (t : ℝ), HasDerivAt Z (Z₁ t) t) ∧ (∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * F₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * F t) t) ∧ (∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) ∧ (∀ (ξ : α), ∀ τ ∈ Set.Icc 0 T, EulerPacketRay.norm3 (scaledRay m v (r ξ) s₀ t₀ a ε τ 0 - σ ^ 2 * τ ^ 2) (scaledRay m v (r ξ) s₀ t₀ a ε τ 1 + 2 * σ ^ 2 * τ) (scaledRay m v (r ξ) s₀ t₀ a ε τ 2 - 1) ≤ 800 * e * Θ ^ 5 ∧ 1 / 2 ≤ scaledRay m v (r ξ) s₀ t₀ a ε τ 2 ∧ inner ℝ (r ξ (physicalTime t₀ a ε τ)) (w ξ (physicalTime t₀ a ε τ)) = 0) ∧ (∀ (ξ : α), ∀ τ ∈ Set.Icc 0 T, |scaledVelocity m v (w ξ) t₀ a ε τ 1 - Z τ| + |scaledVelocity m v (w ξ) t₀ a ε τ 0 + Z₁ τ| ≤ 400000000 * e * Θ ^ 29 * (1 + lam) * F τ) ∧ (∀ (ξ : α), ∀ τ ∈ Set.Icc 1 T, 0 < scaledVelocity m v (w ξ) t₀ a ε τ 1 ∧ |scaledVelocity m v (w ξ) t₀ a ε τ 1 / Z τ - 1| ≤ neighborStabilityConstant * e * Θ ^ 29 ∧ |scaledVelocity m v (w ξ) t₀ a ε τ 0 / scaledVelocity m v (w ξ) t₀ a ε τ 1 + Z₁ τ / Z τ| ≤ 10 * (neighborStabilityConstant * e * Θ ^ 29)) ∧ ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 T, ‖r ξ (physicalTime t₀ a ε τ)‖ * ‖w ξ (physicalTime t₀ a ε τ)‖ ≤ 64 * (‖r center (physicalTime t₀ a ε T)‖ * ‖w center (physicalTime t₀ a ε T)‖)

Relative propagator estimates on arbitrary subintervals for actual velocity states.

theorem EulerPacketMovingFrame.velocity_propagator_bound {σ Θ s t δ : ℝ} {F F₁ G G₁ U U₁ V V₁ : ℝ → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hs : 0 ≤ s) (hst : s ≤ t) (ht : t ≤ Θ) (hδ : 0 ≤ δ) (hsmall : 20 * Θ ^ 8 * δ * (t - s) ≤ 1 / 2) (hF : ∀ (x : ℝ), 0 ≤ x → HasDerivAt F (F₁ x) x) (hG : ∀ (x : ℝ), 0 ≤ x → HasDerivAt G (G₁ x) x) (hfluxF : ∀ (x : ℝ), 0 ≤ x → HasDerivAt (fun (u : ℝ) => (1 + (σ ^ 2 * u ^ 2) ^ 2) * F₁ u) (2 * (1 - σ ^ 2 * (σ ^ 2 * x ^ 2)) * F x) x) (hfluxG : ∀ (x : ℝ), 0 ≤ x → HasDerivAt (fun (u : ℝ) => (1 + (σ ^ 2 * u ^ 2) ^ 2) * G₁ u) (2 * (1 - σ ^ 2 * (σ ^ 2 * x ^ 2)) * G x) x) (hF0 : F 0 = 1) (hF₁0 : F₁ 0 = 0) (hG₁0 : G₁ 0 = 1) (hU : ∀ x ∈ Set.Icc s t, HasDerivAt U (U₁ x) x) (hV : ∀ x ∈ Set.Icc s t, HasDerivAt V (V₁ x) x) (hU₁c : ContinuousOn U₁ (Set.Icc s t)) (hV₁c : ContinuousOn V₁ (Set.Icc s t)) (herror : ∀ x ∈ Set.Icc s t, |U₁ x - EulerPacketBridge.idealVelocityFirst (σ ^ 2) x (U x) (V x)| + |V₁ x + U x| ≤ δ * (|U x| + |V x|)) : |U t| + |V t| ≤ 40 * Θ ^ 8 * (F t / F s) * (|U s| + |V s|)

theorem EulerPacketMovingFrame.velocity_propagator_bound_within {σ Θ T e : ℝ} {F F₁ G G₁ U U₁ V V₁ : ℝ → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hT0 : 0 < T) (hT : T ≤ Θ) (he : 0 ≤ e) (hsmall : 40 * e * Θ ^ 21 ≤ 1) (hF : ∀ (x : ℝ), 0 ≤ x → HasDerivAt F (F₁ x) x) (hG : ∀ (x : ℝ), 0 ≤ x → HasDerivAt G (G₁ x) x) (hfluxF : ∀ (x : ℝ), 0 ≤ x → HasDerivAt (fun (u : ℝ) => (1 + (σ ^ 2 * u ^ 2) ^ 2) * F₁ u) (2 * (1 - σ ^ 2 * (σ ^ 2 * x ^ 2)) * F x) x) (hfluxG : ∀ (x : ℝ), 0 ≤ x → HasDerivAt (fun (u : ℝ) => (1 + (σ ^ 2 * u ^ 2) ^ 2) * G₁ u) (2 * (1 - σ ^ 2 * (σ ^ 2 * x ^ 2)) * G x) x) (hF0 : F 0 = 1) (hF₁0 : F₁ 0 = 0) (hG₁0 : G₁ 0 = 1) (hU : ∀ x ∈ Set.Icc 0 T, HasDerivWithinAt U (U₁ x) (Set.Icc 0 T) x) (hV : ∀ x ∈ Set.Icc 0 T, HasDerivWithinAt V (V₁ x) (Set.Icc 0 T) x) (hU₁c : ContinuousOn U₁ (Set.Icc 0 T)) (hV₁c : ContinuousOn V₁ (Set.Icc 0 T)) (herror : ∀ x ∈ Set.Icc 0 T, |U₁ x - EulerPacketBridge.idealVelocityFirst (σ ^ 2) x (U x) (V x)| + |V₁ x + U x| ≤ e * Θ ^ 12 * (|U x| + |V x|)) (s t : ℝ) : 0 ≤ s → s ≤ t → t ≤ T → |U t| + |V t| ≤ 40 * Θ ^ 8 * (F t / F s) * (|U s| + |V s|)

Polynomial conversion between physical tangent vectors and the two-state system.

theorem EulerPacketMovingFrame.scaled_pair_le_physical_norm (m v w : ℝ → EulerSmoothLimit.Space) {t₀ a ε τ : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hm : m (physicalTime t₀ a ε τ) ≠ 0) (hv : v (physicalTime t₀ a ε τ) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) : |scaledVelocity m v w t₀ a ε τ 0| + |scaledVelocity m v w t₀ a ε τ 1| ≤ 2 / ε * ‖w (physicalTime t₀ a ε τ)‖

theorem EulerPacketMovingFrame.physical_velocity_le_scaled_state (m v r w : ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε τ Θ ρ P₀ Q₀ : ℝ} (hs₀ : s₀ ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hm : m (physicalTime t₀ a ε τ) ≠ 0) (hv : v (physicalTime t₀ a ε τ) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) (hrw : inner ℝ (r (physicalTime t₀ a ε τ)) (w (physicalTime t₀ a ε τ)) = 0) (hΘ : 1 ≤ Θ) (hρ0 : 0 ≤ ρ) (hρ : ρ ≤ 1 / 2) (hP₀ : |P₀| ≤ Θ ^ 2) (hQ₀ : |Q₀| ≤ 2 * Θ ^ 2) (hP : |scaledRay m v r s₀ t₀ a ε τ 0 - P₀| ≤ ρ) (hQ : |scaledRay m v r s₀ t₀ a ε τ 1 - Q₀| ≤ ρ) (hN : |scaledRay m v r s₀ t₀ a ε τ 2 - 1| ≤ ρ) : ‖w (physicalTime t₀ a ε τ)‖ ≤ 7 * Θ ^ 2 * (|scaledVelocity m v w t₀ a ε τ 0| + |scaledVelocity m v w t₀ a ε τ 1|)

The arbitrary physical tangent propagator has polynomial loss relative to the actual primary scalar profile. All scaled coefficients and tangency properties are derived from the physical ODEs and parent decomposition.

The actual controlled velocity system has polynomial relative propagation.

Relative growth of the primary scalar reference dominates zero slope.

theorem EulerPacketMovingFrame.equation30_slope_ratio_dominates {σ lam s t : ℝ} {F F₁ Z Z₁ : ℝ → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hlam : 0 ≤ lam) (hF : ∀ (x : ℝ), 0 ≤ x → HasDerivAt F (F₁ x) x) (hZ : ∀ (x : ℝ), 0 ≤ x → HasDerivAt Z (Z₁ x) x) (hfluxF : ∀ (x : ℝ), 0 ≤ x → HasDerivAt (fun (u : ℝ) => (1 + (σ ^ 2 * u ^ 2) ^ 2) * F₁ u) (2 * (1 - σ ^ 2 * (σ ^ 2 * x ^ 2)) * F x) x) (hfluxZ : ∀ (x : ℝ), 0 ≤ x → HasDerivAt (fun (u : ℝ) => (1 + (σ ^ 2 * u ^ 2) ^ 2) * Z₁ u) (2 * (1 - σ ^ 2 * (σ ^ 2 * x ^ 2)) * Z x) x) (hF0 : F 0 = 1) (hF₁0 : F₁ 0 = 0) (hZ0 : Z 0 = 1) (hZ₁0 : Z₁ 0 = lam) (hs : 0 ≤ s) (hst : s ≤ t) : F t / F s ≤ Z t / Z s

theorem EulerPacketMovingFrame.controlled_velocity_propagator_within {σ Θ T e ε : ℝ} {Z Z₁ U V P Q N : ℝ → ℝ} {R A C : ℝ → Fin 3 → Fin 3 → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hT0 : 0 < T) (hT : T ≤ Θ) (he : 0 ≤ e) (hε : 0 ≤ ε) (hεe : ε ≤ e) (hsmall : 8000000 * e * Θ ^ 21 ≤ 1) (hRc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => R t i j) (Set.Icc 0 T)) (hAc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => A t i j) (Set.Icc 0 T)) (hCc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => C t i j) (Set.Icc 0 T)) (hP : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt P (R t 0 0 * P t + R t 0 1 * Q t + R t 0 2 * N t) (Set.Icc 0 T) t) (hQ : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Q (R t 1 0 * P t + R t 1 1 * Q t + R t 1 2 * N t) (Set.Icc 0 T) t) (hN : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt N (R t 2 0 * P t + R t 2 1 * Q t + R t 2 2 * N t) (Set.Icc 0 T) t) (hU : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt U (EulerPacketRay.velocityFirstRhs (A t) (C t) ε (P t) (Q t) (N t) (U t) (V t)) (Set.Icc 0 T) t) (hV : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt V (EulerPacketRay.velocitySecondRhs (A t) (C t) ε (P t) (Q t) (N t) (U t) (V t)) (Set.Icc 0 T) t) (hRclose : ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), |R t i j - EulerPacketRay.idealRayEntry (σ ^ 2) i j| ≤ 4 * e) (hAclose : ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), |A t i j - EulerPacketRay.idealVelocityEntry (σ ^ 2) i j| ≤ 3 * e) (hCclose : ∀ t ∈ Set.Icc 0 T, ∀ (j : Fin 3), |C t 0 j - EulerPacketRay.idealUnprojectedEntry 0 j| ≤ 5 * e ∧ |C t 1 j - EulerPacketRay.idealUnprojectedEntry 1 j| ≤ 5 * e) (hrayInitial : EulerPacketRay.norm3 (P 0) (Q 0) (N 0 - 1) ≤ e) (hZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (hZ0 : Z 0 = 1) (hZ₁0 : 0 ≤ Z₁ 0) (s t : ℝ) : 0 ≤ s → s ≤ t → t ≤ T → |U t| + |V t| ≤ 40 * Θ ^ 8 * (Z t / Z s) * (|U s| + |V s|)

No initial velocity restriction is imposed. The reference can have any nonnegative initial slope, and the bound retains its ratio.

theorem EulerPacketMovingFrame.physical_tangent_propagator {B B₁ M E : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} {m v r w : ℝ → EulerSmoothLimit.Space} {c s₀ t₀ a ε σ Θ T G d : ℝ} {S : Set ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hT0 : 0 < T) (hT : T ≤ Θ) (ha : 1 / 2 ≤ a) (hε : 0 < ε) (hΘ : 1 ≤ Θ) (hG : 1 ≤ G) (hd : 0 ≤ d) (hs₀ : s₀ ≠ 0) (hsmall : 8000000 * (16 * (ε * Θ * (4 * G) ^ 2 + d)) * Θ ^ 21 ≤ 1) (hmap : Set.MapsTo (physicalTime t₀ a ε) (Set.Icc 0 Θ) S) (hMc : ContinuousOn M 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) (hrd : ∀ t ∈ S, HasDerivWithinAt r (-(ContinuousLinearMap.adjoint (M t)) (r t)) S t) (hwd : ∀ t ∈ S, HasDerivWithinAt w (-(M t) (w t) + (2 * inner ℝ (r t) ((M t) (w t)) / ‖r t‖ ^ 2) • r t) S t) (hm0 : ∀ t ∈ S, m t ≠ 0) (hv0 : ∀ t ∈ S, v t ≠ 0) (hmv : ∀ t ∈ S, inner ℝ (m t) (v t) = 0) (hrw0 : inner ℝ (r t₀) (w t₀) = 0) (hB : ∀ t ∈ S, ‖B t‖ ≤ G) (hB₁ : ∀ t ∈ S, ‖B₁ t‖ ≤ G ^ 2) (hE : ∀ t ∈ S, ‖E t‖ ≤ d) (hparent : ∀ t ∈ S, M t = B t + primaryShear c m v t • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit (v t))) (EulerPacketNormalizedPrimary.unit (m t)) + E t) (hb0 : rescaledFrame B m v t₀ a ε 0 0 1 = a) (hk0 : rescaledFrame B m v t₀ a ε 0 2 1 = a * σ ^ 2) (hh0 : rescaledShear c m v t₀ a ε 0 = a / ε ^ 2) (hrInitial : EulerPacketRay.norm3 (scaledRay m v r s₀ t₀ a ε 0 0) (scaledRay m v r s₀ t₀ a ε 0 1) (scaledRay m v r s₀ t₀ a ε 0 2 - 1) ≤ 16 * (ε * Θ * (4 * G) ^ 2 + d)) {Z Z₁ : ℝ → ℝ} (hZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (hZ0 : Z 0 = 1) (hZ₁0 : 0 ≤ Z₁ 0) : ContinuousOn Z (Set.Icc 0 T) ∧ (∀ t ∈ Set.Icc 0 T, 0 < Z t) ∧ ∀ (s t : ℝ), 0 ≤ s → s ≤ t → t ≤ T → ‖w (physicalTime t₀ a ε t)‖ ≤ 560 * Θ ^ 10 / ε * (Z t / Z s) * ‖w (physicalTime t₀ a ε s)‖

Packet Stage

noncomputable def EulerPacketStage.stabilityConstant : ℝ

Absolute relative-stability constant obtained from the propagator bound and the primary-solution lower comparison.

Equations

• EulerPacketStage.stabilityConstant = 320000000 * Real.exp 6

theorem EulerPacketStage.stabilityConstant_ge : 320000000 ≤ stabilityConstant

theorem EulerPacketStage.controlled_stage_references {σ Θ T e ε lam : ℝ} {U V P Q N : ℝ → ℝ} {R A C : ℝ → Fin 3 → Fin 3 → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hT0 : 0 ≤ T) (hT : T ≤ Θ) (he : 0 ≤ e) (hε : 0 ≤ ε) (hεe : ε ≤ e) (hlam : 0 ≤ lam) (hsmall : 1000000 * stabilityConstant * e * Θ ^ 40 ≤ 1) (hRc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => R t i j) (Set.Icc 0 T)) (hAc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => A t i j) (Set.Icc 0 T)) (hCc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => C t i j) (Set.Icc 0 T)) (hP : ∀ t ∈ Set.Icc 0 T, HasDerivAt P (R t 0 0 * P t + R t 0 1 * Q t + R t 0 2 * N t) t) (hQ : ∀ t ∈ Set.Icc 0 T, HasDerivAt Q (R t 1 0 * P t + R t 1 1 * Q t + R t 1 2 * N t) t) (hN : ∀ t ∈ Set.Icc 0 T, HasDerivAt N (R t 2 0 * P t + R t 2 1 * Q t + R t 2 2 * N t) t) (hU : ∀ t ∈ Set.Icc 0 T, HasDerivAt U (EulerPacketRay.velocityFirstRhs (A t) (C t) ε (P t) (Q t) (N t) (U t) (V t)) t) (hV : ∀ t ∈ Set.Icc 0 T, HasDerivAt V (EulerPacketRay.velocitySecondRhs (A t) (C t) ε (P t) (Q t) (N t) (U t) (V t)) t) (hRclose : ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), |R t i j - EulerPacketRay.idealRayEntry (σ ^ 2) i j| ≤ 4 * e) (hAclose : ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), |A t i j - EulerPacketRay.idealVelocityEntry (σ ^ 2) i j| ≤ 3 * e) (hCclose : ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), |C t i j - EulerPacketRay.idealUnprojectedEntry i j| ≤ 5 * e) (hrayInitial : EulerPacketRay.norm3 (P 0) (Q 0) (N 0 - 1) ≤ e) (hU0 : U 0 = -lam) (hV0 : V 0 = 1) : ∃ (F : ℝ → ℝ) (F₁ : ℝ → ℝ) (Z : ℝ → ℝ) (Z₁ : ℝ → ℝ), F 0 = 1 ∧ F₁ 0 = 0 ∧ Z 0 = 1 ∧ Z₁ 0 = lam ∧ (∀ (t : ℝ), HasDerivAt F (F₁ t) t) ∧ (∀ (t : ℝ), HasDerivAt Z (Z₁ t) t) ∧ (∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * F₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * F t) t) ∧ (∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) ∧ (∀ t ∈ Set.Icc 0 T, |V t - Z t| + |U t + Z₁ t| ≤ 160000000 * e * Θ ^ 29 * (1 + lam) * F t) ∧ ∀ t ∈ Set.Icc 1 T, 0 < V t ∧ |V t / Z t - 1| ≤ stabilityConstant * e * Θ ^ 29 ∧ |U t / V t + Z₁ t / Z t| ≤ 10 * (stabilityConstant * e * Θ ^ 29)

The controlled velocity system has an exact scalar comparison solution, constructed from the axioms rather than supplied as a hypothesis.

theorem EulerPacketStage.early_forward_exponential_suppression {σ Θ T lam δ : ℝ} {F F₁ Z Z₁ U V : ℝ → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (_hΘ : 1 ≤ Θ) (hT : T ≤ Θ) (hTtarget : 1 / σ ≤ T) (hlam : 0 ≤ lam) (hδ : 0 ≤ δ) (hδsmall : 4 * Real.exp 6 * δ ≤ 1) (hF : ∀ (t : ℝ), HasDerivAt F (F₁ t) t) (hZ : ∀ (t : ℝ), HasDerivAt Z (Z₁ t) t) (hfluxF : ∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * F₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * F t) t) (hfluxZ : ∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (hF0 : F 0 = 1) (hF₁0 : F₁ 0 = 0) (hZ0 : Z 0 = 1) (hZ₁0 : Z₁ 0 = lam) (herror : ∀ t ∈ Set.Icc 0 T, |V t - Z t| + |U t + Z₁ t| ≤ δ * (1 + lam) * F t) : 0 < V T ∧ ∀ s ∈ Set.Icc 0 1, (|U s| + |V s|) / V T ≤ 84 * Real.exp 9 * Θ * Real.exp (-(1 / (4 * σ)))

Early forward amplitudes are exponentially small relative to target amplitude, with the initial slope cancelling from the estimate. This is the finite-ODE amplification mechanism underlying equation (36).

The pressure numerator of the actual primary is positive. The scale condition 1 ≤ σ * Θ is the source horizon condition; the smallness of the matrix and ray errors is converted to smallness relative to σ^2.

theorem EulerPacketMovingFrame.controlled_pressure_ratio_lower {A : Fin 3 → Fin 3 → ℝ} {σ Θ K e τ P Q N r : ℝ} {Z Z₁ : ℝ → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hK : 1 ≤ K) (he : 0 ≤ e) (hσΘ : 1 ≤ σ * Θ) (hτ : 1 ≤ τ) (hτΘ : τ ≤ Θ) (hsmall : 1000000 * K * e * Θ ^ 40 ≤ 1) (hZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (hZ0 : Z 0 = 1) (hZ₁0 : 0 ≤ Z₁ 0) (hP : |P - σ ^ 2 * τ ^ 2| ≤ 800 * e * Θ ^ 5) (hQ : |Q - -2 * σ ^ 2 * τ| ≤ 800 * e * Θ ^ 5) (hN : |N - 1| ≤ 800 * e * Θ ^ 5) (hratio : |r + Z₁ τ / Z τ| ≤ 10 * (K * e * Θ ^ 29)) (hA : ∀ (i j : Fin 3), |A i j - EulerPacketRay.idealVelocityEntry (σ ^ 2) i j| ≤ 3 * e) : σ ^ 2 / 2 ≤ EulerPacketRay.velocityNumerator A P Q N r 1 (EulerPacketRay.velocityThird P Q N r 1)

theorem EulerPacketMovingFrame.physical_pressure_positive_order40 (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m v r w : ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε τ σ Θ K e : ℝ} {Z Z₁ : ℝ → ℝ} (ha : 0 < a) (hs₀ : 0 < s₀) (hε : 0 < ε) (hm : m (physicalTime t₀ a ε τ) ≠ 0) (hv : v (physicalTime t₀ a ε τ) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) (hrw : inner ℝ (r (physicalTime t₀ a ε τ)) (w (physicalTime t₀ a ε τ)) = 0) (hV : 0 < scaledVelocity m v w t₀ a ε τ 1) (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hK : 1 ≤ K) (he : 0 ≤ e) (hσΘ : 1 ≤ σ * Θ) (hτ : 1 ≤ τ) (hτΘ : τ ≤ Θ) (hsmall : 1000000 * K * e * Θ ^ 40 ≤ 1) (hZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (hZ0 : Z 0 = 1) (hZ₁0 : 0 ≤ Z₁ 0) (hP : |scaledRay m v r s₀ t₀ a ε τ 0 - σ ^ 2 * τ ^ 2| ≤ 800 * e * Θ ^ 5) (hQ : |scaledRay m v r s₀ t₀ a ε τ 1 - -2 * σ ^ 2 * τ| ≤ 800 * e * Θ ^ 5) (hN : |scaledRay m v r s₀ t₀ a ε τ 2 - 1| ≤ 800 * e * Θ ^ 5) (hratio : |scaledVelocity m v w t₀ a ε τ 0 / scaledVelocity m v w t₀ a ε τ 1 + Z₁ τ / Z τ| ≤ 10 * (K * e * Θ ^ 29)) (hA : ∀ (i j : Fin 3), |scaledAction M m v a ε (physicalTime t₀ a ε τ) i j - EulerPacketRay.idealVelocityEntry (σ ^ 2) i j| ≤ 3 * e) : s₀ * a * scaledVelocity m v w t₀ a ε τ 1 * (σ ^ 2 / 2) ≤ inner ℝ (r (physicalTime t₀ a ε τ)) (M (w (physicalTime t₀ a ε τ))) ∧ 0 < inner ℝ (r (physicalTime t₀ a ε τ)) (M (w (physicalTime t₀ a ε τ)))

Source (33), stated for the actual physical ray and velocity.

Early physical amplitudes are exponentially small relative to the center target amplitude. The initial scalar slope cancels, including for neighboring initial data controlled by the common reference.

theorem EulerPacketMovingFrame.early_neighbor_state_bound {α : Type u_1} (center : α) (U V : α → ℝ → ℝ) {σ Θ T lam δ : ℝ} {F F₁ Z Z₁ : ℝ → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hT : T ≤ Θ) (hTtarget : 1 / σ ≤ T) (hlam : 0 ≤ lam) (hδ : 0 ≤ δ) (hδsmall : 4 * Real.exp 6 * δ ≤ 1) (hF : ∀ (t : ℝ), HasDerivAt F (F₁ t) t) (hZ : ∀ (t : ℝ), HasDerivAt Z (Z₁ t) t) (hfluxF : ∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * F₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * F t) t) (hfluxZ : ∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (hF0 : F 0 = 1) (hF₁0 : F₁ 0 = 0) (hZ0 : Z 0 = 1) (hZ₁0 : Z₁ 0 = lam) (herror : ∀ (ξ : α), ∀ t ∈ Set.Icc 0 T, |V ξ t - Z t| + |U ξ t + Z₁ t| ≤ δ * (1 + lam) * F t) : 0 < V center T ∧ ∀ (ξ : α), ∀ s ∈ Set.Icc 0 1, (|U ξ s| + |V ξ s|) / V center T ≤ 84 * Real.exp 9 * Θ * Real.exp (-(1 / (4 * σ)))

theorem EulerPacketMovingFrame.early_physical_size_suppression {α : Type u_1} (center : α) (m v : ℝ → EulerSmoothLimit.Space) (r w : α → ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε σ Θ T lam δ ρ : ℝ} {F F₁ Z Z₁ : ℝ → ℝ} (hs₀ : 0 < s₀) (hε : 0 < ε) (hε1 : ε ≤ 1) (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hT : T ≤ Θ) (hTtarget : 1 / σ ≤ T) (hlam : 0 ≤ lam) (hδ : 0 ≤ δ) (hδsmall : 4 * Real.exp 6 * δ ≤ 1) (hρ0 : 0 ≤ ρ) (hρ : ρ ≤ 1 / 2) (hm : ∀ τ ∈ Set.Icc 0 T, m (physicalTime t₀ a ε τ) ≠ 0) (hv : ∀ τ ∈ Set.Icc 0 T, v (physicalTime t₀ a ε τ) ≠ 0) (hmv : ∀ τ ∈ Set.Icc 0 T, inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) (hrw : ∀ (ξ : α), ∀ τ ∈ Set.Icc 0 T, inner ℝ (r ξ (physicalTime t₀ a ε τ)) (w ξ (physicalTime t₀ a ε τ)) = 0) (hP : ∀ (ξ : α), ∀ τ ∈ Set.Icc 0 T, |scaledRay m v (r ξ) s₀ t₀ a ε τ 0 - σ ^ 2 * τ ^ 2| ≤ ρ) (hQ : ∀ (ξ : α), ∀ τ ∈ Set.Icc 0 T, |scaledRay m v (r ξ) s₀ t₀ a ε τ 1 - -2 * σ ^ 2 * τ| ≤ ρ) (hN : ∀ (ξ : α), ∀ τ ∈ Set.Icc 0 T, |scaledRay m v (r ξ) s₀ t₀ a ε τ 2 - 1| ≤ ρ) (hF : ∀ (t : ℝ), HasDerivAt F (F₁ t) t) (hZ : ∀ (t : ℝ), HasDerivAt Z (Z₁ t) t) (hfluxF : ∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * F₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * F t) t) (hfluxZ : ∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (hF0 : F 0 = 1) (hF₁0 : F₁ 0 = 0) (hZ0 : Z 0 = 1) (hZ₁0 : Z₁ 0 = lam) (herror : ∀ (ξ : α), ∀ τ ∈ Set.Icc 0 T, |scaledVelocity m v (w ξ) t₀ a ε τ 1 - Z τ| + |scaledVelocity m v (w ξ) t₀ a ε τ 0 + Z₁ τ| ≤ δ * (1 + lam) * F τ) : 0 < ‖r center (physicalTime t₀ a ε T)‖ * ‖w center (physicalTime t₀ a ε T)‖ ∧ ∀ (ξ : α), ∀ τ ∈ Set.Icc 0 1, ‖r ξ (physicalTime t₀ a ε τ)‖ * ‖w ξ (physicalTime t₀ a ε τ)‖ / (‖r center (physicalTime t₀ a ε T)‖ * ‖w center (physicalTime t₀ a ε T)‖) ≤ 8232 * Real.exp 9 * Θ ^ 5 * Real.exp (-(1 / (4 * σ)))

The early part of source (36) for actual Euclidean norm products. The estimate is uniform over neighboring labels and over the nonnegative initial slope of the common scalar reference.

structure EulerPacketMovingFrame.PhysicalGeometryConclusion {α : Type u_1} (D : PhysicalGeometryData α) (F F₁ Z Z₁ : ℝ → ℝ) : Prop

Physical geometry conclusion data, collecting initial_values, F_derivative, Z_derivative, F_flux, Z_flux, ray_control and their compatibility conditions.

• initial_values : F 0 = 1 ∧ F₁ 0 = 0 ∧ Z 0 = 1 ∧ Z₁ 0 = D.lam
• F_derivative (t : ℝ) : HasDerivAt F (F₁ t) t
• Z_derivative (t : ℝ) : HasDerivAt Z (Z₁ t) t
• F_flux (t : ℝ) : HasDerivAt (fun (s : ℝ) => (1 + (D.σ ^ 2 * s ^ 2) ^ 2) * F₁ s) (2 * (1 - D.σ ^ 2 * (D.σ ^ 2 * t ^ 2)) * F t) t
• Z_flux (t : ℝ) : HasDerivAt (fun (s : ℝ) => (1 + (D.σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - D.σ ^ 2 * (D.σ ^ 2 * t ^ 2)) * Z t) t
• ray_control (ξ : α) (τ : ℝ) : τ ∈ Set.Icc 0 D.H → EulerPacketRay.norm3 (D.ray ξ τ 0 - D.σ ^ 2 * τ ^ 2) (D.ray ξ τ 1 + 2 * D.σ ^ 2 * τ) (D.ray ξ τ 2 - 1) ≤ 800 * D.error * D.Θ ^ 5 ∧ 1 / 2 ≤ D.ray ξ τ 2 ∧ inner ℝ (D.r ξ (D.time τ)) (D.w ξ (D.time τ)) = 0
• state_error (ξ : α) (τ : ℝ) : τ ∈ Set.Icc 0 D.H → |D.velocity ξ τ 1 - Z τ| + |D.velocity ξ τ 0 + Z₁ τ| ≤ 400000000 * D.error * D.Θ ^ 29 * (1 + D.lam) * F τ
• relative_error (ξ : α) (τ : ℝ) : τ ∈ Set.Icc 1 D.H → 0 < D.velocity ξ τ 1 ∧ |D.velocity ξ τ 1 / Z τ - 1| ≤ neighborStabilityConstant * D.error * D.Θ ^ 29 ∧ |D.velocity ξ τ 0 / D.velocity ξ τ 1 + Z₁ τ / Z τ| ≤ 10 * (neighborStabilityConstant * D.error * D.Θ ^ 29)
• positive_pressure (ξ : α) (τ : ℝ) : τ ∈ Set.Icc 1 D.H → 0 < inner ℝ (D.r ξ (D.time τ)) ((D.M ξ (D.time τ)) (D.w ξ (D.time τ)))
• target_positive : 0 < D.targetSize
• target_growth : D.s₀ * Real.exp (1 / (4 * D.σ)) ≤ 4 * D.Θ * D.targetSize
• horizon_size (ξ : α) (τ : ℝ) : τ ∈ Set.Icc 1 D.H → D.size ξ τ ≤ 64 * Real.exp 6 * D.targetSize
• early_size (ξ : α) (τ : ℝ) : τ ∈ Set.Icc 0 1 → D.size ξ τ / D.targetSize ≤ 8232 * Real.exp 9 * D.Θ ^ 5 * Real.exp (-(1 / (4 * D.σ)))
• next_frame : |D.nextCoupling / D.a - 1| ≤ D.y ^ 4 + D.σ ^ 2 * D.y ^ 2 + 8 * D.σ * D.y ^ 3 + 30000000 * neighborStabilityConstant * D.error * D.Θ ^ 40 ∧ |D.y⁻¹ ^ 2 * D.nextTilt - 1| ≤ 1500 * D.σ + 30000000 * neighborStabilityConstant * D.error * D.Θ ^ 40
• compression_bound : D.nextCompression ≤ -(D.targetShear * D.ε) / (10 * D.target) + 3 * (D.G + D.d)
• compression_negative : D.nextCompression < 0
• amplitude_nonneg : 0 ≤ D.amplitude
• amplitude_normalization : D.amplitude * D.targetSize = D.δ * D.hchild
• amplitude_exponential : D.amplitude ≤ 4 * D.Θ * D.δ * D.hchild / D.s₀ * Real.exp (-(1 / (4 * D.σ)))
• amplitude_profile (τ : ℝ) : τ ∈ Set.Icc 0 D.H → D.amplitude * Z τ ≤ 8 * Real.exp 6 * D.δ * D.hchild / D.s₀
• amplitude_profile_sup : sSup ((fun (τ : ℝ) => D.amplitude * Z τ) '' Set.Icc 0 D.H) ≤ 8 * Real.exp 6 * D.δ * D.hchild / D.s₀
• physical_profile_continuous : ContinuousOn (physicalProfile Z D.t₀ D.a D.ε) (Set.Icc D.t₀ (D.time D.H))
• physical_profile_positive (t : ℝ) : t ∈ Set.Icc D.t₀ (D.time D.H) → 0 < physicalProfile Z D.t₀ D.a D.ε t
• tangent_propagator (ξ : α) (u : ℝ → EulerSmoothLimit.Space) : (∀ t ∈ D.S, HasDerivWithinAt u (-(D.M ξ t) (u t) + (2 * inner ℝ (D.r ξ t) ((D.M ξ t) (u t)) / ‖D.r ξ t‖ ^ 2) • D.r ξ t) D.S t) → inner ℝ (D.r ξ D.t₀) (u D.t₀) = 0 → ∀ (s t : ℝ), s ∈ Set.Icc D.t₀ (D.time D.H) → t ∈ Set.Icc D.t₀ (D.time D.H) → s ≤ t → ‖u t‖ ≤ 560 * D.Θ ^ 10 / D.ε * (physicalProfile Z D.t₀ D.a D.ε t / physicalProfile Z D.t₀ D.a D.ε s) * ‖u s‖

theorem EulerPacketMovingFrame.PhysicalGeometryData.exists_geometry {α : Type u_1} (D : PhysicalGeometryData α) : ∃ (F : ℝ → ℝ) (F₁ : ℝ → ℝ) (Z : ℝ → ℝ) (Z₁ : ℝ → ℝ), PhysicalGeometryConclusion D F F₁ Z Z₁