GapCVP hardness below exponent 1/2

This repository contains a Lean 4 formalization of the following result:

For every fixed real constant c with 0 < c < 1/2, integer-target GapCVP with approximation factor N^c is NP-hard, where N is the dimension of the lattice instance.

The formalization extends the GapCVP framework in OpenAI's ten-proofs, imported by Lean under the package name autograd-experiments and pinned at commit 94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6. It uses that development's instance encoding, promise-problem framework, Turing-machine model, and NP-hardness theorem for 3-SAT. The reduction establishing the bound above is proved independently of OpenAI's N^(1/400) GapCVP reduction.

For a self-contained mathematical account of the construction and soundness argument, see THEOREM_NOTE.md.

Formal statement

The main theorem is CVPFormalization/MainTheorem.lean:

def HardnessBelowHalf : Prop :=
  ∀ c : ℝ, ∀ hc : 0 < c, c < (1 : ℝ) / 2 →
    GapCVP.NPHardPromise
      (OpenAI.integerTargetGapPromiseAt c (le_of_lt hc))

theorem integerTargetGapCVP_hardnessBelowHalf : HardnessBelowHalf

The promise restricts both YES and NO instances to integer targets. A YES instance has distance at most the stated radius; in a NO instance, every lattice vector has distance greater than N^c times that radius.

As a compatibility check, the same file specializes the theorem to c = 1/400 and proves exactly the integer-target proposition defined in the pinned OpenAI development:

theorem integerTargetGapCVP_recoversOpenAIOneDiv400 :
  GapCVP.NPHardPromise
    GapCVP.Factor400BinaryPaperVariableArityUnconditionalPhysicalSourceMachine.integerTargetGapCVP400Promise

This theorem is obtained by specializing integerTargetGapCVP_hardnessBelowHalf; thus the generalized argument supplies an alternative proof of OpenAI's exact proposition.

Proof outline

1. Reduce 3-SAT to a sparse quadratic system over F₂, with power-of-two padding that preserves satisfiability.
2. Encode the quadratic system as a folded residual constraint system over binary extension fields. Seven families of equations enforce the Reed–Solomon, folding, Frobenius, identifier, source, symmetry, and oddness conditions.
3. Prove completeness by constructing a low-weight residual solution from a satisfying assignment. Prove soundness by combining synchronization, coefficient-isolation, and rank/minor arguments to recover a satisfying source assignment from any sufficiently low-weight residual solution.
4. Choose the folding and radix parameters so that the resulting gap, expressed in terms of the final lattice dimension, exceeds N^c for any prescribed c < 1/2.
5. Give polynomial-time algorithms for the required field arithmetic and for the coefficients of every residual-row family. The binary fields are built as explicit Artin–Schreier towers, and closed-form moment identities provide succinct access to the residual system.
6. Serialize the residual system as a binary affine system, choose a canonical basepoint, and apply Construction A. The resulting lattice instance has an integer target, and its Euclidean distance realizes the required Hamming weight gap.
7. Package the construction as a polynomial-time bit Turing machine and compose it with the formalized NP-hardness reduction from 3-SAT.

Reading guide

The shortest route through the final argument is:

1. CVPFormalization/MainTheorem.lean chooses the exponent schedule and applies the uniform reduction certificate.
2. CVPFormalization/Complexity/ConcreteUniformReduction.lean assembles the executable reduction, completeness and soundness results, and the integer-target lattice construction.
3. CVPFormalization/Complexity/ResidualConcreteCheckMachineTM.lean supplies the concrete coefficient procedure for the seven residual-row families.

The source tree is organized as follows:

• CVPFormalization/Source: 3-SAT and sparse-quadratic source reductions.
• CVPFormalization/Algebra: finite fields, extension towers, and rank algebra.
• CVPFormalization/Compiler: the residual system and its executable semantics.
• CVPFormalization/Soundness: synchronization, coefficient isolation, and rank recovery.
• CVPFormalization/Lattice: Construction A and the integer-target argument.
• CVPFormalization/Complexity: parameter bounds, serializers, coefficient machines, and the uniform polynomial-time reduction.
• CVPFormalization/OpenAI: interfaces to the pinned OpenAI definitions.

Build and verification

Install Lean using elan, then run:

git clone git@github.com:Mira-acc/cvp.git
cd cvp
lake update
lake build

The project pins Lean and Mathlib to v4.32.0. A cold build also compiles the large pinned OpenAI module and can therefore take some time; later builds reuse Lean's cached artifacts.

To inspect the axioms of the main theorem and its principal certificates, run:

lake env lean AxiomAudit.lean

Lean reports only propext, Classical.choice, and Quot.sound. In particular, the final results do not depend on sorryAx; the source tree contains no sorry, admit, custom axiom, or unsafe declaration.