HardControls.lean

1 import MachineTheory.HardSemantics
2 import MachineTheory.RecipientExamples
3 import Mathlib.Tactic.NormNum
4 
5 /-! # Source-bound hard-budget and actual-state controls -/
6 namespace Komorebi.MachineTheory.HardControls
7 open HardInquiry Finset
8 
9 /-- Read one immutable Boolean state; both report branches must be installed. -/
10 def readBit : Model Bool Unit Bool Bool Unit where
11   permitted := fun _ _ => true
12   next := fun _ x => x
13   observe := fun _ x => x
14   accept := fun x c => decide (x=c)
15   stepCost := fun _ _ => 1
16   terminalCost := fun _ _ _ => 0
17 
18 def bitTree : Tree Unit Bool Bool 1 := .inr ((),fun o => some o)
19 def missingBranch : Tree Unit Bool Bool 1 := .inr ((),fun o => if o then none else some false)
20 
21 theorem bit_tree_valid : readBit.Valid 1 univ bitTree := by decide
22 theorem bit_tree_cost : readBit.profile 1 univ bitTree = (fun _ => 1,3) := by decide
23 theorem missing_reachable_rejected : ¬ readBit.Valid 1 univ missingBranch := by decide
24 
25 def restricted : Model Bool Unit Bool Bool Unit :=
26   { readBit with permitted := fun _ x => !x }
27 
28 theorem permission_at_one_case : restricted.permitted () false = true := rfl
29 theorem permission_not_uniform : ¬ restricted.Allowed univ () := by decide
30 theorem existential_permission_insufficient : ¬ restricted.Valid 1 univ bitTree := by decide
31 
32 def constantReport : Model Bool Unit Bool Bool Unit :=
33   { readBit with observe := fun _ _ => false, accept := fun _ _ => true }
34 
35 def constantTree : Tree Unit Bool Bool 1 := .inr ((),fun o => if o then none else some false)
36 
37 theorem impossible_report_absent : constantReport.Valid 1 univ constantTree := by decide
38 theorem impossible_report_has_no_record : constantReport.profile 1 univ constantTree = (fun _ => 1,2) := by decide
39 theorem invented_child_rejected : ¬ constantReport.Valid 1 univ bitTree := by decide
40 
41 def noArtifact : Model Bool Unit Bool Bool Unit := { readBit with accept := fun _ _ => false }
42 theorem unsolved_children_not_free : noArtifact.compute 1 univ = ∅ := by decide
43 theorem noArtifact_no_tree : ¬ ∃ t : Tree Unit Bool Bool 1, noArtifact.Valid 1 univ t := by
44   apply (noArtifact.no_tree_iff_empty 1 univ).mpr
45   rw [← noArtifact.compute_eq_solve,unsolved_children_not_free]
46 
47 /-- Terminal execution costs are charged after the observation. -/
48 def paidTerminal : Model Bool Unit Bool Bool Unit :=
49   { readBit with terminalCost := fun _ _ _ => 3 }
50 
51 theorem terminal_cost_included : paidTerminal.profile 1 univ bitTree = (fun _ => 4,3) := by decide
52 theorem one_unit_not_total_work : ¬ paidTerminal.profile 1 univ bitTree ≤ (fun _ => 1,3) := by decide
53 
54 /-- A reset produces knowledge of the new state, not of the old one. -/
55 def reset : Model Bool Unit Unit Bool Unit where
56   permitted := fun _ _ => true
57   next := fun _ _ => false
58   observe := fun _ _ => ()
59   accept := fun x c => decide (x=c)
60   stepCost := fun _ _ => 1
61   terminalCost := fun _ _ _ => 0
62 
63 def resetTree : Tree Unit Unit Bool 1 := .inr ((),fun _ => some false)
64 
65 theorem reset_post_support : reset.update univ () () = {false} := by decide
66 theorem reset_current_valid : reset.Valid 1 univ resetTree := by decide
67 theorem reset_current_profile : reset.profile 1 univ resetTree = (fun _ => 1,2) := by decide
68 
69 def taggedReset : Model (Bool × Bool) Unit Unit Bool Unit where
70   permitted := fun _ _ => true
71   next := fun _ x => (x.1,false)
72   observe := fun _ _ => ()
73   accept := fun x c => decide (x.1=c)
74   stepCost := fun _ _ => 1
75   terminalCost := fun _ _ _ => 0
76 
77 def origins : Finset (Bool × Bool) := {(false,false),(true,true)}
78 theorem origin_tag_survives : taggedReset.update origins () () = {(false,false),(true,false)} := by decide
79 theorem reset_does_not_recover_origin : ¬ taggedReset.Valid 1 origins resetTree := by decide
80 theorem origin_inquiry_still_unresolved : taggedReset.compute 1 origins = ∅ := by decide
81 
82 /-- Separate coordinates can attain their maxima on different executions. -/
83 def twoCoordinates : Model Bool Unit Bool Bool Bool where
84   permitted := fun _ _ => true
85   next := fun _ x => x
86   observe := fun _ x => x
87   accept := fun x c => decide (x=c)
88   stepCost := fun _ _ => 0
89   terminalCost := fun _ V j => V.sup (fun x => if x=j then 10 else 0)
90 
91 def twoCharge (_ : Bool) (x j : Bool) : ℕ := if x=j then 10 else 0
92 
93 theorem coordinate_charge_exact : twoCoordinates.ExactCharges twoCharge := fun _ _ _ => rfl
94 theorem coordinate_tree_valid : twoCoordinates.Valid 1 univ bitTree := by decide
95 theorem coordinate_profile : twoCoordinates.profile 1 univ bitTree = (fun _ => 10,3) := by decide
96 theorem maxima_not_one_execution : ∀ x : Bool,
97     (twoCoordinates.execute twoCharge 1 bitTree x).map (fun r => (r.cost false,r.cost true)) ≠ some (10,10) := by decide
98 
99 theorem coordinate_each_attained (j : Bool) : ∃ x ∈ (univ : Finset Bool), ∃ r,
100     twoCoordinates.execute twoCharge 1 bitTree x = some r ∧ r.cost j = 10 := by
101   simpa only [coordinate_profile] using
102     twoCoordinates.worst_coordinate_attained twoCharge coordinate_charge_exact 1 univ bitTree coordinate_tree_valid j
103 
104 /-- Source sensor: observations, combined recipient arithmetic, and message bits stay separate. -/
105 def sensorCharge (_ : Bool) (_ : RecipientExamples.Sensor) (j : Fin 3) : ℕ :=
106   if j=0 then 0 else if j=1 then 2 else 1
107 
108 def sensor : Model RecipientExamples.Sensor Unit Bool Bool (Fin 3) where
109   permitted := fun _ _ => true
110   next := fun _ x => x
111   observe := fun _ x => RecipientExamples.display x
112   accept := fun x c => decide (c=RecipientExamples.display x)
113   stepCost := fun _ j => if j=0 then 1 else 0
114   terminalCost := fun c V j => V.sup (fun x => sensorCharge c x j)
115 
116 /-- The finite terminal table is proved to be the unchanged installed audience contract. -/
117 theorem sensor_accept_iff (x : RecipientExamples.Sensor) (c : Bool) :
118     sensor.accept x c = true ↔ RecipientExamples.xorAudience.Accepts x c := by
119   simp only [sensor,decide_eq_true_eq,RecipientExamples.xor_accepts_iff]
120 
121 theorem sensor_needs_observation : sensor.compute 0 univ = ∅ := by decide
122 theorem sensor_tree_valid : sensor.Valid 1 univ bitTree := by decide
123 theorem sensor_tree_profile : sensor.profile 1 univ bitTree =
124     (fun j => if j=0 then 1 else if j=1 then 2 else 1, 3) := by decide
125 
126 theorem sensor_frontier : sensor.compute 1 univ =
127     {(fun j => if j=0 then 1 else if j=1 then 2 else 1, 3)} := by decide
128 
129 theorem sensor_charge_exact : sensor.ExactCharges sensorCharge := fun _ _ _ => rfl
130 
131 /-- The same single observation and broadcast succeeds for both actual fixed recipients. -/
132 theorem sensor_recipient_execution (x : RecipientExamples.Sensor) :
133     ∃ r, sensor.execute sensorCharge 1 bitTree x = some r ∧
134       RecipientExamples.xorAudience.Accepts r.finalState r.artifact ∧
135       (r.cost 0,r.cost 1,r.cost 2,r.history.length) = (1,2,1,1) := by
136   obtain ⟨r,hr,ha,_,_⟩ := sensor.execution_sound sensorCharge sensor_charge_exact.bounded
137     1 univ bitTree sensor_tree_valid x (mem_univ _)
138   refine ⟨r,hr,(sensor_accept_iff _ _).mp ha,?_⟩
139   have he : (sensor.execute sensorCharge 1 bitTree x).map
140       (fun r => (r.cost 0,r.cost 1,r.cost 2,r.history.length)) = some (1,2,1,1) := by
141     rcases x with ⟨b,s,n⟩
142     cases b <;> cases s <;> cases n <;> decide
143   rw [hr] at he
144   exact Option.some.inj he
145 
146 /-- With fewer stored records the complete two-branch controller is unavailable. -/
147 theorem sensor_two_records_insufficient :
148     ¬ ∃ t : Tree Unit Bool Bool 1, sensor.Valid 1 univ t ∧
149       sensor.profile 1 univ t ≤ (fun j => if j=0 then 1 else if j=1 then 2 else 1, 2) := by
150   rw [sensor.computed_budget_iff, sensor_frontier]
151   simp only [mem_singleton,exists_eq_left]
152   intro h
153   have hc := h.2
154   exact (by decide : ¬ (3 ≤ 2)) hc
155 
156 end Komorebi.MachineTheory.HardControls

Back to source controls