Examples.lean

1 import MachineTheory.Transfer
2 import MachineTheory.Correction
3 import MachineTheory.Feedback
4 import Mathlib.Tactic.NormNum
5 import Mathlib.Data.Fintype.BigOperators
6 
7 /-! Kernel-checked witnesses and counterexamples, not sampled agent behavior. -/
8 namespace Komorebi.MachineTheory.Examples
9 open scoped BigOperators
10 open Instrument
11 noncomputable section
12 
13 abbrev Sensor := Bool × Bool × Bool
14 
15 def physical (x : Sensor) : Bool := x.1
16 def display (x : Sensor) : Bool := Bool.xor x.1 x.2.1
17 def calibrated (x : Sensor) : Bool × Bool := (display x, x.2.1)
18 def flip (_ : Unit) (x : Sensor) : Sensor := (!x.1, x.2.1, x.2.2)
19 def displayStep (_ : Unit) (y : Bool) : Bool := !y
20 
21 theorem sensor_local_transport (a : Unit) (x : Sensor) :
22     display (flip a x) = displayStep a (display x) := by
23   rcases x with ⟨b, s, n⟩
24   cases b <;> cases s <;> rfl
25 
26 /-- The display is reusable for arbitrarily many flips despite unidentified physical state. -/
27 theorem sensor_all_words (word : List Unit) (x : Sensor) :
28     display (run flip word x) = run displayStep word (display x) := by
29   simpa using forward_transport flip displayStep display id sensor_local_transport word x
30 
31 theorem no_physical_decoder_from_display :
32     ¬ ∃ d : Attained display → Bool, ∀ x, d (record display x) = physical x := by
33   exact no_decoder_of_collision (false, false, false) (true, true, false) rfl (by decide)
34 
35 theorem calibrated_recovers_physical (x : Sensor) :
36     Bool.xor (calibrated x).1 (calibrated x).2 = physical x := by
37   rcases x with ⟨b, s, n⟩
38   cases b <;> cases s <;> rfl
39 
40 theorem calibrated_decoder_exists :
41     ∃ d : Attained calibrated → Bool, ∀ x, d (record calibrated x) = physical x := by
42   exact ⟨fun h => Bool.xor h.val.1 h.val.2, calibrated_recovers_physical⟩
43 
44 /-- The order convention is executable: successor then doubling differs from the reverse. -/
45 def noncommuting (a : Bool) (n : Nat) : Nat := if a then 2 * n else n + 1
46 
47 theorem action_order_matters :
48     run noncommuting [false, true] 1 = 4 ∧ run noncommuting [true, false] 1 = 3 := by
49   decide
50 
51 /-- Exact version of Core counterexample 2.2. -/
52 def compress (x : ℚ × ℚ) : ℚ := x.1
53 def reconstruct (z : ℚ) : ℚ × ℚ := (z, 0)
54 def swap (x : ℚ × ℚ) : ℚ × ℚ := (x.2, x.1)
55 
56 theorem hidden_return_counterexample :
57     compress (swap (reconstruct 1)) = 0 ∧
58     compress (swap (swap (reconstruct 1))) = 1 ∧
59     compress (swap (reconstruct (compress (swap (reconstruct 1))))) = 0 := by
60   norm_num [compress, reconstruct, swap]
61 
62 /-- Local agreement at zero is not enough when an action leaves that domain. -/
63 def partialRead (n : Nat) : Nat := if n ≤ 1 then 0 else 1
64 
65 theorem invariant_domain_is_necessary :
66     partialRead (Nat.succ 0) = 0 ∧ partialRead (Nat.succ (Nat.succ 0)) ≠ 0 := by
67   decide
68 
69 def candidatesV : Set Sensor := {x | x.1 = x.2.1}
70 def candidatesW : Set Sensor := {x | x.1 ≠ x.2.1}
71 def conventionZero : Set Sensor := {x | x.2.1 = false}
72 
73 theorem same_present_target : physical '' candidatesV = physical '' candidatesW := by
74   ext b
75   have hv : b ∈ physical '' candidatesV := ⟨(b, b, false), rfl, rfl⟩
76   have hw : b ∈ physical '' candidatesW := by
77     refine ⟨(b, !b, false), ?_, rfl⟩
78     change b ≠ !b
79     cases b <;> decide
80   exact ⟨fun _ => hw, fun _ => hv⟩
81 
82 theorem corrected_target_V : physical '' (candidatesV ∩ conventionZero) = {false} := by
83   ext b
84   constructor
85   · rintro ⟨⟨b', s, n⟩, ⟨hv, he⟩, hb⟩
86     change b' = s at hv
87     change s = false at he
88     change b' = b at hb
89     exact hb.symm.trans (hv.trans he)
90   · intro hb
91     have hb' : b = false := hb
92     subst b
93     exact ⟨(false, false, false), ⟨rfl, rfl⟩, rfl⟩
94 
95 theorem corrected_target_W : physical '' (candidatesW ∩ conventionZero) = {true} := by
96   ext b
97   constructor
98   · rintro ⟨⟨b', s, n⟩, ⟨hw, he⟩, hb⟩
99     change b' ≠ s at hw
100     change s = false at he
101     change b' = b at hb
102     subst s
103     subst b
104     cases b' <;> simp_all
105   · intro hb
106     have hb' : b = true := hb
107     subst b
108     exact ⟨(true, false, false), ⟨by change true ≠ false; decide, rfl⟩, rfl⟩
109 
110 /-- Correct target marginals are insufficient memory for a later calibration. -/
111 theorem present_target_does_not_preserve_correction :
112     physical '' candidatesV = physical '' candidatesW ∧
113     physical '' (candidatesV ∩ conventionZero) ≠ physical '' (candidatesW ∩ conventionZero) := by
114   refine ⟨same_present_target, ?_⟩
115   rw [corrected_target_V, corrected_target_W]
116   intro h
117   have : false ∈ ({true} : Set Bool) := h ▸ (by simp : false ∈ ({false} : Set Bool))
118   simp at this
119 
120 /-- Two normalized joint kernels with the same separate marginals. -/
121 def correlated : Unit → Bool → Bool → Bool → ℝ :=
122   fun _ o y _ => if y = o then 1 / 2 else 0
123 
124 def anticorrelated : Unit → Bool → Bool → Bool → ℝ :=
125   fun _ o y _ => if y = !o then 1 / 2 else 0
126 
127 def correlatedLaw : Law Bool Unit Bool where
128   kernel := correlated
129   nonnegative _ o y _ := by unfold correlated; split_ifs <;> norm_num
130   normalized _ _ := by norm_num [correlated, Fintype.sum_bool]
131 
132 def anticorrelatedLaw : Law Bool Unit Bool where
133   kernel := anticorrelated
134   nonnegative _ o y _ := by unfold anticorrelated; split_ifs <;> norm_num
135   normalized _ _ := by norm_num [anticorrelated, Fintype.sum_bool]
136 
137 theorem equal_transition_marginals (y x : Bool) :
138     (∑ o, correlated () o y x) = ∑ o, anticorrelated () o y x := by
139   cases y <;> norm_num [correlated, anticorrelated, Fintype.sum_bool]
140 
141 theorem equal_report_marginals (o x : Bool) :
142     (∑ y, correlated () o y x) = ∑ y, anticorrelated () o y x := by
143   cases o <;> norm_num [correlated, anticorrelated, Fintype.sum_bool]
144 
145 /-- Same transition/report marginals, but opposite positive-report posteriors. -/
146 theorem joint_marginal_counterexample :
147     mass (applyKernel (correlated () true) (basis false)) = 1 / 2 ∧
148     mass (applyKernel (anticorrelated () true) (basis false)) = 1 / 2 ∧
149     normalize (applyKernel (correlated () true) (basis false)) true = 1 ∧
150     normalize (applyKernel (anticorrelated () true) (basis false)) true = 0 := by
151   norm_num [mass, applyKernel, normalize, basis, correlated, anticorrelated, Fintype.sum_bool]
152 
153 theorem no_posterior_for_zero_mass : posterior? (fun _ : Bool => (0 : ℝ)) = none := by
154   simp [posterior?, mass]
155 
156 /-- Within one instrument, a hidden bit changes the report/successor association. -/
157 abbrev PairState := Bool × Bool
158 
159 def mixedKernel : Unit → Bool → PairState → PairState → ℝ :=
160   fun _ o y x => if y.2 = false ∧ y.1 = Bool.xor o x.2 then 1 / 2 else 0
161 
162 def mixedLaw : Law PairState Unit Bool where
163   kernel := mixedKernel
164   nonnegative _ o y x := by unfold mixedKernel; split_ifs <;> norm_num
165   normalized _ x := by
166     rcases x with ⟨v, h⟩
167     cases h <;> norm_num [mixedKernel, Fintype.sum_prod_type, Fintype.sum_bool]
168 
169 def visible (x : PairState) : Bool := x.1
170 
171 theorem visible_surjective : Function.Surjective visible := fun b => ⟨(b, false), rfl⟩
172 
173 /-- Exact obstruction to a quotient despite separately correct marginals. -/
174 theorem mixed_fiber_failure : ¬ FiberCriterion visible mixedLaw.kernel := by
175   intro h
176   have he := h () true true (false, false) (false, true) rfl
177   norm_num [mixedLaw, mixedKernel, visible, Fintype.sum_prod_type, Fintype.sum_bool] at he
178 
179 theorem no_joint_quotient_for_lost_association :
180     ¬ ∃ L : Law Bool Unit Bool,
181       ∀ a o, Intertwines visible (mixedLaw.kernel a o) (L.kernel a o) := by
182   intro h
183   exact mixed_fiber_failure ((quotient_exists_iff visible visible_surjective mixedLaw).mp h)
184 
185 /-- A nontrivial many-to-one positive example: hidden input does not affect the instrument. -/
186 def insensitiveKernel : Unit → Bool → PairState → PairState → ℝ :=
187   fun _ o y x => if y.2 = x.2 ∧ y.1 = !x.1 ∧ o = y.1 then 1 else 0
188 
189 def insensitiveLaw : Law PairState Unit Bool where
190   kernel := insensitiveKernel
191   nonnegative _ o y x := by unfold insensitiveKernel; split_ifs <;> norm_num
192   normalized _ x := by
193     rcases x with ⟨v, h⟩
194     cases v <;> cases h <;>
195       norm_num [insensitiveKernel, Fintype.sum_prod_type, Fintype.sum_bool] <;> decide
196 
197 theorem insensitive_fiber_closed : FiberCriterion visible insensitiveLaw.kernel := by
198   intro a o z x y h
199   rcases x with ⟨v, n⟩
200   rcases y with ⟨v', n'⟩
201   change v = v' at h
202   subst v'
203   cases v <;> cases n <;> cases n' <;> cases z <;> cases o <;>
204     norm_num [insensitiveLaw, insensitiveKernel, visible,
205       Fintype.sum_prod_type, Fintype.sum_bool] <;> decide
206 
207 /-- Its hidden coordinate is discarded without imposing a horizon on feedback. -/
208 theorem insensitive_feedback (g : Policy Unit Bool) (p : PairState → ℝ)
209     (events : History Unit Bool) :
210     let L := coarseLaw visible visible_surjective insensitiveLaw
211     mass (evolve insensitiveLaw.kernel g.probability [] events p) =
212       mass (evolve L.kernel g.probability [] events (push visible p)) ∧
213     Option.map (push visible) (posterior? (evolve insensitiveLaw.kernel g.probability [] events p)) =
214       posterior? (evolve L.kernel g.probability [] events (push visible p)) :=
215   quotient_feedback_law visible visible_surjective insensitiveLaw insensitive_fiber_closed g p events
216 
217 end
218 end Komorebi.MachineTheory.Examples

Back to source controls