The only eventual frequency conditions left after the uniform source cost comparison form one fixed, parent-independent numerical record.

structure EulerPacketSourceFrequency.UniversalFrequency (k : ℝ) : Prop

Universal frequency data, collecting four, expansion_bound, log_bound, delta_bound, root_bound, trace_bound and their compatibility conditions.

• four : 4 ≤ k
• expansion_bound : 64 ≤ expansion k
• log_bound : 1 ≤ Real.log k
• delta_bound : EulerPacketCorrectionScalar.delta (expansion k) ≤ k ^ (-3)
• root_bound : 16 ≤ k ^ (1 / 4)
• trace_bound : max 71 √(2 / EulerPacketTerminalDatum.period + 2 * EulerPacketTerminalDatum.period) ≤ k ^ (1 / 24)
• child_bound : 69 ≤ k
• embedding_bound : 2 + 45 * EulerPacketParentLabelBounds.embeddingCost ≤ k
• derivative_bound : EulerSobolevSourceExponent.fixedCost 6 ≤ k

theorem EulerPacketSourceFrequency.universal_frequency_eventually : ∀ᶠ (k : ℝ) in Filter.atTop, UniversalFrequency k

theorem EulerPacketSourceFrequency.exists_universal_frequency_threshold : ∃ (K : ℝ), 1 ≤ K ∧ ∀ (k : ℝ), K ≤ k → UniversalFrequency k

theorem EulerPacketSourceFrequency.UniversalFrequency.one_le {k : ℝ} (h : UniversalFrequency k) : 1 ≤ k

theorem EulerPacketSourceFrequency.UniversalFrequency.pos {k : ℝ} (h : UniversalFrequency k) : 0 < k

theorem EulerPacketSourceFrequency.UniversalFrequency.truncation_one {k : ℝ} (h : UniversalFrequency k) : 1 ≤ truncation k