Resolution Semantics

Download original file

This is the original source text. Reading it does not run or verify the program.

Read the typeset paper

1 /-!
2 Komorebi Resolution Semantics 0.1.0
3 
4 STATUS: UNCOMPILED SOURCE SCAFFOLD.
5 This file was not checked by a Lean compiler in the release environment.
6 It is not proof evidence for the PDF. The scope is only the two-valued core.
7 No model of ZFC, forcing theorem, graph classification, or general Boolean-ring
8 instance is constructed here.
9 
10 Reproduction target with a local Lean 4 installation:
11   lean formal/KRS_Core.lean
12 -/
13 import Std
14 
15 namespace KRS
16 
17 def defect (a b : Bool) : Bool := Bool.xor a b
18 
19 theorem defect_self (a : Bool) : defect a a = false := by
20   cases a <;> rfl
21 
22 theorem defect_comm (a b : Bool) : defect a b = defect b a := by
23   cases a <;> cases b <;> rfl
24 
25 theorem defect_zero (a : Bool) : defect a false = a := by
26   cases a <;> rfl
27 
28 theorem defect_eq_false_iff (a b : Bool) : defect a b = false ↔ a = b := by
29   cases a <;> cases b <;> simp [defect]
30 
31 theorem defect_composition (a b c : Bool) :
32     defect a c = Bool.xor (defect a b) (defect b c) := by
33   cases a <;> cases b <;> cases c <;> rfl
34 
35 theorem defect_reconstruction (a b : Bool) :
36     Bool.xor a (defect a b) = b := by
37   cases a <;> cases b <;> rfl
38 
39 theorem defect_additive (a b c d : Bool) :
40     defect (Bool.xor a b) (Bool.xor c d) =
41       Bool.xor (defect a c) (defect b d) := by
42   cases a <;> cases b <;> cases c <;> cases d <;> rfl
43 
44 theorem defect_twisted_product (a b c d : Bool) :
45     defect (a && b) (c && d) =
46       Bool.xor ((defect a c) && b) (c && (defect b d)) := by
47   cases a <;> cases b <;> cases c <;> cases d <;> rfl
48 
49 theorem defect_complement (a b : Bool) :
50     defect (!a) (!b) = defect a b := by
51   cases a <;> cases b <;> rfl
52 
53 theorem triangle_telescope (a b c : Bool) :
54     Bool.xor (Bool.xor (defect a b) (defect b c)) (defect c a) = false := by
55   cases a <;> cases b <;> cases c <;> rfl
56 
57 universe u
58 variable {W : Type u}
59 
60 def Invariant (E : W → W → Prop) (a : W → Bool) : Prop :=
61   ∀ w z, E w z → a w = a z
62 
63 theorem invariant_constant (E : W → W → Prop) (b : Bool) :
64     Invariant E (fun _ => b) := by
65   intro w z _
66   rfl
67 
68 theorem invariant_complement (E : W → W → Prop) (a : W → Bool)
69     (ha : Invariant E a) : Invariant E (fun w => !(a w)) := by
70   intro w z h
71   rw [ha w z h]
72 
73 theorem invariant_xor (E : W → W → Prop) (a b : W → Bool)
74     (ha : Invariant E a) (hb : Invariant E b) :
75     Invariant E (fun w => Bool.xor (a w) (b w)) := by
76   intro w z h
77   rw [ha w z h, hb w z h]
78 
79 theorem invariant_and (E : W → W → Prop) (a b : W → Bool)
80     (ha : Invariant E a) (hb : Invariant E b) :
81     Invariant E (fun w => (a w) && (b w)) := by
82   intro w z h
83   rw [ha w z h, hb w z h]
84 
85 theorem invariant_of_more_edges (E F : W → W → Prop)
86     (hEF : ∀ w z, E w z → F w z) (a : W → Bool)
87     (ha : Invariant F a) : Invariant E a := by
88   intro w z h
89   exact ha w z (hEF w z h)
90 
91 end KRS

Back to source controls

Back to Resolution Semantics