The actual forward primary has the same universal good-time size and pressure sign as the joined primary. At time zero and on the early interval its size has the exponential target-ratio gain.

The first normal stage satisfies the full physical amplification geometry. The source normal, primary and all ODEs are the actual forward fields, including exact initial data at time zero.

theorem EulerPacketSourceGeometry.ForwardGuards.error_le_scaled_error {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) : P.forwardError G.radius ≤ 16 * (P.epsilon * P.horizon * (4 * P.G) ^ 2 + P.forwardError G.radius)

noncomputable def EulerPacketSourceGeometry.ForwardGuards.geometryData {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (Ω : Set EulerSmoothLimit.Space) (h0 : 0 ∈ Ω) (hΩ : ∀ x ∈ Ω, ‖x‖ ≤ G.radius) : EulerPacketMovingFrame.PhysicalGeometryData { x : EulerSmoothLimit.Space // x ∈ Ω }

Geometry data, bundling center, B, B₁, M and the required compatibility proofs.

Equations

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

theorem EulerPacketSourceGeometry.ForwardGuards.source_interval {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (Ω : Set EulerSmoothLimit.Space) (h0 : 0 ∈ Ω) (hΩ : ∀ x ∈ Ω, ‖x‖ ≤ G.radius) : (G.geometryData Ω h0 hΩ).S = Set.Icc (G.geometryData Ω h0 hΩ).t₀ ((G.geometryData Ω h0 hΩ).t₀ + D.T)

theorem EulerPacketSourceGeometry.ForwardGuards.source_horizon {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (Ω : Set EulerSmoothLimit.Space) (h0 : 0 ∈ Ω) (hΩ : ∀ x ∈ Ω, ‖x‖ ≤ G.radius) : (G.geometryData Ω h0 hΩ).time (G.geometryData Ω h0 hΩ).H = (G.geometryData Ω h0 hΩ).t₀ + D.T

theorem EulerPacketSourceGeometry.ForwardGuards.exists_geometry_and_growth {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (Ω : Set EulerSmoothLimit.Space) (h0 : 0 ∈ Ω) (hΩ : ∀ x ∈ Ω, ‖x‖ ≤ G.radius) : ∃ (F : ℝ → ℝ) (F₁ : ℝ → ℝ) (Z : ℝ → ℝ) (Z₁ : ℝ → ℝ) (J : EulerPacketMovingFrame.PhysicalGeometryConclusion (G.geometryData Ω h0 hΩ) F F₁ Z Z₁), (∀ (t : ↑(Set.Icc 0 D.T)), 0 < (EulerPacketGeometrySourceGrowth.growthProfile D (G.geometryData Ω h0 hΩ) J) t) ∧ (EulerPacketGeometrySourceGrowth.growthProfile D (G.geometryData Ω h0 hΩ) J) ⟨0, ⋯⟩ = 1 ∧ EulerPacketSourcePropagator.PhysicalGrowth D Ω (⇑(EulerPacketGeometrySourceGrowth.growthProfile D (G.geometryData Ω h0 hΩ) J)) (560 * P.horizon ^ 10 / P.epsilon)

theorem EulerPacketSourceGeometry.ForwardGuards.halfBall_physicalGrowth {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) : ∃ (g : C(↑(Set.Icc 0 D.T), ℝ)), (∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) ∧ g ⟨0, ⋯⟩ = 1 ∧ EulerPacketSourcePropagator.PhysicalGrowth D {x : EulerSmoothLimit.Space | ‖x‖ ≤ 1 / 2} (⇑g) (560 * P.horizon ^ 10 / P.epsilon)

noncomputable def EulerPacketSourceGeometry.ForwardGuards.lowGeometry {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) : EulerPacketMovingFrame.PhysicalGeometryData { x : EulerSmoothLimit.Space // ‖x‖ ≤ 1 / 2 }

Low geometry, given by G.geometryData {x | ‖x‖ ≤ (1/2 : ℝ)} (by norm_num) (fun _ hx => hx.trans hball).

Equations

• G.lowGeometry hball = G.geometryData {x : EulerSmoothLimit.Space | ‖x‖ ≤ 1 / 2} EulerPacketSourceGeometry.ForwardGuards.lowGeometry._proof_1 ⋯

noncomputable def EulerPacketSourceGeometry.ForwardGuards.primaryAmplitude {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) : ℝ

Primary amplitude, given by (G.lowGeometry hball).amplitude.

Equations

• G.primaryAmplitude hball = (G.lowGeometry hball).amplitude

theorem EulerPacketSourceGeometry.ForwardGuards.primaryAmplitude_nonneg {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) : 0 ≤ G.primaryAmplitude hball

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

Early ratio, given by cutoffBound*(8232*Real.exp 9*P.horizon^5*Real.exp (-(1/(4*P.sigma)))).

Equations

• _G.earlyRatio = EulerPacketGeometryLowBounds.cutoffBound * (8232 * Real.exp 9 * P.horizon ^ 5 * Real.exp (-(1 / (4 * P.sigma))))

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

theorem EulerPacketSourceGeometry.ForwardGuards.scaledTime_mem {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (t : ↑(Set.Icc 0 D.T)) : EulerPacketMovingFrame.scaledTime 0 P.a P.epsilon ↑t ∈ Set.Icc 0 P.horizon

theorem EulerPacketSourceGeometry.ForwardGuards.lowGeometry_size {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (hx : ‖x‖ ≤ 1 / 2) : (G.lowGeometry hball).size ⟨x, hx⟩ (EulerPacketMovingFrame.scaledTime 0 P.a P.epsilon ↑t) = ‖(D.normal.field t) x‖ * ‖EulerPacketForwardFactorization.uncutVelocity D G.initialCoordinate (↑t) x‖

theorem EulerPacketSourceGeometry.ForwardGuards.cutoff_amplitude_size {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : G.primaryAmplitude hball * (‖(D.normal.field t) x‖ * ‖EulerPacketForwardFactorization.canonicalVelocity D G.initialCoordinate (↑t) x‖) = EulerSpatialCutoffs.innerCutoff x * (G.primaryAmplitude hball * (‖(D.normal.field t) x‖ * ‖EulerPacketForwardFactorization.uncutVelocity D G.initialCoordinate (↑t) x‖))

theorem EulerPacketSourceGeometry.ForwardGuards.good_primary_size {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (t : ↑(Set.Icc 0 D.T)) (ht : 1 ≤ EulerPacketMovingFrame.scaledTime 0 P.a P.epsilon ↑t) (x : EulerSmoothLimit.Space) : G.primaryAmplitude hball * (‖(D.normal.field t) x‖ * ‖EulerPacketForwardFactorization.canonicalVelocity D G.initialCoordinate (↑t) x‖) ≤ G.δ * G.hchild * EulerPacketGeometryLowBounds.goodRatio

theorem EulerPacketSourceGeometry.ForwardGuards.good_primary_flux {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (t : ↑(Set.Icc 0 D.T)) (ht : 1 ≤ EulerPacketMovingFrame.scaledTime 0 P.a P.epsilon ↑t) (x : EulerSmoothLimit.Space) : 0 ≤ inner ℝ ((D.normal.field t) x) (((D.M.field t) x) (EulerPacketForwardFactorization.canonicalVelocity D G.initialCoordinate (↑t) x))

theorem EulerPacketSourceGeometry.ForwardGuards.early_primary_size {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (G : ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (t : ↑(Set.Icc 0 D.T)) (ht : EulerPacketMovingFrame.scaledTime 0 P.a P.epsilon ↑t ≤ 1) (x : EulerSmoothLimit.Space) : G.primaryAmplitude hball * (‖(D.normal.field t) x‖ * ‖EulerPacketForwardFactorization.canonicalVelocity D G.initialCoordinate (↑t) x‖) ≤ G.δ * G.hchild * G.earlyRatio