forked from google-deepmind/formal-conjectures
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathPiHeeg.lean
More file actions
31 lines (24 loc) · 829 Bytes
/
Copy pathPiHeeg.lean
File metadata and controls
31 lines (24 loc) · 829 Bytes
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
/-
PiHeeg.lean — TIGHT theorem BES-12
Π_Heeg = -QR((Z/840)*) = W-mirror of Mordell.
-/
import Bes.Definitions
namespace Bes
/-- W-mirror operator: x → -x in ZMod 840 (equivalently, 840 - x). -/
def W_mirror (x : ZMod M840) : ZMod M840 := -x
/-- BES-12a: Π_Heeg equals W-mirror of Mordell. -/
theorem pi_heeg_eq_W_mordell :
PiHeeg = Mordell.image W_mirror := by
native_decide
/-- BES-12b: Π_Heeg disjoint from Mordell (since -1 ∉ QR mod 840). -/
theorem mordell_pi_heeg_disjoint :
Mordell ∩ PiHeeg = ∅ := by
native_decide
/-- BES-12c: |Π_Heeg| = 6, same size as Mordell. -/
theorem pi_heeg_card_eq_six : PiHeeg.card = 6 := by
native_decide
/-- BES-12d: Mordell ∪ Π_Heeg has 12 elements. -/
theorem mordell_union_pi_heeg_card :
(Mordell ∪ PiHeeg).card = 12 := by
native_decide
end Bes