The physical-label estimate (21) supplies the multiplier inputs in (H1). The displacement, velocity and acceleration are the actual L² fields. The identity part of the deformation is never asserted to lie in L².

Source (21) controls actual ordered physical-label derivatives in a fixed Sobolev norm. This file converts those genuine L² blocks to uniform spatial coefficient bounds. The embedding constant is independent of the external order; only the one derivative from displacement to deformation enlarges the coefficient radius.

noncomputable def EulerPacketParentLabelBounds.direction (i : Fin 3) : EulerSmoothLimit.Space

Direction, given by EuclideanSpace.single i 1.

Equations

• EulerPacketParentLabelBounds.direction i = EuclideanSpace.single i 1

noncomputable def EulerPacketParentLabelBounds.embeddingCost : ℝ

Embedding cost, given by sobolevEmbeddingConstant 1 3.

Equations

• EulerPacketParentLabelBounds.embeddingCost = EulerCylinderSobolevSpace.sobolevEmbeddingConstant 1 3

theorem EulerPacketParentLabelBounds.embeddingCost_nonneg : 0 ≤ embeddingCost

theorem EulerPacketParentLabelBounds.tensor_le_wordSum {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n f x‖ ≤ EulerParameterWordGevrey.wordSum direction f n x

theorem EulerPacketParentLabelBounds.representative_norm_le_base (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) (q : ℕ) (hq : 3 ≤ q) (x : EulerSmoothLimit.Space) : ‖EulerMeanSmoothRepresentative.representative u hu x‖ ≤ embeddingCost * EulerParameterWordGevrey.baseSize direction q (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) 0

theorem EulerPacketParentLabelBounds.representative_tensor_le_block (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) (q : ℕ) (hq : 3 ≤ q) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanSmoothRepresentative.representative u hu) x‖ ≤ embeddingCost * EulerParameterWordGevrey.block direction q (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) n 0

Fixed H³ evaluation is applied after each external word, without a tensor-coordinate norm equivalence depending on the word length.

theorem EulerPacketParentLabelBounds.field_tensor_le_block (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : Continuous f) (hrep : ↑↑u =ᵐ[MeasureTheory.volume] f) (q : ℕ) (hq : 3 ≤ q) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n f x‖ ≤ embeddingCost * EulerParameterWordGevrey.block direction q (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) n 0

The bound applies to the actual continuous representative, not merely to a field chosen by the Sobolev reconstruction.

theorem EulerPacketParentLabelBounds.field_tensor_gevrey (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : Continuous f) (hrep : ↑↑u =ᵐ[MeasureTheory.volume] f) (q : ℕ) (hq : 3 ≤ q) (R A : ℝ) (hb : ∀ (n : ℕ), EulerParameterWordGevrey.block direction q (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) n 0 ≤ A * EulerGevrey.majorant R 0 n) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n f x‖ ≤ embeddingCost * A * EulerGevrey.majorant R 0 n

theorem EulerPacketParentLabelBounds.gradient_gevrey (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : Continuous f) (hrep : ↑↑u =ᵐ[MeasureTheory.volume] f) (q : ℕ) (hq : 3 ≤ q) (R A : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hb : ∀ (n : ℕ), EulerParameterWordGevrey.block direction q (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) n 0 ≤ A * EulerGevrey.majorant R 0 n) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fderiv ℝ f) x‖ ≤ embeddingCost * A * R * EulerGevrey.majorant (4 * R) 0 n

Differentiating the parent particle map once costs a fixed coefficient radius factor four and a single polynomial amplitude factor R.

theorem EulerPacketParentLabelBounds.gradient_scaled_gevrey (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (hrep : ↑↑u =ᵐ[MeasureTheory.volume] f) (q : ℕ) (hq : 3 ≤ q) (R A : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hb : ∀ (n : ℕ), EulerParameterWordGevrey.block direction q (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) n 0 ≤ A * EulerGevrey.majorant R 0 n) (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hL : ‖L‖ ≤ 1) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (y : EulerSmoothLimit.Space) => fderiv ℝ f (L y)) x‖ ≤ embeddingCost * A * R * EulerGevrey.majorant (4 * R) 0 n

Label normalization by a contraction does not enlarge positive spatial derivatives. This applies to the source scaling a=ℓ y.

theorem EulerPacketParentLabelBounds.deformation_scaled_gevrey (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (hrep : ↑↑u =ᵐ[MeasureTheory.volume] f) (q : ℕ) (hq : 3 ≤ q) (R A : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hb : ∀ (n : ℕ), EulerParameterWordGevrey.block direction q (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) n 0 ≤ A * EulerGevrey.majorant R 0 n) (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hL : ‖L‖ ≤ 1) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (y : EulerSmoothLimit.Space) => ContinuousLinearMap.id ℝ EulerSmoothLimit.Space + fderiv ℝ f (L y)) x‖ ≤ (1 + embeddingCost * A * R) * EulerGevrey.majorant (4 * R) 0 n

The actual deformation is identity plus the derivative of the L² displacement. The identity is kept out of the spatial L² datum.

def EulerPacketParentLabelBounds.coefficientRadius (K : ℝ) : ℝ

Coefficient radius, given by max 1024 (4*K).

Equations

• EulerPacketParentLabelBounds.coefficientRadius K = max 1024 (4 * K)

noncomputable def EulerPacketParentLabelBounds.gradientAmplitude (K : ℝ) : ℝ

Gradient amplitude, given by embeddingCost*K^2.

Equations

• EulerPacketParentLabelBounds.gradientAmplitude K = EulerPacketParentLabelBounds.embeddingCost * K ^ 2

noncomputable def EulerPacketParentLabelBounds.frameAmplitude (K : ℝ) : ℝ

Frame amplitude, given by 1+gradientAmplitude K.

Equations

• EulerPacketParentLabelBounds.frameAmplitude K = 1 + EulerPacketParentLabelBounds.gradientAmplitude K

theorem EulerPacketParentLabelBounds.coefficientRadius_lower (K : ℝ) : 1024 ≤ coefficientRadius K

theorem EulerPacketParentLabelBounds.coefficientRadius_nonneg (K : ℝ) : 0 ≤ coefficientRadius K

theorem EulerPacketParentLabelBounds.gradientAmplitude_nonneg (K : ℝ) : 0 ≤ gradientAmplitude K

theorem EulerPacketParentLabelBounds.frameAmplitude_nonneg (K : ℝ) : 0 ≤ frameAmplitude K

theorem EulerPacketParentLabelBounds.labelScaling_norm_le (ℓ : ℝ) (hℓ : 0 ≤ ℓ) (hℓ1 : ℓ ≤ 1) : ‖ℓ • ContinuousLinearMap.id ℝ EulerSmoothLimit.Space‖ ≤ 1

An actual scalar label scaling with 0≤ℓ≤1 is a linear contraction.

theorem EulerPacketParentLabelBounds.source_block_bound (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) (K : ℝ) (hb : ∀ (n : ℕ), EulerMeanClassicalWordBounds.classicalBlockSize direction 6 u hu n ≤ K ^ (n + 1) * ↑n.factorial ^ 2) (n : ℕ) : EulerParameterWordGevrey.block direction 6 (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) n 0 ≤ K * EulerGevrey.majorant K 0 n

theorem EulerPacketParentLabelBounds.source_gradient_bound (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (hrep : ↑↑u =ᵐ[MeasureTheory.volume] f) (K : ℝ) (hK : 0 ≤ K) (hb : ∀ (n : ℕ), EulerMeanClassicalWordBounds.classicalBlockSize direction 6 u hu n ≤ K ^ (n + 1) * ↑n.factorial ^ 2) (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hL : ‖L‖ ≤ 1) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (y : EulerSmoothLimit.Space) => fderiv ℝ f (L y)) x‖ ≤ gradientAmplitude K * EulerGevrey.majorant (coefficientRadius K) 0 n

A velocity or acceleration in the literal physical-label H⁶ word norm gives its actual spatial Jacobian at one polynomial coefficient radius.

theorem EulerPacketParentLabelBounds.source_deformation_bound (u : ↥EulerMeanSolenoidal.L2) (hu : EulerMeanSmoothRepresentative.SmoothOrbit u) (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (hrep : ↑↑u =ᵐ[MeasureTheory.volume] f) (K : ℝ) (hK : 0 ≤ K) (hb : ∀ (n : ℕ), EulerMeanClassicalWordBounds.classicalBlockSize direction 6 u hu n ≤ K ^ (n + 1) * ↑n.factorial ^ 2) (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hL : ‖L‖ ≤ 1) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (y : EulerSmoothLimit.Space) => ContinuousLinearMap.id ℝ EulerSmoothLimit.Space + fderiv ℝ f (L y)) x‖ ≤ frameAmplitude K * EulerGevrey.majorant (coefficientRadius K) 0 n

The parent displacement bound gives the full deformation, including its constant identity, without making the identity an L² datum.