SeedObstructions.lean

1 import RealizationBoundaries.SeedGeneration
2 
3 /-! # Finite seeds cannot reach omitted prime coordinates -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace RealizationBoundaries
7 
8 /-- All finite direct-sum seed families share a missing prime coordinate. -/
9 theorem finiteSupport_finite_seeds_missing (S : Set finiteSupport) (hS : S.Finite) :
10     ∃ p : Prime, ∀ x ∈ S, x.val p = 0 := by
11   let E : Set Prime := ⋃ x ∈ S, support x.val
12   have hE : E.Finite := hS.biUnion fun x _ => x.property
13   have hpre : {n : ℕ | primeAt n ∈ E}.Finite :=
14     hE.preimage primeAt_injective.injOn
15   obtain ⟨n, hn⟩ := hpre.exists_notMem
16   refine ⟨primeAt n, ?_⟩
17   intro x hx
18   by_contra h
19   exact hn (Set.mem_iUnion.mpr ⟨x, Set.mem_iUnion.mpr ⟨hx, h⟩⟩)
20 
21 /-- A closed coordinate certificate survives the full endomorphism orbit and closure. -/
22 theorem finiteSupport_seed_certificate (S : Set finiteSupport) (hS : S.Finite) :
23     ∃ p : Prime, endomorphismHull S ≤ coordinateKernel finiteSupport p ∧
24       topologicalEndomorphismHull S ≤ coordinateKernel finiteSupport p ∧
25       coordinateKernel finiteSupport p ≠ ⊤ := by
26   obtain ⟨p, hp⟩ := finiteSupport_finite_seeds_missing S hS
27   have h := coordinate_obstruction finiteSupport p S hp
28     (fun f x hx => finiteSupport_endomorphism_preserves_zero f x p hx)
29   exact ⟨p, h.1, h.2, coordinateKernel_ne_top finiteSupport le_rfl p⟩
30 
31 theorem finiteSupport_no_finite_endomorphism_seeds (S : Set finiteSupport) (hS : S.Finite) :
32     endomorphismHull S ≠ ⊤ := by
33   obtain ⟨p, h, _, hne⟩ := finiteSupport_seed_certificate S hS
34   intro heq
35   exact hne (top_unique (heq ▸ h))
36 
37 theorem finiteSupport_no_finite_topological_seeds (S : Set finiteSupport) (hS : S.Finite) :
38     topologicalEndomorphismHull S ≠ ⊤ := by
39   obtain ⟨p, _, h, hne⟩ := finiteSupport_seed_certificate S hS
40   intro heq
41   exact hne (top_unique (heq ▸ h))
42 
43 /-- Every actual selector-group element has finite support off the selected primes,
44 including elements with rational coordinate zero. -/
45 theorem selector_outside_support_finite (T : Set Prime) (x : selectorGroup T) :
46     (support x.val \ T).Finite := by
47   classical
48   obtain ⟨r, d, hd⟩ := normalForm_exists T x
49   apply d.property.subset
50   intro p hp
51   have he : x.val p = d.val p := by
52     rw [hd]
53     simp [rationalSection, hp.2]
54   exact fun hz => hp.1 (he.trans hz)
55 
56 theorem omittedIndex_injective (a : ℕ → Bool) : Function.Injective (omittedIndex a) := by
57   intro i j h
58   have hi := omittedIndex_bounds a i
59   have hj := omittedIndex_bounds a j
60   omega
61 
62 /-- A finite family misses an unselected prime even if each seed has infinite support. -/
63 theorem paired_finite_seeds_missing (a : ℕ → Bool) (S : Set (pairedGroup a))
64     (hS : S.Finite) :
65     ∃ n : ℕ, ∀ x ∈ S, x.val (primeAt (omittedIndex a n)) = 0 := by
66   let E : Set Prime := ⋃ x ∈ S, support x.val \ pairedSelector a
67   have hE : E.Finite := hS.biUnion fun x _ => selector_outside_support_finite _ x
68   have hi := primeAt_injective.comp (omittedIndex_injective a)
69   have hpre : {n : ℕ | primeAt (omittedIndex a n) ∈ E}.Finite := hE.preimage hi.injOn
70   obtain ⟨n, hn⟩ := hpre.exists_notMem
71   refine ⟨n, ?_⟩
72   intro x hx
73   by_contra h
74   exact hn (Set.mem_iUnion.mpr ⟨x,
75     Set.mem_iUnion.mpr ⟨hx, h, omitted_not_mem a n⟩⟩)
76 
77 /-- The certificate uses a genuine nonzero prime seed in the original group. -/
78 theorem paired_seed_certificate (a : ℕ → Bool) (S : Set (pairedGroup a)) (hS : S.Finite) :
79     ∃ p : Prime, p ∉ pairedSelector a ∧
80       endomorphismHull S ≤ coordinateKernel (pairedGroup a) p ∧
81       topologicalEndomorphismHull S ≤ coordinateKernel (pairedGroup a) p ∧
82       coordinateKernel (pairedGroup a) p ≠ ⊤ := by
83   obtain ⟨n, hn⟩ := paired_finite_seeds_missing a S hS
84   let p := primeAt (omittedIndex a n)
85   have h := coordinate_obstruction (pairedGroup a) p S hn
86     (fun f x hx => hom_preserves_zero_coordinate _ _ f x p hx)
87   exact ⟨p, omitted_not_mem a n, h.1, h.2,
88     coordinateKernel_ne_top _ (finiteSupport_le_preimage _) p⟩
89 
90 theorem paired_no_finite_endomorphism_seeds (a : ℕ → Bool)
91     (S : Set (pairedGroup a)) (hS : S.Finite) : endomorphismHull S ≠ ⊤ := by
92   obtain ⟨p, _, h, _, hne⟩ := paired_seed_certificate a S hS
93   intro heq
94   exact hne (top_unique (heq ▸ h))
95 
96 theorem paired_no_finite_topological_seeds (a : ℕ → Bool)
97     (S : Set (pairedGroup a)) (hS : S.Finite) : topologicalEndomorphismHull S ≠ ⊤ := by
98   obtain ⟨p, _, _, h, hne⟩ := paired_seed_certificate a S hS
99   intro heq
100   exact hne (top_unique (heq ▸ h))
101 
102 end RealizationBoundaries

Back to source controls