Registry · Definition III.D45 tau-effective formalized

III.D45 — Gap Constant Γ*

Γ* = inf{Δ(f,n) : f non-trivial, n ≥ n₀}. The gap constant is computable at each finite primorial level and stabilizes as depth increases.

Book III Part 5 Ch. 39

Dependency Graph

Depends on (1)

Depended on by (1)

Lean Formalization

Module: TauLib.BookIII.Physics.GapTheorem

Symbol: gap_constant_check