Documentation

LeanPool.Zeta32.FstarPointsW.Points

The 15 point checks Wlow_(k-1) ≤ Wt (x_k), x_k = aMinus·k/16. Each is Wt_ge applied to the rational atom bounds of Bounds.lean, followed by one norm_num over exact rationals. Parameters (arctan mode, scaling 2^k and Taylor lengths for the two logs) were attributed upstream to tools/choose_params.py and tools/gen_points.py. Those scripts are not distributed upstream; see CertificateReproduction.lean for the exact inputs and a self-contained rational reproduction procedure.

source
theorem Zeta32.Fstar.PW.Wt_x1 :
↑(17 / 250) ≤ Wt (xk 1)

x_1 = 0.11666375; exact slack of the rational bound ≈ 0.0015.

source
theorem Zeta32.Fstar.PW.Wt_x2 :
↑(153 / 1000) ≤ Wt (xk 2)

x_2 = 0.23332750; exact slack of the rational bound ≈ 0.0003.

source
theorem Zeta32.Fstar.PW.Wt_x3 :
↑(127 / 500) ≤ Wt (xk 3)

x_3 = 0.34999125; exact slack of the rational bound ≈ 0.0042.

source
theorem Zeta32.Fstar.PW.Wt_x4 :
↑(369 / 1000) ≤ Wt (xk 4)

x_4 = 0.46665500; exact slack of the rational bound ≈ 0.0015.

source
theorem Zeta32.Fstar.PW.Wt_x5 :
↑(499 / 1000) ≤ Wt (xk 5)

x_5 = 0.58331875; exact slack of the rational bound ≈ 0.0058.

source
theorem Zeta32.Fstar.PW.Wt_x6 :
↑(641 / 1000) ≤ Wt (xk 6)

x_6 = 0.69998250; exact slack of the rational bound ≈ 0.0055.

source
theorem Zeta32.Fstar.PW.Wt_x7 :
↑(397 / 500) ≤ Wt (xk 7)

x_7 = 0.81664625; exact slack of the rational bound ≈ 0.0113.

source
theorem Zeta32.Fstar.PW.Wt_x8 :
↑(239 / 250) ≤ Wt (xk 8)

x_8 = 0.93331000; exact slack of the rational bound ≈ 0.0156.

source
theorem Zeta32.Fstar.PW.Wt_x9 :
↑(141 / 125) ≤ Wt (xk 9)

x_9 = 1.04997375; exact slack of the rational bound ≈ 0.0199.

source
theorem Zeta32.Fstar.PW.Wt_x10 :
↑(1307 / 1000) ≤ Wt (xk 10)

x_10 = 1.16663750; exact slack of the rational bound ≈ 0.0222.

source
theorem Zeta32.Fstar.PW.Wt_x11 :
↑(1493 / 1000) ≤ Wt (xk 11)

x_11 = 1.28330125; exact slack of the rational bound ≈ 0.0014.

source
theorem Zeta32.Fstar.PW.Wt_x12 :
↑(421 / 250) ≤ Wt (xk 12)

x_12 = 1.39996500; exact slack of the rational bound ≈ 0.0115.

source
theorem Zeta32.Fstar.PW.Wt_x13 :
↑(1881 / 1000) ≤ Wt (xk 13)

x_13 = 1.51662875; exact slack of the rational bound ≈ 0.0020.

source
theorem Zeta32.Fstar.PW.Wt_x14 :
↑(2083 / 1000) ≤ Wt (xk 14)

x_14 = 1.63329250; exact slack of the rational bound ≈ 0.0291.

source
theorem Zeta32.Fstar.PW.Wt_x15 :
↑(286 / 125) ≤ Wt (xk 15)

x_15 = 1.74995625; exact slack of the rational bound ≈ 0.0387.