Final assembly (§9 of the proof notes). The main theorem follows from three nodes: the arithmetic bound on the primitive content (arith_node), the analytic bound on the Hankel determinant at ζ(3) − r ζ(2) (analytic_node), and the nonvanishing modulo primes (prime_edge_node); linear independence then follows from the irrationality of ζ(3) − r ζ(2) for every rational r and of ζ(2).

theorem Zeta32.fstarPoints : FstarPoints

FstarPoints, from Fstar.pointsW and Fstar.pointsRho.

theorem Zeta32.arith_node (r : ℚ) : ArithNode r

theorem Zeta32.analytic_node (r : ℚ) : AnalyticNode r

theorem Zeta32.prime_edge_node (r : ℚ) : PrimeEdgeNode r

theorem Zeta32.zeta3_sub_rat_mul_zeta2_irrational (r : ℚ) : Irrational (∑' (k : ℕ), 1 / (↑k + 1) ^ 3 - ↑r * ∑' (k : ℕ), 1 / (↑k + 1) ^ 2)

theorem Zeta32.one_zeta_two_zeta_three_linearIndependent : LinearIndependent ℚ ![1, riemannZeta 2, riemannZeta 3]

The main theorem in its strong form.