File size: 1,257 Bytes
3d3ccd7 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 | -- Pattern match for the missing Red2 functor.
-- Wired fields are definitional. identify and preserve are not inhabited.
-- This file does not prove the Riemann hypothesis.
import Mathlib.Data.ZMod.Basic
import Mathlib.Data.Complex.Basic
open Complex
/-- Euler factor, the gas mode. Real s > 1 in the analytic theory. -/
def eulerFactor (p : ℕ) (s : ℂ) : ℂ :=
1 / (1 - (p : ℂ) ^ (-s))
/-- Carrier of the F2 finite part: vectors over ZMod 2. -/
def FiniteCarrier (g : ℕ) : Type := Fin (2 * g) → ZMod 2
/-- Carrier of the complex finite part used by the HOL script. -/
def ComplexFinite : Type := ℂ
/-- The only pattern that matches on F2: x ↦ x^2 is the identity. -/
theorem f2_square_id (x : ZMod 2) : x ^ 2 = x := ZMod.sq_eq_self x
/-- What Red2 would have to be. The two holes are the assessment's B1 and B2. -/
structure Red2 (g : ℕ) where
/-- Object map. Not constructed. -/
map : FiniteCarrier g → (ℂ → ℂ)
/-- GAP-4: classical zeta is in the image. -/
identify : Prop
/-- GAP-3: zeros of the image lie on the critical line. -/
preserve : Prop
/-- No instance is given. An axiom here would be the hypothesis renamed. -/
def red2_holes_open (g : ℕ) : Prop :=
∀ R : Red2 g, R.identify ∧ R.preserve
|