A computer checked ten hard math proofs. Here is what it checked, and what it could not.

Formal name: Sharp Cohn–Elkies sphere-packing asymptotics. Certifies 4 theorems in SpherePacking.lean. Allowed axioms: propext Quot.sound Classical.choice. Independent kernel check: on.

• PackingBounds.FullMain.exact_limit
• PackingBounds.FullMain.exact_binary_exponent
• PackingBounds.PackingBridge.sphere_packing_sharp_asymptotic_upper
• PackingBounds.sharpFullCohnElkiesManuscriptConclusions

Why the excerpt below contains sorry: this is the statement-only audit layer used for human comparison, with proof bodies intentionally collapsed. The separate formal certificate contains the complete proof and is sorry-free.

import Mathlib

set_option autoImplicit false

noncomputable section

open Filter MeasureTheory Metric
open scoped ENNReal FourierTransform SchwartzMap Topology

namespace CohnElkies

abbrev Euclidean (d : ℕ) := EuclideanSpace ℝ (Fin d)

abbrev TestFunction (d : ℕ) := 𝓢(Euclidean d, ℂ)

def unitBallVolume (d : ℕ) : ℝ :=
  Real.pi ^ ((d : ℝ) / 2) / Real.Gamma ((d : ℝ) / 2 + 1)

instance numeralTwoAtLeast : Nat.AtLeastTwo 2 := ⟨by decide⟩

instance euclideanFiniteDimensional (d : ℕ) :
    FiniteDimensional ℝ (EuclideanSpace ℝ (Fin d)) := by
  infer_instance

instance euclideanBorelSpace (d : ℕ) :
    BorelSpace (EuclideanSpace ℝ (Fin d)) := by
  infer_instance

end CohnElkies

namespace PackingBounds

structure FullAdmissible (d : ℕ) where
  function : CohnElkies.TestFunction d
  real : ∀ x : CohnElkies.Euclidean d, (function x).im = 0
  fourier_real :
    ∀ x : CohnElkies.Euclidean d, ((𝓕 function) x).im = 0
  fourier_nonneg :
    ∀ x : CohnElkies.Euclidean d, 0 ≤ ((𝓕 function) x).re
  fourier_zero_pos :
    0 < ((𝓕 function) (0 : CohnElkies.Euclidean d)).re
  outside_nonpos :
    ∀ x : CohnElkies.Euclidean d, 1 ≤ ‖x‖ → (function x).re ≤ 0

def fullQuotient {d : ℕ} (f : FullAdmissible d) : ℝ :=
  (f.function (0 : CohnElkies.Euclidean d)).re /
    ((𝓕 f.function) (0 : CohnElkies.Euclidean d)).re

def fullQuotientSet (d : ℕ) : Set ℝ :=
  Set.range (fullQuotient (d := d))

def fullLinearProgram (d : ℕ) : ℝ :=
  CohnElkies.unitBallVolume d / (2 : ℝ) ^ d *
    sInf (fullQuotientSet d)

end PackingBounds

structure SpherePacking (d : ℕ) where
  centers : Set (EuclideanSpace ℝ (Fin d))
  separation : ℝ
  separation_pos : 0 < separation := by positivity
  centers_dist : Pairwise (separation ≤ dist · · : centers → centers → Prop)

@[reducible] def SpherePacking.occupiedBallRegion {d : ℕ} (S : SpherePacking d) :
    Set (EuclideanSpace ℝ (Fin d)) :=
  ⋃ x : S.centers, ball (x : EuclideanSpace ℝ (Fin d)) (S.separation / 2)

noncomputable def SpherePacking.densityInsideRadius {d : ℕ}
    (S : SpherePacking d) (R : ℝ) : ℝ≥0∞ :=
  volume (S.occupiedBallRegion ∩ ball 0 R) / volume (ball (0 : EuclideanSpace ℝ (Fin d)) R)

noncomputable def SpherePacking.upperPackingDensity {d : ℕ}
    (S : SpherePacking d) : ℝ≥0∞ :=
  limsup S.densityInsideRadius atTop

def SpherePackingConstant (d : ℕ) : ℝ≥0∞ :=
  ⨆ S : SpherePacking d, S.upperPackingDensity

namespace PackingBounds

structure SharpFullCohnElkiesManuscriptConclusions : Prop where
  root_before_infimum :
    Tendsto
      (fun d : ℕ =>
        sInf {q : ℝ | ∃ f : FullAdmissible d,
          fullQuotient f ^ ((d : ℝ)⁻¹) = q} /
          Real.sqrt (d : ℝ))
      atTop (𝓝 (1 / Real.pi))
  root_before_infimum_vanishing_error :
    ∃ err : ℕ → ℝ,
      Tendsto err atTop (𝓝 0) ∧
      ∀ d : ℕ, 0 < d →
        sInf {q : ℝ | ∃ f : FullAdmissible d,
          fullQuotient f ^ ((d : ℝ)⁻¹) = q} =
          (1 / Real.pi + err d) * Real.sqrt (d : ℝ)
  linear_program_root :
    Tendsto
      (fun d : ℕ => (fullLinearProgram d) ^ ((d : ℝ)⁻¹))
      atTop (𝓝 (Real.sqrt (Real.exp 1 / (2 * Real.pi))))
  natural_logarithmic_rate :
    Tendsto
      (fun d : ℕ => Real.log (fullLinearProgram d) / (d : ℝ))
      atTop
      (𝓝 ((1 / 2 : ℝ) * Real.log (Real.exp 1 / (2 * Real.pi))))
  natural_vanishing_exponential_error :
    ∃ err : ℕ → ℝ,
      Tendsto err atTop (𝓝 0) ∧
      (∀ᶠ d : ℕ in atTop,
        fullLinearProgram d =
          (Real.sqrt (Real.exp 1 / (2 * Real.pi)) + err d) ^ d)
  universal_nonnegative_delta :
    ∃ δ : ℕ → ℝ,
      Tendsto δ atTop (𝓝 0) ∧
      (∀ d : ℕ, 0 ≤ δ d) ∧
      (∀ᶠ d : ℕ in atTop, ∀ f : FullAdmissible d,
        (2 : ℝ) ^ d / CohnElkies.unitBallVolume d *
          (Real.sqrt (Real.exp 1 / (2 * Real.pi)) - δ d) ^ d ≤
            fullQuotient f)
  base_two_exponent_positive :
    0 < (1 / 2 : ℝ) * Real.logb 2 (2 * Real.pi / Real.exp 1)
  base_two_decimal_certificate :
    (1 / 2 : ℝ) * Real.logb 2 (2 * Real.pi / Real.exp 1) ∈
      Set.Ioo
        (0.604400544291677695341677307053 : ℝ)
        0.604400544291677695341677307054
  base_two_logarithmic_rate :
    Tendsto
      (fun d : ℕ => Real.logb 2 (fullLinearProgram d) / (d : ℝ))
      atTop
      (𝓝 (-((1 / 2 : ℝ) * Real.logb 2 (2 * Real.pi / Real.exp 1))))
  base_two_vanishing_exponential_error :
    ∃ err : ℕ → ℝ,
      Tendsto err atTop (𝓝 0) ∧
      (∀ᶠ d : ℕ in atTop,
        fullLinearProgram d =
          (2 : ℝ) ^
            (-((1 / 2 : ℝ) *
                Real.logb 2 (2 * Real.pi / Real.exp 1) + err d) *
              (d : ℝ)))

end PackingBounds

namespace PackingBounds.FullMain

theorem exact_limit :
    Tendsto
      (fun d : ℕ =>
        PackingBounds.fullLinearProgram d ^ ((d : ℝ)⁻¹))
      atTop
      (nhds (Real.sqrt (Real.exp 1 / (2 * Real.pi)))) := by
  sorry

theorem exact_binary_exponent :
    Tendsto
      (fun d : ℕ =>
        Real.logb 2 (PackingBounds.fullLinearProgram d) / (d : ℝ))
      atTop
      (nhds (-(1 / 2 : ℝ) *
        Real.logb 2 (2 * Real.pi / Real.exp 1))) := by
  sorry

end PackingBounds.FullMain

namespace PackingBounds.PackingBridge

theorem sphere_packing_sharp_asymptotic_upper :
    ∃ e : ℕ → ℝ,
      Asymptotics.IsLittleO atTop e (fun _ : ℕ => (1 : ℝ)) ∧
      ∀ d : ℕ, 0 < d →
        SpherePackingConstant d ≤
          ENNReal.ofReal
            ((Real.sqrt (Real.exp 1 / (2 * Real.pi)) + e d) ^ d) := by
  sorry

end PackingBounds.PackingBridge

namespace PackingBounds

theorem sharpFullCohnElkiesManuscriptConclusions :
    SharpFullCohnElkiesManuscriptConclusions := by
  sorry

end PackingBounds

end

Formal name: Strict hierarchy of improved spherical-code bounds. Certifies 4 theorems in MetricCodes.lean. Allowed axioms: propext Quot.sound Classical.choice. Independent kernel check: on.

• MetricCodes.Johnson.main_binary_theorem
• MetricCodes.Spherical.HigherHierarchy.main_general
• MetricCodes.Spherical.HigherHierarchy.strict_hierarchy
• MetricCodes.Spherical.HigherHierarchy.NumericalMaximum.eventually_kissingNumber_lt_published

Why the excerpt below contains sorry: this is the statement-only audit layer used for human comparison, with proof bodies intentionally collapsed. The separate formal certificate contains the complete proof and is sorry-free.

import Mathlib

set_option autoImplicit false

noncomputable section

open Filter Metric
open scoped BigOperators InnerProductSpace Topology

namespace MetricCodes

instance numeralTwoAtLeast : Nat.AtLeastTwo 2 := ⟨by decide⟩

abbrev BinaryWord (n : ℕ) := Fin n → Bool

def hammingDist {n : ℕ} (x y : BinaryWord n) : ℕ :=
  (Finset.univ.filter fun i => x i ≠ y i).card

def IsBinaryCode {n : ℕ} (d : ℕ) (C : Finset (BinaryWord n)) : Prop :=
  ∀ ⦃x⦄, x ∈ C → ∀ ⦃y⦄, y ∈ C → x ≠ y → d ≤ hammingDist x y

def binaryEntropy (u : ℝ) : ℝ :=
  -(u * Real.logb 2 u) - (1 - u) * Real.logb 2 (1 - u)

def hammingGamma (a b : ℝ) : ℝ :=
  (2 * (a - b) * (1 - a - b)) / Real.sqrt (a * (1 - a))

def sphericalEntropy (u : ℝ) : ℝ :=
  (1 + u) * Real.logb 2 (1 + u) - u * Real.logb 2 u

def Gamma (a b : ℝ) : ℝ :=
  ((a - b) * (1 + a + b)) /
    ((1 + 2 * a) * Real.sqrt (a * (1 + a)))

def classicalThreshold (s : ℝ) : ℝ :=
  (1 / Real.sqrt (1 - s ^ 2) - 1) / 2

namespace Hamming

noncomputable def validCodes (n d : ℕ) : Finset (Finset (BinaryWord n)) := by
  classical
  exact Finset.univ.filter (MetricCodes.IsBinaryCode d)

noncomputable def codeNumber (n d : ℕ) : ℕ :=
  (validCodes n d).sup fun C => C.card

def binaryRate (δ : ℝ) : ℝ :=
  Filter.limsup
    (fun n : ℕ =>
      Real.logb 2
        (codeNumber n (Nat.ceil (δ * (n : ℝ))) : ℝ) / (n : ℝ))
    Filter.atTop

def Feasible (δ a b : ℝ) : Prop :=
  0 ≤ b ∧ b < a ∧ a ≤ (1 : ℝ) / 2 ∧
    1 - 2 * δ < MetricCodes.hammingGamma a b

def rateSet (δ : ℝ) : Set ℝ :=
  {r | ∃ a b : ℝ, Feasible δ a b ∧
    r = MetricCodes.binaryEntropy a - MetricCodes.binaryEntropy b}

def variationalRate (δ : ℝ) : ℝ := sInf (rateSet δ)

end Hamming

namespace Johnson

def centeredDegree (u : ℝ) : ℝ := 1 - 2 * u

def centeredWeight (α : ℝ) : ℝ := 1 - 2 * α

def centeredSigma (β γ : ℝ) : ℝ := 1 - 2 * β - 2 * γ

def centeredEta (α β γ : ℝ) : ℝ := 1 - 2 * α + 2 * β - 2 * γ

def spectralLimit (α β γ u : ℝ) : ℝ :=
  let z := centeredDegree u
  let m := centeredWeight α
  let σ := centeredSigma β γ
  let η := centeredEta α β γ
  (σ * η - m * z ^ 2) ^ 2 /
      (z ^ 2 * (1 - m ^ 2) * (1 - z ^ 2)) +
    ((z ^ 2 - η ^ 2) * (σ ^ 2 - z ^ 2)) /
      (z ^ 2 * (1 - m ^ 2) * Real.sqrt (1 - z ^ 2))

def asymptoticThreshold (δ α : ℝ) : ℝ :=
  1 - δ / (2 * α * (1 - α))

def rankPenalty (α β γ : ℝ) : ℝ :=
  α * MetricCodes.binaryEntropy (β / α) +
    (1 - α) * MetricCodes.binaryEntropy (γ / (1 - α))

def shellRate (α β γ u : ℝ) : ℝ :=
  1 - MetricCodes.binaryEntropy α + MetricCodes.binaryEntropy u -
    rankPenalty α β γ

structure AsymptoticParameters (δ α β γ u : ℝ) : Prop where
  distance_pos : 0 < δ
  distance_lt_half : δ < (1 : ℝ) / 2
  weight_gt_distance : δ / 2 < α
  weight_lt_half : α < (1 : ℝ) / 2
  support_nonneg : 0 ≤ β
  support_lt_half : β < α / 2
  complement_nonneg : 0 ≤ γ
  complement_lt_half : γ < (1 - α) / 2
  first_lt_degree : β + γ < u
  degree_lt_weight : u < α
  degree_lt_left : u < α - β + γ
  degree_lt_right : u < 1 - α + β - γ

def IsSpectrallyFeasible (δ α β γ u : ℝ) : Prop :=
  asymptoticThreshold δ α < spectralLimit α β γ u

def Feasible (δ α β γ u : ℝ) : Prop :=
  AsymptoticParameters δ α β γ u ∧
    IsSpectrallyFeasible δ α β γ u

def rateSet (δ : ℝ) : Set ℝ :=
  {r | ∃ α β γ u : ℝ,
    Feasible δ α β γ u ∧ r = shellRate α β γ u}

def variationalRate (δ : ℝ) : ℝ := sInf (rateSet δ)

def combinedVariationalRate (δ : ℝ) : ℝ :=
  min (MetricCodes.Hamming.variationalRate δ) (variationalRate δ)

def mrrwG (v : ℝ) : ℝ :=
  MetricCodes.binaryEntropy ((1 - Real.sqrt (1 - v)) / 2)

def mrrwObjective (δ r : ℝ) : ℝ :=
  1 + mrrwG (r ^ 2) - mrrwG (r ^ 2 + 2 * δ * r + 2 * δ)

def mrrwRateSet (δ : ℝ) : Set ℝ :=
  {t | ∃ r : ℝ, 0 ≤ r ∧ r ≤ 1 - 2 * δ ∧
    t = mrrwObjective δ r}

def mrrwRate (δ : ℝ) : ℝ := sInf (mrrwRateSet δ)

theorem main_binary_theorem {δ : ℝ}
    (hδ : 0 < δ) (hhalf : δ < (1 : ℝ) / 2) :
    MetricCodes.Hamming.binaryRate δ ≤ combinedVariationalRate δ ∧
      combinedVariationalRate δ < mrrwRate δ := by
  sorry

end Johnson

end MetricCodes

namespace SpherePacking

abbrev Euclidean (n : ℕ) := EuclideanSpace ℝ (Fin n)

structure SphericalCode (n : ℕ) (s : ℝ) where
  points : Finset (Euclidean n)
  unit_norm : ∀ x ∈ points, ‖x‖ = 1
  inner_le : ∀ x ∈ points, ∀ y ∈ points, x ≠ y →
    ⟪x, y⟫_ℝ ≤ s

def sphericalCodeNumber (n : ℕ) (s : ℝ) : ℕ∞ :=
  ⨆ C : SphericalCode n s, (C.points.card : ℕ∞)

def kissingNumber (n : ℕ) : ℕ∞ :=
  sphericalCodeNumber n ((1 : ℝ) / 2)

end SpherePacking

namespace MetricCodes

namespace Spherical

def Feasible (s a b : ℝ) : Prop :=
  0 < b ∧ b < a ∧ s < 2 * MetricCodes.Gamma a b

def rateSet (s : ℝ) : Set ℝ :=
  {r | ∃ a b : ℝ, Feasible s a b ∧
    r = MetricCodes.sphericalEntropy a - MetricCodes.sphericalEntropy b}

def variationalRate (s : ℝ) : ℝ := sInf (rateSet s)

namespace SidelnikovLocalization

def sliceCost (s t : ℝ) : ℝ :=
  (1 / 2 : ℝ) * Real.logb 2 ((1 - t) / (1 - s))

def localizedEnvelope (κ : ℝ → ℝ) (s : ℝ) : ℝ :=
  sInf ((fun t => κ t + sliceCost s t) '' Set.Icc 0 s)

end SidelnikovLocalization

namespace HigherHierarchy

def quadraticCoordinate (u : ℝ) : ℝ := u * (1 + u)

def spectralAtom (u : ℝ) : ℝ :=
  Real.sqrt (quadraticCoordinate u) / (1 + 2 * u)

def Interlacing {r : ℕ}
    (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) : Prop :=
  0 ≤ a (Fin.last r) ∧
    ∀ i : Fin r, a i.castSucc > b i ∧ b i > a i.succ

def lagrangeNumerator {r : ℕ}
    (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ)
    (ℓ : Fin (r + 1)) : ℝ :=
  ∏ m : Fin r, (quadraticCoordinate (a ℓ) - quadraticCoordinate (b m))

def lagrangeDenominator {r : ℕ}
    (a : Fin (r + 1) → ℝ) (ℓ : Fin (r + 1)) : ℝ :=
  ∏ m : Fin r,
    (quadraticCoordinate (a ℓ) - quadraticCoordinate (a (ℓ.succAbove m)))

def lagrangeWeight {r : ℕ}
    (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ)
    (ℓ : Fin (r + 1)) : ℝ :=
  lagrangeNumerator a b ℓ / lagrangeDenominator a ℓ

def Gamma {r : ℕ}
    (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) : ℝ :=
  ∑ ℓ : Fin (r + 1), lagrangeWeight a b ℓ * spectralAtom (a ℓ)

def Phi {r : ℕ}
    (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) : ℝ :=
  (∑ ℓ : Fin (r + 1), MetricCodes.sphericalEntropy (a ℓ)) -
    ∑ m : Fin r, MetricCodes.sphericalEntropy (b m)

def hierarchyRateSet (s : ℝ) : Set ℝ :=
  {z | ∃ (r : ℕ) (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ),
    Interlacing a b ∧ s < 2 * Gamma a b ∧ z = Phi a b}

def hierarchyVariationalRate (s : ℝ) : ℝ := sInf (hierarchyRateSet s)

def closedHierarchyRateSet (s : ℝ) : Set ℝ :=
  {z | ∃ (r : ℕ) (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ),
    Interlacing a b ∧ s ≤ 2 * Gamma a b ∧ z = Phi a b}

def closedHierarchyVariationalRate (s : ℝ) : ℝ :=
  sInf (closedHierarchyRateSet s)

def sphericalCodeRate (s : ℝ) : ℝ :=
  Filter.limsup
    (fun n : ℕ =>
      Real.logb 2
        ((SpherePacking.sphericalCodeNumber n s).toNat : ℝ) / (n : ℝ))
    Filter.atTop

def levelRateSet (r : ℕ) (s : ℝ) : Set ℝ :=
  {R | ∃ (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ),
    Interlacing a b ∧ s < 2 * Gamma a b ∧ R = Phi a b}

def levelRate (r : ℕ) (s : ℝ) : ℝ := sInf (levelRateSet r s)

def localizedLevelRate (r : ℕ) (s : ℝ) : ℝ :=
  SidelnikovLocalization.localizedEnvelope (levelRate r) s

def localizedHierarchyRate (s : ℝ) : ℝ :=
  sInf (Set.range fun r : ℕ => localizedLevelRate r s)

def localizedRowRate (s : ℝ) : ℝ :=
  SidelnikovLocalization.localizedEnvelope
    MetricCodes.Spherical.variationalRate s

def classicalLocalizedRate (s : ℝ) : ℝ :=
  SidelnikovLocalization.localizedEnvelope
    (fun t => MetricCodes.sphericalEntropy (MetricCodes.classicalThreshold t)) s

theorem main_general {s : ℝ} (hs : 0 < s) (hs' : s < 1) :
    (∀ {r : ℕ} {R : ℝ}
      (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ),
      Interlacing a b → s < 2 * Gamma a b → Phi a b < R →
        ∀ᶠ n : ℕ in atTop, ∀ C : SpherePacking.SphericalCode n s,
          (C.points.card : ℝ) < (2 : ℝ) ^ (R * (n : ℝ))) ∧
      sphericalCodeRate s ≤ closedHierarchyVariationalRate s := by
  sorry

theorem strict_hierarchy {s : ℝ} (hs : 0 < s) (hs' : s < 1) :
    (∀ r : ℕ,
      levelRate (r + 1) s < levelRate r s ∧
        localizedLevelRate (r + 1) s < localizedLevelRate r s) ∧
      sphericalCodeRate s ≤ localizedHierarchyRate s ∧
      localizedHierarchyRate s < localizedLevelRate 1 s ∧
      localizedLevelRate 1 s < localizedRowRate s ∧
      localizedRowRate s < localizedLevelRate 0 s ∧
      localizedLevelRate 0 s = classicalLocalizedRate s := by
  sorry

namespace NumericalMaximum

theorem eventually_kissingNumber_lt_published :
    ∀ᶠ n : ℕ in atTop,
      ((SpherePacking.kissingNumber n).toNat : ℝ) ≤
        (2 : ℝ) ^ ((0.39661 : ℝ) * (n : ℝ)) := by
  sorry

end NumericalMaximum

end HigherHierarchy

end Spherical

end MetricCodes

end

Formal name: Permanent lower bounds for formulas with division. Certifies 2 theorems in Permanent.lean. Allowed axioms: propext Quot.sound Classical.choice. Independent kernel check: on.

• PermanentFormulaLowerBound.permanent_divisionFree_formula_logarithmic_lower_bound
• PermanentFormulaLowerBound.permanent_rational_formula_logarithmic_lower_bound

Why the excerpt below contains sorry: this is the statement-only audit layer used for human comparison, with proof bodies intentionally collapsed. The separate formal certificate contains the complete proof and is sorry-free.

import Mathlib

namespace PermanentFormulaLowerBound

universe u v w

inductive Formula (ι : Type u) (R : Type v) where
  | var : ι → Formula ι R
  | const : R → Formula ι R
  | add : Formula ι R → Formula ι R → Formula ι R
  | sub : Formula ι R → Formula ι R → Formula ι R
  | mul : Formula ι R → Formula ι R → Formula ι R

namespace Formula

variable {ι : Type u} {R : Type v}

noncomputable def eval [CommRing R] : Formula ι R → MvPolynomial ι R
  | .var i => MvPolynomial.X i
  | .const c => MvPolynomial.C c
  | .add f g => eval f + eval g
  | .sub f g => eval f - eval g
  | .mul f g => eval f * eval g

def variableLeaves : Formula ι R → ℕ
  | .var _ => 1
  | .const _ => 0
  | .add f g => variableLeaves f + variableLeaves g
  | .sub f g => variableLeaves f + variableLeaves g
  | .mul f g => variableLeaves f + variableLeaves g

end Formula

inductive RationalFormula (ι : Type u) (R : Type v) where
  | var : ι → RationalFormula ι R
  | const : R → RationalFormula ι R
  | add : RationalFormula ι R → RationalFormula ι R → RationalFormula ι R
  | sub : RationalFormula ι R → RationalFormula ι R → RationalFormula ι R
  | mul : RationalFormula ι R → RationalFormula ι R → RationalFormula ι R
  | div : RationalFormula ι R → RationalFormula ι R → RationalFormula ι R

namespace RationalFormula

variable {ι : Type u} {R : Type v}

noncomputable def eval [Field R] :
    RationalFormula ι R → FractionRing (MvPolynomial ι R)
  | .var i =>
      algebraMap (MvPolynomial ι R) (FractionRing (MvPolynomial ι R))
        (MvPolynomial.X i)
  | .const c =>
      algebraMap (MvPolynomial ι R) (FractionRing (MvPolynomial ι R))
        (MvPolynomial.C c)
  | .add f g => eval f + eval g
  | .sub f g => eval f - eval g
  | .mul f g => eval f * eval g
  | .div f g => eval f / eval g

inductive Valid [Field R] : RationalFormula ι R → Prop where
  | var (i : ι) : Valid (.var i)
  | const (c : R) : Valid (.const c)
  | add {f g : RationalFormula ι R} : Valid f → Valid g → Valid (.add f g)
  | sub {f g : RationalFormula ι R} : Valid f → Valid g → Valid (.sub f g)
  | mul {f g : RationalFormula ι R} : Valid f → Valid g → Valid (.mul f g)
  | div {f g : RationalFormula ι R} :
      Valid f → Valid g → eval g ≠ 0 → Valid (.div f g)

def variableLeaves : RationalFormula ι R → ℕ
  | .var _ => 1
  | .const _ => 0
  | .add f g => variableLeaves f + variableLeaves g
  | .sub f g => variableLeaves f + variableLeaves g
  | .mul f g => variableLeaves f + variableLeaves g
  | .div f g => variableLeaves f + variableLeaves g

end RationalFormula

noncomputable def permanentPolynomial (n : ℕ) :
    MvPolynomial (Fin n × Fin n) ℂ :=
  (Matrix.mvPolynomialX (Fin n) (Fin n) ℂ).permanent

theorem permanent_divisionFree_formula_logarithmic_lower_bound
    {n : ℕ} (hn : 32 ≤ n)
    (f : Formula (Fin n × Fin n) ℂ)
    (hf : Formula.eval f = permanentPolynomial n) :
    (n : ℝ) ^ 4 / (128 * Real.logb 2 (n : ℝ)) ≤
      (Formula.variableLeaves f : ℝ) := by
  sorry

theorem permanent_rational_formula_logarithmic_lower_bound
    {n : ℕ} (hn : 32 ≤ n)
    (f : RationalFormula (Fin n × Fin n) ℂ)
    (hvalid : RationalFormula.Valid f)
    (hf : RationalFormula.eval f =
      algebraMap (MvPolynomial (Fin n × Fin n) ℂ)
        (FractionRing (MvPolynomial (Fin n × Fin n) ℂ))
        (permanentPolynomial n)) :
    (n : ℝ) ^ 4 / (192 * Real.logb 2 (n : ℝ)) ≤
      (RationalFormula.variableLeaves f : ℝ) := by
  sorry

end PermanentFormulaLowerBound

Formal name: Polynomial-factor NP-hardness of the closest vector problem. Certifies 4 theorems in GapCVP.lean. Allowed axioms: propext Quot.sound Classical.choice. Independent kernel check: on.

• GapCVP.Comparator.gapCVP400IsNPHard
• GapCVP.Comparator.binaryNearestCodewordIsNPHard
• GapCVP.Comparator.binarySyndromeDecodingIsNPHard
• GapCVP.Comparator.finitePNormGapCVPIsNPHard

Why the excerpt below contains sorry: this is the statement-only audit layer used for human comparison, with proof bodies intentionally collapsed. The separate formal certificate contains the complete proof and is sorry-free.

import Mathlib

noncomputable section

open scoped BigOperators

namespace GapCVP.BinaryEncoding

def lengthPrefixedWord (word : List Bool) : List Bool :=
  List.replicate word.length true ++ false :: word

def encodeAtomic {α : Type*} [Encodable α] (value : α) : List Bool :=
  lengthPrefixedWord (Computability.encodeNat (Encodable.encode value))

def encodeFinValues {α : Type*} [Encodable α] :
    (n : ℕ) → (Fin n → α) → List Bool
  | 0, _ => []
  | n + 1, values =>
      encodeAtomic (values 0) ++
        encodeFinValues n (fun i => values i.succ)

def encodeMatrixRows :
    (m n : ℕ) → (Fin m → Fin n → ℤ) → List Bool
  | 0, _, _ => []
  | m + 1, n, matrix =>
      encodeFinValues n (matrix 0) ++
        encodeMatrixRows m n (fun i => matrix i.succ)

end GapCVP.BinaryEncoding

namespace GapCVP

abbrev BitLanguage := List Bool → Bool

abbrev bitEncoding : List Bool → List Bool := id

def pairBitEncoding : (List Bool × List Bool) → List (Bool ⊕ Bool) :=
  (Computability.encodingProd
    (Computability.encodingList Bool)
    (Computability.encodingList Bool)).encode

abbrev BitTM (map : List Bool → List Bool) :=
  Turing.TM2ComputableInPolyTime bitEncoding bitEncoding map

abbrev VerifierTM (verifier : List Bool × List Bool → Bool) :=
  Turing.TM2ComputableInPolyTime
    pairBitEncoding Computability.encodeBool verifier

noncomputable def IsNP (language : BitLanguage) : Bool :=
  @decide
    (∃ (bound : Polynomial ℕ) (verifier : List Bool × List Bool → Bool),
      Nonempty (VerifierTM verifier) ∧
        ∀ input : List Bool,
          language input ↔ ∃ certificate : List Bool,
            certificate.length ≤ bound.eval input.length ∧
              verifier (input, certificate) = true)
    (Classical.propDecidable _)

end GapCVP

namespace GapCVP.Comparator

structure Instance where
  dimension : ℕ
  basis : Matrix (Fin dimension) (Fin dimension) ℤ
  target : Fin dimension → ℚ
  radius : ℚ

export GapCVP.BinaryEncoding
  (lengthPrefixedWord encodeAtomic encodeFinValues encodeMatrixRows)

export GapCVP (BitLanguage bitEncoding pairBitEncoding IsNP)

def encodeInstance (I : Instance) : List Bool :=
  encodeAtomic I.dimension ++
    encodeAtomic I.radius ++
    encodeFinValues I.dimension I.target ++
    encodeMatrixRows I.dimension I.dimension I.basis

def wellFormed (record : Instance) : Bool :=
  @decide
    (0 < record.dimension ∧ record.basis.det ≠ 0 ∧ 0 < record.radius)
    (Classical.propDecidable _)

def hasIntegerTarget (record : Instance) : Bool :=
  @decide
    (∀ index : Fin record.dimension,
      ∃ value : ℤ, record.target index = (value : ℚ))
    (Classical.propDecidable _)

noncomputable def distanceSquared (I : Instance)
    (vector : Fin I.dimension → ℤ) : ℝ :=
  ∑ i : Fin I.dimension,
    (((∑ j : Fin I.dimension,
      (I.basis i j : ℝ) * (vector j : ℝ)) -
        (I.target i : ℝ)) ^ 2)

noncomputable def gapFactor400 (I : Instance) : ℝ :=
  (I.dimension : ℝ) ^ ((1 : ℝ) / 400)

def gapYES400 (record : Instance) : Bool :=
  @decide
    (wellFormed record ∧
      ∃ vector : Fin record.dimension → ℤ,
        distanceSquared record vector ≤ (record.radius : ℝ) ^ 2)
    (Classical.propDecidable _)

def gapNO400 (record : Instance) : Bool :=
  @decide
    (wellFormed record ∧
      ∀ vector : Fin record.dimension → ℤ,
        (gapFactor400 record * (record.radius : ℝ)) ^ 2 <
          distanceSquared record vector)
    (Classical.propDecidable _)

def yesLanguage (bits : List Bool) : Bool :=
  @decide
    (∃ record : Instance,
      encodeInstance record = bits ∧
        hasIntegerTarget record ∧ gapYES400 record)
    (Classical.propDecidable _)

def noLanguage (bits : List Bool) : Bool :=
  @decide
    (∃ record : Instance,
      encodeInstance record = bits ∧
        hasIntegerTarget record ∧ gapNO400 record)
    (Classical.propDecidable _)

structure PromiseProblem where
  yes : BitLanguage
  no : BitLanguage
  disjoint : ∀ bits, yes bits → no bits → False

def gapCVP400Promise : PromiseProblem where
  yes := yesLanguage
  no := noLanguage
  disjoint := by sorry

structure PromiseReduction (language : BitLanguage) (problem : PromiseProblem) where
  map : List Bool → List Bool
  polynomial_time : Nonempty
    (BitTM map)
  completeness : ∀ input, language input → problem.yes (map input)
  soundness : ∀ input, ¬ language input → problem.no (map input)

def IsNPHardPromise (problem : PromiseProblem) : Bool :=
  @decide
    (∀ language : BitLanguage,
      IsNP language → Nonempty (PromiseReduction language problem))
    (Classical.propDecidable _)

theorem gapCVP400IsNPHard : IsNPHardPromise gapCVP400Promise := by
  sorry

structure BinaryNearestCodewordInstance where
  blockLength : ℕ
  generatorRank : ℕ
  generator : Fin blockLength → Fin generatorRank → ZMod 2
  target : Fin blockLength → ZMod 2
  radius : ℕ

def encodeBinaryNearestCodewordInstance
    (record : BinaryNearestCodewordInstance) : List Bool :=
  encodeAtomic record.blockLength ++
    encodeAtomic record.generatorRank ++
    encodeAtomic record.radius ++
    encodeFinValues record.blockLength
      (fun index => ((record.target index).val : ℤ)) ++
    encodeMatrixRows record.blockLength record.generatorRank
      (fun row column => ((record.generator row column).val : ℤ))

def binaryNearestCodeword
    (record : BinaryNearestCodewordInstance)
    (coefficients : Fin record.generatorRank → ZMod 2) :
    Fin record.blockLength → ZMod 2 :=
  fun index => ∑ column : Fin record.generatorRank,
    record.generator index column * coefficients column

def binaryNearestTarget (record : BinaryNearestCodewordInstance) :
    Fin record.blockLength → ZMod 2 :=
  record.target

noncomputable def binaryCodeGapFactor (blockLength : ℕ) : ℝ :=
  (blockLength : ℝ) ^ ((1 : ℝ) / 200)

noncomputable def binaryNearestCodewordPromise : PromiseProblem where
  yes bits :=
    @decide
      (∃ record : BinaryNearestCodewordInstance,
        encodeBinaryNearestCodewordInstance record = bits ∧
        0 < record.blockLength ∧ 0 < record.radius ∧
        ∃ coefficients : Fin record.generatorRank → ZMod 2,
          hammingNorm
            (binaryNearestTarget record -
              binaryNearestCodeword record coefficients) ≤ record.radius)
      (Classical.propDecidable _)
  no bits :=
    @decide
      (∃ record : BinaryNearestCodewordInstance,
        encodeBinaryNearestCodewordInstance record = bits ∧
        0 < record.blockLength ∧ 0 < record.radius ∧
        ∀ coefficients : Fin record.generatorRank → ZMod 2,
          binaryCodeGapFactor record.blockLength *
              (record.radius : ℝ) <
            (hammingNorm
              (binaryNearestTarget record -
                binaryNearestCodeword record coefficients) : ℝ))
      (Classical.propDecidable _)
  disjoint := by sorry

theorem binaryNearestCodewordIsNPHard :
    IsNPHardPromise binaryNearestCodewordPromise := by
  sorry

structure BinarySyndromeDecodingInstance where
  checkCount : ℕ
  blockLength : ℕ
  parityCheck : Fin checkCount → Fin blockLength → ZMod 2
  syndrome : Fin checkCount → ZMod 2
  radius : ℕ

def encodeBinarySyndromeDecodingInstance
    (record : BinarySyndromeDecodingInstance) : List Bool :=
  encodeAtomic record.checkCount ++
    encodeAtomic record.blockLength ++
    encodeAtomic record.radius ++
    encodeFinValues record.checkCount
      (fun row => ((record.syndrome row).val : ℤ)) ++
    encodeMatrixRows record.checkCount record.blockLength
      (fun row column => ((record.parityCheck row column).val : ℤ))

def binarySyndromeProduct
    (record : BinarySyndromeDecodingInstance)
    (word : Fin record.blockLength → ZMod 2) :
    Fin record.checkCount → ZMod 2 :=
  fun row => ∑ column : Fin record.blockLength,
    record.parityCheck row column * word column

def binarySyndromeTarget (record : BinarySyndromeDecodingInstance) :
    Fin record.checkCount → ZMod 2 :=
  record.syndrome

noncomputable def binarySyndromeDecodingPromise : PromiseProblem where
  yes bits :=
    @decide
      (∃ record : BinarySyndromeDecodingInstance,
        encodeBinarySyndromeDecodingInstance record = bits ∧
        0 < record.blockLength ∧ 0 < record.radius ∧
        ∃ word : Fin record.blockLength → ZMod 2,
          binarySyndromeProduct record word = binarySyndromeTarget record ∧
            hammingNorm word ≤ record.radius)
      (Classical.propDecidable _)
  no bits :=
    @decide
      (∃ record : BinarySyndromeDecodingInstance,
        encodeBinarySyndromeDecodingInstance record = bits ∧
        0 < record.blockLength ∧ 0 < record.radius ∧
        (∃ word : Fin record.blockLength → ZMod 2,
          binarySyndromeProduct record word = binarySyndromeTarget record) ∧
        ∀ word : Fin record.blockLength → ZMod 2,
          binarySyndromeProduct record word = binarySyndromeTarget record →
            binaryCodeGapFactor record.blockLength *
                (record.radius : ℝ) < (hammingNorm word : ℝ))
      (Classical.propDecidable _)
  disjoint := by sorry

theorem binarySyndromeDecodingIsNPHard :
    IsNPHardPromise binarySyndromeDecodingPromise := by
  sorry

noncomputable def finitePNorm (p : ℚ) {n : ℕ} (vector : Fin n → ℝ) : ℝ :=
  (∑ i : Fin n, |vector i| ^ (p : ℝ)) ^ ((p : ℝ)⁻¹)

noncomputable def finitePLatticeDiscrepancy (I : Instance)
    (vector : Fin I.dimension → ℤ) : Fin I.dimension → ℝ := fun i =>
  (I.target i : ℝ) -
    ∑ j : Fin I.dimension, (I.basis i j : ℝ) * (vector j : ℝ)

noncomputable def finitePLatticeDistance (p : ℚ) (I : Instance)
    (vector : Fin I.dimension → ℤ) : ℝ :=
  finitePNorm p (finitePLatticeDiscrepancy I vector)

noncomputable def finitePGapFactor (p : ℚ) (I : Instance) : ℝ :=
  (I.dimension : ℝ) ^ (((200 : ℝ) * (p : ℝ))⁻¹)

noncomputable def finitePGapCVPPromise (p : ℚ) (hp : 1 ≤ p) : PromiseProblem where
  yes bits :=
    @decide
      (∃ I : Instance,
        encodeInstance I = bits ∧
          wellFormed I ∧
          ∃ vector : Fin I.dimension → ℤ,
            finitePLatticeDistance p I vector ≤ (I.radius : ℝ))
      (Classical.propDecidable _)
  no bits :=
    @decide
      (∃ I : Instance,
        encodeInstance I = bits ∧
          wellFormed I ∧
          ∀ vector : Fin I.dimension → ℤ,
            finitePGapFactor p I * (I.radius : ℝ) <
              finitePLatticeDistance p I vector)
      (Classical.propDecidable _)
  disjoint := by sorry

theorem finitePNormGapCVPIsNPHard (p : ℚ) (hp : 1 ≤ p) :
    IsNPHardPromise (finitePGapCVPPromise p hp) := by
  sorry

end GapCVP.Comparator

end