The uniform direct-forward source comparison constructs the actual next parent and its k^80 labels, with the same global physical errors.
theorem
EulerParentPacketFrames.LabelData.forward_uniform_child
{A : Parent}
(L : LabelData A)
(I : ParticleInverse A)
(H : LowBounds A)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(J : ForwardInputs (A.meanData H) (A.transverseData m hm R S hS))
(δ : ℝ)
(hδ : 0 < δ)
(hδ1 : δ ≤ 1)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ S)
(α : ℝ)
(hα : 0 < α)
(W : ℝ)
(hW :
EulerPacketForwardRadius.RadiusPrimitives J.linear J.mean J.normal
(EulerPacketCylinderField.forwardCoefficientBudget EulerPacketTerminalDatum.period (A.meanData H)
(A.transverseData m hm R S hS) ⋯ J.normal)
δ ξ W)
(hprofile : ∀ (t : ↑(Set.Icc 0 (A.transverseData m hm R S hS).T)), α * J.linear.g t ≤ W)
(k : ℝ)
(hk : EulerPacketSourceFrequency.UniversalFrequency k)
(hfrequency :
EulerPacketInitializedOutputCost.uniformConstant * W ^ EulerPacketInitializedOutputCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower k)
(hKk : L.K ≤ k)
(hinv : A.ell⁻¹ ≤ k ^ (3 / 4))
(nextEll : ℝ)
(hnext : 0 < nextEll)
(hnext1 : nextEll ≤ 1)
:
∃ (hn : 1 ≤ EulerPacketSourceFrequency.truncation k) (Q :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketTerminalDatum.forwardInitializedCorrectionData (A.meanData H) (A.transverseData m hm R S hS) ⋯ δ hδ ξ hs
α ⋯ (EulerPacketSourceFrequency.truncation k) hn k ⋯))
(G : EulerPhysicalGraphFlowBounds.Data EulerPacketTerminalDatum.period A.T) (hgraph :
∀ (t : ↑(Set.Icc 0 A.T)) (z : EulerLiftedGradientSpace.LiftTangent),
(EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0),
G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient EulerPacketTerminalDatum.period Q
(EulerPacketTerminalDatum.forwardInitializedNormalizedField (A.meanData H) (A.transverseData m hm R S hS) ⋯ δ hδ
ξ hs α (EulerPacketSourceFrequency.truncation k) k) ∧ (∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space),
‖fderiv ℝ
(EulerPacketTerminalDatum.forwardInitializedExactPhysicalVelocity (A.meanData H)
(A.transverseData m hm R S hS) ⋯ δ hδ ξ hs α ⋯ (EulerPacketSourceFrequency.truncation k) hn k ⋯ Q t
(I.normalized t))
x - (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ m (I.normalized t x))) • ((InnerProductSpace.rankOne ℝ)
(EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm R S hS) ξ (↑t)
(I.normalized t x)))
(((A.transverseData m hm R S hS).normal.field t) (I.normalized t x))‖ ≤ k ^ (-(1 / 4)) ∧ ‖fderiv ℝ
(gradient
(EulerPacketTerminalDatum.forwardInitializedExactPhysicalPressure (A.meanData H)
(A.transverseData m hm R S hS) ⋯ δ hδ ξ hs α ⋯ (EulerPacketSourceFrequency.truncation k) hn k ⋯ Q
t (I.normalized t)))
x - (EulerPacketForwardShear.pressureCoefficient (A.transverseData m hm R S hS) ξ α t (I.normalized t x) * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ m (I.normalized t x))) • ((InnerProductSpace.rankOne ℝ) (((A.transverseData m hm R S hS).normal.field t) (I.normalized t x)))
(((A.transverseData m hm R S hS).normal.field t) (I.normalized t x))‖ ≤ k ^ (-(1 / 4))) ∧ (∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space),
‖(G.displacementField k m A.ell ⋯ t).field x‖ ≤ k ^ (-(1 / 4))) ∧ ∃ (LC : LabelData (A.child G k m hgraph nextEll hnext hnext1)), LC.K = k ^ 80