The actual first-normal-stage geometry supplies the same polynomial source guard for its direct-forward packet.

The first normal stage's actual direct-forward factory has a canonical radius controlled by the same fixed parent polynomial. Its genuine geometric propagator constant is retained, without replacing the growth profile.

noncomputable def EulerParentPacketFrames.LabelData.geometryCanonicalRadius {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {A : Parent} (L : LabelData A) (H : LowBounds A) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm R S hS) 0) (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (Ti : ℝ) (hT1 : A.T ≤ 1) (hTi : A.T⁻¹ ≤ Ti) (δ : ℝ) (ξ : U) : ℝ

Geometry canonical radius, given by EulerPacketForwardRadius.canonicalRadius (J).linear (J).mean (J).normal BC δ ξ.

Equations

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

theorem EulerParentPacketFrames.LabelData.geometryForward_radius_primitives {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {A : Parent} (L : LabelData A) (H : LowBounds A) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm R S hS) 0) (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (Ti : ℝ) (hT1 : A.T ≤ 1) (hTi : A.T⁻¹ ≤ Ti) (δ : ℝ) (ξ : U) (X : ℝ) (hKX : L.K ≤ X) (hTiX : Ti ≤ X) (hCpX : 560 * P.horizon ^ 10 / P.epsilon ≤ X) (hLX : H.L ≤ X) (hδX : δ⁻¹ ≤ X) (hξX : ‖ξ‖ ≤ X) : EulerPacketForwardRadius.RadiusPrimitives (L.geometryForwardInputs H m hm R S hS P G hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi).linear (L.geometryForwardInputs H m hm R S hS P G hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi).mean (L.geometryForwardInputs H m hm R S hS P G hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi).normal (EulerPacketCylinderField.forwardCoefficientBudget EulerPacketTerminalDatum.period (A.meanData H) (A.transverseData m hm R S hS) ⋯ (L.geometryForwardInputs H m hm R S hS P G hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi).normal) δ ξ (EulerParentInitializedRadius.sourceEnvelope X)

theorem EulerParentPacketFrames.LabelData.geometryCanonicalRadius_power {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {A : Parent} (L : LabelData A) (H : LowBounds A) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm R S hS) 0) (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (Ti : ℝ) (hT1 : A.T ≤ 1) (hTi : A.T⁻¹ ≤ Ti) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (X : ℝ) (hKX : L.K ≤ X) (hTiX : Ti ≤ X) (hCpX : 560 * P.horizon ^ 10 / P.epsilon ≤ X) (hLX : H.L ≤ X) (hδX : δ⁻¹ ≤ X) (hξX : ‖ξ‖ ≤ X) : L.geometryCanonicalRadius H m hm R S hS P G hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi δ ξ ≤ EulerParentInitializedRadius.fullConstant * X ^ EulerParentInitializedRadius.fullPower

theorem EulerParentPacketFrames.LabelData.geometryForward_radius_primitive_polynomial {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {A : Parent} (L : LabelData A) (H : LowBounds A) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm R S hS) 0) (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (Ti : ℝ) (hT1 : A.T ≤ 1) (hTi : A.T⁻¹ ≤ Ti) (δ : ℝ) (hδ : 0 < δ) (ξ : U) : have X := EulerParentInitializedRadius.parameterSize L.K 0 Ti (560 * P.horizon ^ 10 / P.epsilon) H.L δ ‖ξ‖; EulerPacketForwardRadius.RadiusPrimitives (L.geometryForwardInputs H m hm R S hS P G hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi).linear (L.geometryForwardInputs H m hm R S hS P G hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi).mean (L.geometryForwardInputs H m hm R S hS P G hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi).normal (EulerPacketCylinderField.forwardCoefficientBudget EulerPacketTerminalDatum.period (A.meanData H) (A.transverseData m hm R S hS) ⋯ (L.geometryForwardInputs H m hm R S hS P G hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi).normal) δ ξ (EulerParentInitializedRadius.sourceEnvelope X) ∧ EulerParentInitializedRadius.sourceEnvelope X ≤ EulerParentInitializedRadius.sourceConstant * X ^ EulerParentInitializedRadius.sourcePower

theorem EulerParentPacketFrames.LabelData.geometryCanonicalRadius_polynomial {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {A : Parent} (L : LabelData A) (H : LowBounds A) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm R S hS) 0) (G : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ G.radius) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (Ti : ℝ) (hT1 : A.T ≤ 1) (hTi : A.T⁻¹ ≤ Ti) (δ : ℝ) (hδ : 0 < δ) (ξ : U) : L.geometryCanonicalRadius H m hm R S hS P G hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi δ ξ ≤ EulerParentInitializedRadius.fullConstant * EulerParentInitializedRadius.parameterSize L.K 0 Ti (560 * P.horizon ^ 10 / P.epsilon) H.L δ ‖ξ‖ ^ EulerParentInitializedRadius.fullPower

noncomputable def EulerParentPacketFrames.LabelData.geometryForwardParameterSize {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {G : Parent} (L : LabelData G) (H : LowBounds G) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) 0) (J : EulerPacketSourceGeometry.ForwardGuards P) (Ti : ℝ) (ξ : U) : ℝ

Geometry forward parameter size, given by parameterSize L.K 0 Ti (560*P.horizon^10/P.epsilon) H.L J.δ ‖ξ‖+J.hchild.

Equations

• L.geometryForwardParameterSize H m hm R S hS P J Ti ξ = EulerParentInitializedRadius.parameterSize L.K 0 Ti (560 * P.horizon ^ 10 / P.epsilon) H.L J.δ ‖ξ‖ + J.hchild

theorem EulerParentPacketFrames.LabelData.geometryForward_uniform_primitives {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {G : Parent} (L : LabelData G) (H : LowBounds G) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) 0) (J : EulerPacketSourceGeometry.ForwardGuards P) (hball : 1 / 2 ≤ J.radius) (Ti : ℝ) (hT1 : G.T ≤ 1) (hTi : G.T⁻¹ ≤ Ti) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (ξ : U) (hδ : 0 < J.δ) (hδ1 : J.δ ≤ 1) : have X := L.geometryForwardParameterSize H m hm R S hS P J Ti ξ; EulerPacketForwardRadius.RadiusPrimitives (L.geometryForwardInputs H m hm R S hS P J hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi).linear (L.geometryForwardInputs H m hm R S hS P J hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi).mean (L.geometryForwardInputs H m hm R S hS P J hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi).normal (EulerPacketCylinderField.forwardCoefficientBudget EulerPacketTerminalDatum.period (G.meanData H) (G.transverseData m hm R S hS) ⋯ (L.geometryForwardInputs H m hm R S hS P J hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi).normal) J.δ ξ (EulerPacketUniformSource.profileEnvelope X) ∧ (∀ (t : ↑(Set.Icc 0 (G.transverseData m hm R S hS).T)), J.primaryAmplitude hball * (L.geometryForwardInputs H m hm R S hS P J hball Ω hΩ hΩo hsub hΩball Ti hT1 hTi).linear.g t ≤ EulerPacketUniformSource.profileEnvelope X) ∧ EulerPacketInitializedOutputCost.uniformConstant * EulerPacketUniformSource.profileEnvelope X ^ EulerPacketInitializedOutputCost.uniformPower ≤ EulerPacketUniformSource.frequencyConstant * X ^ EulerPacketUniformSource.frequencyPower