LegalQuotientExamples.lean

1 import MachineTheory.LegalQuotient
2 import MachineTheory.LegalTrace
3 
4 /-! # Exact legal-operation quotients
5 
6 False names observation and true names repair. The visible bit records an
7 outstanding repair. A second bit is historical detail. Observation is always
8 enabled; repair is enabled only while outstanding. Successful steps toggle
9 the historical bit. Forgetting history preserves the operational interface.
10 
11 Separate examples isolate the label, availability, and projected-successor
12 conditions. These are stipulated finite institutions, not claims of external
13 legal or moral authorization.
14 -/
15 namespace Komorebi.MachineTheory.LegalQuotientExamples
16 open LegalQuotient
17 
18 abbrev FineState := Bool × Bool
19 
20 def fine : System FineState Bool Bool where
21   label x := x.1
22   step x a := if a then
23     if x.1 then some (false, !x.2) else none
24     else some (x.1, !x.2)
25 
26 def coarse : System Bool Bool Bool where
27   label b := b
28   step b a := if a then if b then some false else none else some b
29 
30 def forgetHistory : FineState → Bool := Prod.fst
31 
32 theorem forgetHistory_surjective : Function.Surjective forgetHistory :=
33   fun b => ⟨(b,false), rfl⟩
34 
35 theorem history_quotient_factors : Factors fine coarse forgetHistory := by
36   apply factors_of_label_step
37   · intro x; rfl
38   · rintro ⟨b,h⟩ a
39     cases b <;> cases a <;> rfl
40 
41 /-- Fine successors may differ, provided their retained projections agree. -/
42 theorem projected_not_literal_successors :
43     fine.step (true,false) false ≠ fine.step (true,true) false ∧
44     (fine.step (true,false) false).map forgetHistory =
45       (fine.step (true,true) false).map forgetHistory := by
46   decide
47 
48 theorem repair_then_observe :
49     execute fine (true,false) [true,false] =
50       some [(true,false),(false,true),(false,false)] ∧
51     execute coarse true [true,false] = some [true,false,false] ∧
52     labels fine (true,false) [true,false] = some [true,false,false] := by
53   decide
54 
55 theorem repeated_repair_refused :
56     execute fine (true,false) [true,true] = none ∧
57     execute coarse true [true,true] = none := by
58   decide
59 
60 theorem empty_trace_keeps_initial_label :
61     labels fine (true,false) [] = some [true] := by
62   rfl
63 
64 /-- Label loss alone invalidates the collapse, though no actions are enabled. -/
65 def labelBad : System Bool Bool Bool where
66   label := id
67   step _ _ := none
68 
69 theorem labels_block_collapse : ¬ FibreCompatible labelBad (fun _ => ()) := by
70   intro h
71   exact Bool.false_ne_true (h.label_eq false true rfl)
72 
73 /-- The sensor label is identical, but only the true state permits repair. -/
74 def permissionBad : System Bool Bool Bool where
75   label _ := false
76   step b a := if a then if b then some false else none else some b
77 
78 theorem same_sensor_different_permission :
79     permissionBad.label false = permissionBad.label true ∧
80     permissionBad.step false true = none ∧
81     permissionBad.step true true = some false := by
82   decide
83 
84 theorem permissions_block_collapse :
85     ¬ FibreCompatible permissionBad (fun _ => ()) := by
86   intro h
87   have he := h.enabled_eq false true rfl
88   have ht : true ∈ enabled permissionBad false := by
89     rw [he]
90     simp [enabled, permissionBad]
91   simp [enabled, permissionBad] at ht
92 
93 /-- Every label and enabled set is constant, but hidden history affects the next visible bit. -/
94 def successorBad : System FineState Bool Bool where
95   label _ := false
96   step x _ := some (x.2,x.2)
97 
98 theorem same_label_and_permissions_different_successor :
99     successorBad.label (false,false) = successorBad.label (false,true) ∧
100     enabled successorBad (false,false) = enabled successorBad (false,true) ∧
101     (successorBad.step (false,false) true).map forgetHistory ≠
102       (successorBad.step (false,true) true).map forgetHistory := by
103   refine ⟨rfl, ?_, by decide⟩
104   ext a
105   simp [enabled, successorBad]
106 
107 theorem successors_block_quotient : ¬ FibreCompatible successorBad forgetHistory := by
108   intro h
109   have he := h.successor_eq (false,false) (false,true) true
110     (false,false) (true,true) rfl rfl rfl
111   exact Bool.false_ne_true he
112 
113 /-- A source reaching only false cannot constrain the quotient's label at true. -/
114 def oneSource : System Unit Bool Bool where
115   label _ := false
116   step _ _ := none
117 
118 def offImage₀ : System Bool Bool Bool where
119   label _ := false
120   step _ _ := none
121 
122 def offImage₁ : System Bool Bool Bool where
123   label := id
124   step _ _ := none
125 
126 def onlyFalse (_ : Unit) : Bool := false
127 
128 theorem missing_surjectivity_two_quotients :
129     Factors oneSource offImage₀ onlyFalse ∧
130     Factors oneSource offImage₁ onlyFalse ∧ offImage₀ ≠ offImage₁ := by
131   constructor
132   · apply factors_of_label_step
133     · intro x; rfl
134     · intro x a; rfl
135   constructor
136   · apply factors_of_label_step
137     · intro x; rfl
138     · intro x a; rfl
139   · intro h
140     have he := congrArg (fun M : System Bool Bool Bool => M.label true) h
141     exact Bool.false_ne_true he
142 
143 theorem onlyFalse_not_surjective : ¬ Function.Surjective onlyFalse := by
144   intro h
145   obtain ⟨x, hx⟩ := h true
146   exact Bool.false_ne_true hx
147 
148 /-- Disabled successors have no operational value. Arbitrary defaults are not quotient data. -/
149 theorem disabled_totalizations_not_unique :
150     coarse.step false true = none ∧
151     (coarse.step false true).getD false ≠ (coarse.step false true).getD true := by
152   decide
153 
154 end Komorebi.MachineTheory.LegalQuotientExamples

Back to source controls