noncomputable def full_C₂ (β : ℝ) : ℕ

Equations

• full_C₂ β = 374 ^ ⌈Real.logb (3 / 2) (1 / β)⌉₊

noncomputable def full_C (β : ℝ) : ℕ

Equations

• full_C β = full_C₂ β * 9