import Omega.Floor

namespace Omega

def period : ℕ := 500000000000000
def halfQ : ℕ := 169974885672389
def inverse : ℕ := 281419755786509

theorem gcd_constants : Nat.gcd Q S=2 := by decide
theorem inverse_identity : halfQ*inverse=1+95668581631527*period := by decide

theorem remainder_halved (d : ℕ) : rho d/2=(halfQ*d)%period := by
  have hQ : Q=2*halfQ := by decide
  have hS : S=2*period := by decide
  rw [rho,hQ,hS,mul_assoc,Nat.mul_mod_mul_left]
  omega

def seedFromRemainder (r : ℕ) : ℕ := (inverse*(r/2))%period

theorem first_remainder_reconstruction (d : ℕ) (hd : d < period) :
    seedFromRemainder (rho d)=d := by
  have hinv : inverse*halfQ%period=1 := by norm_num [inverse,halfQ,period]
  unfold seedFromRemainder
  rw [remainder_halved]
  calc
    inverse*(halfQ*d%period)%period=(inverse*halfQ*d)%period := by
      simp [Nat.mul_mod,Nat.mul_assoc]
    _ = d%period := by
      rw [Nat.mul_mod (inverse*halfQ),hinv,one_mul,Nat.mod_mod]
    _ = d := Nat.mod_eq_of_lt hd

theorem first_remainder_injective :
    Set.InjOn rho {d : ℕ | d < period} := by
  intro d hd e he h
  have hi := congrArg seedFromRemainder h
  simpa only [first_remainder_reconstruction d hd,
    first_remainder_reconstruction e he] using hi

theorem first_remainder_injective_domain :
    Set.InjOn rho {d : ℕ | d < domainSize} := by
  intro d hd e he h
  have hD : domainSize < period := by norm_num [domainSize,period]
  exact first_remainder_injective
    (lt_trans hd hD) (lt_trans he hD) h

set_option maxRecDepth 1000000 in
set_option maxHeartbeats 0 in
/-- Finite certificate computed by Lean's ordinary decision procedure and
checked by the kernel. No external native evaluator is used. -/
theorem finite_gap_certificate :
    (List.range 128).all (fun b => (List.range 256).all
      (fun i => decide (34535026732 ≤ S-rho (256*b+i))))=true := by decide

theorem certified_gap (d : ℕ) (hd : d < domainSize) :
    34535026732 ≤ S-rho d := by
  have hb : d/256 ∈ List.range 128 := by
    rw [List.mem_range]
    unfold domainSize at hd
    omega
  have hi : d%256 ∈ List.range 256 := List.mem_range.mpr (Nat.mod_lt _ (by decide))
  have h := List.all_eq_true.mp (List.all_eq_true.mp finite_gap_certificate _ hb) _ hi
  have he : 256*(d/256)+d%256=d := Nat.div_add_mod d 256
  simpa only [he,decide_eq_true_eq] using h

theorem minimum_gap_attained : S-rho 20706=34535026732 := by norm_num [S,rho,Q]

theorem finite_certificate_inequality :
    (32767:ℕ)<34535026732 := by decide

end Omega