The same normal-stage frequency comparison also supplies the parent-label and physical support-scale inequalities for the child flow.

theorem EulerNormalPacketParameters.sourceConstant_one (C : ℝ) : 1 ≤ sourceConstant C

theorem EulerNormalPacketParameters.exponential_le_envelope (J : ℕ) (hJ : 1 ≤ J) (C X c : ℝ) (hX : 1 ≤ X) (hc : c ≤ 320) (n : ℕ) : Real.exp (c * EulerPacketSourceParameterScales.predecessorExponent J X n) ≤ envelope J C X n

theorem EulerNormalPacketParameters.envelope_one (J : ℕ) (hJ : 1 ≤ J) (C X : ℝ) (hX : 1 ≤ X) (n : ℕ) : 1 ≤ envelope J C X n

theorem EulerNormalPacketParameters.envelope_le_smallPower (J : ℕ) (hJ : 1 ≤ J) (C X : ℝ) (hX : 1 ≤ X) (n : ℕ) (hcost : (frequencySpec C).cost J (EulerPacketSourceScaleChoice.scaleSequence J X) n ≤ 1) : envelope J C X n ≤ EulerPacketSourceFrequency.smallPower (EulerPacketSourceScaleSequence.frequency J X n)

theorem EulerNormalPacketParameters.support_inverse_le_envelope (J : ℕ) (hJ : 2 ≤ J) (C X : ℝ) (hX : 1 ≤ X) (n : ℕ) : (EulerPacketSourceScaleSequence.supportScale J X n)⁻¹ ≤ envelope J C X n

theorem EulerNormalPacketParameters.secondary_frequency_guards (J D : ℕ) (hJ : 2 ≤ J) (C X K : ℝ) (hX : 1 ≤ X) (n : ℕ) (hbase : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4)) (hK : K ≤ EulerPacketSourceScaleSequence.previousFrequency J D X n ^ 80) (hcost : (frequencySpec C).cost J (EulerPacketSourceScaleChoice.scaleSequence J X) n ≤ 1) (hk : 1 ≤ EulerPacketSourceScaleSequence.frequency J X n) : K ≤ EulerPacketSourceScaleSequence.frequency J X n ∧ (EulerPacketSourceScaleSequence.supportScale J X n)⁻¹ ≤ EulerPacketSourceScaleSequence.frequency J X n ^ (3 / 4)