Registry · Proposition IV.P06 established formalized

IV.P06 — √3 Approximation Quality

17320508² × 100000 > 299999 × 10000000²: the √3 rational approximation is accurate to 7+ significant digits. Proved by native_decide.

Book IV Part 3 Ch. 23

Dependency Graph

Depends on (1)

IV.D43

Lean Formalization

Module: TauLib.BookIV.Physics.LemniscateCapacity

Symbol: Tau.BookIV.Physics.sqrt3_approx_quality