PairedPrimes.lean

1 import RealizationBoundaries.Cocycle
2 import Mathlib.Data.Nat.Prime.Nth
3 
4 /-! # The actual paired-prime selector groups and their marked root tests -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace RealizationBoundaries
8 
9 def primeAt (n : ℕ) : Prime :=
10   ⟨Nat.nth Nat.Prime n, Nat.nth_mem_of_infinite Nat.infinite_setOfPred_prime n⟩
11 
12 theorem primeAt_injective : Function.Injective primeAt := by
13   intro i j h
14   exact Nat.nth_injective Nat.infinite_setOfPred_prime (congrArg Subtype.val h)
15 
16 def chosenIndex (a : ℕ → Bool) (n : ℕ) : ℕ := 2*n + if a n then 1 else 0
17 
18 def omittedIndex (a : ℕ → Bool) (n : ℕ) : ℕ := 2*n + if a n then 0 else 1
19 
20 theorem chosenIndex_bounds (a : ℕ → Bool) (n : ℕ) :
21     2*n ≤ chosenIndex a n ∧ chosenIndex a n < 2*n+2 := by
22   simp only [chosenIndex]
23   split <;> omega
24 
25 theorem omittedIndex_bounds (a : ℕ → Bool) (n : ℕ) :
26     2*n ≤ omittedIndex a n ∧ omittedIndex a n < 2*n+2 := by
27   simp only [omittedIndex]
28   split <;> omega
29 
30 theorem chosenIndex_injective (a : ℕ → Bool) : Function.Injective (chosenIndex a) := by
31   intro i j h
32   have hi := chosenIndex_bounds a i
33   have hj := chosenIndex_bounds a j
34   omega
35 
36 def pairedSelector (a : ℕ → Bool) : Set Prime := Set.range (fun n => primeAt (chosenIndex a n))
37 
38 theorem pairedSelector_infinite (a : ℕ → Bool) : (pairedSelector a).Infinite :=
39   Set.infinite_range_of_injective (primeAt_injective.comp (chosenIndex_injective a))
40 
41 theorem chosen_mem (a : ℕ → Bool) (n : ℕ) :
42     primeAt (chosenIndex a n) ∈ pairedSelector a := ⟨n, rfl⟩
43 
44 theorem omitted_not_mem (a : ℕ → Bool) (n : ℕ) :
45     primeAt (omittedIndex a n) ∉ pairedSelector a := by
46   rintro ⟨j, hj⟩
47   have h := primeAt_injective hj
48   have h1 := chosenIndex_bounds a j
49   have h2 := omittedIndex_bounds a n
50   have hjn : j = n := by omega
51   subst j
52   cases ha : a n <;> simp [chosenIndex, omittedIndex, ha] at h
53 
54 /-- The group is the preimage of its actual rational line in P/D. -/
55 def pairedGroup (a : ℕ → Bool) : AddSubgroup Ambient := selectorGroup (pairedSelector a)
56 
57 def markedElement (S : Set Prime) : selectorGroup S :=
58   ⟨indicator S, by simpa using rationalSection_mem S 1⟩
59 
60 /-- Exact marked divisibility holds at every prime, not just outside finitely many exceptions. -/
61 theorem marked_prime_root_iff (S : Set Prime) (p : Prime) :
62     (∃ y : selectorGroup S, p.val • y = markedElement S) ↔ p ∉ S := by
63   classical
64   refine (preimage_root_iff (selectorLine S) p.property.pos (markedElement S)).trans ?_
65   constructor
66   · intro h hs
67     have h0 := h p (dvd_refl _)
68     change indicator S p = 0 at h0
69     simp [hs] at h0
70   · intro hp q hq
71     have hqp : q = p := Subtype.ext ((p.property.dvd_iff_eq q.property.ne_one).mp hq).symm
72     subst q
73     exact indicator_apply_not_mem hp
74 
75 theorem chosen_prime_obstructs (a : ℕ → Bool) (n : ℕ) :
76     ¬ ∃ y : pairedGroup a,
77       (primeAt (chosenIndex a n)).val • y = markedElement (pairedSelector a) := by
78   intro h
79   exact ((marked_prime_root_iff _ _).mp h) (chosen_mem a n)
80 
81 theorem omitted_prime_has_root (a : ℕ → Bool) (n : ℕ) :
82     ∃ y : pairedGroup a,
83       (primeAt (omittedIndex a n)).val • y = markedElement (pairedSelector a) :=
84   (marked_prime_root_iff _ _).mpr (omitted_not_mem a n)
85 
86 /-- The formal normal-form bijection applies to every binary selector, without an extra
87 infinite-support assumption on the caller. -/
88 def pairedNormalFormEquiv (a : ℕ → Bool) :
89     (ℚ × finiteSupport) ≃ pairedGroup a := normalFormEquiv (pairedSelector_infinite a)
90 
91 end RealizationBoundaries

Back to source controls