The ℓ and ρ parts of FstarPoints: ℓ(a) ≤ −159/100 uniformly on [a₋, a₊] (FstarPointsRho/Ell.lean) and Rlow k ≤ ρ_{a₋}(x_{k+1}) for all 15 points (FstarPointsRho/Points.lean, one declaration per point). Generic lemmas: FstarPointsRho/Basic.lean.

theorem Zeta32.Fstar.pointsRho : (∀ a ∈ Set.Icc aMinus aPlus, ellA a ≤ -159 / 100) ∧ ∀ (k : Fin 15), ↑(Rlow k) ≤ rhoA aMinus (xk (↑k + 1))