HardExamples.lean

1 import MachineTheory.HardSemantics
2 import Mathlib.Data.Fintype.Powerset
3 import Mathlib.Tactic.NormNum
4 import Mathlib.Tactic.FinCases
5 
6 /-! # Exact hard-budget examples and scope controls -/
7 namespace Komorebi.MachineTheory.HardExamples
8 open HardInquiry Finset
9 
10 /-- Scalar cost displayed in a one-coordinate resource vector. -/
11 def scalar (w m : ℕ) : Profile Unit := (fun _ => w, m)
12 
13 /-- Four immutable cases. `none` is direct reveal; `some i` is equality testing. -/
14 def four : Model (Fin 4) (Option (Fin 4)) (Fin 4) (Fin 4) Unit where
15   permitted := fun _ _ => true
16   next := fun _ x => x
17   observe := fun e x => match e with | none => x | some i => if x=i then 1 else 0
18   accept := fun x c => decide (x=c)
19   stepCost := fun e _ => if e.isNone then 4 else 1
20   terminalCost := fun _ _ _ => 0
21 
22 
23 set_option maxRecDepth 16384 in
24 set_option maxHeartbeats 2000000 in
25 theorem four_frontier_three : four.compute 3 univ = {scalar 4 5, scalar 3 7} := by
26   decide
27 
28 /-- A finite invariant table, not a fit inferred from a few horizons. -/
29 def fourTable (V : Finset (Fin 4)) : Finset (Profile Unit) :=
30   match V.card with
31   | 0 => ∅
32   | 1 => {scalar 0 1}
33   | 2 => {scalar 1 3}
34   | 3 => {scalar 2 5, scalar 4 4}
35   | _ => {scalar 3 7, scalar 4 5}
36 
37 set_option maxRecDepth 16384 in
38 set_option maxHeartbeats 2000000 in
39 theorem fourTable_closed : ∀ V : Finset (Fin 4),
40     Model.prune (four.backup fourTable V) = fourTable V := by
41   decide
42 
43 theorem fourTable_full : fourTable univ = {scalar 4 5, scalar 3 7} := by decide
44 
45 /-- The certificate is a fixed-point argument for every horizon, not extrapolated tests. -/
46 theorem four_frontier_all (n : ℕ) : four.solve (3+n) univ = {scalar 4 5, scalar 3 7} := by
47   rw [← fourTable_full]
48   apply four.closed_family_exact fourTable fourTable_closed (3+n) univ
49   intro p hp
50   have hb : p ∈ four.solve 3 univ := by
51     rw [← four.compute_eq_solve, four_frontier_three]
52     simpa only [fourTable_full] using hp
53   obtain ⟨t,ht,he⟩ := four.solve_witness 3 univ p hb
54   obtain ⟨u,hu,hue⟩ := four.pad_horizon 3 n univ t ht
55   exact ⟨u,hu,hue.trans he⟩
56 
57 /-- No controller at ANY finite depth can combine the separate resource minima. -/
58 theorem four_no_mixed_budget (h : ℕ) :
59     ¬ ∃ t : Tree (Option (Fin 4)) (Fin 4) (Fin 4) h,
60       four.Valid h univ t ∧ four.profile h univ t ≤ scalar 3 5 := by
61   rintro ⟨t,ht,hb⟩
62   obtain ⟨p,hp,hpt⟩ := four.closed_family_dominates fourTable fourTable_closed h univ t ht
63   have hpb := hpt.trans hb
64   rw [fourTable_full, mem_insert, mem_singleton] at hp
65   rcases hp with rfl | rfl
66   · have h := hpb.1 (); norm_num [scalar] at h
67   · have h := hpb.2; norm_num [scalar] at h
68 
69 /-- Both nondominated profiles are actually achieved, not just lower bounds. -/
70 theorem four_two_witnesses :
71     (∃ t : Tree (Option (Fin 4)) (Fin 4) (Fin 4) 3,
72       four.Valid 3 univ t ∧ four.profile 3 univ t = scalar 4 5) ∧
73     (∃ t : Tree (Option (Fin 4)) (Fin 4) (Fin 4) 3,
74       four.Valid 3 univ t ∧ four.profile 3 univ t = scalar 3 7) := by
75   constructor
76   · apply four.solve_witness 3 univ
77     rw [← four.compute_eq_solve, four_frontier_three]
78     exact mem_insert_self _ _
79   · apply four.solve_witness 3 univ
80     rw [← four.compute_eq_solve, four_frontier_three]
81     exact mem_insert_of_mem (mem_singleton_self _)
82 
83 /-- One direct reveal, one branch for each of four reports. -/
84 def direct : Tree (Option (Fin 4)) (Fin 4) (Fin 4) 1 := .inr (none,fun o => some o)
85 
86 def equalLast : Tree (Option (Fin 4)) (Fin 4) (Fin 4) 1 :=
87   .inr (some 2, fun o => if o=1 then some (2 : Fin 4) else if o=0 then some (3 : Fin 4) else none)
88 def equalMiddle : Tree (Option (Fin 4)) (Fin 4) (Fin 4) 2 :=
89   .inr (some 1, fun o => if o=1 then some (.inl 1) else if o=0 then some equalLast else none)
90 def equality : Tree (Option (Fin 4)) (Fin 4) (Fin 4) 3 :=
91   .inr (some 0, fun o => if o=1 then some (.inl 0) else if o=0 then some equalMiddle else none)
92 
93 theorem direct_valid : four.Valid 1 univ direct := by decide
94 theorem direct_profile : four.profile 1 univ direct = scalar 4 5 := by decide
95 theorem equality_valid : four.Valid 3 univ equality := by decide
96 theorem equality_profile : four.profile 3 univ equality = scalar 3 7 := by decide
97 
98 /-- The four full execution traces, not a count of only one selected branch. -/
99 theorem equality_report_counts : ∀ x : Fin 4,
100     (four.execute (fun _ _ _ => 0) 3 equality x).map (fun r => r.history.length) =
101       some (if x=0 then 1 else if x=1 then 2 else 3) := by decide
102 
103 theorem equality_terminal_outputs : ∀ x : Fin 4,
104     (four.execute (fun _ _ _ => 0) 3 equality x).map (fun r => r.artifact) = some x := by decide
105 
106 theorem equality_records : Model.records 3 equality = 7 := by decide
107 theorem direct_records : Model.records 1 direct = 5 := by decide
108 
109 end Komorebi.MachineTheory.HardExamples

Back to source controls