Zeta32 — Assembly.

theorem Zeta32.abs_P_aeval_eq_dtilde_Qtilde (r : ℚ) (n : ℕ) (x : ℝ) : |(Polynomial.aeval x) (P r n)| = ↑(dtilde r n) * |(Polynomial.aeval x) (Qtilde r n)|

theorem Zeta32.P_eq_zero_of_Q_eq_zero (r : ℚ) (n : ℕ) (hQ : Q r n = 0) : P r n = 0

If Q r n = 0 then the primitive polynomial is 0.

def Zeta32.ArithNode (r : ℚ) : Prop

The two growth nodes of the proof notes, §9, as hypotheses: arithmetic (A = 283/50, only needed when Q r n ≠ 0) and analytic (F = −6).

Equations

• Zeta32.ArithNode r = ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, Zeta32.Q r n ≠ 0 → Real.log ↑(Zeta32.dtilde r n) ≤ (283 / 50 + ε) * ↑n ^ 2

def Zeta32.AnalyticNode (r : ℚ) : Prop

Eventual exponential bound for the scaled polynomial evaluated at the target zeta value.

Equations

• Zeta32.AnalyticNode r = ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, |(Polynomial.aeval (Zeta32.Cr r)) (Zeta32.Qtilde r n)| ≤ Real.exp ((-6 + ε) * ↑n ^ 2)

def Zeta32.PrimeEdgeNode (r : ℚ) : Prop

Nonzero constant reduction of the primitive polynomial at admissible prime edges.

Equations

• One or more equations did not get rendered due to their size.

theorem Zeta32.denominator_decay (r : ℚ) (hArith : ArithNode r) (hAnalytic : AnalyticNode r) (b : ℕ) (hb : 0 < b) : Filter.Tendsto (fun (n : ℕ) => ↑b ^ (3 * n) * |(Polynomial.aeval (Cr r)) (P r n)|) Filter.atTop (nhds 0)

theorem Zeta32.rational_nonzero_infinitely_often (r : ℚ) (hEdge : PrimeEdgeNode r) (q : ℚ) : ∃ᶠ (n : ℕ) in Filter.atTop, (Polynomial.aeval ↑q) (P r n) ≠ 0

theorem Zeta32.main_of_nodes (r : ℚ) (hArith : ArithNode r) (hAnalytic : AnalyticNode r) (hEdge : PrimeEdgeNode r) : Irrational (Cr r)

the proof notes, §9: the three nodes imply irrationality.