import FsLowerBound

/-!
# Proved solution

This module repeats the Challenge definitions and theorem signatures verbatim. The proof
development is the ported `FsLowerBound` library. The three short bridges below are by
definitional equality to its audited target theorems.
-/

namespace FsFormal

/-- A finite set is square-difference-free when no ordered pair of its elements has
positive difference equal to a nonzero square. The additive equation avoids truncated
subtraction on natural numbers. -/
def sdfFinset (A : Finset Nat) : Prop :=
  ∀ a ∈ A, ∀ b ∈ A, a < b → ¬ ∃ k, 0 < k ∧ b = a + k * k

/-- `D N` is the largest size of a square-difference-free subset of `{1, ..., N}`. -/
noncomputable def D (N : Nat) : Nat :=
  letI := Classical.decPred sdfFinset
  ((Finset.Icc 1 N).powerset.filter sdfFinset).sup Finset.card

/-- The eleven certified blocks, recorded as `(modulus, support size, ranking height)`.
The first nine are Paley-chain blocks; the last two are square-DAG certificates on the
square-free composite moduli `235` and `299`. -/
def pool : List (Nat × Nat × Nat) :=
  [(3, 2, 2), (7, 3, 3), (11, 4, 4), (19, 5, 5), (31, 7, 7), (43, 7, 7),
   (59, 9, 9), (71, 9, 9), (103, 11, 11), (235, 17, 11), (299, 19, 12)]

/-- The explicit asymptotic exponent

`(sum_i log(m_i t_i) / log(H_i)) / (1 + 2 sum_i log(m_i) / log(H_i))`

evaluated on `pool`. -/
noncomputable def alphaInf : Real :=
  (pool.map fun x => Real.log (x.1 * x.2.1) / Real.log x.2.2).sum /
  (1 + 2 * (pool.map fun x => Real.log x.1 / Real.log x.2.2).sum)

/-- The explicit constant `alphaInf` bounds from below the liminf exponent of the largest
square-difference-free subsets of `{1, ..., N}`. -/
theorem sdf_liminf_ge :
    alphaInf ≤ Filter.liminf (fun N : Nat => Real.log (D N) / Real.log N) Filter.atTop := by
  change _root_.alphaInf ≤
    Filter.liminf (fun N : Nat => Real.log (_root_.D N) / Real.log N) Filter.atTop
  exact _root_.sdf_liminf_ge

/-- Every exponent strictly below `alphaInf` is an eventual pointwise lower-bound
exponent for `D`. This does not claim the endpoint exponent with a uniform constant. -/
theorem sdf_pointwise (rho : Real) (hrho : rho < alphaInf) :
    ∀ᶠ N : Nat in Filter.atTop, (N : Real) ^ rho ≤ (D N : Real) := by
  change ∀ᶠ N : Nat in Filter.atTop,
    (N : Real) ^ rho ≤ (_root_.D N : Real)
  exact _root_.sdf_pointwise rho hrho

/-- Kernel-certified numerical consequence of the closed form: only the displayed
rational threshold `0.7537` is part of this formal statement. -/
theorem alphaInf_gt : (0.7537 : Real) < alphaInf := by
  change (0.7537 : Real) < _root_.alphaInf
  exact _root_.alphaInf_gt

end FsFormal