PredictiveClosure.lean

1 import KomorebiLSM.Realization
2 
3 /-! P6 and the set-level part of P22. The codomain is onto its image.
4 Representative choice constructs a reduced map; fiber constancy, not a
5 supplied transition, establishes that the construction is well defined.
6 -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM
9 universe u v w t
10 
11 /-- Exactly the information-loss criterion needed for a factor map. -/
12 def FiberConstant {X : Type u} {Z : Type v} {Y : Type w}
13     (gamma : X → Z) (eta : X → Y) : Prop :=
14   ∀ x y, gamma x = gamma y → eta x = eta y
15 
16 theorem factor_exists_unique_iff {X : Type u} {Z : Type v} {Y : Type w}
17     (gamma : X → Z) (onto : ∀ z, ∃ x, gamma x = z) (eta : X → Y) :
18     (∃ J : Z → Y, (∀ x, J (gamma x) = eta x) ∧
19       (∀ K : Z → Y, (∀ x, K (gamma x) = eta x) → K = J)) ↔
20     FiberConstant gamma eta := by
21   constructor
22   · rintro ⟨J, hj, _⟩ x y h
23     exact (hj x).symm.trans ((congrArg J h).trans (hj y))
24   · intro h
25     classical
26     let chooseX (z : Z) : X := Classical.choose (onto z)
27     have hx (z : Z) : gamma (chooseX z) = z := Classical.choose_spec (onto z)
28     let J : Z → Y := fun z => eta (chooseX z)
29     have hj (x : X) : J (gamma x) = eta x := h _ _ (hx (gamma x))
30     refine ⟨J, hj, ?_⟩
31     intro K hk
32     funext z
33     obtain ⟨x, rfl⟩ := onto z
34     exact (hk x).trans (hj x).symm
35 
36 /-- The reduced transition is unique on the actual summary space. -/
37 theorem predictive_closure_iff {X : Type u} {Z : Type v}
38     (gamma : X → Z) (onto : ∀ z, ∃ x, gamma x = z) (F : X → X) :
39     (∃ f : Z → Z, (∀ x, f (gamma x) = gamma (F x)) ∧
40       (∀ g : Z → Z, (∀ x, g (gamma x) = gamma (F x)) → g = f)) ↔
41     FiberConstant gamma (fun x => gamma (F x)) :=
42   factor_exists_unique_iff gamma onto (fun x => gamma (F x))
43 
44 def SummaryState {X : Type u} {Z : Type v} (gamma : X → Z) :=
45   {z : Z // ∃ x, gamma x = z}
46 
47 def summarize {X : Type u} {Z : Type v} (gamma : X → Z) (x : X) :
48     SummaryState gamma := ⟨gamma x, x, rfl⟩
49 
50 theorem summarize_onto {X : Type u} {Z : Type v} (gamma : X → Z)
51     (z : SummaryState gamma) : ∃ x, summarize gamma x = z := by
52   obtain ⟨x, hx⟩ := z.property
53   exact ⟨x, Subtype.ext hx⟩
54 
55 theorem closure_on_image_iff {X : Type u} {Z : Type v}
56     (gamma : X → Z) (F : X → X) :
57     (∃ f : SummaryState gamma → SummaryState gamma,
58       (∀ x, f (summarize gamma x) = summarize gamma (F x)) ∧
59       (∀ g : SummaryState gamma → SummaryState gamma,
60         (∀ x, g (summarize gamma x) = summarize gamma (F x)) → g = f)) ↔
61     FiberConstant gamma (fun x => gamma (F x)) := by
62   rw [predictive_closure_iff (summarize gamma) (summarize_onto gamma)]
63   constructor
64   · intro h x y hxy
65     exact congrArg Subtype.val (h x y (Subtype.ext hxy))
66   · intro h x y hxy
67     exact Subtype.ext (h x y (congrArg Subtype.val hxy))
68 
69 /-- Upward lift between the actual images, not ambient codomains. -/
70 theorem factor_on_images_iff {X : Type u} {Z : Type v} {Y : Type w}
71     (gamma : X → Z) (eta : X → Y) :
72     (∃ J : SummaryState gamma → SummaryState eta,
73       (∀ x, J (summarize gamma x) = summarize eta x) ∧
74       (∀ K : SummaryState gamma → SummaryState eta,
75         (∀ x, K (summarize gamma x) = summarize eta x) → K = J)) ↔
76     FiberConstant gamma eta := by
77   rw [factor_exists_unique_iff (summarize gamma) (summarize_onto gamma)
78     (summarize eta)]
79   constructor
80   · intro h x y hxy
81     exact congrArg Subtype.val (h x y (Subtype.ext hxy))
82   · intro h x y hxy
83     exact Subtype.ext (h x y (congrArg Subtype.val hxy))
84 
85 /-- Actions need simultaneous fiber constancy. No transition is assumed. -/
86 theorem controlled_closure_iff {X : Type u} {Z : Type v} {A : Type w}
87     (gamma : X → Z) (onto : ∀ z, ∃ x, gamma x = z) (F : A → X → X) :
88     (∃ f : A → Z → Z, ∀ a x, f a (gamma x) = gamma (F a x)) ↔
89     (∀ a, FiberConstant gamma (fun x => gamma (F a x))) := by
90   constructor
91   · rintro ⟨f, hf⟩ a x y h
92     exact (hf a x).symm.trans ((congrArg (f a) h).trans (hf a y))
93   · intro h
94     classical
95     have ex (a : A) := (predictive_closure_iff gamma onto (F a)).mpr (h a)
96     exact ⟨fun a => Classical.choose (ex a),
97       fun a => (Classical.choose_spec (ex a)).1⟩
98 
99 /-- Exact closure is preserved under composition of operations. -/
100 theorem factor_composition {X : Type u} {Z : Type v}
101     (gamma : X → Z) (F G : X → X) (f g : Z → Z)
102     (hf : ∀ x, f (gamma x) = gamma (F x))
103     (hg : ∀ x, g (gamma x) = gamma (G x)) (x : X) :
104     g (f (gamma x)) = gamma (G (F x)) := by
105   rw [hf, hg]
106 
107 /-- One explicit pair in a lost-information fiber refutes every proposed factor. -/
108 theorem no_factor_of_witness {X : Type u} {Z : Type v} {Y : Type w}
109     (gamma : X → Z) (eta : X → Y) (x y : X)
110     (same : gamma x = gamma y) (different : eta x ≠ eta y) :
111     ¬ ∃ J : Z → Y, ∀ t, J (gamma t) = eta t := by
112   rintro ⟨J, hj⟩
113   exact different ((hj x).symm.trans ((congrArg J same).trans (hj y)))
114 
115 end Komorebi.LSM

Back to source controls