OccupancyExamples.lean

1 import MachineTheory.OccupancyBinary
2 
3 /-!
4 # Partition memory examples and boundaries
5 
6 These examples preserve empty candidates, unused target values, target values
7 shared by distinct cells, and cells containing several target values. The
8 four-cell/eight-world example uses exactly the source variables (b,s,nuisance).
9 -/
10 namespace Komorebi.MachineTheory.PartitionCorrection.Examples
11 
12 noncomputable section
13 
14 abbrev SensorWorld := Bool × Bool × Bool
15 
16 def sensorCell (w : SensorWorld) : Bool × Bool := (w.1, w.2.1)
17 def sensorTarget (w : SensorWorld) : Bool := w.1
18 
19 theorem sensorCell_surjective : Function.Surjective sensorCell := by
20   intro p
21   exact ⟨(p.1, p.2, false), rfl⟩
22 
23 def sensorPairEquiv : Pair sensorCell sensorTarget ≃ (Bool × Bool) where
24   toFun d := d.val.1
25   invFun p := pair sensorCell sensorTarget (p.1, p.2, false)
26   left_inv d := by
27     apply Subtype.ext
28     change ((d.val.1.1, d.val.1.2), d.val.1.1) = d.val
29     obtain ⟨w, hw⟩ := d.property
30     rw [← hw]
31     rfl
32   right_inv _ := rfl
33 
34 theorem sensor_pair_count : Fintype.card (Pair sensorCell sensorTarget) = 4 := by
35   rw [Fintype.card_congr sensorPairEquiv]
36   decide
37 
38 theorem sensor_world_count : Fintype.card SensorWorld = 8 := by decide
39 
40 theorem sensor_signature_count :
41     Fintype.card ((algebra sensorCell).Memory sensorTarget) = 16 := by
42   rw [card_memory, sensor_pair_count]
43   decide
44 
45 theorem sensor_no_three_bit_memory :
46     ¬ ∃ (r : Set SensorWorld → (Fin 3 → Bool))
47       (q : (Fin 3 → Bool) → Set Bool)
48       (step : (algebra sensorCell).Event → (Fin 3 → Bool) → (Fin 3 → Bool)),
49       (∀ V, q (r V) = sensorTarget '' V) ∧
50       (∀ e V, step e (r V) = r ((algebra sensorCell).filter e V)) := by
51   rintro ⟨r, q, step, hq, hs⟩
52   have h := fixed_bits_necessary sensorCell sensorTarget 3 r q step hq hs
53   rw [sensor_pair_count] at h
54   exact (by decide : ¬ 4 ≤ 3) h
55 
56 def sensorV : Set SensorWorld := {(false, false, false), (true, true, false)}
57 def sensorW : Set SensorWorld := {(false, true, false), (true, false, false)}
58 def calibrationCells : Set (Bool × Bool) := {p | p.2 = false}
59 
60 theorem sensor_present_targets_equal : sensorTarget '' sensorV = sensorTarget '' sensorW := by
61   simp [sensorV, sensorW, sensorTarget]
62 
63 theorem sensor_filter_V : sensorV ∩ sensorCell ⁻¹' calibrationCells =
64     {(false, false, false)} := by
65   ext w
66   rcases w with ⟨b, s, n⟩
67   cases b <;> cases s <;> cases n <;> simp [sensorV, sensorCell, calibrationCells]
68 
69 theorem sensor_filter_W : sensorW ∩ sensorCell ⁻¹' calibrationCells =
70     {(true, false, false)} := by
71   ext w
72   rcases w with ⟨b, s, n⟩
73   cases b <;> cases s <;> cases n <;> simp [sensorW, sensorCell, calibrationCells]
74 
75 theorem sensor_signatures_ne :
76     (algebra sensorCell).signature sensorTarget sensorV ≠
77       (algebra sensorCell).signature sensorTarget sensorW := by
78   intro h
79   have he := congrFun h (event sensorCell calibrationCells)
80   change sensorTarget '' (sensorV ∩ sensorCell ⁻¹' calibrationCells) =
81     sensorTarget '' (sensorW ∩ sensorCell ⁻¹' calibrationCells) at he
82   rw [sensor_filter_V, sensor_filter_W] at he
83   have ht := congrArg (fun S : Set Bool => false ∈ S) he
84   simp [sensorTarget] at ht
85 
86 theorem current_target_set_does_not_determine_correction :
87     ¬ ∀ V W : Set SensorWorld, sensorTarget '' V = sensorTarget '' W →
88       (algebra sensorCell).signature sensorTarget V =
89         (algebra sensorCell).signature sensorTarget W := by
90   intro h
91   exact sensor_signatures_ne (h sensorV sensorW sensor_present_targets_equal)
92 
93 @[simp] theorem empty_occupancy {Ω I Y : Type*} (c : Ω → I) (t : Ω → Y) :
94     occupancy c t ∅ = ∅ := by simp [occupancy]
95 
96 /-- An impossible admitted event produces the contradictory candidate state. -/
97 theorem contradictory_filter {Ω I : Type*} (c : Ω → I) (V : Set Ω) :
98     (algebra c).filter (event c ∅) V = ∅ := by
99   simp [EvidenceAlgebra.filter, event]
100 
101 /-- The binary readout retains contradiction, rather than choosing a target. -/
102 theorem contradictory_binary_readout {Ω I Y : Type*} [Fintype Ω]
103     (c : Ω → I) (t : Ω → Y) (V : Set Ω) :
104     readBits c t (updateBits c t (event c ∅) (encode c t V)) = ∅ := by
105   rw [encode_update, encode_read, contradictory_filter]
106   exact Set.image_empty t
107 
108 def emptyCell : Empty → Empty := Empty.elim
109 def emptyTarget : Empty → Nat := Empty.elim
110 
111 theorem empty_pair_count : Fintype.card (Pair emptyCell emptyTarget) = 0 := by
112   let : IsEmpty (Pair emptyCell emptyTarget) := ⟨fun d => by
113     obtain ⟨w, _⟩ := d.property
114     exact Empty.elim w⟩
115   simp
116 
117 theorem empty_signature_count :
118     Fintype.card ((algebra emptyCell).Memory emptyTarget) = 1 := by
119   rw [card_memory, empty_pair_count]
120   decide
121 
122 def oneCell (_ : Bool) : Unit := ()
123 def constantTarget (_ : Bool) : Bool := false
124 
125 def constantPairEquiv : Pair oneCell constantTarget ≃ Unit where
126   toFun _ := ()
127   invFun _ := pair oneCell constantTarget false
128   left_inv d := by
129     apply Subtype.ext
130     obtain ⟨w, hw⟩ := d.property
131     rw [← hw]
132     rfl
133   right_inv p := by cases p; rfl
134 
135 theorem one_cell_pair_count : Fintype.card (Pair oneCell constantTarget) = 1 := by
136   rw [Fintype.card_congr constantPairEquiv]
137   decide
138 
139 theorem one_cell_signature_count :
140     Fintype.card ((algebra oneCell).Memory constantTarget) = 2 := by
141   rw [card_memory, one_cell_pair_count]
142   decide
143 
144 theorem constant_singletons_same_occupancy :
145     occupancy oneCell constantTarget {false} = occupancy oneCell constantTarget {true} := by
146   simp [occupancy, pair, record, oneCell, constantTarget]
147 
148 def splitAlgebra : EvidenceAlgebra Bool where
149   events := Set.univ
150   univ_mem := Set.mem_univ _
151   inter_mem := by intros; trivial
152 
153 def splitEvent : splitAlgebra.Event := ⟨{false}, Set.mem_univ _⟩
154 
155 theorem splitting_cell_changes_signature :
156     splitAlgebra.signature constantTarget {false} ≠
157       splitAlgebra.signature constantTarget {true} := by
158   intro h
159   have ht := congrArg (fun S : Set Bool => false ∈ S) (congrFun h splitEvent)
160   simp [EvidenceAlgebra.signature, splitEvent, constantTarget] at ht
161 
162 theorem singleton_event_not_old_admitted : ({false} : Set Bool) ∉ (algebra oneCell).events := by
163   rintro ⟨J, hJ⟩
164   change oneCell ⁻¹' J = {false} at hJ
165   have hf : oneCell false ∈ J := by
166     change false ∈ oneCell ⁻¹' J
167     rw [hJ]
168     exact Set.mem_singleton false
169   have ht : true ∈ oneCell ⁻¹' J := hf
170   rw [hJ] at ht
171   simp at ht
172 
173 def separateCells : Bool → Bool := id
174 
175 theorem separate_singletons_different_occupancy :
176     occupancy separateCells constantTarget {false} ≠
177       occupancy separateCells constantTarget {true} := by
178   intro h
179   have hm : pair separateCells constantTarget false ∈
180       occupancy separateCells constantTarget {false} := ⟨false, Set.mem_singleton _, rfl⟩
181   rw [h] at hm
182   obtain ⟨w, hw, hp⟩ := hm
183   have hw' : w = true := hw
184   subst w
185   have hb := congrArg (fun d : Pair separateCells constantTarget => d.val.1) hp
186   change true = false at hb
187   cases hb
188 
189 theorem missing_cells_merges_signatures :
190     (algebra oneCell).signature constantTarget {false} =
191       (algebra oneCell).signature constantTarget {true} :=
192   (signature_eq_iff_occupancy_eq oneCell constantTarget _ _).mpr
193     constant_singletons_same_occupancy
194 
195 def multiCell (w : Bool × Bool) : Bool := w.1
196 def multiTarget (w : Bool × Bool) : Bool := w.2
197 
198 def multiPairEquiv : Pair multiCell multiTarget ≃ (Bool × Bool) where
199   toFun d := d.val
200   invFun p := pair multiCell multiTarget p
201   left_inv _ := Subtype.ext rfl
202   right_inv _ := rfl
203 
204 theorem multi_target_pair_count : Fintype.card (Pair multiCell multiTarget) = 4 := by
205   rw [Fintype.card_congr multiPairEquiv]
206   decide
207 
208 theorem multi_target_signature_count :
209     Fintype.card ((algebra multiCell).Memory multiTarget) = 16 := by
210   rw [card_memory, multi_target_pair_count]
211   decide
212 
213 def natTarget (b : Bool) : Nat := if b then 1 else 0
214 
215 theorem target_two_unattained : 2 ∉ Set.range natTarget := by
216   rintro ⟨b, hb⟩
217   cases b <;> simp [natTarget] at hb
218 
219 theorem no_unattained_pair (d : Pair oneCell natTarget) : d.val.2 ≠ 2 := by
220   have ht : d.val.2 ∈ Set.range natTarget := by
221     obtain ⟨b, hb⟩ := d.property
222     exact ⟨b, congrArg Prod.snd hb⟩
223   intro h
224   rw [h] at ht
225   exact target_two_unattained ht
226 
227 end
228 end Komorebi.MachineTheory.PartitionCorrection.Examples

Back to source controls