ObservationPatternClosure.lean

1 import RealizationBoundaries.SubgroupSpectrum
2 
3 /-! # Coherent finite prime observations reconstruct exactly one selector -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace RealizationBoundaries
7 
8 /-- Each finite observation is supported on its finite domain, and restricting
9 a larger observation gives exactly the smaller one. -/
10 structure CompatibleSpectrumPatterns where
11   pattern : Finset Prime → Set Prime
12   supported : ∀ F, pattern F ⊆ (F : Set Prime)
13   compatible : ∀ F G, F ⊆ G → pattern F = pattern G ∩ (F : Set Prime)
14 
15 /-- A full compatible family reads each selector bit from its singleton pattern. -/
16 def CompatibleSpectrumPatterns.selector (P : CompatibleSpectrumPatterns) : Set Prime :=
17   {p | p ∈ P.pattern {p}}
18 
19 /-- Compatibility is sufficient for existence of the global selector. -/
20 theorem CompatibleSpectrumPatterns.pattern_eq_restriction (P : CompatibleSpectrumPatterns)
21     (F : Finset Prime) : P.pattern F = P.selector ∩ (F : Set Prime) := by
22   classical
23   ext p
24   constructor
25   · intro hp
26     have hpF : p ∈ F := P.supported F hp
27     refine ⟨?_, hpF⟩
28     change p ∈ P.pattern {p}
29     rw [P.compatible {p} F (Finset.singleton_subset_iff.mpr hpF)]
30     exact ⟨hp, Finset.mem_singleton_self p⟩
31   · rintro ⟨hp, hpF⟩
32     change p ∈ P.pattern {p} at hp
33     rw [P.compatible {p} F (Finset.singleton_subset_iff.mpr hpF)] at hp
34     exact hp.1
35 
36 /-- Every full compatible collection of finite membership patterns determines
37 one and only one prime selector, including existence rather than uniqueness alone. -/
38 theorem compatible_spectrum_patterns_exists_unique (P : CompatibleSpectrumPatterns) :
39     ∃! B : Set Prime, ∀ F : Finset Prime, P.pattern F = B ∩ (F : Set Prime) := by
40   classical
41   refine ⟨P.selector, P.pattern_eq_restriction, ?_⟩
42   intro B hB
43   ext p
44   have he := hB {p}
45   have hp : p ∈ P.pattern {p} ↔ p ∈ B := by
46     rw [he]
47     simp
48   exact hp.symm
49 
50 /-- Coherent finite data therefore determine one actual subgroup of D. -/
51 theorem compatible_spectrum_patterns_group_unique (P : CompatibleSpectrumPatterns)
52     (B C : Set Prime)
53     (hB : ∀ F : Finset Prime, P.pattern F = B ∩ (F : Set Prime))
54     (hC : ∀ F : Finset Prime, P.pattern F = C ∩ (F : Set Prime)) :
55     spectrumSubgroup B = spectrumSubgroup C := by
56   have h := compatible_spectrum_patterns_exists_unique P
57   exact congrArg spectrumSubgroup (h.unique hB hC)
58 
59 end RealizationBoundaries

Back to source controls