FstarPoints → FstarInput: the proof notes, 5.4, Lemma 12 and the "Numerical conclusion", for layout (4,5,3) and Fconst = −6.

1. massA is nondecreasing on [0, ∞), so massA a = 1 forces aMinus < a < aPlus.
2. W ≥ 0 nondecreasing (Fstar/Wt.lean); ρ_a ≥ 0, nonincreasing in x, nondecreasing in a, and W·ρ_a interval integrable on [0, a] (Fstar/Rho.lean).
3. Lower Riemann sum on [x₁, x₁₅], x_k = aMinus·k/16, with the pieces [0, x₁] and [x₁₅, a] dropped (≥ 0): ∫₀^a Wρ_a ≥ (aMinus/16)·Σ_{j<14} Wlow_j·Rlow_{j+1}.
4. ellA a ≤ −159/100, log 3 > 549/500; the final rational inequality by linarith (F ≤ −6.2474 < −6). No code copied from other repositories.

theorem Zeta32.Fstar.massA_mono {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) : massA a ≤ massA b

theorem Zeta32.Fstar.lt_aMinus_of_mass {a : ℝ} (ha : 0 < a) (hm : massA a = 1) (hlo : massA aMinus < 1) : aMinus < a

theorem Zeta32.Fstar.lt_aPlus_of_mass {a : ℝ} (hm : massA a = 1) (hhi : 1 < massA aPlus) : a < aPlus

theorem Zeta32.Fstar.xk_pos {n : ℕ} (hn : 0 < n) : 0 < xk n

theorem Zeta32.Fstar.xk_le_aMinus {n : ℕ} (hn : n ≤ 16) : xk n ≤ aMinus

theorem Zeta32.Fstar.xk_succ_sub (n : ℕ) : xk (n + 1) - xk n = aMinus / 16

theorem Zeta32.Fstar.Rlow_nonneg (k : Fin 15) : 0 ≤ ↑(Rlow k)

theorem Zeta32.Fstar.lowerSum_eq : ∑ j : Fin 14, Wlow j.castSucc * Rlow j.succ = 1209903 / 500000

theorem Zeta32.Fstar.integral_lower {a : ℝ} (ha : aMinus < a) (hW : ∀ (k : Fin 15), ↑(Wlow k) ≤ Wt (xk (↑k + 1))) (hR : ∀ (k : Fin 15), ↑(Rlow k) ≤ rhoA aMinus (xk (↑k + 1))) : aMinus / 16 * ↑(∑ j : Fin 14, Wlow j.castSucc * Rlow j.succ) ≤ ∫ (x : ℝ) in 0..a, Wt x * rhoA a x

Lemma 12 lower Riemann sum.

theorem Zeta32.Fstar.fstarInput_of_points : FstarPoints → FstarInput