RecipientExamples.lean

1 import MachineTheory.RecipientExecution
2 import Mathlib.Data.Fintype.Prod
3 
4 /-! Exact fixed-interpreter examples for Core 4.2, with no host execution or learned-decoder claim. -/
5 namespace Komorebi.MachineTheory.RecipientExamples
6 open Recipient RecipientExecution
7 
8 abbrev Sensor := Bool × Bool × Bool
9 
10 def display (x : Sensor) : Bool := xor x.1 x.2.1
11 
12 /-- Recipient false knows the convention; recipient true knows the target bit. -/
13 def xorAudience : Audience Sensor Bool Bool (fun _ => Bool) (fun _ => Bool) where
14   background i x := if i then x.1 else x.2.1
15   target i x := if i then x.2.1 else x.1
16   run _ b c := .completed ⟨xor c b, 1, 1⟩
17   permitted _ _ _ := True
18   workLimit _ _ := 1
19   spaceLimit _ _ := 1
20 
21 theorem xor_accepts_iff (x : Sensor) (c : Bool) :
22     xorAudience.Accepts x c ↔ c = display x := by
23   rcases x with ⟨b, s, n⟩
24   cases b <;> cases s <;> cases n <;> cases c <;>
25     simp [Audience.Accepts, xorAudience, display]
26 
27 theorem xor_sender_valid : Valid display xorAudience.Accepts (fun h => h.val) := by
28   intro x
29   exact (xor_accepts_iff x _).mpr rfl
30 
31 theorem xor_feasible : Feasible display xorAudience.Accepts :=
32   ⟨fun h => h.val, xor_sender_valid⟩
33 
34 theorem xor_sender_does_not_know_target :
35     ¬ ∃ d : Attained display → Bool, ∀ x : Sensor, d (record display x) = x.1 := by
36   exact no_decoder_of_collision (r := display) (t := fun x : Sensor => x.1)
37     (false, false, false) (true, true, false) rfl (by decide)
38 
39 theorem xor_image_for_every_valid_sender (f : Attained display → Bool)
40     (hf : Valid display xorAudience.Accepts f) : image display f = Finset.univ := by
41   have hforced : Valid display (fun x c => c = display x) f :=
42     fun x => (xor_accepts_iff x _).mp (hf x)
43   rw [forced_image display display f hforced]
44   decide
45 
46 theorem xor_minimum_codebook : minCoverSize xor_feasible = 2 := by
47   rw [← minimum_image_eq_cover xor_feasible]
48   obtain ⟨f, hf, he⟩ := minImage_attained xor_feasible
49   rw [← he, xor_image_for_every_valid_sender f hf]
50   decide
51 
52 theorem xor_one_artifact_impossible :
53     ¬ ∃ f : Attained display → Bool,
54       Valid display xorAudience.Accepts f ∧ (image display f).card ≤ 1 := by
55   rintro ⟨f, hf, hc⟩
56   have h := minCover_le xor_feasible _ (image_hits display xorAudience.Accepts f hf)
57   rw [xor_minimum_codebook] at h
58   omega
59 
60 /-- Return the background while ignoring the transmitted artifact. -/
61 def ignoresMessage : Audience Sensor Bool Bool (fun _ => Bool) (fun _ => Bool) :=
62   { xorAudience with run := fun _ b _ => .completed ⟨b, 1, 1⟩ }
63 
64 theorem ignored_message_fails (c : Bool) :
65     ¬ ignoresMessage.Accepts (true, false, false) c := by
66   cases c <;> simp [Audience.Accepts, ignoresMessage, xorAudience]
67 
68 theorem fixed_ignoring_decoder_has_no_encoder : ¬ Feasible display ignoresMessage.Accepts := by
69   rintro ⟨f, hf⟩
70   exact ignored_message_fails _ (hf (true, false, false))
71 
72 /-- Correct output with a two-unit run cannot use the unchanged one-unit contract. -/
73 def tooSlow : Audience Sensor Bool Bool (fun _ => Bool) (fun _ => Bool) :=
74   { xorAudience with run := fun _ b c => .completed ⟨xor c b, 2, 1⟩ }
75 
76 theorem correct_output_still_over_budget (x : Sensor) (c : Bool) : ¬ tooSlow.Accepts x c := by
77   apply tooSlow.no_work_overrun false ⟨xor c x.2.1, 2, 1⟩ rfl
78   change 1 < 2
79   decide
80 
81 def tooLarge : Audience Sensor Bool Bool (fun _ => Bool) (fun _ => Bool) :=
82   { xorAudience with run := fun _ b c => .completed ⟨xor c b, 1, 2⟩ }
83 
84 theorem correct_output_still_over_space (x : Sensor) (c : Bool) : ¬ tooLarge.Accepts x c := by
85   apply tooLarge.no_space_overrun false ⟨xor c x.2.1, 1, 2⟩ rfl
86   change 1 < 2
87   decide
88 
89 def timedOut : Audience Sensor Bool Bool (fun _ => Bool) (fun _ => Bool) :=
90   { xorAudience with run := fun _ _ _ => .timeout }
91 
92 theorem timeout_is_not_success (x : Sensor) (c : Bool) : ¬ timedOut.Accepts x c :=
93   timedOut.no_timeout false rfl
94 
95 def malformed : Audience Sensor Bool Bool (fun _ => Bool) (fun _ => Bool) :=
96   { xorAudience with run := fun _ _ _ => .malformed }
97 
98 theorem malformed_is_not_success (x : Sensor) (c : Bool) : ¬ malformed.Accepts x c :=
99   malformed.no_malformed false rfl
100 
101 def forbidden : Audience Sensor Bool Bool (fun _ => Bool) (fun _ => Bool) :=
102   { xorAudience with permitted := fun _ _ _ => False }
103 
104 theorem correct_output_still_forbidden (x : Sensor) (c : Bool) : ¬ forbidden.Accepts x c :=
105   forbidden.no_permission false id
106 
107 /-- Manuscript Counterexample 4.3: each case is soluble, but not from this record. -/
108 def blindRecord (_ : Bool) : Unit := ()
109 
110 theorem individual_cases_have_artifacts : ∀ x : Bool, ∃ c : Bool, c = x :=
111   fun x => ⟨x, rfl⟩
112 
113 theorem individually_possible_not_common :
114     ¬ Feasible blindRecord (fun x c : Bool => c = x) := by
115   apply no_encoder_of_disjoint blindRecord (fun x c : Bool => c = x) false true rfl
116   intro c h
117   have he : false = true := h.1.symm.trans h.2
118   cases he
119 
120 /-- A separate artifact for each recipient does not supply one common artifact. -/
121 theorem separate_recipient_artifacts_exist : ∀ i : Bool, ∃ c : Bool, c = i :=
122   fun i => ⟨i, rfl⟩
123 
124 theorem no_one_artifact_for_opposed_recipients : ¬ ∃ c : Bool, ∀ i : Bool, c = i := by
125   rintro ⟨c, hc⟩
126   have he : false = true := (hc false).symm.trans (hc true)
127   cases he
128 
129 /-- Recipient false reads the first component, recipient true the second. -/
130 def pairAudience : Audience (Bool × Bool) (Bool × Bool) Bool (fun _ => Unit) (fun _ => Bool) where
131   background _ _ := ()
132   target i x := if i then x.2 else x.1
133   run i _ c := .completed ⟨if i then c.2 else c.1, 1, 1⟩
134   permitted _ _ _ := True
135   workLimit _ _ := 1
136   spaceLimit _ _ := 1
137 
138 theorem pair_accepts_iff (x c : Bool × Bool) : pairAudience.Accepts x c ↔ c = x := by
139   rcases x with ⟨x₀, x₁⟩
140   rcases c with ⟨c₀, c₁⟩
141   cases x₀ <;> cases x₁ <;> cases c₀ <;> cases c₁ <;>
142     simp [Audience.Accepts, pairAudience, Bool.forall_bool]
143 
144 def pairRecord (x : Bool × Bool) : Bool × Bool := x
145 
146 theorem pair_feasible : Feasible pairRecord pairAudience.Accepts := by
147   refine ⟨fun h => h.val, ?_⟩
148   intro x
149   exact (pair_accepts_iff x x).mpr rfl
150 
151 theorem pair_minimum_codebook : minCoverSize pair_feasible = 4 := by
152   rw [← minimum_image_eq_cover pair_feasible]
153   obtain ⟨f, hf, he⟩ := minImage_attained pair_feasible
154   have hforced : Valid pairRecord (fun x c => c = x) f :=
155     fun x => (pair_accepts_iff x _).mp (hf x)
156   rw [← he, forced_image pairRecord id f hforced]
157   decide
158 
159 theorem pair_single_binary_message_impossible (send : Attained pairRecord → Bool)
160     (decode : Bool → Bool × Bool) :
161     ¬ Valid pairRecord pairAudience.Accepts (decode ∘ send) := by
162   intro hv
163   have h := decoded_alphabet_bound pair_feasible send decode hv
164   rw [pair_minimum_codebook] at h
165   have hc : Fintype.card Bool = 2 := rfl
166   omega
167 
168 /-- Each projection can separately be explained with one binary symbol. -/
169 theorem individual_projection_codes (x : Bool × Bool) :
170     ((x.1, false) : Bool × Bool).1 = x.1 ∧
171     ((false, x.2) : Bool × Bool).2 = x.2 := ⟨rfl, rfl⟩
172 
173 /-- No impossible input needs a default artifact: both source and artifact types can be empty. -/
174 def emptyRecord (x : Empty) : Bool := nomatch x
175 
176 theorem empty_problem_feasible : Feasible emptyRecord (fun (_ : Empty) (_ : Empty) => False) := by
177   apply (encoder_exists_iff _ _).mpr
178   intro h
179   obtain ⟨x, _⟩ := h.property
180   cases x
181 
182 theorem empty_codebook_hits : Hits emptyRecord (fun (_ : Empty) (_ : Empty) => False) ∅ := by
183   intro h
184   obtain ⟨x, _⟩ := h.property
185   cases x
186 
187 theorem empty_minimum_zero : minCoverSize empty_problem_feasible = 0 := by
188   have h := minCover_le empty_problem_feasible ∅ empty_codebook_hits
189   simpa using Nat.eq_zero_of_le_zero h
190 
191 theorem requiring_a_total_decoder_would_fail : ¬ Nonempty (Bool → Empty) := by
192   rintro ⟨f⟩
193   exact Empty.elim (f false)
194 
195 /-- Three different sender records, with overlapping two-element acceptance sets. -/
196 def tripleRecord (x : Fin 3) : Fin 3 := x
197 
198 theorem triple_pairwise_intersections :
199     ∀ x y : Fin 3, ∃ c : Fin 3, c ≠ x ∧ c ≠ y := by decide
200 
201 theorem triple_no_global_intersection : ¬ ∃ c : Fin 3, ∀ x : Fin 3, c ≠ x := by
202   rintro ⟨c, hc⟩
203   exact hc c rfl
204 
205 theorem triple_two_codebook_hits :
206     Hits tripleRecord (fun x c : Fin 3 => c ≠ x) {0, 1} := by
207   intro h
208   by_cases hh : h.val = 0
209   · refine ⟨1, by simp, ?_⟩
210     intro x hx
211     have he : x = 0 := hx.trans hh
212     rw [he]
213     decide
214   · refine ⟨0, by simp, ?_⟩
215     intro x hx hzero
216     exact hh (hx.symm.trans hzero.symm)
217 
218 theorem triple_feasible : Feasible tripleRecord (fun x c : Fin 3 => c ≠ x) := by
219   obtain ⟨f, hf, _⟩ := (encoder_within_iff tripleRecord _ {0, 1}).mpr triple_two_codebook_hits
220   exact ⟨f, hf⟩
221 
222 theorem triple_hitting_needs_two (S : Finset (Fin 3))
223     (hs : Hits tripleRecord (fun x c : Fin 3 => c ≠ x) S) : 2 ≤ S.card := by
224   by_contra hn
225   have hsmall : S.card ≤ 1 := by omega
226   have hsub := Finset.card_le_one.mp hsmall
227   obtain ⟨c, hc, _⟩ := hs (record tripleRecord 0)
228   obtain ⟨d, hd, hdc⟩ := hs (record tripleRecord c)
229   exact hdc c rfl (hsub d hd c hc)
230 
231 theorem triple_minimum_codebook : minCoverSize triple_feasible = 2 := by
232   apply le_antisymm
233   · have h := minCover_le triple_feasible {0, 1} triple_two_codebook_hits
234     exact h.trans_eq (by decide)
235   · obtain ⟨S, hs, he⟩ := minCover_attained triple_feasible
236     exact (triple_hitting_needs_two S hs).trans_eq he
237 
238 /-- Pairwise-compatible cases still need a joint intersection when the sender is blind. -/
239 theorem triple_blind_sender_impossible :
240     ¬ Feasible (fun _ : Fin 3 => ()) (fun x c : Fin 3 => c ≠ x) := by
241   rintro ⟨f, hf⟩
242   let c := f (record (fun _ : Fin 3 => ()) 0)
243   have he : record (fun _ : Fin 3 => ()) c = record (fun _ : Fin 3 => ()) 0 :=
244     Subtype.ext rfl
245   have h := hf c
246   rw [he] at h
247   exact h rfl
248 
249 end Komorebi.MachineTheory.RecipientExamples

Back to source controls