LegalQuotient.lean

1 import Mathlib.Data.Fintype.Basic
2 import Mathlib.Data.Set.Basic
3 
4 /-! # Quotients preserving labels and legal operations
5 
6 Core 8.2. `none` means disabled, while `some y` records the unique legal successor.
7 Thus there are no unspecified successors on disabled actions. `ofEnabled` embeds
8 the manuscript's separately supplied enabled sets and dependent legal successors
9 into this canonical partial representation without changing them.
10 
11 The quotient below is constructed by choosing an actual representative of each
12 fibre. Compatibility is the three explicit local conditions on the input system,
13 not the prior existence of a quotient. No nonempty state space is assumed.
14 These are conditions on encoded institutional permissions, not a derivation of
15 external moral or legal authority.
16 -/
17 namespace Komorebi.MachineTheory.LegalQuotient
18 
19 universe u v w l
20 
21 /-- A deterministic partial operational system with protected labels. -/
22 @[ext] structure System (X : Type u) (Action : Type v) (Label : Type l) where
23   label : X → Label
24   step : X → Action → Option X
25 
26 variable {X : Type u} {Z : Type w} {Action : Type v} {Label : Type l}
27 
28 /-- Exactly the actions for which the system supplies a legal successor. -/
29 def enabled (M : System X Action Label) (x : X) : Set Action :=
30   {a | (M.step x a).isSome}
31 
32 /-- Enabled actions and existing legal successors are the same domain. -/
33 theorem mem_enabled_iff (M : System X Action Label) (x : X) (a : Action) :
34     a ∈ enabled M x ↔ ∃ y, M.step x a = some y := by
35   cases hs : M.step x a <;> simp [enabled, hs]
36 
37 /-- A disabled action has no successor in the partial system. -/
38 theorem not_enabled_iff (M : System X Action Label) (x : X) (a : Action) :
39     a ∉ enabled M x ↔ M.step x a = none := by
40   cases hs : M.step x a <;> simp [enabled, hs]
41 
42 /-- The source's given enabled sets and legal-only successor function. -/
43 noncomputable def ofEnabled (label : X → Label) (D : X → Set Action)
44     (F : ∀ x a, a ∈ D x → X) : System X Action Label := by
45   classical
46   exact ⟨label, fun x a => if h : a ∈ D x then some (F x a h) else none⟩
47 
48 @[simp] theorem ofEnabled_label (label : X → Label) (D : X → Set Action)
49     (F : ∀ x a, a ∈ D x → X) (x : X) : (ofEnabled label D F).label x = label x := rfl
50 
51 /-- Translation preserves every supplied legal successor. -/
52 theorem ofEnabled_step_of_mem (label : X → Label) (D : X → Set Action)
53     (F : ∀ x a, a ∈ D x → X) (x : X) (a : Action) (ha : a ∈ D x) :
54     (ofEnabled label D F).step x a = some (F x a ha) := by
55   simp [ofEnabled, ha]
56 
57 /-- Translation invents no successor for a disabled action. -/
58 theorem ofEnabled_step_of_not_mem (label : X → Label) (D : X → Set Action)
59     (F : ∀ x a, a ∈ D x → X) (x : X) (a : Action) (ha : a ∉ D x) :
60     (ofEnabled label D F).step x a = none := by
61   simp [ofEnabled, ha]
62 
63 /-- The encoded permission set is literally the source's supplied set. -/
64 @[simp] theorem enabled_ofEnabled (label : X → Label) (D : X → Set Action)
65     (F : ∀ x a, a ∈ D x → X) (x : X) : enabled (ofEnabled label D F) x = D x := by
66   classical
67   ext a
68   by_cases ha : a ∈ D x <;> simp [enabled, ofEnabled, ha]
69 
70 /-- Recover the typed legal successor without assigning disabled-action values. -/
71 noncomputable def legalSuccessor (M : System X Action Label) (x : X) (a : Action)
72     (ha : a ∈ enabled M x) : X :=
73   Classical.choose ((mem_enabled_iff M x a).mp ha)
74 
75 theorem legalSuccessor_spec (M : System X Action Label) (x : X) (a : Action)
76     (ha : a ∈ enabled M x) : M.step x a = some (legalSuccessor M x a ha) :=
77   Classical.choose_spec ((mem_enabled_iff M x a).mp ha)
78 
79 /-- Translating a partial system to legal-only successors and back changes nothing. -/
80 theorem ofEnabled_reconstruct (M : System X Action Label) :
81     ofEnabled M.label (enabled M) (legalSuccessor M) = M := by
82   apply System.ext
83   · rfl
84   · funext x a
85     by_cases ha : a ∈ enabled M x
86     · exact (ofEnabled_step_of_mem _ _ _ x a ha).trans (legalSuccessor_spec M x a ha).symm
87     · exact (ofEnabled_step_of_not_mem _ _ _ x a ha).trans ((not_enabled_iff M x a).mp ha).symm
88 
89 /-- The source's three separate equations for quotient data. -/
90 structure Factors (M : System X Action Label) (Q : System Z Action Label) (π : X → Z) : Prop where
91   label_eq : ∀ x, M.label x = Q.label (π x)
92   enabled_eq : ∀ x, enabled M x = enabled Q (π x)
93   successor_eq : ∀ x a y, M.step x a = some y → Q.step (π x) a = some (π y)
94 
95 /-- The three actual input conditions on equal fibres, before a quotient is constructed. -/
96 structure FibreCompatible (M : System X Action Label) (π : X → Z) : Prop where
97   label_eq : ∀ x y, π x = π y → M.label x = M.label y
98   enabled_eq : ∀ x y, π x = π y → enabled M x = enabled M y
99   successor_eq : ∀ x y a x' y', π x = π y →
100     M.step x a = some x' → M.step y a = some y' → π x' = π y'
101 
102 /-- Legal-domain equations imply equality of the complete canonical partial steps. -/
103 theorem Factors.step_map {M : System X Action Label} {Q : System Z Action Label} {π : X → Z}
104     (h : Factors M Q π) (x : X) (a : Action) :
105     Q.step (π x) a = (M.step x a).map π := by
106   cases hx : M.step x a with
107   | none =>
108       have hn : a ∉ enabled M x := (not_enabled_iff M x a).mpr hx
109       rw [h.enabled_eq x] at hn
110       simpa [hx] using (not_enabled_iff Q (π x) a).mp hn
111   | some y => simpa [hx] using h.successor_eq x a y hx
112 
113 /-- Pointwise partial-step agreement supplies all three source equations. -/
114 theorem factors_of_label_step (M : System X Action Label) (Q : System Z Action Label) (π : X → Z)
115     (hl : ∀ x, M.label x = Q.label (π x))
116     (hs : ∀ x a, Q.step (π x) a = (M.step x a).map π) : Factors M Q π := by
117   refine ⟨hl, ?_, ?_⟩
118   · intro x
119     ext a
120     simp [enabled, hs]
121   · intro x a y hy
122     rw [hs, hy]
123     rfl
124 
125 /-- The partial representation is equivalent to, rather than weaker than, the source contract. -/
126 theorem factors_iff_label_step (M : System X Action Label) (Q : System Z Action Label) (π : X → Z) :
127     Factors M Q π ↔
128       (∀ x, M.label x = Q.label (π x)) ∧
129       (∀ x a, Q.step (π x) a = (M.step x a).map π) :=
130   ⟨fun h => ⟨h.label_eq, h.step_map⟩, fun h => factors_of_label_step M Q π h.1 h.2⟩
131 
132 /-- Necessity uses the actual quotient equations. It does not need surjectivity. -/
133 theorem compatible_of_factors {M : System X Action Label} {Q : System Z Action Label} {π : X → Z}
134     (h : Factors M Q π) : FibreCompatible M π := by
135   refine ⟨?_, ?_, ?_⟩
136   · intro x y hxy
137     rw [h.label_eq x, h.label_eq y, hxy]
138   · intro x y hxy
139     rw [h.enabled_eq x, h.enabled_eq y, hxy]
140   · intro x y a x' y' hxy hx hy
141     have hxq := h.successor_eq x a x' hx
142     rw [hxy] at hxq
143     exact Option.some.inj (hxq.symm.trans (h.successor_eq y a y' hy))
144 
145 /-- Equal fibres have equal projected partial steps, including equal disabled status. -/
146 theorem FibreCompatible.step_map_eq {M : System X Action Label} {π : X → Z}
147     (h : FibreCompatible M π) (x y : X) (hxy : π x = π y) (a : Action) :
148     (M.step x a).map π = (M.step y a).map π := by
149   cases hx : M.step x a with
150   | none =>
151       have hn : a ∉ enabled M x := (not_enabled_iff M x a).mpr hx
152       rw [h.enabled_eq x y hxy] at hn
153       rw [(not_enabled_iff M y a).mp hn]
154   | some x' =>
155       have he : a ∈ enabled M x := (mem_enabled_iff M x a).mpr ⟨x',hx⟩
156       rw [h.enabled_eq x y hxy] at he
157       obtain ⟨y',hy⟩ := (mem_enabled_iff M y a).mp he
158       rw [hy]
159       exact congrArg some (h.successor_eq x y a x' y' hxy hx hy)
160 
161 /-- An actual representative of every quotient state, supplied only by surjectivity. -/
162 noncomputable def representative (π : X → Z) (hs : Function.Surjective π) (z : Z) : X :=
163   Classical.choose (hs z)
164 
165 theorem representative_spec (π : X → Z) (hs : Function.Surjective π) (z : Z) :
166     π (representative π hs z) = z := Classical.choose_spec (hs z)
167 
168 /-- Explicit candidate quotient data, defined by representative labels and projected steps. -/
169 noncomputable def representativeQuotient (M : System X Action Label) (π : X → Z)
170     (hs : Function.Surjective π) : System Z Action Label where
171   label z := M.label (representative π hs z)
172   step z a := (M.step (representative π hs z) a).map π
173 
174 /-- Compatibility makes the explicit representative construction a true quotient. -/
175 theorem representativeQuotient_factors (M : System X Action Label) (π : X → Z)
176     (hs : Function.Surjective π) (h : FibreCompatible M π) :
177     Factors M (representativeQuotient M π hs) π := by
178   apply factors_of_label_step
179   · intro x
180     exact h.label_eq x _ (representative_spec π hs (π x)).symm
181   · intro x a
182     exact h.step_map_eq _ x (representative_spec π hs (π x)) a
183 
184 /-- Core 8.2 existence criterion, proved by constructing quotient data from representatives. -/
185 theorem exists_quotient_iff (M : System X Action Label) (π : X → Z)
186     (hs : Function.Surjective π) :
187     (∃ Q : System Z Action Label, Factors M Q π) ↔ FibreCompatible M π :=
188   ⟨fun ⟨_,h⟩ => compatible_of_factors h,
189     fun h => ⟨representativeQuotient M π hs, representativeQuotient_factors M π hs h⟩⟩
190 
191 /-- Surjectivity makes the actual partial quotient data unique on its whole domain. -/
192 theorem quotient_unique (M : System X Action Label) (π : X → Z) (hs : Function.Surjective π)
193     (Q R : System Z Action Label) (hQ : Factors M Q π) (hR : Factors M R π) : Q = R := by
194   apply System.ext
195   · funext z
196     obtain ⟨x,rfl⟩ := hs z
197     exact (hQ.label_eq x).symm.trans (hR.label_eq x)
198   · funext z a
199     obtain ⟨x,rfl⟩ := hs z
200     exact (hQ.step_map x a).trans (hR.step_map x a).symm
201 
202 /-- Compatibility is equivalent to existence of exactly one canonical partial quotient. -/
203 theorem existsUnique_quotient_iff (M : System X Action Label) (π : X → Z)
204     (hs : Function.Surjective π) :
205     (∃! Q : System Z Action Label, Factors M Q π) ↔ FibreCompatible M π := by
206   constructor
207   · intro h
208     exact (exists_quotient_iff M π hs).mp h.exists
209   · intro h
210     obtain ⟨Q,hQ⟩ := (exists_quotient_iff M π hs).mpr h
211     exact ⟨Q,hQ, fun R hR => quotient_unique M π hs R Q hR hQ⟩
212 
213 /-- Source-facing finite institutional-state and finite-action version of Core 8.2. -/
214 theorem finite_legal_quotient [Fintype X] [Fintype Action]
215     (M : System X Action Label) (π : X → Z) (hs : Function.Surjective π) :
216     (∃! Q : System Z Action Label, Factors M Q π) ↔ FibreCompatible M π :=
217   existsUnique_quotient_iff M π hs
218 
219 /-- The canonical partial compatibility test is exactly the source's raw-input test. -/
220 theorem ofEnabled_fibre_iff (label : X → Label) (D : X → Set Action)
221     (F : ∀ x a, a ∈ D x → X) (π : X → Z) :
222     FibreCompatible (ofEnabled label D F) π ↔
223       (∀ x y, π x = π y → label x = label y) ∧
224       (∀ x y, π x = π y → D x = D y) ∧
225       (∀ x y a, π x = π y → ∀ hx : a ∈ D x, ∀ hy : a ∈ D y,
226         π (F x a hx) = π (F y a hy)) := by
227   constructor
228   · intro h
229     refine ⟨h.label_eq, ?_, ?_⟩
230     · intro x y hxy
231       simpa only [enabled_ofEnabled] using h.enabled_eq x y hxy
232     · intro x y a hxy hx hy
233       exact h.successor_eq x y a _ _ hxy
234         (ofEnabled_step_of_mem label D F x a hx)
235         (ofEnabled_step_of_mem label D F y a hy)
236   · rintro ⟨hl,hd,hf⟩
237     refine ⟨hl, ?_, ?_⟩
238     · intro x y hxy
239       simpa only [enabled_ofEnabled] using hd x y hxy
240     · intro x y a x' y' hxy hx hy
241       have hmx : a ∈ D x := by
242         simpa only [enabled_ofEnabled] using
243           (mem_enabled_iff (ofEnabled label D F) x a).mpr ⟨x',hx⟩
244       have hmy : a ∈ D y := by
245         simpa only [enabled_ofEnabled] using
246           (mem_enabled_iff (ofEnabled label D F) y a).mpr ⟨y',hy⟩
247       have heX : F x a hmx = x' :=
248         Option.some.inj ((ofEnabled_step_of_mem label D F x a hmx).symm.trans hx)
249       have heY : F y a hmy = y' :=
250         Option.some.inj ((ofEnabled_step_of_mem label D F y a hmy).symm.trans hy)
251       rw [← heX, ← heY]
252       exact hf x y a hxy hmx hmy
253 
254 /-- Core 8.2 stated directly for finite states, supplied permissions and legal successors. -/
255 theorem finite_source_legal_quotient [Fintype X] [Fintype Action]
256     (label : X → Label) (D : X → Set Action) (F : ∀ x a, a ∈ D x → X)
257     (π : X → Z) (hs : Function.Surjective π) :
258     (∃! Q : System Z Action Label, Factors (ofEnabled label D F) Q π) ↔
259       (∀ x y, π x = π y → label x = label y) ∧
260       (∀ x y, π x = π y → D x = D y) ∧
261       (∀ x y a, π x = π y → ∀ hx : a ∈ D x, ∀ hy : a ∈ D y,
262         π (F x a hx) = π (F y a hy)) :=
263   (finite_legal_quotient (ofEnabled label D F) π hs).trans (ofEnabled_fibre_iff label D F π)
264 
265 end Komorebi.MachineTheory.LegalQuotient

Back to source controls