The actual parent and chosen geometric profile supply every primitive of the uniform correction and physical-output comparison.

The actual activation geometry fills the remaining propagator input in the parent-to-packet constructor. All three source budgets share one radius and retain the growth profile derived from that geometry.

noncomputable def EulerParentPacketFrames.LabelData.geometryInputs {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) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) (P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ) (J : EulerPacketSourceGeometry.Guards hτ hτT P (G.historyOn H m hm R S hS τ hτ hτT)) (hball : 1 / 2 ≤ J.radius) (Ti TiTotal : ℝ) (hτ1 : τ ≤ 1) (hTi : τ⁻¹ ≤ Ti) (hT1 : G.T ≤ 1) (hTiTotal : G.T⁻¹ ≤ TiTotal) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) : JoinedInputs (G.meanData H) (G.transverseData m hm R S hS) τ hτ hτT (G.historyOn H m hm R S hS τ hτ hτT)

Geometry inputs, constructed using L.joinedInputs.

Equations

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

theorem EulerParentPacketFrames.LabelData.geometryInputs_growth {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) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) (P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ) (J : EulerPacketSourceGeometry.Guards hτ hτT P (G.historyOn H m hm R S hS τ hτ hτT)) (hball : 1 / 2 ≤ J.radius) (Ti TiTotal : ℝ) (hτ1 : τ ≤ 1) (hTi : τ⁻¹ ≤ Ti) (hT1 : G.T ≤ 1) (hTiTotal : G.T⁻¹ ≤ TiTotal) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) : (L.geometryInputs H m hm R S hS τ hτ hτT P J hball Ti TiTotal hτ1 hTi hT1 hTiTotal Ω hΩ hΩo hsub hΩball).linear.g = J.sourceGrowthProfile hball

noncomputable def EulerParentPacketFrames.LabelData.geometryParameterSize {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) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) (P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ) (J : EulerPacketSourceGeometry.Guards hτ hτT P (G.historyOn H m hm R S hS τ hτ hτT)) (Ti TiTotal : ℝ) (ξ : U) : ℝ

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

Equations

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

theorem EulerParentPacketFrames.LabelData.geometry_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) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) (P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ) (J : EulerPacketSourceGeometry.Guards hτ hτT P (G.historyOn H m hm R S hS τ hτ hτT)) (hball : 1 / 2 ≤ J.radius) (Ti TiTotal : ℝ) (hτ1 : τ ≤ 1) (hTi : τ⁻¹ ≤ Ti) (hT1 : G.T ≤ 1) (hTiTotal : G.T⁻¹ ≤ TiTotal) (Ω : 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.geometryParameterSize H m hm R S hS τ hτ hτT P J Ti TiTotal ξ; EulerPacketRadiusPolynomial.RadiusPrimitives (L.geometryInputs H m hm R S hS τ hτ hτT P J hball Ti TiTotal hτ1 hTi hT1 hTiTotal Ω hΩ hΩo hsub hΩball).mean (L.geometryInputs H m hm R S hS τ hτ hτT P J hball Ti TiTotal hτ1 hTi hT1 hTiTotal Ω hΩ hΩo hsub hΩball).linear (L.geometryInputs H m hm R S hS τ hτ hτT P J hball Ti TiTotal hτ1 hTi hT1 hTiTotal Ω hΩ hΩo hsub hΩball).normal (EulerPacketCylinderField.joinedCoefficientBudget EulerPacketTerminalDatum.period (G.meanData H) (G.transverseData m hm R S hS) ⋯ τ hτ hτT (G.historyOn H m hm R S hS τ hτ hτT) (L.geometryInputs H m hm R S hS τ hτ hτT P J hball Ti TiTotal hτ1 hTi hT1 hTiTotal Ω hΩ hΩo hsub hΩball).normal) J.δ ξ (EulerPacketUniformSource.profileEnvelope X) ∧ (∀ (t : ↑(Set.Icc 0 (G.transverseData m hm R S hS).T)), J.primaryAmplitude hball * (L.geometryInputs H m hm R S hS τ hτ hτT P J hball Ti TiTotal hτ1 hTi hT1 hTiTotal Ω hΩ hΩo hsub hΩball).linear.fullProfile t ≤ EulerPacketUniformSource.profileEnvelope X) ∧ EulerPacketInitializedOutputCost.uniformConstant * EulerPacketUniformSource.profileEnvelope X ^ EulerPacketInitializedOutputCost.uniformPower ≤ EulerPacketUniformSource.frequencyConstant * X ^ EulerPacketUniformSource.frequencyPower