feat: preserve the completed zeta(5) irrationality formalization

LeanPool.lean

@@ -8092,6 +8092,216 @@ public import LeanPool.Zeta3Irrational.Equality
 public import LeanPool.Zeta3Irrational.Integral
 public import LeanPool.Zeta3Irrational.LegendrePoly
 public import LeanPool.Zeta3Irrational.LinearForm
+public import LeanPool.Zeta5Irrational
+public import LeanPool.Zeta5Irrational.Andreief
+public import LeanPool.Zeta5Irrational.ArcsineAtoms
+public import LeanPool.Zeta5Irrational.ArcsinePotential
+public import LeanPool.Zeta5Irrational.Arith.BasisChange
+public import LeanPool.Zeta5Irrational.Arith.BinomBasis
+public import LeanPool.Zeta5Irrational.Arith.ClassCount
+public import LeanPool.Zeta5Irrational.Arith.ClassFrame
+public import LeanPool.Zeta5Irrational.Arith.DirectBound
+public import LeanPool.Zeta5Irrational.Arith.DirectPoly
+public import LeanPool.Zeta5Irrational.Arith.InnerAlloc
+public import LeanPool.Zeta5Irrational.Arith.InnerWeights
+public import LeanPool.Zeta5Irrational.Arith.IntPoly
+public import LeanPool.Zeta5Irrational.Arith.LowRank
+public import LeanPool.Zeta5Irrational.Arith.MomentVal
+public import LeanPool.Zeta5Irrational.Arith.OuterBasis
+public import LeanPool.Zeta5Irrational.Arith.OuterEntries
+public import LeanPool.Zeta5Irrational.Arith.OuterEntry
+public import LeanPool.Zeta5Irrational.Arith.OuterEntryMain
+public import LeanPool.Zeta5Irrational.Arith.OuterFrame
+public import LeanPool.Zeta5Irrational.Arith.PoleFun
+public import LeanPool.Zeta5Irrational.Arith.PoleVal
+public import LeanPool.Zeta5Irrational.Arith.Pullback
+public import LeanPool.Zeta5Irrational.Arith.SmallPrime
+public import LeanPool.Zeta5Irrational.Arith.SmallPrimeF
+public import LeanPool.Zeta5Irrational.Arith.SmallPrimeRes
+public import LeanPool.Zeta5Irrational.Arith.SmallPrimeTau
+public import LeanPool.Zeta5Irrational.Arith.TEntry
+public import LeanPool.Zeta5Irrational.Arith.TauBound
+public import LeanPool.Zeta5Irrational.Arith.Unimodular
+public import LeanPool.Zeta5Irrational.Arith.Val
+public import LeanPool.Zeta5Irrational.Certificates
+public import LeanPool.Zeta5Irrational.CircleAtoms
+public import LeanPool.Zeta5Irrational.Constants
+public import LeanPool.Zeta5Irrational.Construction
+public import LeanPool.Zeta5Irrational.Criterion
+public import LeanPool.Zeta5Irrational.Degree
+public import LeanPool.Zeta5Irrational.DetIntegral
+public import LeanPool.Zeta5Irrational.Energy
+public import LeanPool.Zeta5Irrational.EnergyAtoms
+public import LeanPool.Zeta5Irrational.EnergyBlocks
+public import LeanPool.Zeta5Irrational.EnergyBound
+public import LeanPool.Zeta5Irrational.EnergyConst
+public import LeanPool.Zeta5Irrational.EnergyFinal
+public import LeanPool.Zeta5Irrational.EnergyLimit
+public import LeanPool.Zeta5Irrational.EnergyRaw
+public import LeanPool.Zeta5Irrational.Gaussian
+public import LeanPool.Zeta5Irrational.Growth
+public import LeanPool.Zeta5Irrational.Growth.Assembly1
+public import LeanPool.Zeta5Irrational.Growth.Assembly2
+public import LeanPool.Zeta5Irrational.Growth.Assembly3
+public import LeanPool.Zeta5Irrational.Growth.Assembly4
+public import LeanPool.Zeta5Irrational.Growth.ClassData
+public import LeanPool.Zeta5Irrational.Growth.ClassSum
+public import LeanPool.Zeta5Irrational.Growth.Constants
+public import LeanPool.Zeta5Irrational.Growth.InnerPrime
+public import LeanPool.Zeta5Irrational.Growth.InnerSum
+public import LeanPool.Zeta5Irrational.Growth.InnerTable
+public import LeanPool.Zeta5Irrational.Growth.OuterPrime
+public import LeanPool.Zeta5Irrational.Growth.OuterTable
+public import LeanPool.Zeta5Irrational.Growth.PieceIdx
+public import LeanPool.Zeta5Irrational.Growth.TableGen
+public import LeanPool.Zeta5Irrational.Growth.TableIntegrals
+public import LeanPool.Zeta5Irrational.Growth.TablePrime
+public import LeanPool.Zeta5Irrational.Growth.TailIntegral
+public import LeanPool.Zeta5Irrational.Growth.TailPrime
+public import LeanPool.Zeta5Irrational.Hermite
+public import LeanPool.Zeta5Irrational.HermiteFormula
+public import LeanPool.Zeta5Irrational.HermiteIBP
+public import LeanPool.Zeta5Irrational.HermiteIntegrals
+public import LeanPool.Zeta5Irrational.Kernel
+public import LeanPool.Zeta5Irrational.Legendre
+public import LeanPool.Zeta5Irrational.Main
+public import LeanPool.Zeta5Irrational.MainEstimate
+public import LeanPool.Zeta5Irrational.Measure
+public import LeanPool.Zeta5Irrational.Moments
+public import LeanPool.Zeta5Irrational.Norm
+public import LeanPool.Zeta5Irrational.PNT
+public import LeanPool.Zeta5Irrational.PartialFractions
+public import LeanPool.Zeta5Irrational.Positivity
+public import LeanPool.Zeta5Irrational.Potential
+public import LeanPool.Zeta5Irrational.PotentialV
+public import LeanPool.Zeta5Irrational.PrimeSum
+public import LeanPool.Zeta5Irrational.PrimeSumIntegral
+public import LeanPool.Zeta5Irrational.PrimeSumStep
+public import LeanPool.Zeta5Irrational.RealBound
+public import LeanPool.Zeta5Irrational.Stirling
+public import LeanPool.Zeta5Irrational.Table.Bracket
+public import LeanPool.Zeta5Irrational.Table.Common
+public import LeanPool.Zeta5Irrational.Table.Intervals
+public import LeanPool.Zeta5Irrational.Table.Tail
+public import LeanPool.Zeta5Irrational.Table.U00
+public import LeanPool.Zeta5Irrational.Table.U01
+public import LeanPool.Zeta5Irrational.Table.U02
+public import LeanPool.Zeta5Irrational.Table.U03
+public import LeanPool.Zeta5Irrational.Table.U04
+public import LeanPool.Zeta5Irrational.Table.U05
+public import LeanPool.Zeta5Irrational.Table.U06
+public import LeanPool.Zeta5Irrational.Table.U07
+public import LeanPool.Zeta5Irrational.Table.U08
+public import LeanPool.Zeta5Irrational.Table.U09
+public import LeanPool.Zeta5Irrational.Table.U10
+public import LeanPool.Zeta5Irrational.Table.U11
+public import LeanPool.Zeta5Irrational.Table.U12
+public import LeanPool.Zeta5Irrational.Table.U13
+public import LeanPool.Zeta5Irrational.Table.U14
+public import LeanPool.Zeta5Irrational.Table.U15
+public import LeanPool.Zeta5Irrational.Table.U16
+public import LeanPool.Zeta5Irrational.Table.U17
+public import LeanPool.Zeta5Irrational.Table.U18
+public import LeanPool.Zeta5Irrational.Table.U19
+public import LeanPool.Zeta5Irrational.Table.U20
+public import LeanPool.Zeta5Irrational.Table.U21
+public import LeanPool.Zeta5Irrational.Table.U22
+public import LeanPool.Zeta5Irrational.Table.U23
+public import LeanPool.Zeta5Irrational.Table.U24
+public import LeanPool.Zeta5Irrational.Table.U25
+public import LeanPool.Zeta5Irrational.Table.U26
+public import LeanPool.Zeta5Irrational.Table.U27
+public import LeanPool.Zeta5Irrational.Table.U28
+public import LeanPool.Zeta5Irrational.Table.U29
+public import LeanPool.Zeta5Irrational.Table.U30
+public import LeanPool.Zeta5Irrational.Table.U31
+public import LeanPool.Zeta5Irrational.Table.U32
+public import LeanPool.Zeta5Irrational.Table.U33
+public import LeanPool.Zeta5Irrational.Table.U34
+public import LeanPool.Zeta5Irrational.Table.U35
+public import LeanPool.Zeta5Irrational.Table.U36
+public import LeanPool.Zeta5Irrational.Table.U37
+public import LeanPool.Zeta5Irrational.Table.U38
+public import LeanPool.Zeta5Irrational.Table.U39
+public import LeanPool.Zeta5Irrational.Table.U40
+public import LeanPool.Zeta5Irrational.Table.U41
+public import LeanPool.Zeta5Irrational.Table.U42
+public import LeanPool.Zeta5Irrational.Table.U43
+public import LeanPool.Zeta5Irrational.Table.U44
+public import LeanPool.Zeta5Irrational.Table.U45
+public import LeanPool.Zeta5Irrational.Table.U46
+public import LeanPool.Zeta5Irrational.Table.U47
+public import LeanPool.Zeta5Irrational.Table.U48
+public import LeanPool.Zeta5Irrational.Table.U49
+public import LeanPool.Zeta5Irrational.Table.U50
+public import LeanPool.Zeta5Irrational.Table.U51
+public import LeanPool.Zeta5Irrational.Table.U52
+public import LeanPool.Zeta5Irrational.Table.U53
+public import LeanPool.Zeta5Irrational.Table.U54
+public import LeanPool.Zeta5Irrational.Table.U55
+public import LeanPool.Zeta5Irrational.Table.U56
+public import LeanPool.Zeta5Irrational.Table.UpperCertificate
+public import LeanPool.Zeta5Irrational.Table.V00
+public import LeanPool.Zeta5Irrational.Table.V01
+public import LeanPool.Zeta5Irrational.Table.V02
+public import LeanPool.Zeta5Irrational.Table.V03
+public import LeanPool.Zeta5Irrational.Table.V04
+public import LeanPool.Zeta5Irrational.Table.V05
+public import LeanPool.Zeta5Irrational.Table.V06
+public import LeanPool.Zeta5Irrational.Table.V07
+public import LeanPool.Zeta5Irrational.Table.V08
+public import LeanPool.Zeta5Irrational.Table.V09
+public import LeanPool.Zeta5Irrational.Table.V10
+public import LeanPool.Zeta5Irrational.Table.V11
+public import LeanPool.Zeta5Irrational.Table.V12
+public import LeanPool.Zeta5Irrational.Table.V13
+public import LeanPool.Zeta5Irrational.Table.V14
+public import LeanPool.Zeta5Irrational.Table.V15
+public import LeanPool.Zeta5Irrational.Table.V16
+public import LeanPool.Zeta5Irrational.Table.V17
+public import LeanPool.Zeta5Irrational.Table.V18
+public import LeanPool.Zeta5Irrational.Table.V19
+public import LeanPool.Zeta5Irrational.Table.V20
+public import LeanPool.Zeta5Irrational.Table.V21
+public import LeanPool.Zeta5Irrational.Table.V22
+public import LeanPool.Zeta5Irrational.Table.V23
+public import LeanPool.Zeta5Irrational.Table.V24
+public import LeanPool.Zeta5Irrational.Table.V25
+public import LeanPool.Zeta5Irrational.Table.V26
+public import LeanPool.Zeta5Irrational.Table.V27
+public import LeanPool.Zeta5Irrational.Table.V28
+public import LeanPool.Zeta5Irrational.Table.V29
+public import LeanPool.Zeta5Irrational.Table.V30
+public import LeanPool.Zeta5Irrational.Table.V31
+public import LeanPool.Zeta5Irrational.Table.V32
+public import LeanPool.Zeta5Irrational.Table.V33
+public import LeanPool.Zeta5Irrational.Table.V34
+public import LeanPool.Zeta5Irrational.Table.V35
+public import LeanPool.Zeta5Irrational.Table.V36
+public import LeanPool.Zeta5Irrational.Table.V37
+public import LeanPool.Zeta5Irrational.Table.V38
+public import LeanPool.Zeta5Irrational.Table.V39
+public import LeanPool.Zeta5Irrational.Table.V40
+public import LeanPool.Zeta5Irrational.Table.V41
+public import LeanPool.Zeta5Irrational.Table.V42
+public import LeanPool.Zeta5Irrational.Table.V43
+public import LeanPool.Zeta5Irrational.Table.V44
+public import LeanPool.Zeta5Irrational.Table.V45
+public import LeanPool.Zeta5Irrational.Table.V46
+public import LeanPool.Zeta5Irrational.Table.V47
+public import LeanPool.Zeta5Irrational.Table.V48
+public import LeanPool.Zeta5Irrational.Table.V49
+public import LeanPool.Zeta5Irrational.Table.V50
+public import LeanPool.Zeta5Irrational.Table.V51
+public import LeanPool.Zeta5Irrational.Table.V52
+public import LeanPool.Zeta5Irrational.Table.V53
+public import LeanPool.Zeta5Irrational.Table.V54
+public import LeanPool.Zeta5Irrational.Table.V55
+public import LeanPool.Zeta5Irrational.Table.V56
+public import LeanPool.Zeta5Irrational.TableCheck
+public import LeanPool.Zeta5Irrational.Weight
+public import LeanPool.Zeta5Irrational.ZeroMass
+public import LeanPool.Zeta5Irrational.Zeta5
 public import LeanPool.ZetaH123
 public import LeanPool.ZetaH123.H1
 public import LeanPool.ZetaH123.H2

LeanPool/Zeta5Irrational.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Moritz Firsching. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Firsching
+-/
+
+module
+
+public import LeanPool.Zeta5Irrational.Main
+public import LeanPool.Zeta5Irrational.MainEstimate
+public import LeanPool.Zeta5Irrational.Criterion
+public import LeanPool.Zeta5Irrational.Andreief
+public import LeanPool.Zeta5Irrational.Arith.Val
+public import LeanPool.Zeta5Irrational.Table.UpperCertificate
+
+/-!
+# Irrationality of the Riemann zeta function at five
+
+Source: url:https://github.com/mo271/Zeta5/tree/f19a1960609f7d38e7b63fd2acb05e6f60a7b741
+Authors: Moritz Firsching
+Status: verified
+Main declarations: `Zeta5Irrational.irrational_five`
+Tags: irrationality, zeta-function, hankel-determinants, potential-theory, certified-computation
+MSC: 11J72, 11M06, 31A15
+-/

LeanPool/Zeta5Irrational/Andreief.lean

@@ -0,0 +1,148 @@
+/-
+Copyright (c) 2026 Moritz Firsching. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Firsching
+-/
+
+module
+
+public import Mathlib.Analysis.InnerProductSpace.Basic
+public import Mathlib.MeasureTheory.Integral.Bochner.Basic
+import Mathlib.MeasureTheory.Integral.Pi
+import Mathlib.Tactic.ENatToNat
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Positivity.Basic
+import Mathlib.Tactic.Ring.Basic
+
+/-! # Andréief's identity
+
+For functions `f i, g j : ℝ → ℝ` with `f i * g j` integrable,
+`det (∫ f i g j dμ) = (1/n!) ∫ det (f i (x j)) det (g i (x j)) dμⁿ(x)`.
+This is (6.10) of the paper in the form used for the Hankel determinant.
+-/
+
+@[expose] public section
+
+open MeasureTheory Finset Equiv
+
+namespace Zeta5Irrational
+
+variable {n : ℕ} {μ : Measure ℝ} [SigmaFinite μ]
+
+/-- The coordinate permutation `x ↦ (i ↦ x (τ i))` as a measurable equivalence. -/
+noncomputable def permEquiv (τ : Perm (Fin n)) : (Fin n → ℝ) ≃ᵐ (Fin n → ℝ) :=
+  MeasurableEquiv.arrowCongr' τ.symm (MeasurableEquiv.refl ℝ)
+
+lemma permEquiv_apply (τ : Perm (Fin n)) (x : Fin n → ℝ) (i : Fin n) :
+    permEquiv τ x i = x (τ i) := by
+  simp [permEquiv, MeasurableEquiv.arrowCongr', Equiv.arrowCongr']
+
+lemma measurePreserving_permEquiv (τ : Perm (Fin n)) :
+    MeasurePreserving (permEquiv τ) (Measure.pi fun _ : Fin n => μ)
+      (Measure.pi fun _ : Fin n => μ) :=
+  measurePreserving_arrowCongr' (fun _ : Fin n => μ) (fun _ : Fin n => μ) τ.symm
+    (MeasurableEquiv.refl ℝ) (fun _ => ⟨(MeasurableEquiv.refl ℝ).measurable, Measure.map_id⟩)
+
+/-- The basic integral `I(ρ) = ∫ ∏ᵢ f (ρ i) (xᵢ) g i (xᵢ)`. -/
+noncomputable def andreiefI (f g : Fin n → ℝ → ℝ) (ρ : Perm (Fin n)) : ℝ :=
+  ∫ x : Fin n → ℝ, ∏ i, f (ρ i) (x i) * g i (x i) ∂(Measure.pi fun _ : Fin n => μ)
+
+lemma integral_prod_prod_eq (f g : Fin n → ℝ → ℝ) (σ τ : Perm (Fin n)) :
+    ∫ x : Fin n → ℝ,
+        (∏ i, f (σ i) (x i)) * (∏ i, g (τ i) (x i)) ∂(Measure.pi fun _ : Fin n => μ) =
+      andreiefI (μ := μ) f g (σ * τ⁻¹) := by
+  unfold andreiefI
+  have hpt :
+    ∀ x : Fin n → ℝ,
+      (∏ i, f (σ i) (x i)) * (∏ i, g (τ i) (x i)) =
+        (fun y : Fin n → ℝ => ∏ k, f ((σ * τ⁻¹) k) (y k) * g k (y k)) (permEquiv τ⁻¹ x) := by
+    intro x
+    simp only [permEquiv_apply, ← Finset.prod_mul_distrib]
+    rw [← Equiv.prod_comp τ (fun k => f ((σ * τ⁻¹) k) (x (τ⁻¹ k)) * g k (x (τ⁻¹ k)))]
+    refine Finset.prod_congr rfl fun i _ => ?_
+    simp [Perm.mul_apply]
+  simp_rw [hpt]
+  exact
+    (measurePreserving_permEquiv (μ := μ) τ⁻¹).integral_comp (permEquiv τ⁻¹).measurableEmbedding
+      (fun y : Fin n → ℝ => ∏ k, f ((σ * τ⁻¹) k) (y k) * g k (y k))
+
+/-- **Andréief's identity**. -/
+theorem andreief (f g : Fin n → ℝ → ℝ) (hfg : ∀ i j, Integrable (fun x => f i x * g j x) μ) :
+    (Matrix.of fun i j => ∫ x, f i x * g j x ∂μ).det =
+      (1 / (n.factorial : ℝ)) *
+        ∫ x : Fin n → ℝ,
+          (Matrix.of fun i j => f i (x j)).det *
+            (Matrix.of fun i j => g i (x j)).det ∂(Measure.pi fun _ : Fin n => μ) := by
+  -- the left-hand side as a sum over permutations of basic integrals
+  have hL :
+    (Matrix.of fun i j => ∫ x, f i x * g j x ∂μ).det =
+      ∑ ρ : Perm (Fin n), (Perm.sign ρ : ℝ) * andreiefI (μ := μ) f g ρ := by
+    rw [Matrix.det_apply']
+    refine Finset.sum_congr rfl fun ρ _ => ?_
+    simp only [Matrix.of_apply, andreiefI]
+    rw [integral_fintype_prod_eq_prod (fun i x => f (ρ i) x * g i x)]
+      -- the right-hand side
+  have hint :
+    ∀ σ τ : Perm (Fin n),
+      Integrable
+        (fun x : Fin n → ℝ =>
+          (Perm.sign σ : ℝ) * (Perm.sign τ : ℝ) * ((∏ i, f (σ i) (x i)) * (∏ i, g (τ i) (x i))))
+        (Measure.pi fun _ : Fin n => μ) := by
+    intro σ τ
+    have :
+      (fun x : Fin n → ℝ => (∏ i, f (σ i) (x i)) * (∏ i, g (τ i) (x i))) = fun x =>
+        ∏ i, (fun i y => f (σ i) y * g (τ i) y) i (x i) :=
+      by funext x; simp only [← Finset.prod_mul_distrib]
+    refine Integrable.const_mul ?_ _
+    rw [this]
+    exact Integrable.fintype_prod fun i => hfg (σ i) (τ i)
+  have hR :
+    ∫ x : Fin n → ℝ,
+        (Matrix.of fun i j => f i (x j)).det *
+          (Matrix.of fun i j => g i (x j)).det ∂(Measure.pi fun _ : Fin n => μ) =
+      ∑ τ : Perm (Fin n),
+        ∑ σ : Perm (Fin n),
+          (Perm.sign σ : ℝ) * (Perm.sign τ : ℝ) * andreiefI (μ := μ) f g (σ * τ⁻¹) := by
+    have hpt :
+      ∀ x : Fin n → ℝ,
+        (Matrix.of fun i j => f i (x j)).det * (Matrix.of fun i j => g i (x j)).det =
+          ∑ τ : Perm (Fin n),
+            ∑ σ : Perm (Fin n),
+              (Perm.sign σ : ℝ) * (Perm.sign τ : ℝ) *
+                ((∏ i, f (σ i) (x i)) * (∏ i, g (τ i) (x i))) := by
+      intro x
+      rw [Matrix.det_apply', Matrix.det_apply', Finset.sum_mul_sum, Finset.sum_comm]
+      refine Finset.sum_congr rfl fun τ _ => Finset.sum_congr rfl fun σ _ => ?_
+      simp only [Matrix.of_apply]
+      ring
+    simp_rw [hpt]
+    rw [integral_finsetSum _ (fun τ _ => integrable_finsetSum _ (fun σ _ => hint σ τ))]
+    refine Finset.sum_congr rfl fun τ _ => ?_
+    rw [integral_finsetSum _ (fun σ _ => hint σ τ)]
+    refine Finset.sum_congr rfl fun σ _ => ?_
+    rw [integral_const_mul, integral_prod_prod_eq]
+      -- each inner sum is the left-hand side
+  have hsign :
+    ∀ σ τ : Perm (Fin n), (Perm.sign (σ * τ⁻¹) : ℝ) = (Perm.sign σ : ℝ) * (Perm.sign τ : ℝ) := by
+    intro σ τ
+    rw [Perm.sign_mul, Perm.sign_inv]
+    push_cast
+    ring
+  have hinner :
+    ∀ τ : Perm (Fin n),
+      ∑ σ : Perm (Fin n),
+          (Perm.sign σ : ℝ) * (Perm.sign τ : ℝ) * andreiefI (μ := μ) f g (σ * τ⁻¹) =
+        ∑ ρ : Perm (Fin n), (Perm.sign ρ : ℝ) * andreiefI (μ := μ) f g ρ := by
+    intro τ
+    conv_rhs => rw [← Equiv.sum_comp (Equiv.mulRight τ⁻¹)]
+    refine Finset.sum_congr rfl fun σ _ => ?_
+    simp only [Equiv.coe_mulRight]
+    rw [hsign]
+  rw [hR]
+  simp_rw [hinner]
+  rw [Finset.sum_const, Finset.card_univ, Fintype.card_perm, Fintype.card_fin, nsmul_eq_mul, hL]
+  have : (n.factorial : ℝ) ≠ 0 := by positivity
+  field_simp
+  try ring
+
+end Zeta5Irrational