Root of the point checks for F* ≤ -6: the mass bracket, the log 3 lower bound and the 15 lower bounds for Wt at x_k = aMinus·k/16 (index k : Fin 15 stands for x_(k+1)). No sorry, no new axioms, no native_decide.

theorem Zeta32.Fstar.pointsW : massA aMinus < 1 ∧ 1 < massA aPlus ∧ 549 / 500 < Real.log 3 ∧ ∀ (k : Fin 15), ↑(Wlow k) ≤ Wt (xk (↑k + 1))