RevisionControls.lean

1 import MachineTheory.RevisionExamples
2 import MachineTheory.PrefixExamples
3 
4 /-! # Boundaries of selective certificate reuse
5 
6 Staleness is an exact syntactic dependency-closure result, not a semantic refutation.
7 The false registry and cyclic example are intentionally not admitted as sound old proofs.
8 -/
9 namespace Komorebi.MachineTheory.RevisionControls
10 open Dependency RevisionExamples HardInquiry BinaryDiagnosis BinaryExamples Finset
11 
12 /-- The omitted second input is a real value, not an unresolved hash collision. -/
13 def omitted : Graph Unit Bool where
14   parents := fun _ => ∅
15   direct := fun _ => {false}
16 
17 def zeroState : Bool → Bool := fun _ => false
18 
19 def changedSecond : Bool → Bool := id
20 
21 theorem omitted_dependency :
22     omitted.view zeroState () = omitted.view changedSecond () ∧
23     omitted.stale zeroState changedSecond = ∅ ∧
24     zeroState false = zeroState true ∧ changedSecond false ≠ changedSecond true := by
25   refine ⟨?_,by decide,rfl,by decide⟩
26   funext i
27   have hi : i.val=false := by simpa [omitted] using i.property
28   simp [Graph.view,zeroState,changedSecond,hi]
29 
30 /-- No semantically complete declaration can justify the missing-dependency claim. -/
31 theorem omitted_not_complete :
32     ¬ (∀ a b : Bool → Bool, omitted.view a () = omitted.view b () →
33       (a false=a true ↔ b false=b true)) := by
34   intro hc
35   have hh := (hc zeroState changedSecond omitted_dependency.1).mp rfl
36   exact omitted_dependency.2.2.2 hh
37 
38 /-- A local-only unchecked test can pass even while the intended equality is false. -/
39 def incompleteCheck (a : {i // i ∈ omitted.direct ()} → Bool) : Bool := !a ⟨false,by decide⟩
40 
41 theorem flawless_local_replay_can_be_wrong :
42     incompleteCheck (omitted.view zeroState ()) = true ∧
43     incompleteCheck (omitted.view changedSecond ()) = true ∧
44     changedSecond false ≠ changedSecond true := by decide
45 
46 /-- Exact copies of printed names carry no implication of value equality. -/
47 theorem same_name_not_same_artifact :
48     ("repair" : String) = "repair" ∧
49     ¬ Scope universalRepair ∧ Scope eight :=
50   ⟨rfl,universal_not_scope,eight_scope⟩
51 
52 /-- A cyclic pair of implications does not establish either false premise. -/
53 def cyclic : Graph Bool Unit where
54   parents := fun v => {!v}
55   direct := fun _ => ∅
56 
57 def cyclicSystem : System cyclic (fun _ => Bool) (fun _ => Bool) where
58   claim := fun _ _ => False
59   external := fun _ _ => True
60   check := fun _ _ w => w
61   sound := by
62     intro a v _ _ _ hp
63     exact hp (!v) (by simp [cyclic])
64 
65 theorem cycle_has_no_rank : ¬ ∃ r : Bool → ℕ, cyclic.Ranked r := by
66   rintro ⟨r,hr⟩
67   have h0 := hr false true (by simp [cyclic])
68   have h1 := hr true false (by simp [cyclic])
69   omega
70 
71 theorem cyclic_flags_are_not_proofs :
72     (∀ v, cyclicSystem.check v (cyclic.view (fun _ => false) v) true = true) ∧
73     ¬ (∀ v, cyclicSystem.Established (fun _ => false) v true) := by
74   refine ⟨fun _ => rfl,?_⟩
75   intro h
76   exact (h false).2.2
77 
78 theorem cycle_guard_rejects (r : Bool → ℕ) :
79     replayGuard cyclic (fun _ => false) (fun _ => false) (fun _ => true) r = false := by
80   apply Bool.eq_false_iff.mpr
81   intro h
82   exact cycle_has_no_rank ⟨r,((replayGuard_iff _ _ _ _ _).mp h).1⟩
83 
84 /-- Guard refusal is not a proof that a sound independent arithmetic fact is false. -/
85 theorem bad_order_rejected :
86     replayGuard graph before repairAdded externalOK (fun _ => 0) = false ∧
87     system.claim repairAdded 0 := by
88   refine ⟨by decide,?_⟩
89   intro n
90   simp
91 
92 /-- Unchanged claims with unavailable external assurance cannot be admitted for copying. -/
93 theorem external_guard_rejects :
94     system.checkedFinish before before oldWitness allFresh (fun _ => false) rank = none := by
95   unfold System.checkedFinish
96   have hg : replayGuard graph before before (fun _ => false) rank = false := by decide
97   rw [hg]
98   rfl
99 
100 /-- A false submitted witness is rejected even when the mathematical claim happens to be true. -/
101 def badFresh : Node → Option Bool := fun v => if v=3 then some false else some true
102 
103 def rejectedRun := system.finish before repairAdded oldWitness badFresh externalOK rank
104 
105 set_option maxRecDepth 8192 in
106 set_option maxHeartbeats 2000000 in
107 theorem rejection_not_false : rejectedRun 3 = .rejected ∧ system.claim repairAdded 3 := by
108   exact ⟨by decide,by change universalRepair.Valid 3 univ balanced; decide⟩
109 
110 set_option maxRecDepth 8192 in
111 set_option maxHeartbeats 2000000 in
112 theorem unchecked_parent_blocks_true_child :
113     rejectedRun 4 = .blockedParents ∧ system.claim repairAdded 4 := by
114   exact ⟨by decide,missing_is_not_false.2⟩
115 
116 /-- Stale is not false: the controller remains valid while its justification is re-established. -/
117 theorem stale_can_remain_true : (3 : Node) ∈ graph.stale before repairAdded ∧
118     system.claim repairAdded 3 :=
119   ⟨by decide,rejection_not_false.2⟩
120 
121 /-- Direct-only invalidation misses the unmodified-profile descendant. -/
122 theorem closure_is_necessary : (4 : Node) ∉ graph.changedRoots before repairAdded ∧
123     (4 : Node) ∈ graph.stale before repairAdded := by decide
124 
125 /-- A supplied local flag cannot bypass unavailable parent evidence. -/
126 theorem parent_required_for_local_return :
127     system.evaluate repairAdded allFresh externalOK (fun _ => .pending) 2 = .blockedParents ∧
128     system.check 2 (graph.view repairAdded 2) true = true := by decide
129 
130 /-- Changing a query order has an actual literal-controller consequence in Block10. -/
131 theorem query_order_is_semantic_input :
132     (OrderedCompiler.search OrderedCompiler.streamScanner three [0,1,2] [0,1,2] 2 [0,1,2]).answer ≠
133     (OrderedCompiler.search OrderedCompiler.streamScanner three [1,0,2] [0,1,2] 2 [0,1,2]).answer :=
134   PrefixExamples.query_order_changes_tree
135 
136 /-- A fingerprint not proved injective cannot replace equality of declared values. -/
137 theorem constant_digest_not_identity :
138     (fun _ : Bool => (0 : ℕ)) false = (fun _ : Bool => (0 : ℕ)) true ∧
139     false ≠ true := by decide
140 
141 end Komorebi.MachineTheory.RevisionControls

Back to source controls