Correction.lean

1 import MachineTheory.Behavior
2 import Mathlib.Data.Fintype.Powerset
3 
4 /-! Reviewed Core v0.2, Theorem 3.1. Empty candidate sets and contradictory evidence are retained. -/
5 namespace Komorebi.MachineTheory
6 
7 structure EvidenceAlgebra (Ω : Type*) where
8   events : Set (Set Ω)
9   univ_mem : Set.univ ∈ events
10   inter_mem : ∀ E ∈ events, ∀ F ∈ events, E ∩ F ∈ events
11 
12 namespace EvidenceAlgebra
13 variable {Ω Y : Type*} (E : EvidenceAlgebra Ω)
14 abbrev Event := {e : Set Ω // e ∈ E.events}
15 def total : E.Event := ⟨Set.univ, E.univ_mem⟩
16 def meet (e f : E.Event) : E.Event := ⟨e.val ∩ f.val, E.inter_mem _ e.property _ f.property⟩
17 def filter (e : E.Event) (V : Set Ω) : Set Ω := V ∩ e.val
18 
19 def signature (t : Ω → Y) (V : Set Ω) : E.Event → Set Y :=
20   fun e => t '' (V ∩ e.val)
21 
22 @[simp] theorem signature_total (t : Ω → Y) (V : Set Ω) :
23     E.signature t V E.total = t '' V := by
24   simp [signature, total]
25 
26 /-- A later correction is another coordinate of the original signature. -/
27 theorem signature_filter (t : Ω → Y) (V : Set Ω) (e f : E.Event) :
28     E.signature t (E.filter e V) f = E.signature t V (E.meet e f) := by
29   simp only [signature, filter, meet, Set.inter_assoc]
30 
31 /-- Core 3.1, congruence for every permitted intersection filter. -/
32 theorem signature_congruence (t : Ω → Y) {V W : Set Ω}
33     (h : E.signature t V = E.signature t W) (e : E.Event) :
34     E.signature t (E.filter e V) = E.signature t (E.filter e W) := by
35   funext f
36   rw [E.signature_filter, E.signature_filter, h]
37 
38 /-- The actual memory type contains attainable correction signatures only. -/
39 abbrev Memory (t : Ω → Y) := Attained (E.signature t)
40 
41 def remember (t : Ω → Y) (V : Set Ω) : E.Memory t := record (E.signature t) V
42 
43 noncomputable def update (t : Ω → Y) (e : E.Event) (s : E.Memory t) : E.Memory t := by
44   let V := Classical.choose s.property
45   exact E.remember t (E.filter e V)
46 
47 /-- Choice of a realizing candidate set cannot alter the updated memory. -/
48 @[simp] theorem update_remember (t : Ω → Y) (e : E.Event) (V : Set Ω) :
49     E.update t e (E.remember t V) = E.remember t (E.filter e V) := by
50   apply Subtype.ext
51   apply E.signature_congruence t
52   exact Classical.choose_spec (E.remember t V).property
53 
54 def read (t : Ω → Y) (s : E.Memory t) : Set Y := s.val E.total
55 
56 @[simp] theorem read_remember (t : Ω → Y) (V : Set Ω) :
57     E.read t (E.remember t V) = t '' V := E.signature_total t V
58 
59 /-- The signature representation works after *every finite* evidence sequence. -/
60 theorem memory_finite_continuation (t : Ω → Y) (events : List E.Event) (V : Set Ω) :
61     run (E.update t) events (E.remember t V) =
62       E.remember t (run E.filter events V) := by
63   induction events generalizing V with
64   | nil => rfl
65   | cons e events ih =>
66     simp only [run_cons, E.update_remember]
67     exact ih _
68 
69 theorem memory_readout_continuation (t : Ω → Y) (events : List E.Event) (V : Set Ω) :
70     E.read t (run (E.update t) events (E.remember t V)) =
71       t '' (run E.filter events V) := by
72   rw [E.memory_finite_continuation, E.read_remember]
73 
74 /-- Every other exact deterministic memory must retain the whole signature. -/
75 theorem any_exact_memory_separates (t : Ω → Y) {M : Type*}
76     (r : Set Ω → M) (readout : M → Set Y) (step : E.Event → M → M)
77     (hq : ∀ V, readout (r V) = t '' V)
78     (hs : ∀ e V, step e (r V) = r (E.filter e V)) :
79     FiberConstant r (E.signature t) := by
80   intro V W h
81   funext e
82   change t '' (E.filter e V) = t '' (E.filter e W)
83   rw [← hq, ← hq, ← hs, ← hs, h]
84 
85 /-- Strong minimality: a surjection from every exact initialized memory to signatures. -/
86 theorem memory_universal_property (t : Ω → Y) {M : Type*}
87     (r : Set Ω → M) (readout : M → Set Y) (step : E.Event → M → M)
88     (hq : ∀ V, readout (r V) = t '' V)
89     (hs : ∀ e V, step e (r V) = r (E.filter e V)) :
90     ∃ d : Attained r → E.Memory t, Function.Surjective d ∧
91       ∀ V, d (record r V) = E.remember t V := by
92   have hf : FiberConstant r (E.remember t) := by
93     intro V W h
94     exact Subtype.ext (E.any_exact_memory_separates t r readout step hq hs V W h)
95   obtain ⟨d, hd⟩ := (decoder_exists_iff r (E.remember t)).mpr hf
96   refine ⟨d, ?_, hd⟩
97   intro s
98   obtain ⟨V, hV⟩ := s.property
99   refine ⟨record r V, ?_⟩
100   rw [hd]
101   exact Subtype.ext hV
102 
103 /-- Core 3.1, finite cardinality bound on attained states, not whole ambient M. -/
104 theorem memory_minimal_card [Fintype Ω] (t : Ω → Y) {M : Type*}
105     (r : Set Ω → M) (readout : M → Set Y) (step : E.Event → M → M)
106     (hq : ∀ V, readout (r V) = t '' V)
107     (hs : ∀ e V, step e (r V) = r (E.filter e V)) :
108     Fintype.card (E.Memory t) ≤ Fintype.card (Attained r) := by
109   classical
110   obtain ⟨d, hd, _⟩ := E.memory_universal_property t r readout step hq hs
111   exact Fintype.card_le_of_surjective d hd
112 
113 /-- Contradiction is retained, rather than replaced by an arbitrary model. -/
114 @[simp] theorem signature_empty (t : Ω → Y) :
115     E.signature t ∅ = fun _ => ∅ := by
116   funext e
117   simp [signature]
118 
119 end EvidenceAlgebra
120 end Komorebi.MachineTheory

Back to source controls