The actual normal-stage source size is controlled by one fixed envelope. This includes the chosen terminal coordinate and canonical boundary coefficient, with the polynomial first shear retained.

The source size used by the canonical packet solve is bounded by one explicit polynomial-exponential envelope, including the base-sized boundary coefficient and both reciprocal time intervals.

def EulerPacketParameterEnvelope.boundConstant (Cθ CB Cξ : ℝ) : ℝ

Bound constant, given by 8+1120*(2*Cθ)^10+CB+Cξ.

Equations

• EulerPacketParameterEnvelope.boundConstant Cθ CB Cξ = 8 + 1120 * (2 * Cθ) ^ 10 + CB + Cξ

theorem EulerPacketParameterEnvelope.constant_pos (Cθ CB Cξ : ℝ) (hB : 0 ≤ CB) (hξ : 0 ≤ Cξ) : 0 < boundConstant Cθ CB Cξ

theorem EulerPacketParameterEnvelope.source_size_le (J D : ℕ) (hJ : 2 ≤ J) (X : ℝ) (hX : 1 ≤ X) (Cθ CB Cξ d c : ℝ) (hθ : 1 ≤ Cθ) (hB : 0 ≤ CB) (hξC : 0 ≤ Cξ) (hd : 0 ≤ d) (hc : 1 ≤ c) (hdc : d ≤ c) (R : ℕ) (hRc : ↑R * d ≤ c) (hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (hbaseK : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4)) (n : ℕ) (K Ti TiTotal Cp B ξ Θ Ei : ℝ) (hK0 : 0 ≤ K) (hK : K ≤ EulerPacketSourceScaleSequence.previousFrequency J D X n ^ d) (hTi : Ti ≤ 12 / EulerPacketBaseGuardScales.baseHorizon J X) (hTiTotal : TiTotal ≤ 12 / EulerPacketBaseGuardScales.baseHorizon J X) (hBc : B ≤ CB * X ^ 1000) (hξ : ξ ≤ Cξ * K ^ R) (hΘ0 : 0 ≤ Θ) (hΘ : Θ ≤ EulerPacketSourceScales.sourceTheta J Cθ (EulerPacketSourceScaleChoice.scaleSequence J X) n) (hEi0 : 0 ≤ Ei) (hEi : Ei ≤ 2 * EulerPacketSourceScaleSequence.previousShear J X n) (hCp : Cp ≤ 560 * Θ ^ 10 * Ei) : EulerParentInitializedRadius.parameterSize K Ti TiTotal Cp B (EulerPacketSourceScaleSequence.spike J X n) ξ + EulerPacketSourceScaleSequence.shear J X n ≤ EulerPacketUniformFrequencyScales.parameterEnvelope J (boundConstant Cθ CB Cξ) c 20 1000 X n

Actual selected terminal coordinates and the canonical boundary parameter have fixed polynomial caps. They are inputs to the uniform normal-stage source envelope.

noncomputable def EulerParentPacketParameterCaps.terminalConstant (CM CH : ℝ) : ℝ

Terminal constant, given by 8*(activationConstant CM CH+1)*(1+3*(1+embeddingCost)^2).

Equations

• EulerParentPacketParameterCaps.terminalConstant CM CH = 8 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) * (1 + 3 * (1 + EulerPacketParentLabelBounds.embeddingCost) ^ 2)

theorem EulerParentPacketParameterCaps.terminalConstant_nonneg (CM CH : ℝ) (hCH : 0 ≤ CH) : 0 ≤ terminalConstant CM CH

noncomputable def EulerParentPacketParameterCaps.boundaryConstant (CM : ℝ) : ℝ

Boundary constant, given by boundaryLocalizationC1*(CM+2)+1.

Equations

• EulerParentPacketParameterCaps.boundaryConstant CM = EulerMeanHarmonic.boundaryLocalizationC1 * (CM + 2) + 1

theorem EulerParentPacketParameterCaps.boundaryConstant_pos (CM : ℝ) (hCM : 0 ≤ CM) : 0 < boundaryConstant CM

theorem EulerParentPacketParameterCaps.boundary_parameter_bound (CM Bc L X : ℝ) (hX : 1 ≤ X) (hBc : Bc ≤ CM * X ^ 1000 + 2) (hL : L = EulerMeanHarmonic.boundaryLocalizationC1 * Bc + 1) : L ≤ boundaryConstant CM * X ^ 1000

theorem EulerParentPacketFrames.LabelData.selected_terminal_bound {A : Parent} (L : LabelData A) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hsupport : IsCompact support) {τ : ℝ} {hτ : 0 < τ} {hτT : τ < A.T} {P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm R support hsupport) τ} {H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm R support hsupport).initial τ hτ ⋯)} (G : EulerPacketSourceGeometry.Guards hτ hτT P H) (hH : 1 ≤ P.shear) : ‖EulerPacketSourceGeometry.Guards.terminal hτ hτT P H G‖ ≤ EulerParentPacketParameterCaps.terminalConstant G.CM G.CH * L.K ^ 4

noncomputable def EulerNormalPacketParameters.terminalCap : ℝ

Terminal cap, given by 1+terminalConstant gradientConstant hessianConstant.

Equations

• EulerNormalPacketParameters.terminalCap = 1 + EulerParentPacketParameterCaps.terminalConstant EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant

noncomputable def EulerNormalPacketParameters.sourceConstant (C : ℝ) : ℝ

Source constant, given by EulerPacketParameterEnvelope.boundConstant C (boundaryConstant gradientConstant) terminalCap.

Equations

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

theorem EulerNormalPacketParameters.terminalCap_one : 1 ≤ terminalCap

theorem EulerNormalPacketParameters.sourceConstant_pos (C : ℝ) : 0 < sourceConstant C

noncomputable def EulerNormalPacketParameters.envelope (J : ℕ) (C X : ℝ) (n : ℕ) : ℝ

Envelope, given by parameterEnvelope J (sourceConstant C) 320 20 1000 X n.

Equations

• EulerNormalPacketParameters.envelope J C X n = EulerPacketUniformFrequencyScales.parameterEnvelope J (EulerNormalPacketParameters.sourceConstant C) 320 20 1000 X n

noncomputable def EulerNormalPacketParameters.frequencySpec (C : ℝ) : EulerPacketSourceScaleChoice.CostSpec

Frequency spec, constructed using frequencyCostSpec.

Equations

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

theorem EulerNormalPacketParameters.previousShear_one (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 1 ≤ X) (n : ℕ) : 1 ≤ EulerPacketSourceScaleSequence.previousShear J X n

theorem EulerNormalPacketParameters.frequency_guard (J : ℕ) (C X P : ℝ) (n : ℕ) (hP : 1 ≤ P) (hPE : P ≤ envelope J C X n) (hcost : (frequencySpec C).cost J (EulerPacketSourceScaleChoice.scaleSequence J X) n ≤ 1) : EulerPacketUniformSource.frequencyConstant * P ^ EulerPacketUniformSource.frequencyPower ≤ EulerPacketSourceFrequency.smallPower (EulerPacketSourceScaleSequence.frequency J X n)

theorem EulerParentPacketFrames.LabelData.normalParameterSize_bound {A : Parent} (L : LabelData A) (H : LowBounds A) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hsupport : IsCompact support) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < A.T) (P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm R support hsupport) τ) (G : EulerPacketSourceGeometry.Guards hτ hτT P (A.historyOn H m hm R support hsupport τ hτ hτT)) (J D : ℕ) (hJ : 2 ≤ J) (C X : ℝ) (hC : 1 ≤ C) (hX : 1 ≤ X) (n : ℕ) (Ti TiTotal : ℝ) (hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (hbaseK : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4)) (hK : L.K ≤ EulerPacketSourceScaleSequence.previousFrequency J D X n ^ 80) (hTi : Ti ≤ 12 / EulerPacketBaseGuardScales.baseHorizon J X) (hTiTotal : TiTotal ≤ 12 / EulerPacketBaseGuardScales.baseHorizon J X) (hBc : H.Bc ≤ EulerPacketLowConstants.gradientConstant * X ^ 1000 + 2) (hL : H.L = EulerMeanHarmonic.boundaryLocalizationC1 * H.Bc + 1) (hM : G.CM = EulerPacketLowConstants.gradientConstant) (hH : G.CH = EulerPacketLowConstants.hessianConstant) (hΘ : P.horizon ≤ EulerPacketSourceScales.sourceTheta J C (EulerPacketSourceScaleChoice.scaleSequence J X) n) (hδ : G.δ = EulerPacketSourceScaleSequence.spike J X n) (hh : G.hchild = EulerPacketSourceScaleSequence.shear J X n) (hshear : P.shear = EulerPacketSourceScaleSequence.previousShear J X n) : L.geometryParameterSize H m hm R support hsupport τ hτ hτT P G Ti TiTotal (EulerPacketSourceGeometry.Guards.terminal hτ hτT P (A.historyOn H m hm R support hsupport τ hτ hτT) G) ≤ EulerNormalPacketParameters.envelope J C X n