The packet stage invariant

GrowthData contains the Euler state, activation time and strain decomposition used to prove gradient growth. Stage adds the source bounds and frame guards needed to construct the next packet. Separating them lets the growth theorem apply without assuming the successor construction's hypotheses. All cumulative bounds use only earlier indices.

noncomputable def EulerPacketInduction.frameData (A : EulerParentPacketFrames.Parent) : EulerTransversePacketProvider.Data ↥EulerBaseDatum.FirstPlane

The transverse packet data of a parent in the fixed reference plane: its frame, inverse frame and strain along the centre trajectory, against which a stage's ParentFrame is measured.

Equations

• EulerPacketInduction.frameData A = A.transverseData EulerBaseDatum.firstNormal EulerBaseDatum.firstNormal_unit EulerBaseDatum.firstFrame EulerPacketSupport.support EulerPacketSupport.compact

structure EulerPacketInduction.GrowthData {c B : ℝ} (S : EulerPacketInductionScales.Scales c B) (n : ℕ) : Type

The state, activation and strain bounds used by the growth argument. The common horizon and Sobolev realisation also support comparison with other Euler evolutions. These data impose no hypotheses on a successor packet.

• parent : EulerParentPacketFrames.Parent

  The parent: the volume-preserving particle map, with its velocity and acceleration, that carries the current Euler state on [0, parent.T]. Its frame, strain and curvature are the coefficients every estimate reads.

• state : EulerParentPacketFrames.SmoothState self.parent

  The current Euler solution on the parent: a pointwise classical Evolution, its Sobolev realisation regularity (converted to an ordinary evolution by the contradiction), its label bounds, and its odd symmetry, which makes the strain at the origin equal to the velocity gradient there (strain_origin).

• time : ℝ

  The activation time of the most recently added packet (0 at the base stage). The divergent quantity activationGradient is the velocity gradient at (time, 0).

• time_nonneg : 0 ≤ self.time

  The activation time is a time of the stage solution.

• horizon_eq : self.parent.T = self.time + 2 * EulerPacketSourceScaleSequence.timeWidth S.J S.X n

  The stage solution lives exactly 2·timeWidth n beyond the activation. This gives time < parent.T, so the activation is an interior time, and it lets the next stage's horizon nest strictly inside this one.

• horizon_le : self.parent.T ≤ EulerPacketBaseGuardScales.baseHorizon S.J S.X

  Every stage horizon lies inside the base horizon, so all stage solutions can be compared with one hypothetical evolution on [0, baseHorizon].

• frame : EulerPacketSourceGeometry.ParentFrame (frameData self.parent) self.time

  The frame of the parent strain along the centre trajectory at the activation time: background B, ray m, velocity v, shear coefficient, and the bounds G on B and error on the remainder.

• frame_shear : self.frame.shear = EulerPacketSourceScaleSequence.previousShear S.J S.X n

  The leading rank-one part of the strain at the centre has shear previousShear n, the target shear of the latest packet. This is the term the growth argument isolates.

• frame_bound : self.frame.G ≤ EulerPacketLowConstants.frameConstant * (1 + EulerPacketSourceScaleSequence.olderShear S.J S.X n)

  The background B is bounded one shear level lower, by frameConstant·(1 + olderShear n), so that the leading term dominates it.

• frame_error : self.frame.error ≤ EulerPacketSourceScaleActual.priorError S.J S.D S.X n

  The remainder after B and the rank-one shear are removed is at most priorError n, an inverse fourth root of the previous frequency, which is negligible against the leading shear.

structure EulerPacketInduction.Stage {c B : ℝ} (S : EulerPacketInductionScales.Scales c B) (n : ℕ) : Type

A full packet stage, including the induction hypotheses needed by the successor construction. Stage.toGrowthData retains only the state, activation and frame bounds needed for gradient growth. The full record keeps its original projection interface.

• parent : EulerParentPacketFrames.Parent

  The parent: the volume-preserving particle map, with its velocity and acceleration, that carries the current Euler state on [0, parent.T]. Its frame, strain and curvature are the coefficients every estimate reads.

• state : EulerParentPacketFrames.SmoothState self.parent

  The current Euler solution on the parent: a pointwise classical Evolution, its Sobolev realisation regularity (converted to an ordinary evolution by the contradiction), its label bounds, and its odd symmetry, which makes the strain at the origin equal to the velocity gradient there (strain_origin).

• low : EulerParentPacketFrames.LowBounds self.parent

  The low-frequency source bounds of the parent: exterior and core lower bounds Be, Bc on the initial strain, the curvature bound K, the localization length L and the core radius r. They feed the coercivity guard small of the next parent.

• time : ℝ

  The activation time of the most recently added packet (0 at the base stage). The divergent quantity activationGradient is the velocity gradient at (time, 0).

• time_nonneg : 0 ≤ self.time

  The activation time is a time of the stage solution.

• time_zero : n = 0 → self.time = 0

  The base stage is activated at time 0; the forward step poses its packet there.

• time_lower : n ≠ 0 → EulerPacketBaseGuardScales.baseHorizon S.J S.X / 12 ≤ self.time

  After the first step the activation time is at least a twelfth of the base horizon. This bounds time⁻¹, and through it the history terms of the joined step (history_layer).

• horizon_eq : self.parent.T = self.time + 2 * EulerPacketSourceScaleSequence.timeWidth S.J S.X n

  The stage solution lives exactly 2·timeWidth n beyond the activation. This gives time < parent.T, so the activation is an interior time, and it lets the next stage's horizon nest strictly inside this one.

• horizon_le : self.parent.T ≤ EulerPacketBaseGuardScales.baseHorizon S.J S.X

  Every stage horizon lies inside the base horizon, so all stage solutions can be compared with one hypothetical evolution on [0, baseHorizon].

• scale_eq : self.parent.ell = EulerPacketSourceScaleSequence.supportScale S.J S.X n

  The parent's scale is supportScale n: the next increment is supported in a ball of radius half this scale.

• label_eq : self.state.labels.K = EulerPacketSourceScaleSequence.previousFrequency S.J S.D S.X n ^ 80

  The label constant of the state (the Sobolev size of the parent's displacement, velocity and acceleration) is previousFrequency n ^ 80; the next packet's frequency guard must dominate it.

• gradient_bound (t : ↑(Set.Icc 0 self.parent.T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => self.state.evolution.velocity (↑t, y)) x‖ ≤ EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n

  The velocity gradient is bounded on the whole horizon by gradientConstant·previousShear n: the upper bound matching the lower bound at the centre, consumed by the next step's low bounds and history data.

• hessian_bound (t : ↑(Set.Icc 0 self.parent.T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (self.state.evolution.force t) x‖ ≤ EulerPacketLowConstants.hessianConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n * EulerPacketSourceScaleSequence.olderShear S.J S.X n

  The pressure Hessian (the gradient of the force) is bounded by hessianConstant·previousShear n·olderShear n.

• exterior_bound : self.low.Be ≤ EulerBaseDatum.initialCoefficientCost + ∑ i ∈ Finset.range n, EulerPacketInductionScales.initialIncrement S.J S.X i

  Cumulative bound on the exterior strain constant: the base cost plus the summable per-stage increments of the scale choice.

• core_bound : self.low.Bc ≤ EulerPacketLowConstants.gradientConstant * S.X ^ 1000 + ∑ i ∈ Finset.range n, EulerPacketInductionScales.initialIncrement S.J S.X i

  Cumulative bound on the core strain constant, starting from the base shear X^1000.

• pressure_bound : self.low.K ≤ EulerBaseDatum.initialCoefficientCost + EulerBaseDatum.literalInitialPressureCost S.D S.X + ∑ i ∈ Finset.range n, EulerPacketInductionScales.pressureIncrement S.J S.X i

  Cumulative bound on the curvature constant, starting from the base pressure cost. Together with the two bounds above it keeps the coercivity guard small true at every stage.

• boundary_eq : self.low.L = EulerMeanHarmonic.boundaryLocalizationC1 * self.low.Bc + 1

  The localization length is determined by the core bound.

• radius_eq : self.low.r = EulerPacketBaseGuardScales.baseRadius S.X

  The core radius is the base radius X^(-1000) at every stage.

• frame : EulerPacketSourceGeometry.ParentFrame (frameData self.parent) self.time

  The frame of the parent strain along the centre trajectory at the activation time: background B, ray m, velocity v, shear coefficient, and the bounds G on B and error on the remainder.

• frame_shear : self.frame.shear = EulerPacketSourceScaleSequence.previousShear S.J S.X n

  The leading rank-one part of the strain at the centre has shear previousShear n, the target shear of the latest packet. This is the term the growth argument isolates.

• frame_bound : self.frame.G ≤ EulerPacketLowConstants.frameConstant * (1 + EulerPacketSourceScaleSequence.olderShear S.J S.X n)

  The background B is bounded one shear level lower, by frameConstant·(1 + olderShear n), so that the leading term dominates it.

• frame_error : self.frame.error ≤ EulerPacketSourceScaleActual.priorError S.J S.D S.X n

  The remainder after B and the rank-one shear are removed is at most priorError n, an inverse fourth root of the previous frequency, which is negligible against the leading shear.

• coupling_error : |self.frame.a - 1| ≤ 2 * ∑ i ∈ Finset.range n, EulerParentRenewalScale.renewalCost S.J S.D 4 c EulerPacketLowConstants.frameConstant S.X i

  The normalised coupling a = ⟨m̂, B v̂⟩ stays within a summable distance of 1; each renewal moves it by at most renewalCost i. This gives 1/2 ≤ a ≤ 2 (coupling_bounds).

• tilt_lower : 1 / 2 ≤ self.frame.sigma ^ 2 * EulerPacketSourceScaleChoice.scaleSequence S.J S.X n ^ 2

  The normalised tilt σ² = ⟨m̂ × v̂, B v̂⟩/a is at least 1/(2 x_n²).

• tilt_upper : self.frame.sigma ^ 2 * EulerPacketSourceScaleChoice.scaleSequence S.J S.X n ^ 2 ≤ 2

  The normalised tilt is at most 2/x_n²: the renewed frame is nearly untilted, at the scale of the sequence.

• compression : n ≠ 0 → inner ℝ ((self.frame.B self.time) (EulerPacketNormalizedPrimary.unit (self.frame.m self.time))) (EulerPacketNormalizedPrimary.unit (self.frame.m self.time)) + EulerPacketSourceScaleActual.priorError S.J S.D S.X n < 0

  After the first step the background strain compresses along the ray with a margin exceeding priorError n. Since m' = -Bᵀm, this makes ‖m‖, and with it the shear c‖m‖‖v‖ of the next packet, grow; the joined guards take it as input and the renewal re-establishes it.

theorem EulerPacketInduction.GrowthData.time_lt {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : GrowthData S n) : P.time < P.parent.T

The positive post-activation time width puts activation inside the horizon.

theorem EulerPacketInduction.GrowthData.time_one {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : GrowthData S n) : P.time ≤ 1

The common base horizon bounds every activation time by one.

def EulerPacketInduction.Stage.toGrowthData {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : GrowthData S n

Forget the source bounds and frame guards that only the successor construction needs.

Equations

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

theorem EulerPacketInduction.Stage.coupling_bounds {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : 1 / 2 ≤ P.frame.a ∧ P.frame.a ≤ 2

theorem EulerPacketInduction.Stage.coupling_pos {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : 0 < P.frame.a

theorem EulerPacketInduction.Stage.sigma_nonneg {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : 0 ≤ P.frame.sigma

theorem EulerPacketInduction.Stage.sigma_pos {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : 0 < P.frame.sigma

theorem EulerPacketInduction.Stage.time_lt {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.time < P.parent.T

The activation time is strictly inside the stage horizon.

theorem EulerPacketInduction.Stage.time_one {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.time ≤ 1

Every activation occurs before time one.

theorem EulerPacketInduction.Stage.horizon_lower {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : EulerPacketBaseGuardScales.baseHorizon S.J S.X / 12 < P.parent.T

theorem EulerPacketInduction.Stage.horizon_reciprocal {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.parent.T⁻¹ ≤ 12 / EulerPacketBaseGuardScales.baseHorizon S.J S.X

theorem EulerPacketInduction.Stage.time_pos {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) : 0 < P.time

theorem EulerPacketInduction.Stage.time_reciprocal {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) : P.time⁻¹ ≤ 12 / EulerPacketBaseGuardScales.baseHorizon S.J S.X

theorem EulerPacketInduction.Stage.exterior_cap {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.low.Be ≤ EulerBaseDatum.initialCoefficientCost + 1

theorem EulerPacketInduction.Stage.core_cap {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.low.Bc ≤ EulerPacketLowConstants.gradientConstant * S.X ^ 1000 + 2

theorem EulerPacketInduction.Stage.pressure_cap {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.low.K ≤ EulerBaseDatum.initialCoefficientCost + 1

theorem EulerPacketInduction.Stage.source_stage {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : EulerPacketSourceScaleGuards.StageGuards S.J S.D 4 c S.X EulerPacketInductionScales.geometryConstant (fun (x : ℕ) => P.frame.a) (fun (x : ℕ) => P.frame.sigma ^ 2) n

theorem EulerPacketInduction.Stage.normalized_sigma {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.frame.sigma * EulerPacketSourceScaleChoice.scaleSequence S.J S.X n ≤ 2

theorem EulerPacketInduction.Stage.strain_bound {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) (t : ↑(Set.Icc 0 P.parent.T)) (x : EulerSmoothLimit.Space) : ‖(P.parent.strain.field t) x‖ ≤ EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n

theorem EulerPacketInduction.Stage.curvature_bound {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) (t : ↑(Set.Icc 0 P.parent.T)) (x : EulerSmoothLimit.Space) : ‖(P.parent.curvature.field t) x‖ ≤ EulerPacketLowConstants.hessianConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n * EulerPacketSourceScaleSequence.olderShear S.J S.X n