The fifteen lower bounds Rlow k ≤ ρ_{a₋}(x_{k+1}), one declaration per point. The upstream comments attribute the data (sl ≤ s ≤ sh, P, m) to tools/b2_numerics.py, which is not distributed upstream. The exact inputs and a replacement rational reproduction procedure are documented in CertificateReproduction.lean. Each side goal is a small norm_num on rationals. U₁ ≤ 211761/100000, U₅ ≥ 266853/50000.

theorem Zeta32.Fstar.B2.rho_pt1 : 223 / 500 ≤ rhoA aMinus (xk 1)

ρ_{a₋}(x_1) ≥ 223/500.

theorem Zeta32.Fstar.B2.rho_pt2 : 203 / 500 ≤ rhoA aMinus (xk 2)

ρ_{a₋}(x_2) ≥ 203/500.

theorem Zeta32.Fstar.B2.rho_pt3 : 377 / 1000 ≤ rhoA aMinus (xk 3)

ρ_{a₋}(x_3) ≥ 377/1000.

theorem Zeta32.Fstar.B2.rho_pt4 : 44 / 125 ≤ rhoA aMinus (xk 4)

ρ_{a₋}(x_4) ≥ 44/125.

theorem Zeta32.Fstar.B2.rho_pt5 : 329 / 1000 ≤ rhoA aMinus (xk 5)

ρ_{a₋}(x_5) ≥ 329/1000.

theorem Zeta32.Fstar.B2.rho_pt6 : 153 / 500 ≤ rhoA aMinus (xk 6)

ρ_{a₋}(x_6) ≥ 153/500.

theorem Zeta32.Fstar.B2.rho_pt7 : 283 / 1000 ≤ rhoA aMinus (xk 7)

ρ_{a₋}(x_7) ≥ 283/1000.

theorem Zeta32.Fstar.B2.rho_pt8 : 13 / 50 ≤ rhoA aMinus (xk 8)

ρ_{a₋}(x_8) ≥ 13/50.

theorem Zeta32.Fstar.B2.rho_pt9 : 119 / 500 ≤ rhoA aMinus (xk 9)

ρ_{a₋}(x_9) ≥ 119/500.

theorem Zeta32.Fstar.B2.rho_pt10 : 43 / 200 ≤ rhoA aMinus (xk 10)

ρ_{a₋}(x_10) ≥ 43/200.

theorem Zeta32.Fstar.B2.rho_pt11 : 191 / 1000 ≤ rhoA aMinus (xk 11)

ρ_{a₋}(x_11) ≥ 191/1000.

theorem Zeta32.Fstar.B2.rho_pt12 : 167 / 1000 ≤ rhoA aMinus (xk 12)

ρ_{a₋}(x_12) ≥ 167/1000.

theorem Zeta32.Fstar.B2.rho_pt13 : 71 / 500 ≤ rhoA aMinus (xk 13)

ρ_{a₋}(x_13) ≥ 71/500.

theorem Zeta32.Fstar.B2.rho_pt14 : 113 / 1000 ≤ rhoA aMinus (xk 14)

ρ_{a₋}(x_14) ≥ 113/1000.

theorem Zeta32.Fstar.B2.rho_pt15 : 39 / 500 ≤ rhoA aMinus (xk 15)

ρ_{a₋}(x_15) ≥ 39/500.

theorem Zeta32.Fstar.B2.rho_all (k : Fin 15) : ↑(Rlow k) ≤ rhoA aMinus (xk (↑k + 1))