The successor step, written once #
The forward step (stage 0, no history) and the joined step (positive
history) build stage n + 1 from stage n by the same assembly. They differ in
the analytic pipeline that constructs the packet and in the ratio, earlyRatio
or badRatio, by which its guards measure the source error. Step records
what either pipeline delivers, phrased against the scale sequences, and next
is the one assembly of the Stage invariant from it. PacketForwardSuccessor
and PacketInfiniteConstruction instantiate Step; nothing below reads a guard.
Adapted from Code4me2/NavierStokesAndEuler, commit
26e896edbdbe1215c0d50ddba24b2b6453646f5f, Euler/PacketStageSuccessor.lean.
The initial-gradient increment of the next packet, h·r for its target
shear h and error ratio r plus the frequency error, fits the stage's
initialIncrement budget once its bad-pressure cost does.
The coercivity guard of the next parent's low bounds, from the packet's
budgets: h is the packet's target shear, d its spike and r its error
ratio. The parent's cumulative bounds absorb the increments (next_localized).
What one chosen packet delivers to the successor assembly at stage n.
The scalars targetShear, spikeAmplitude, errorRatio are the packet's target shear, spike and
error ratio as its guards name them. targetShear_eq identifies the shear with the
scale sequence; the ratio is earlyRatio in the forward step and badRatio
in the joined step. The rest is what the packet choice
produces on the restricted parent: the new parent and state (parent_horizon,
parent_scale, label_eq), the parent's low bounds updated by the packet's
error terms (low_*), the whole-horizon physical bounds, the pressure
budgets that the scale choice makes summable, and the renewed frame matched
to the packet's lowGeometry at its target time nextTime.
- parent : EulerParentPacketFrames.Parent
The parent particle map carrying the new packet.
- state : EulerParentPacketFrames.SmoothState self.parent
The Euler state constructed on the new parent.
- targetShear : ℝ
The target shear of the packet.
- spikeAmplitude : ℝ
The spike amplitude appearing in the pressure increment.
- errorRatio : ℝ
The error ratio of the selected packet pipeline.
The error ratio is nonnegative.
The target shear agrees with the next prescribed shear level.
The child uses the shortened horizon of the current stage.
The child uses the next prescribed support scale.
The child labels obey the next frequency bound.
- low : EulerParentPacketFrames.LowBounds self.parent
The updated source bounds of the new parent.
- low_exterior : self.low.Be = P.low.Be + (self.targetShear * self.errorRatio + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4)))
The exterior source bound increases by the initial-gradient error.
- low_core : self.low.Bc = P.low.Bc + (self.targetShear * self.errorRatio + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4)))
The core source bound increases by the same initial-gradient error.
- low_pressure : self.low.K = P.low.K + 2 * (EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n) * self.targetShear * (self.spikeAmplitude * EulerPacketGeometryLowBounds.goodRatio + self.errorRatio) + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4))
The curvature bound includes the packet pressure error.
The localization length is determined by the updated core bound.
The source core keeps the current radius.
- physical_bounds (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 + self.targetShear * (EulerPacketGeometryLowBounds.goodRatio + self.errorRatio) + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4)) ∧ ‖fderiv ℝ (self.state.evolution.force t) x‖ ≤ EulerPacketLowConstants.hessianConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n * EulerPacketSourceScaleSequence.olderShear S.J S.X n + 2 * (EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n) * self.targetShear * (EulerPacketGeometryLowBounds.goodRatio + self.errorRatio) + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4))
The new velocity gradient and pressure Hessian satisfy the packet estimates.
- bad_cost : 2 * (EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n) * self.targetShear * self.errorRatio ≤ EulerPacketPressureScale.badCost S.J 4 EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant 80 (EulerPacketSourceScaleChoice.scaleSequence S.J S.X) n
The ratio-dependent pressure error fits the bad-cost budget.
- pressure_cost : 2 * (EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n) * self.targetShear * (self.spikeAmplitude * EulerPacketGeometryLowBounds.goodRatio + self.errorRatio) + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4)) ≤ EulerPacketInductionScales.pressureIncrement S.J S.X n
The complete pressure error fits the summable pressure budget.
- geometry : EulerPacketMovingFrame.PhysicalGeometryData { x : EulerSmoothLimit.Space // ‖x‖ ≤ 1 / 2 }
The physical geometry to which the renewed frame is matched.
The geometric target time is the next activation time.
The geometry uses the current frame coupling.
The geometric tilt scale agrees with the next scale level.
The geometric spike is positive, as required for shear renewal.
The geometric target shear is the packet shear.
- renewal_errors : self.geometry.couplingError ≤ EulerParentRenewalScale.renewalCost S.J S.D 4 c EulerPacketLowConstants.frameConstant S.X n ∧ self.geometry.tiltError ≤ EulerParentRenewalScale.renewalCost S.J S.D 4 c EulerPacketLowConstants.frameConstant S.X n
Coupling and tilt errors fit the common summable renewal budget.
- renewal : EulerPacketSourceGeometry.ParentFrame (frameData self.parent) self.geometry.targetTime
The renewed frame on the new parent at the geometric target time.
- renewal_matches : EulerParentPacketFrames.RenewalAtTarget self.geometry self.renewal
The renewed frame satisfies the selected geometry.
- renewal_G : self.renewal.G = EulerPacketLowConstants.frameConstant * (1 + EulerPacketSourceScaleSequence.previousShear S.J S.X n)
The renewed background is controlled by the current shear level.
- renewal_error : self.renewal.error = EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4))
The renewed remainder is the inverse fourth root of the frequency.
Instances For
The selected error ratio fits the next global gradient and Hessian bounds.
Renewal preserves the prescribed coupling and tilt budgets.
One initial-gradient increment extends both cumulative source bounds.
One pressure increment extends the cumulative curvature bound.
The renewed coupling lies in the next cumulative error budget.
The renewed background compresses with the next stage's remainder margin.
Assemble the successor from the packet bounds and renewed frame. The analytic estimates are opaque theorems; the supplied parent, state, low bounds and frame remain available by reduction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The successor uses the renewed frame, reindexed to the next activation time.