PartitionOccupancy.lean

1 import MachineTheory.Correction
2 import Mathlib.Data.Fintype.Pi
3 
4 /-!
5 # Partition correction memory
6 
7 Reviewed Core v0.2, Corollary 3.2. The evidence events are exactly preimages
8 of cell subsets. Target values need not all be attained, and the target type
9 need not be finite. Empty candidate sets are retained. The counting and bit
10 claims concern all candidate subsets and fixed-width binary states only.
11 -/
12 
13 namespace Komorebi.MachineTheory.PartitionCorrection
14 
15 variable {Ω I Y : Type*}
16 
17 /-- Exactly the unions of cells of the cell map. -/
18 def algebra (c : Ω → I) : EvidenceAlgebra Ω where
19   events := Set.range (fun J : Set I => c ⁻¹' J)
20   univ_mem := ⟨Set.univ, Set.preimage_univ⟩
21   inter_mem := by
22     rintro E ⟨J, rfl⟩ F ⟨K, rfl⟩
23     exact ⟨J ∩ K, rfl⟩
24 
25 /-- A specified union of cells is an admitted evidence event. -/
26 def event (c : Ω → I) (J : Set I) : (algebra c).Event :=
27   ⟨c ⁻¹' J, ⟨J, rfl⟩⟩
28 
29 theorem event_membership_iff (c : Ω → I) (E : Set Ω) :
30     E ∈ (algebra c).events ↔ ∃ J : Set I, c ⁻¹' J = E := Iff.rfl
31 
32 /-- The attained cell-target pairs, excluding unoccupied ambient pairs. -/
33 abbrev Pair (c : Ω → I) (t : Ω → Y) := Attained (fun ω => (c ω, t ω))
34 
35 def pair (c : Ω → I) (t : Ω → Y) (ω : Ω) : Pair c t :=
36   record (fun x => (c x, t x)) ω
37 
38 theorem pair_surjective (c : Ω → I) (t : Ω → Y) :
39     Function.Surjective (pair c t) := by
40   intro d
41   obtain ⟨ω, hω⟩ := d.property
42   exact ⟨ω, Subtype.ext hω⟩
43 
44 /-- Occupancy records the attained pairs met by the candidate set. -/
45 def occupancy (c : Ω → I) (t : Ω → Y) (V : Set Ω) : Set (Pair c t) :=
46   pair c t '' V
47 
48 theorem mem_occupancy_iff (c : Ω → I) (t : Ω → Y)
49     (V : Set Ω) (d : Pair c t) :
50     d ∈ occupancy c t V ↔
51       ∃ ω ∈ V, c ω = d.val.1 ∧ t ω = d.val.2 := by
52   constructor
53   · rintro ⟨ω, hω, he⟩
54     have hpair : (c ω, t ω) = d.val := congrArg Subtype.val he
55     exact ⟨ω, hω, congrArg Prod.fst hpair, congrArg Prod.snd hpair⟩
56   · rintro ⟨ω, hω, hc, ht⟩
57     exact ⟨ω, hω, Subtype.ext (Prod.ext hc ht)⟩
58 
59 /-- The single-cell signature coordinate recovers each occupancy bit. -/
60 theorem mem_occupancy_iff_single_cell (c : Ω → I) (t : Ω → Y)
61     (V : Set Ω) (d : Pair c t) :
62     d ∈ occupancy c t V ↔
63       d.val.2 ∈ (algebra c).signature t V (event c {d.val.1}) := by
64   rw [mem_occupancy_iff]
65   constructor
66   · rintro ⟨ω, hω, hc, ht⟩
67     exact ⟨ω, ⟨hω, hc⟩, ht⟩
68   · rintro ⟨ω, ⟨hω, hc⟩, ht⟩
69     exact ⟨ω, hω, hc, ht⟩
70 
71 /-- All correction signatures and occupancy records identify the same subsets. -/
72 theorem signature_eq_iff_occupancy_eq (c : Ω → I) (t : Ω → Y)
73     (V W : Set Ω) :
74     (algebra c).signature t V = (algebra c).signature t W ↔
75       occupancy c t V = occupancy c t W := by
76   constructor
77   · intro h
78     ext d
79     rw [mem_occupancy_iff_single_cell, mem_occupancy_iff_single_cell, h]
80   · intro h
81     funext e
82     obtain ⟨J, hJ⟩ := e.property
83     apply Set.ext
84     intro y
85     change y ∈ t '' (V ∩ e.val) ↔ y ∈ t '' (W ∩ e.val)
86     rw [← hJ]
87     constructor
88     · rintro ⟨ω, ⟨hω, hcell⟩, ht⟩
89       have ho : pair c t ω ∈ occupancy c t W := by
90         rw [← h]
91         exact ⟨ω, hω, rfl⟩
92       obtain ⟨ω', hω', hc', ht'⟩ := (mem_occupancy_iff c t W _).mp ho
93       refine ⟨ω', ⟨hω', ?_⟩, ht'.trans ht⟩
94       change c ω' ∈ J
95       change c ω' = c ω at hc'
96       rw [hc']
97       exact hcell
98     · rintro ⟨ω, ⟨hω, hcell⟩, ht⟩
99       have ho : pair c t ω ∈ occupancy c t V := by
100         rw [h]
101         exact ⟨ω, hω, rfl⟩
102       obtain ⟨ω', hω', hc', ht'⟩ := (mem_occupancy_iff c t V _).mp ho
103       refine ⟨ω', ⟨hω', ?_⟩, ht'.trans ht⟩
104       change c ω' ∈ J
105       change c ω' = c ω at hc'
106       rw [hc']
107       exact hcell
108 
109 /-- A realization uses the full pair-fibre preimage, with no choices of worlds. -/
110 def realize (c : Ω → I) (t : Ω → Y) (S : Set (Pair c t)) : Set Ω :=
111   pair c t ⁻¹' S
112 
113 @[simp] theorem occupancy_realize (c : Ω → I) (t : Ω → Y)
114     (S : Set (Pair c t)) : occupancy c t (realize c t S) = S := by
115   exact Set.image_preimage_eq S (pair_surjective c t)
116 
117 theorem occupancy_surjective (c : Ω → I) (t : Ω → Y) :
118     Function.Surjective (occupancy c t) :=
119   fun S => ⟨realize c t S, occupancy_realize c t S⟩
120 
121 def fromOccupancy (c : Ω → I) (t : Ω → Y) (S : Set (Pair c t)) :
122     (algebra c).Memory t := (algebra c).remember t (realize c t S)
123 
124 theorem fromOccupancy_bijective (c : Ω → I) (t : Ω → Y) :
125     Function.Bijective (fromOccupancy c t) := by
126   constructor
127   · intro S T h
128     have hs : (algebra c).signature t (realize c t S) =
129         (algebra c).signature t (realize c t T) := congrArg Subtype.val h
130     have ho := (signature_eq_iff_occupancy_eq c t _ _).mp hs
131     simpa only [occupancy_realize] using ho
132   · intro m
133     obtain ⟨V, hV⟩ := m.property
134     refine ⟨occupancy c t V, ?_⟩
135     apply Subtype.ext
136     change (algebra c).signature t (realize c t (occupancy c t V)) = m.val
137     rw [← hV]
138     apply (signature_eq_iff_occupancy_eq c t _ _).mpr
139     exact occupancy_realize c t _
140 
141 /-- Actual equivalence, not only matching cardinal inequalities. -/
142 noncomputable def memoryEquiv (c : Ω → I) (t : Ω → Y) :
143     (algebra c).Memory t ≃ Set (Pair c t) :=
144   (Equiv.ofBijective (fromOccupancy c t) (fromOccupancy_bijective c t)).symm
145 
146 @[simp] theorem memoryEquiv_fromOccupancy (c : Ω → I) (t : Ω → Y)
147     (S : Set (Pair c t)) : memoryEquiv c t (fromOccupancy c t S) = S :=
148   (Equiv.ofBijective (fromOccupancy c t) (fromOccupancy_bijective c t)).left_inv S
149 
150 @[simp] theorem fromOccupancy_occupancy (c : Ω → I) (t : Ω → Y)
151     (V : Set Ω) : fromOccupancy c t (occupancy c t V) = (algebra c).remember t V := by
152   apply Subtype.ext
153   exact (signature_eq_iff_occupancy_eq c t _ _).mpr (occupancy_realize c t _)
154 
155 @[simp] theorem memoryEquiv_remember (c : Ω → I) (t : Ω → Y) (V : Set Ω) :
156     memoryEquiv c t ((algebra c).remember t V) = occupancy c t V := by
157   rw [← fromOccupancy_occupancy, memoryEquiv_fromOccupancy]
158 
159 theorem card_memory [Fintype Ω] (c : Ω → I) (t : Ω → Y) :
160     Fintype.card ((algebra c).Memory t) = 2 ^ Fintype.card (Pair c t) := by
161   classical
162   rw [Fintype.card_congr (memoryEquiv c t), Fintype.card_set]
163 
164 /-- Read the occupied target values, without forgetting cell associations in state. -/
165 def readOccupancy (c : Ω → I) (t : Ω → Y) (S : Set (Pair c t)) : Set Y :=
166   (fun d => d.val.2) '' S
167 
168 @[simp] theorem readOccupancy_occupancy (c : Ω → I) (t : Ω → Y) (V : Set Ω) :
169     readOccupancy c t (occupancy c t V) = t '' V := by
170   unfold readOccupancy occupancy
171   rw [Set.image_image]
172   rfl
173 
174 /-- Evidence restricts the existing occupancy vector by its cell coordinate. -/
175 def restrictOccupancy (c : Ω → I) (t : Ω → Y) (J : Set I)
176     (S : Set (Pair c t)) : Set (Pair c t) := S ∩ {d | d.val.1 ∈ J}
177 
178 theorem occupancy_inter_cells (c : Ω → I) (t : Ω → Y) (V : Set Ω) (J : Set I) :
179     occupancy c t (V ∩ c ⁻¹' J) = restrictOccupancy c t J (occupancy c t V) := by
180   ext d
181   constructor
182   · intro h
183     obtain ⟨ω, ⟨hV, hJ⟩, hc, ht⟩ := (mem_occupancy_iff c t _ d).mp h
184     refine ⟨(mem_occupancy_iff c t V d).mpr ⟨ω, hV, hc, ht⟩, ?_⟩
185     change d.val.1 ∈ J
186     rw [← hc]
187     exact hJ
188   · rintro ⟨h, hJ⟩
189     obtain ⟨ω, hV, hc, ht⟩ := (mem_occupancy_iff c t V d).mp h
190     apply (mem_occupancy_iff c t _ d).mpr
191     refine ⟨ω, ⟨hV, ?_⟩, hc, ht⟩
192     change c ω ∈ J
193     rw [hc]
194     exact hJ
195 
196 /-- Every admitted event comes with an actual cell-subset representation. -/
197 noncomputable def eventCells (c : Ω → I) (e : (algebra c).Event) : Set I :=
198   Classical.choose e.property
199 
200 theorem eventCells_preimage (c : Ω → I) (e : (algebra c).Event) :
201     c ⁻¹' eventCells c e = e.val := Classical.choose_spec e.property
202 
203 theorem occupancy_filter (c : Ω → I) (t : Ω → Y)
204     (e : (algebra c).Event) (V : Set Ω) :
205     occupancy c t ((algebra c).filter e V) =
206       restrictOccupancy c t (eventCells c e) (occupancy c t V) := by
207   change occupancy c t (V ∩ e.val) = _
208   rw [← eventCells_preimage c e]
209   exact occupancy_inter_cells c t V _
210 
211 /-- Source-facing partition condition. Surjectivity makes each named cell nonempty. -/
212 theorem nonempty_cells_iff_surjective (c : Ω → I) :
213     (∀ i, (c ⁻¹' ({i} : Set I)).Nonempty) ↔ Function.Surjective c := by
214   constructor
215   · intro h i
216     obtain ⟨ω, hω⟩ := h i
217     exact ⟨ω, hω⟩
218   · intro h i
219     obtain ⟨ω, hω⟩ := h i
220     exact ⟨ω, hω⟩
221 
222 end Komorebi.MachineTheory.PartitionCorrection

Back to source controls