SelectorClassification.lean

1 import RealizationBoundaries.TailSignature
2 
3 /-!
4 # Unmarked and marked classification of the paired-prime groups
5 
6 The unmarked invariant is eventual equality of selectors. Finite changes give
7 literal equality of the ambient subgroups. Homomorphism root preservation is
8 used directly; no coordinate diagonality is assumed.
9 -/
10 set_option autoImplicit false
11 set_option backward.isDefEq.respectTransparency false
12 noncomputable section
13 namespace RealizationBoundaries
14 
15 /-- At a differing bit, the source's chosen prime is the target's omitted prime. -/
16 theorem chosenIndex_eq_omittedIndex_of_ne (a b : ℕ → Bool) (n : ℕ)
17     (h : a n ≠ b n) : chosenIndex a n = omittedIndex b n := by
18   cases ha : a n <;> cases hb : b n <;> simp_all [chosenIndex, omittedIndex]
19 
20 /-- Membership of one selector's chosen prime in another reads equality of that bit. -/
21 theorem chosen_mem_other_iff (a b : ℕ → Bool) (n : ℕ) :
22     primeAt (chosenIndex a n) ∈ pairedSelector b ↔ a n = b n := by
23   constructor
24   · intro hm
25     by_contra h
26     rw [chosenIndex_eq_omittedIndex_of_ne a b n h] at hm
27     exact omitted_not_mem b n hm
28   · intro h
29     have hi : chosenIndex a n = chosenIndex b n := by simp [chosenIndex, h]
30     rw [hi]
31     exact chosen_mem b n
32 
33 /-- One-sided tail containment is enough for paired selectors: one prime is chosen
34 from each pair, so a genuine mismatch violates the containment in one coordinate. -/
35 theorem finite_bit_disagreement_of_tail_inclusion (a b : ℕ → Bool)
36     (E : Set Prime) (hE : E.Finite)
37     (h : ∀ p ∉ E, p ∈ pairedSelector b → p ∈ pairedSelector a) :
38     {n : ℕ | a n ≠ b n}.Finite := by
39   have hi : Function.Injective (fun n => primeAt (chosenIndex b n)) :=
40     primeAt_injective.comp (chosenIndex_injective b)
41   apply (hE.preimage hi.injOn).subset
42   intro n hn
43   change primeAt (chosenIndex b n) ∈ E
44   by_contra hp
45   have hm := h _ hp (chosen_mem b n)
46   exact hn ((chosen_mem_other_iff b a n).mp hm).symm
47 
48 /-- A finite change in bits changes only finitely many prime coordinates. -/
49 theorem pairedSelectors_agree_off_finite (a b : ℕ → Bool)
50     (h : {n : ℕ | a n ≠ b n}.Finite) :
51     ∃ E : Set Prime, E.Finite ∧
52       ∀ p ∉ E, (p ∈ pairedSelector a ↔ p ∈ pairedSelector b) := by
53   let E := (fun n => primeAt (chosenIndex a n)) '' {n | a n ≠ b n} ∪
54     (fun n => primeAt (chosenIndex b n)) '' {n | a n ≠ b n}
55   refine ⟨E, (h.image _).union (h.image _), ?_⟩
56   intro p hp
57   constructor
58   · rintro ⟨n, rfl⟩
59     apply (chosen_mem_other_iff a b n).mpr
60     by_contra hn
61     exact hp (Or.inl ⟨n, hn, rfl⟩)
62   · rintro ⟨n, rfl⟩
63     apply (chosen_mem_other_iff b a n).mpr
64     by_contra hn
65     exact hp (Or.inr ⟨n, Ne.symm hn, rfl⟩)
66 
67 /-- Finite changes in a selector leave its actual quotient line and preimage unchanged. -/
68 theorem selectorGroup_eq_of_agree_off (S T : Set Prime) (E : Set Prime)
69     (hE : E.Finite) (h : ∀ p ∉ E, (p ∈ S ↔ p ∈ T)) :
70     selectorGroup S = selectorGroup T := by
71   classical
72   have hd : indicator S - indicator T ∈ finiteSupport := by
73     apply hE.subset
74     intro p hp
75     by_contra he
76     have hh := h p he
77     apply hp
78     change indicator S p - indicator T p = 0
79     simp [indicator, hh]
80   have hq := (quotientMap_eq_iff (indicator S) (indicator T)).mpr hd
81   unfold selectorGroup selectorLine
82   rw [hq]
83 
84 /-- The converse classification is literal subgroup equality, not merely isomorphism. -/
85 theorem pairedGroup_eq_of_finite_disagreement (a b : ℕ → Bool)
86     (h : {n : ℕ | a n ≠ b n}.Finite) : pairedGroup a = pairedGroup b := by
87   obtain ⟨E, hE, he⟩ := pairedSelectors_agree_off_finite a b h
88   exact selectorGroup_eq_of_agree_off _ _ E hE he
89 
90 /-- An explicitly constructed isomorphism that leaves the underlying ambient point unchanged. -/
91 def pairedEquivOfFiniteDisagreement (a b : ℕ → Bool)
92     (h : {n : ℕ | a n ≠ b n}.Finite) : pairedGroup a ≃+ pairedGroup b :=
93   AddEquiv.addSubgroupCongr (pairedGroup_eq_of_finite_disagreement a b h)
94 
95 @[simp] theorem pairedEquivOfFiniteDisagreement_val (a b : ℕ → Bool)
96     (h : {n : ℕ | a n ≠ b n}.Finite) (x : pairedGroup a) :
97     (pairedEquivOfFiniteDisagreement a b h x).val = x.val :=
98   AddEquiv.addSubgroupCongr_apply _ x
99 
100 /-- A nonzero rational part in the image of even one element forces tail agreement.
101 This is proved for arbitrary additive homomorphisms, without continuity or diagonality assumptions. -/
102 theorem finite_disagreement_of_nontorsion_image (a b : ℕ → Bool)
103     (f : pairedGroup a →+ pairedGroup b) (x : pairedGroup a)
104     (hx : (f x).val ∉ finiteSupport) : {n : ℕ | a n ≠ b n}.Finite := by
105   have hs : x.val ∉ finiteSupport :=
106     nontorsion_source_of_image (selectorLine (pairedSelector a))
107       (selectorLine (pairedSelector b)) f x hx
108   obtain ⟨E, hE, he⟩ := selector_tail_signature (pairedSelector a) x hs
109   obtain ⟨F, hF, hf⟩ := selector_tail_signature (pairedSelector b) (f x) hx
110   apply finite_bit_disagreement_of_tail_inclusion a b (E ∪ F) (hE.union hF)
111   intro p hp hpb
112   by_contra hpa
113   have hpE : p ∉ E := fun h => hp (Or.inl h)
114   have hpF : p ∉ F := fun h => hp (Or.inr h)
115   have hxroot := (he p hpE).mpr hpa
116   exact ((hf p hpF).mp (hasPrimeRoot_map f x p hxroot)) hpb
117 
118 /-- The forward classification derives its invariant from an actual group equivalence. -/
119 theorem finite_disagreement_of_pairedEquiv (a b : ℕ → Bool)
120     (e : pairedGroup a ≃+ pairedGroup b) : {n : ℕ | a n ≠ b n}.Finite := by
121   let x : pairedGroup b := markedElement (pairedSelector b)
122   have hx : x.val ∉ finiteSupport := markedElement_not_finiteSupport (pairedSelector_infinite b)
123   apply finite_disagreement_of_nontorsion_image a b e.toAddMonoidHom (e.symm x)
124   simpa using hx
125 
126 /-- Monograph Theorem 7.2: exact unmarked classification, modulo finite changes. -/
127 theorem pairedGroup_isomorphic_iff (a b : ℕ → Bool) :
128     Nonempty (pairedGroup a ≃+ pairedGroup b) ↔ {n : ℕ | a n ≠ b n}.Finite := by
129   constructor
130   · rintro ⟨e⟩
131     exact finite_disagreement_of_pairedEquiv a b e
132   · intro h
133     exact ⟨pairedEquivOfFiniteDisagreement a b h⟩
134 
135 /-- Naming the original indicator recovers every bit, not merely its tail. -/
136 theorem selectors_equal_of_markedEquiv (a b : ℕ → Bool)
137     (e : pairedGroup a ≃+ pairedGroup b)
138     (he : e (markedElement (pairedSelector a)) = markedElement (pairedSelector b)) : a = b := by
139   funext n
140   by_contra hn
141   let p := primeAt (chosenIndex a n)
142   have hpA : p ∈ pairedSelector a := chosen_mem a n
143   have hpB : p ∉ pairedSelector b := by
144     change primeAt (chosenIndex a n) ∉ pairedSelector b
145     rw [chosenIndex_eq_omittedIndex_of_ne a b n hn]
146     exact omitted_not_mem b n
147   have hrB : HasPrimeRoot (markedElement (pairedSelector b)) p :=
148     (marked_prime_root_iff _ p).mpr hpB
149   have hrA : HasPrimeRoot (markedElement (pairedSelector a)) p := by
150     apply (hasPrimeRoot_equiv e _ p).mp
151     rwa [he]
152   exact ((marked_prime_root_iff _ p).mp hrA) hpA
153 
154 /-- Monograph Theorem 7.3: exact marked classification. -/
155 theorem pairedGroup_marked_isomorphic_iff (a b : ℕ → Bool) :
156     (∃ e : pairedGroup a ≃+ pairedGroup b,
157       e (markedElement (pairedSelector a)) = markedElement (pairedSelector b)) ↔ a = b := by
158   constructor
159   · rintro ⟨e, he⟩
160     exact selectors_equal_of_markedEquiv a b e he
161   · rintro rfl
162     exact ⟨AddEquiv.refl _, rfl⟩
163 
164 end RealizationBoundaries

Back to source controls