Recipient.lean

1 import MachineTheory.Behavior
2 import Mathlib.Data.Finset.Card
3 import Mathlib.Data.Fintype.Powerset
4 import Mathlib.Data.Nat.Find
5 
6 /-!
7 # Fixed-recipient artifact covering
8 
9 Core 4.2. The sender is a function on attained records, never on the hidden case.
10 `ok` is the fixed joint acceptance predicate of all recipients, including their
11 actual outputs, permission and resource conditions. No decoder is redesigned by
12 the covering construction. Codebook cardinality is not byte length or execution cost.
13 -/
14 namespace Komorebi.MachineTheory.Recipient
15 
16 universe u v w
17 variable {X : Type u} {H : Type v} {C : Type w}
18 
19 /-- Artifacts acceptable in every case compatible with this attained record. -/
20 def Common (α : X → H) (ok : X → C → Prop) (h : Attained α) (c : C) : Prop :=
21   ∀ x, α x = h.val → ok x c
22 
23 /-- The encoder reads the sender record only. -/
24 def Valid (α : X → H) (ok : X → C → Prop) (f : Attained α → C) : Prop :=
25   ∀ x, ok x (f (record α x))
26 
27 theorem valid_iff_common (α : X → H) (ok : X → C → Prop) (f : Attained α → C) :
28     Valid α ok f ↔ ∀ h, Common α ok h (f h) := by
29   constructor
30   · intro hf h x hx
31     have he : record α x = h := Subtype.ext hx
32     simpa only [he] using hf x
33   · intro hf x
34     exact hf (record α x) x rfl
35 
36 /-- Core 4.2, existence: only attainable sender records have obligations. -/
37 theorem encoder_exists_iff (α : X → H) (ok : X → C → Prop) :
38     (∃ f : Attained α → C, Valid α ok f) ↔ ∀ h, ∃ c, Common α ok h c := by
39   constructor
40   · rintro ⟨f, hf⟩ h
41     exact ⟨f h, (valid_iff_common α ok f).mp hf h⟩
42   · intro h
43     classical
44     exact ⟨fun z => Classical.choose (h z),
45       (valid_iff_common α ok _).mpr (fun z => Classical.choose_spec (h z))⟩
46 
47 /-- A collision whose acceptance sets are disjoint rules out every encoder. -/
48 theorem no_encoder_of_disjoint (α : X → H) (ok : X → C → Prop)
49     (x y : X) (he : α x = α y) (hd : ∀ c, ¬ (ok x c ∧ ok y c)) :
50     ¬ ∃ f : Attained α → C, Valid α ok f := by
51   rintro ⟨f, hf⟩
52   have hr : record α x = record α y := Subtype.ext he
53   exact hd (f (record α x)) ⟨hf x, by simpa only [hr] using hf y⟩
54 
55 /-- A finite codebook meets every required acceptance intersection. -/
56 def Hits (α : X → H) (ok : X → C → Prop) (S : Finset C) : Prop :=
57   ∀ h, ∃ c, c ∈ S ∧ Common α ok h c
58 
59 /-- Exactly the distinct artifacts transmitted on attained inputs. -/
60 noncomputable def image [Fintype X] (α : X → H) (f : Attained α → C) : Finset C := by
61   classical
62   exact Finset.univ.image f
63 
64 @[simp] theorem mem_image [Fintype X] (α : X → H) (f : Attained α → C) (c : C) :
65     c ∈ image α f ↔ ∃ h, f h = c := by
66   classical
67   simp [image]
68 
69 theorem image_hits [Fintype X] (α : X → H) (ok : X → C → Prop)
70     (f : Attained α → C) (hf : Valid α ok f) : Hits α ok (image α f) := by
71   intro h
72   exact ⟨f h, (mem_image α f _).mpr ⟨h, rfl⟩, (valid_iff_common α ok f).mp hf h⟩
73 
74 /-- Every hitting codebook supplies a valid encoder using only its entries. -/
75 theorem encoder_within_iff [Fintype X] (α : X → H) (ok : X → C → Prop) (S : Finset C) :
76     (∃ f : Attained α → C, Valid α ok f ∧ image α f ⊆ S) ↔ Hits α ok S := by
77   constructor
78   · rintro ⟨f, hf, hs⟩ h
79     exact ⟨f h, hs ((mem_image α f _).mpr ⟨h, rfl⟩),
80       (valid_iff_common α ok f).mp hf h⟩
81   · intro hs
82     classical
83     let f : Attained α → C := fun h => Classical.choose (hs h)
84     have spec : ∀ h, f h ∈ S ∧ Common α ok h (f h) :=
85       fun h => Classical.choose_spec (hs h)
86     refine ⟨f, (valid_iff_common α ok f).mpr (fun h => (spec h).2), ?_⟩
87     intro c hc
88     obtain ⟨h, rfl⟩ := (mem_image α f c).mp hc
89     exact (spec h).1
90 
91 /-- Exact bounded image/cover equivalence, including infeasible and empty cases. -/
92 theorem cardinality_budget_iff [Fintype X] (α : X → H) (ok : X → C → Prop) (k : ℕ) :
93     (∃ f : Attained α → C, Valid α ok f ∧ (image α f).card ≤ k) ↔
94       ∃ S : Finset C, Hits α ok S ∧ S.card ≤ k := by
95   constructor
96   · rintro ⟨f, hf, hk⟩
97     exact ⟨image α f, image_hits α ok f hf, hk⟩
98   · rintro ⟨S, hs, hk⟩
99     obtain ⟨f, hf, hsub⟩ := (encoder_within_iff α ok S).mpr hs
100     exact ⟨f, hf, (Finset.card_le_card hsub).trans hk⟩
101 
102 def Feasible (α : X → H) (ok : X → C → Prop) : Prop :=
103   ∃ f : Attained α → C, Valid α ok f
104 
105 theorem image_size_exists [Fintype X] {α : X → H} {ok : X → C → Prop}
106     (h : Feasible α ok) : ∃ n : ℕ, ∃ f : Attained α → C,
107       Valid α ok f ∧ (image α f).card = n := by
108   obtain ⟨f, hf⟩ := h
109   exact ⟨_, f, hf, rfl⟩
110 
111 theorem cover_size_exists [Fintype X] {α : X → H} {ok : X → C → Prop}
112     (h : Feasible α ok) : ∃ n : ℕ, ∃ S : Finset C, Hits α ok S ∧ S.card = n := by
113   obtain ⟨f, hf⟩ := h
114   exact ⟨_, image α f, image_hits α ok f hf, rfl⟩
115 
116 noncomputable def minImageSize [Fintype X] {α : X → H} {ok : X → C → Prop}
117     (h : Feasible α ok) : ℕ := by
118   classical
119   exact Nat.find (image_size_exists h)
120 
121 noncomputable def minCoverSize [Fintype X] {α : X → H} {ok : X → C → Prop}
122     (h : Feasible α ok) : ℕ := by
123   classical
124   exact Nat.find (cover_size_exists h)
125 
126 theorem minImage_attained [Fintype X] {α : X → H} {ok : X → C → Prop}
127     (h : Feasible α ok) : ∃ f : Attained α → C,
128       Valid α ok f ∧ (image α f).card = minImageSize h := by
129   classical
130   exact Nat.find_spec (image_size_exists h)
131 
132 theorem minCover_attained [Fintype X] {α : X → H} {ok : X → C → Prop}
133     (h : Feasible α ok) : ∃ S : Finset C, Hits α ok S ∧ S.card = minCoverSize h := by
134   classical
135   exact Nat.find_spec (cover_size_exists h)
136 
137 theorem minImage_le [Fintype X] {α : X → H} {ok : X → C → Prop}
138     (h : Feasible α ok) (f : Attained α → C) (hf : Valid α ok f) :
139     minImageSize h ≤ (image α f).card := by
140   classical
141   exact Nat.find_min' (image_size_exists h) ⟨f, hf, rfl⟩
142 
143 theorem minCover_le [Fintype X] {α : X → H} {ok : X → C → Prop}
144     (h : Feasible α ok) (S : Finset C) (hs : Hits α ok S) :
145     minCoverSize h ≤ S.card := by
146   classical
147   exact Nat.find_min' (cover_size_exists h) ⟨S, hs, rfl⟩
148 
149 /-- Core 4.2, the independently defined minima are equal and are both attained. -/
150 theorem minimum_image_eq_cover [Fintype X] {α : X → H} {ok : X → C → Prop}
151     (h : Feasible α ok) : minImageSize h = minCoverSize h := by
152   apply le_antisymm
153   · obtain ⟨S, hs, he⟩ := minCover_attained h
154     obtain ⟨f, hf, hsub⟩ := (encoder_within_iff α ok S).mpr hs
155     exact (minImage_le h f hf).trans ((Finset.card_le_card hsub).trans_eq he)
156   · obtain ⟨f, hf, he⟩ := minImage_attained h
157     exact (minCover_le h _ (image_hits α ok f hf)).trans_eq he
158 
159 /-- A minimum codebook is exactly the image of a valid minimizing encoder. -/
160 theorem minimum_common_artifact [Fintype X] {α : X → H} {ok : X → C → Prop}
161     (h : Feasible α ok) :
162     ∃ f : Attained α → C, ∃ S : Finset C,
163       Valid α ok f ∧ Hits α ok S ∧ image α f = S ∧
164       S.card = minCoverSize h ∧
165       (∀ g : Attained α → C, Valid α ok g → S.card ≤ (image α g).card) ∧
166       (∀ T : Finset C, Hits α ok T → S.card ≤ T.card) := by
167   obtain ⟨f, hf, he⟩ := minImage_attained h
168   refine ⟨f, image α f, hf, image_hits α ok f hf, rfl, ?_, ?_, ?_⟩
169   · exact he.trans (minimum_image_eq_cover h)
170   · intro g hg
171     rw [he]
172     exact minImage_le h g hg
173   · intro T hT
174     rw [he, minimum_image_eq_cover h]
175     exact minCover_le h T hT
176 
177 /-- More actual sender information cannot increase the minimum image size. -/
178 theorem access_refinement [Fintype X] {H' : Type*} (α : X → H) (β : X → H')
179     (forget : H' → H) (haccess : ∀ x, forget (β x) = α x) (ok : X → C → Prop)
180     (f : Attained α → C) (hf : Valid α ok f) :
181     ∃ g : Attained β → C, Valid β ok g ∧ image β g = image α f := by
182   let down : Attained β → Attained α := fun h =>
183     ⟨forget h.val, by obtain ⟨x, hx⟩ := h.property; exact ⟨x, by rw [← hx, haccess]⟩⟩
184   have down_record : ∀ x, down (record β x) = record α x :=
185     fun x => Subtype.ext (haccess x)
186   refine ⟨fun h => f (down h), ?_, ?_⟩
187   · intro x
188     simpa only [down_record] using hf x
189   · ext c
190     simp only [mem_image]
191     constructor
192     · rintro ⟨h, hc⟩
193       exact ⟨down h, hc⟩
194     · rintro ⟨h, hc⟩
195       obtain ⟨x, hx⟩ := h.property
196       refine ⟨record β x, ?_⟩
197       rw [down_record, show record α x = h from Subtype.ext hx]
198       exact hc
199 
200 /-- A transmitted alphabet is useful only through its fixed installed decoder. -/
201 theorem decoded_alphabet_bound [Fintype X] {Msg : Type*} [Fintype Msg]
202     {α : X → H} {ok : X → C → Prop} (h : Feasible α ok)
203     (send : Attained α → Msg) (decode : Msg → C)
204     (hv : Valid α ok (decode ∘ send)) : minCoverSize h ≤ Fintype.card Msg := by
205   classical
206   rw [← minimum_image_eq_cover h]
207   apply (minImage_le h _ hv).trans
208   have hsub : image α (decode ∘ send) ⊆ Finset.univ.image decode := by
209     intro c hc
210     obtain ⟨z, rfl⟩ := (mem_image α (decode ∘ send) c).mp hc
211     exact Finset.mem_image.mpr ⟨send z, Finset.mem_univ _, rfl⟩
212   exact (Finset.card_le_card hsub).trans (by simpa using Finset.card_image_le (s := Finset.univ) (f := decode))
213 
214 /-- If a unique artifact is needed in each case, every valid encoder has that image. -/
215 theorem forced_image [Fintype X] [DecidableEq C] (α : X → H) (target : X → C)
216     (f : Attained α → C) (hf : Valid α (fun x c => c = target x) f) :
217     image α f = Finset.univ.image target := by
218   classical
219   ext c
220   rw [mem_image]
221   simp only [Finset.mem_image, Finset.mem_univ, true_and]
222   constructor
223   · rintro ⟨h, hc⟩
224     obtain ⟨x, hx⟩ := h.property
225     refine ⟨x, ?_⟩
226     have hr : record α x = h := Subtype.ext hx
227     exact (hf x).symm.trans (by simpa only [hr] using hc)
228   · rintro ⟨x, hx⟩
229     exact ⟨record α x, (hf x).trans hx⟩
230 
231 end Komorebi.MachineTheory.Recipient

Back to source controls