import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Data.Finset.Lattice.Fold
import Mathlib.Data.Finset.Powerset
import Mathlib.Order.Filter.AtTopBot.Basic
import Mathlib.Order.Interval.Finset.Nat
import Mathlib.Order.LiminfLimsup

/-!
# An improved lower bound for the Furstenberg--Sárközy problem

This is the small, Mathlib-only statement surface submitted to Palomar. For a natural
number `N`, `D N` is the largest cardinality of a subset of `{1, ..., N}` containing no
two elements whose positive difference is a nonzero perfect square.

The explicit constant `alphaInf` is computed from the eleven triples in `pool`. The main
theorem says that `alphaInf` is a lower bound for the liminf exponent of `D`; the second
theorem gives the corresponding eventual pointwise bound for every strictly smaller
exponent; and the third certifies the rational decimal headline `0.7537 < alphaInf`.
Krachun's preceding explicit exponent was `0.752796455874514...`, so the certified
threshold is a strict improvement and moves the lower bound farther beyond `3/4`.

The formal claims do not assert all displayed digits of the numerical approximation
`0.753741541837329405...`, an endpoint estimate with a fixed multiplicative constant, an
optimal pool or optimal certificates, or the induced-matching corollary discussed in the
informal source.
-/

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
  sorry

/-- 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
  sorry

/-- 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
  sorry

end FsFormal