The actual infinite packet family, from the concrete first stage and the two genuine successor constructions.

The positive-history normal step. One actual correction constructs the next Euler state, localized low bounds, renewed frame and exact initial increment, without any premise about a future stage.

@[reducible, inline]

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

Joined choice: an abbreviation for GeometryJoinedChoice I P.restrictedState k hk ell (S.support_pos (n+1)) (S.support_one (n+1)).

Equations

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

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

Choose joined, choosing the witness provided by Joined.

Equations

• P.chooseJoined hn hq hB = Classical.choice ⋯

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

Joined parent, given by (F).parent.

Equations

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

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

Joined state, given by GeometryJoinedChoice.state I P.restrictedState k hk ell (S.support_pos (n+1)) (S.support_one (n+1)) F symmetric.

Equations

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

theorem EulerPacketInduction.Stage.joined_smallness {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 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 n) * (P.joinedGuards hn hq hB).hchild * ((P.joinedGuards hn hq hB).δ * EulerPacketGeometryLowBounds.goodRatio + (P.joinedGuards hn hq hB).badRatio) + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4))) * (P.nextHorizon ^ 2 / 2) + (P.restrictedLow.Be + ((P.joinedGuards hn hq hB).hchild * (P.joinedGuards hn hq hB).badRatio + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4)))) * P.nextHorizon + EulerMeanHarmonic.boundaryLocalizationC2 * (P.restrictedLow.Bc + ((P.joinedGuards hn hq hB).hchild * (P.joinedGuards hn hq hB).badRatio + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4)))) * P.restrictedLow.r ^ 3 * P.nextHorizon ≤ 1 / 2

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

Joined low as an element of LowBounds (P.joinedParent hn hq hB).

Equations

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

noncomputable def EulerPacketInduction.Stage.joinedRenewal {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : EulerPacketSourceGeometry.ParentFrame (frameData (P.joinedParent hn hq hB)) (P.joinedGeometry hn hq hB).targetTime

Joined renewal as an element of ParentFrame (frameData (P.joinedParent hn hq hB)) (P.joinedGeometry hn hq hB).targetTime.

Equations

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

theorem EulerPacketInduction.Stage.joinedRenewal_matches {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : EulerParentPacketFrames.RenewalAtTarget (P.joinedGeometry hn hq hB) (P.joinedRenewal hn hq hB)

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

Joined next frame, given by (P.joinedRenewal hn hq hB).changeActivation (P.joinedGeometry_targetTime hn hq hB).

Equations

• P.joinedNextFrame hn hq hB = (P.joinedRenewal hn hq hB).changeActivation ⋯

theorem EulerPacketInduction.Stage.joinedPhysicalBounds {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (t : ↑(Set.Icc 0 (EulerParentPacketFrames.GeometryJoinedChoice.parent (P.joinedInput hn hq hB) P.restrictedState (EulerPacketSourceScaleSequence.frequency S.J S.X n) ⋯ (EulerPacketSourceScaleSequence.supportScale S.J S.X (n + 1)) ⋯ ⋯ (P.chooseJoined hn hq hB)).T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => (P.joinedState hn hq hB).evolution.velocity (↑t, y)) x‖ ≤ EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n + (P.joinedGuards hn hq hB).hchild * (EulerPacketGeometryLowBounds.goodRatio + (P.joinedGuards hn hq hB).badRatio) + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4)) ∧ ‖fderiv ℝ ((P.joinedState hn hq hB).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) * (P.joinedGuards hn hq hB).hchild * (EulerPacketGeometryLowBounds.goodRatio + (P.joinedGuards hn hq hB).badRatio) + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4))

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

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

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

Equations

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

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

Assemble the joined packet using the shared successor invariant.

Equations

• P.joinedNext hn hq hB = P.next (P.joinedStep hn hq hB)

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

theorem EulerPacketInduction.Stage.joinedNext_initial_increment {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : (fun (x : EulerSmoothLimit.Space) => (P.joinedNext hn hq hB).state.evolution.velocity (0, x) - P.state.evolution.velocity (0, x)) = (P.joinedInput hn hq hB).high (EulerPacketSourceScaleSequence.frequency S.J S.X n) + (P.joinedInput hn hq hB).mean (EulerPacketSourceScaleSequence.frequency S.J S.X n)

theorem EulerPacketInduction.Stage.joinedNext_initial_velocity {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : (fun (x : EulerSmoothLimit.Space) => (P.joinedNext hn hq hB).state.evolution.velocity (0, x)) = (fun (x : EulerSmoothLimit.Space) => P.state.evolution.velocity (0, x)) + ((P.joinedInput hn hq hB).high (EulerPacketSourceScaleSequence.frequency S.J S.X n) + (P.joinedInput hn hq hB).mean (EulerPacketSourceScaleSequence.frequency S.J S.X n))

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

Successor as an element of Stage S (n+1).

Equations

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

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

def EulerPacketInduction.stages {q : ℕ} {B : ℝ} (S : EulerPacketInductionScales.Scales (↑q) B) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (n : ℕ) : Stage S n

Stages as an element of (n : ℕ) → Stage S n | 0 => S.firstStage | n+1 => (stages n).successor hq hB.

Equations

• EulerPacketInduction.stages S hq hB 0 = S.firstStage
• EulerPacketInduction.stages S hq hB n.succ = (EulerPacketInduction.stages S hq hB n).successor hq hB

theorem EulerPacketInduction.stages_zero {q : ℕ} {B : ℝ} (S : EulerPacketInductionScales.Scales (↑q) B) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : stages S hq hB 0 = S.firstStage

theorem EulerPacketInduction.stages_succ {q : ℕ} {B : ℝ} (S : EulerPacketInductionScales.Scales (↑q) B) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (n : ℕ) : stages S hq hB (n + 1) = (stages S hq hB n).successor hq hB

theorem EulerPacketInduction.stages_time {q : ℕ} {B : ℝ} (S : EulerPacketInductionScales.Scales (↑q) B) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (n : ℕ) : (stages S hq hB (n + 1)).time = (stages S hq hB n).nextTime

theorem EulerPacketInduction.stages_initial_step {q : ℕ} {B : ℝ} (S : EulerPacketInductionScales.Scales (↑q) B) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (n : ℕ) (hn : n ≠ 0) : (fun (x : EulerSmoothLimit.Space) => (stages S hq hB (n + 1)).state.evolution.velocity (0, x)) = (fun (x : EulerSmoothLimit.Space) => (stages S hq hB n).state.evolution.velocity (0, x)) + (((stages S hq hB n).joinedInput hn hq hB).high (EulerPacketSourceScaleSequence.frequency S.J S.X n) + ((stages S hq hB n).joinedInput hn hq hB).mean (EulerPacketSourceScaleSequence.frequency S.J S.X n))

theorem EulerPacketInduction.stages_gradient_atTop {q : ℕ} {B : ℝ} (S : EulerPacketInductionScales.Scales (↑q) B) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : Filter.Tendsto (fun (n : ℕ) => (stages S hq hB n).activationGradient) Filter.atTop Filter.atTop

@[reducible, inline]

abbrev EulerPacketInduction.ConstructionScales : Type

Construction scales: an abbreviation for Scales (requiredExponent : ℝ) (commonThreshold gradientConstant hessianConstant).

Equations

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

noncomputable def EulerPacketInduction.constructionScales : ConstructionScales

Construction scales, given by Classical.choice (exists_scales (requiredExponent : ℝ) (commonThreshold gradientConstant hessianConstant) (Nat.cast_nonneg _)).

Equations

• EulerPacketInduction.constructionScales = Classical.choice EulerPacketInduction.constructionScales._proof_1✝

noncomputable def EulerPacketInduction.packets (n : ℕ) : Stage constructionScales n

Packets, given by stages constructionScales le_rfl le_rfl n.

Equations

• EulerPacketInduction.packets n = EulerPacketInduction.stages EulerPacketInduction.constructionScales ⋯ EulerPacketInduction.packets._proof_1 n

theorem EulerPacketInduction.packets_gradient_atTop : Filter.Tendsto (fun (n : ℕ) => (packets n).activationGradient) Filter.atTop Filter.atTop