The time-zero normal step: the same selected correction supplies the next actual state, low source bounds and renewed geometric frame.

@[reducible, inline]

abbrev EulerPacketInduction.Stage.ForwardChoice {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : Type

Forward choice: an abbreviation for GeometryForwardChoice I P.restrictedState k hk ell (S.support_pos 1) (S.support_one 1).

Equations

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

noncomputable def EulerPacketInduction.Stage.chooseForward {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : P.ForwardChoice hq hB

Choose forward, choosing the witness provided by Forward.

Equations

• P.chooseForward hq hB = Classical.choice ⋯

noncomputable def EulerPacketInduction.Stage.forwardParent {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : EulerParentPacketFrames.Parent

Forward parent, given by (F).parent.

Equations

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

noncomputable def EulerPacketInduction.Stage.forwardState {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : EulerParentPacketFrames.SmoothState (P.forwardParent hq hB)

Forward state, given by GeometryForwardChoice.state I P.restrictedState k hk ell (S.support_pos 1) (S.support_one 1) F symmetric.

Equations

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

theorem EulerPacketInduction.Stage.forward_smallness {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : (P.restrictedLow.K + 2 * (EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X 0) * (P.forwardGuards hq hB).hchild * ((P.forwardGuards hq hB).δ * EulerPacketGeometryLowBounds.goodRatio + (P.forwardGuards hq hB).earlyRatio) + EulerPacketSourceScaleSequence.frequency S.J S.X 0 ^ (-(1 / 4))) * (P.nextHorizon ^ 2 / 2) + (P.restrictedLow.Be + ((P.forwardGuards hq hB).hchild * (P.forwardGuards hq hB).earlyRatio + EulerPacketSourceScaleSequence.frequency S.J S.X 0 ^ (-(1 / 4)))) * P.nextHorizon + EulerMeanHarmonic.boundaryLocalizationC2 * (P.restrictedLow.Bc + ((P.forwardGuards hq hB).hchild * (P.forwardGuards hq hB).earlyRatio + EulerPacketSourceScaleSequence.frequency S.J S.X 0 ^ (-(1 / 4)))) * P.restrictedLow.r ^ 3 * P.nextHorizon ≤ 1 / 2

noncomputable def EulerPacketInduction.Stage.forwardLow {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : EulerParentPacketFrames.LowBounds (P.forwardParent hq hB)

Forward low as an element of LowBounds (P.forwardParent hq hB).

Equations

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

noncomputable def EulerPacketInduction.Stage.forwardRenewal {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : EulerPacketSourceGeometry.ParentFrame (frameData (P.forwardParent hq hB)) (P.forwardGeometry hq hB).targetTime

Forward renewal as an element of ParentFrame (frameData (P.forwardParent hq hB)) (P.forwardGeometry hq hB).targetTime.

Equations

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

theorem EulerPacketInduction.Stage.forwardRenewal_matches {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : EulerParentPacketFrames.RenewalAtTarget (P.forwardGeometry hq hB) (P.forwardRenewal hq hB)

noncomputable def EulerPacketInduction.Stage.forwardNextFrame {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : EulerPacketSourceGeometry.ParentFrame (frameData (P.forwardParent hq hB)) P.nextTime

Forward next frame, given by (P.forwardRenewal hq hB).changeActivation (P.forwardGeometry_targetTime hq hB).

Equations

• P.forwardNextFrame hq hB = (P.forwardRenewal hq hB).changeActivation ⋯

theorem EulerPacketInduction.Stage.forwardPhysicalBounds {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (t : ↑(Set.Icc 0 (EulerParentPacketFrames.GeometryForwardChoice.parent (P.forwardInput hq hB) P.restrictedState (EulerPacketSourceScaleSequence.frequency S.J S.X 0) ⋯ (EulerPacketSourceScaleSequence.supportScale S.J S.X 1) ⋯ ⋯ (P.chooseForward hq hB)).T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => (P.forwardState hq hB).evolution.velocity (↑t, y)) x‖ ≤ EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X 0 + (P.forwardGuards hq hB).hchild * (EulerPacketGeometryLowBounds.goodRatio + (P.forwardGuards hq hB).earlyRatio) + EulerPacketSourceScaleSequence.frequency S.J S.X 0 ^ (-(1 / 4)) ∧ ‖fderiv ℝ ((P.forwardState hq hB).evolution.force t) x‖ ≤ EulerPacketLowConstants.hessianConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X 0 * EulerPacketSourceScaleSequence.olderShear S.J S.X 0 + 2 * (EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X 0) * (P.forwardGuards hq hB).hchild * (EulerPacketGeometryLowBounds.goodRatio + (P.forwardGuards hq hB).earlyRatio) + EulerPacketSourceScaleSequence.frequency S.J S.X 0 ^ (-(1 / 4))

Whole-horizon physical bounds for the forward child, kept as one named proof to avoid elaborating the packet estimate twice inside Step.

noncomputable def EulerPacketInduction.Stage.forwardStep {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : P.Step

The forward choice's parent, state, low bounds, physical bounds and renewed frame, with the guards' shear, spike and earlyRatio.

Equations

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

noncomputable def EulerPacketInduction.Stage.forwardNext {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : Stage S 1

Assemble the forward packet using the shared successor invariant.

Equations

• P.forwardNext hq hB = P.next (P.forwardStep hq hB)

theorem EulerPacketInduction.Stage.forwardNext_time {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : (P.forwardNext hq hB).time = P.nextTime