The literal initial increments of an actual stage family have one smooth L² limit in every Sobolev order. The finite exceptional prefix is retained in the initial velocity of stage one.

Any actual family of packet stages with convergent H³ initial data excludes an ordinary Euler evolution on the base horizon. Each stage is compared only on its own genuine horizon.

theorem EulerPacketInduction.Stage.false_of_evolution {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} (P : (n : ℕ) → Stage S n) (u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hinit : Filter.Tendsto (fun (n : ℕ) => EulerPhysicalL2Scaling.derivativeSum 3 ((fun (x : EulerSmoothLimit.Space) => (P n).state.evolution.velocity (0, x)) - u₀)) Filter.atTop (nhds 0)) (U : EulerOrdinarySobolev.Evolution (EulerPacketBaseGuardScales.baseHorizon S.J S.X) ⋯) (hU₀ : (U.velocity ⟨0, ⋯⟩).field = u₀) : False

theorem EulerPacketInduction.Stage.no_euler_evolution_of_initial_H3 {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} (P : (n : ℕ) → Stage S n) (u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hinit : Filter.Tendsto (fun (n : ℕ) => EulerPhysicalL2Scaling.derivativeSum 3 ((fun (x : EulerSmoothLimit.Space) => (P n).state.evolution.velocity (0, x)) - u₀)) Filter.atTop (nhds 0)) : ¬∃ (U : EulerOrdinarySobolev.Evolution (EulerPacketBaseGuardScales.baseHorizon S.J S.X) ⋯), (U.velocity ⟨0, ⋯⟩).field = u₀

Exact reindexing of the prescribed scale sequence after finitely many exceptional initial stages. No new choice of asymptotic scales is made.

theorem EulerPacketSourceScaleSequence.scaleSequence_shift (J : ℕ) (X : ℝ) (r n : ℕ) : EulerPacketSourceScaleChoice.scaleSequence (J + r) (EulerPacketSourceScaleChoice.scaleSequence J X r) n = EulerPacketSourceScaleChoice.scaleSequence J X (r + n)

theorem EulerPacketSourceScaleSequence.frequency_shift (J : ℕ) (X : ℝ) (r n : ℕ) : frequency (J + r) (EulerPacketSourceScaleChoice.scaleSequence J X r) n = frequency J X (r + n)

theorem EulerPacketSourceScaleSequence.supportScale_shift (J : ℕ) (X : ℝ) (r n : ℕ) : supportScale (J + r) (EulerPacketSourceScaleChoice.scaleSequence J X r) n = supportScale J X (r + n)

theorem EulerPacketSourceScaleSequence.spike_shift (J : ℕ) (X : ℝ) (r n : ℕ) : spike (J + r) (EulerPacketSourceScaleChoice.scaleSequence J X r) n = spike J X (r + n)

theorem EulerPacketSourceScaleSequence.parameterEnvelope_shift (J : ℕ) (hJ : 1 ≤ J) (C c : ℝ) (p q : ℕ) (X : ℝ) (r n : ℕ) : EulerPacketUniformFrequencyScales.parameterEnvelope (J + r) C c p q (EulerPacketSourceScaleChoice.scaleSequence J X r) n = EulerPacketUniformFrequencyScales.parameterEnvelope J C c p q X (r + n)

noncomputable def EulerPacketInduction.Stage.initialTailInput {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : (n : ℕ) → Stage S n) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (i : ℕ) : EulerPacketInitial.Input ↥(EulerTransverseFrameCoordinates.referencePlane ((P (1 + i)).joinedNormal ⋯))

Initial tail input as an element of EulerPacketInitial.Input (referencePlane ((P (1+i)).joinedNormal (by omega))).

Equations

• EulerPacketInduction.Stage.initialTailInput P hq hB i = (P (1 + i)).joinedInput ⋯ hq hB

theorem EulerPacketInduction.Stage.initialTail_parameter {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : (n : ℕ) → Stage S n) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (i : ℕ) : (initialTailInput P hq hB i).parameterSize ≤ EulerPacketUniformFrequencyScales.parameterEnvelope (S.J + 1) (EulerNormalPacketParameters.sourceConstant 4) 320 20 1000 (EulerPacketSourceScaleChoice.scaleSequence S.J S.X 1) i

theorem EulerPacketInduction.Stage.initialTail_scale {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : (n : ℕ) → Stage S n) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (i : ℕ) : (initialTailInput P hq hB i).parent.ell = EulerPacketSourceScaleSequence.supportScale (S.J + 1) (EulerPacketSourceScaleChoice.scaleSequence S.J S.X 1) i

theorem EulerPacketInduction.Stage.initialTail_sigma {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : (n : ℕ) → Stage S n) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (i : ℕ) : (initialTailInput P hq hB i).frame.sigma * EulerPacketSourceScaleChoice.scaleSequence (S.J + 1) (EulerPacketSourceScaleChoice.scaleSequence S.J S.X 1) i ≤ 2

theorem EulerPacketInduction.Stage.initialTail_four {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (i : ℕ) : 4 ≤ EulerPacketSourceScaleSequence.frequency (S.J + 1) (EulerPacketSourceScaleChoice.scaleSequence S.J S.X 1) i

theorem EulerPacketInduction.Stage.initialTail_frequency {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : (n : ℕ) → Stage S n) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (i : ℕ) : (initialTailInput P hq hB i).frequencyGuard (EulerPacketSourceScaleSequence.frequency (S.J + 1) (EulerPacketSourceScaleChoice.scaleSequence S.J S.X 1) i)

def EulerPacketInduction.Stage.initialBase {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : (n : ℕ) → Stage S n) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Initial base, given by (P 1).state.regularity.velocity (P 1).parent.zeroTime.

Equations

• EulerPacketInduction.Stage.initialBase P = (P 1).state.regularity.velocity (P 1).parent.zeroTime

noncomputable def EulerPacketInduction.Stage.initialDataLimit {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : (n : ℕ) → Stage S n) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Initial data limit, constructed using EulerPacketInitial.fullInitialLimit.

Equations

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

theorem EulerPacketInduction.Stage.initial_velocity_partial {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : (n : ℕ) → Stage S n) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (hstep : ∀ (n : ℕ) (hn : n ≠ 0), (fun (x : EulerSmoothLimit.Space) => (P (n + 1)).state.evolution.velocity (0, x)) = (fun (x : EulerSmoothLimit.Space) => (P n).state.evolution.velocity (0, x)) + (((P n).joinedInput hn hq hB).high (EulerPacketSourceScaleSequence.frequency S.J S.X n) + ((P n).joinedInput hn hq hB).mean (EulerPacketSourceScaleSequence.frequency S.J S.X n))) (N : ℕ) : (fun (x : EulerSmoothLimit.Space) => (P (1 + N)).state.evolution.velocity (0, x)) = (initialBase P).field + EulerPacketInitial.initialPartial (initialTailInput P hq hB) (S.J + 1) (EulerPacketSourceScaleChoice.scaleSequence S.J S.X 1) N

theorem EulerPacketInduction.Stage.initialDataLimit_Hm {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : (n : ℕ) → Stage S n) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (hstep : ∀ (n : ℕ) (hn : n ≠ 0), (fun (x : EulerSmoothLimit.Space) => (P (n + 1)).state.evolution.velocity (0, x)) = (fun (x : EulerSmoothLimit.Space) => (P n).state.evolution.velocity (0, x)) + (((P n).joinedInput hn hq hB).high (EulerPacketSourceScaleSequence.frequency S.J S.X n) + ((P n).joinedInput hn hq hB).mean (EulerPacketSourceScaleSequence.frequency S.J S.X n))) (s : ℕ) : Filter.Tendsto (fun (n : ℕ) => EulerPhysicalL2Scaling.derivativeSum s ((fun (x : EulerSmoothLimit.Space) => (P n).state.evolution.velocity (0, x)) - (initialDataLimit P hq hB).field)) Filter.atTop (nhds 0)

theorem EulerPacketInduction.Stage.initialDataLimit_no_euler {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : (n : ℕ) → Stage S n) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (hstep : ∀ (n : ℕ) (hn : n ≠ 0), (fun (x : EulerSmoothLimit.Space) => (P (n + 1)).state.evolution.velocity (0, x)) = (fun (x : EulerSmoothLimit.Space) => (P n).state.evolution.velocity (0, x)) + (((P n).joinedInput hn hq hB).high (EulerPacketSourceScaleSequence.frequency S.J S.X n) + ((P n).joinedInput hn hq hB).mean (EulerPacketSourceScaleSequence.frequency S.J S.X n))) : ¬∃ (U : EulerOrdinarySobolev.Evolution (EulerPacketBaseGuardScales.baseHorizon S.J S.X) ⋯), (U.velocity ⟨0, ⋯⟩).field = (initialDataLimit P hq hB).field