Improving a hardness bound by balancing the costs

A lattice is the set of all integer combinations of some basis vectors. The closest vector problem asks how near a given target lies to that set. In its approximate decision form, the task is to distinguish a nearby target from one that is farther away by a specified factor. A hardness theorem says that solving this promised distinction efficiently would also solve a problem such as Boolean satisfiability efficiently.

The exponent in a dimension-dependent factor matters. A factor of $n^{1/30}$ grows faster than $n^{1/400}$, so hardness for the former excludes a broader approximation guarantee as the dimension grows. Neither statement promises a practical instance generator: the polynomial degrees in the construction here are enormous.

This article revisits the parameter choices in OpenAI’s $n^{1/400}$-Hardness of the Euclidean Closest Vector Problem. That reduction encodes Boolean assignments into a binary system and then converts binary Hamming weight into squared Euclidean distance. We retain that construction and its algebraic reconstruction lemmas. The change is in how its numerical costs are balanced.

Why does squaring matter? Suppose the lattice distance must exceed $M^c$ times the yes-instance radius. Since the lift turns binary weight into squared distance, its binary soundness statement needs a factor $M^{2c}$. Losing the factor two at this interface would give the wrong approximation exponent.

The construction has three adjustable scales. A larger field provides room to avoid exceptional evaluation points. A larger support cutoff permits more candidate values at a point. A larger moment horizon gives the algebraic reconstruction more equations. Increasing one scale may make another obligation harder, so the parameters must be chosen together.

Write their polynomial exponents as $Q,\kappa,\tau$. The retained proof obligations become

$$\kappa>1+2c(1+2Q),\qquad \tau>1+5\kappa,\qquad Q>1+2\kappa+\tau.$$

We can see the limiting exponent without carrying the whole reduction at once. The last two inequalities force $Q>2+7\kappa$. Substituting this into the first gives

$$\kappa>1+10c+28c\kappa,$$

so $(1-28c)\kappa>1+10c$. For $c\ge 1/28$ this is impossible. Below that value, sufficiently large choices with slack work. This proves a boundary for these retained inequalities. It does not prove that some different reduction cannot achieve a larger exponent.

For the concrete value $c=1/30$, choose $(Q,\kappa,\tau)=(242,34,172)$. The three margins are respectively $2/3$, $1$, and $1$. These positive margins leave room for finite coefficients, which must still be checked. For example, the discarded-support estimate reduces to $16^{15}\cdot40<N^{10}$, valid already at the construction’s baseline $N=100$. An asymptotic exponent comparison alone would not establish that finite claim.

The rest of the article explains where each inequality comes from and follows it through the reduction. Its formal-verification statements refer to the archived development identified below: the concrete reduction and the general parameter-feasibility theorem have different scopes. The argument for the full range of exponents is written out mathematically; the archived concrete executable specialization is $c=1/30$.

1 Introduction

OpenAI’s paper $n^{1/400}$-Hardness of the Euclidean Closest Vector Problem gives a deterministic polynomial-time many-one reduction from $3$SAT to Euclidean CVP with approximation factor $n^{1/400}$ [1]. Its main technical step is a binary affine system whose low-weight solutions encode satisfying assignments. The system uses one-hot evaluation tables over a characteristic-two field. Its soundness proof reconstructs algebraic root sets from polynomial moments, recovers Boolean values by valuations, and matches a common root across the clause tables. A dimension-preserving parity lift converts binary weight into squared Euclidean distance.

This note changes the numerical specialization of that construction. It is written as a companion to the OpenAI paper: the notation and the order of the encoding, reconstruction, soundness, and transfer arguments are kept so that the two proofs can be read in parallel.

The parameterization and elimination were developed in FPRD Lab—Finitely Presented Recognition Dynamics—an Insight Forge Boxlab project. Its mathematical contribution was to recast the source’s fixed hierarchy as a system of coupled resource coordinates and then eliminate the internal coordinates to expose the feasible exponent range. Section 7.2 states this procedure explicitly and distinguishes it from the source lemmas retained unchanged.

1.1 Main result

For a nonsingular integer matrix $B\in\mathbb Z^{n\times n}$, write $L(B)=B\mathbb Z^n$. An instance of $\mathsf{GapCVP}^{(2)}_\gamma$ consists of $B$, a target $t\in\mathbb Q^n$, and a positive rational radius $r$. The promise is to distinguish $$\operatorname{dist}_2(t,L(B))\le r \quad\text{from}\quad \operatorname{dist}_2(t,L(B))>\gamma(n)r.$$

For $c=1/30$, the proof has the explicit specialization $$Q=242,\qquad \kappa=34,\qquad \tau=172, \tag{1}$$ where $q\asymp N^Q$, $K=N^\kappa$, and $T=N^\tau$. The resulting binary block length and lattice rank satisfy $$M=n\le40N^{485}. \tag{2}$$

The strict retained resource inequalities have no solution at $c\ge1/28$. This establishes a frontier for the present one-hot representation and the present reconstruction and valuation bounds. It is not a lower bound on the exponent attainable by a different reduction.

1.2 Proof overview and relation to the source paper

The reduction continues to factor through binary nearest codeword: $$3\mathrm{SAT}\longrightarrow \text{binary nearest codeword}\longrightarrow \text{Euclidean CVP}.$$ The comparison with the OpenAI proof is as follows.

1. Encoding and completeness (Section 3). The table types, one-hot coordinates, ordinary and shifted power-sum constraints, and satisfying-assignment solution are unchanged. The retuning changes only the fixed field, support, and moment exponents in the source’s Section 3.5.

2. Algebraic reconstruction (Section 4). OpenAI’s Lemma 10 is invoked without alteration. The retuning verifies its three numerical hypotheses with a larger support cutoff and moment horizon.

3. Nearest-codeword soundness (Section 5). As in the source, large pointwise support fibers are discarded separately for each table type. The available field is divided explicitly between those fibers and the anchor and Hankel-discriminant losses. The shifted-moment valuation and clause-root matching arguments are then unchanged.

4. Transfer to CVP (Section 6). The source parity lift identifies minimum binary weight with squared Euclidean distance. Thus binary exponent $2c$ becomes Euclidean exponent $c$, with lattice rank equal to binary block length.

1.3 Scope of the formal verification

The complete executable Lean reduction is checked for the concrete exponent $c=1/30$, including the physical binary system, integer target, polynomial-time machines, and final NP-hardness statements. A separate Lean module proves that the retained resource inequalities admit natural-number witnesses for every real $0\le c<1/28$ and admit none at or above $1/28$. The complete reduction has not been uniformly parameterized in Lean for arbitrary $c$; the general statement in theorem 1 is the mathematical retuning proved below.

2 Retuned parameters and retained construction

After the preprocessing used in the source, let the formula have $s$ symbols, $m$ variables, and $\ell$ clauses, and put $$N=100+s+m+\ell,\qquad d=m. \tag{3}$$ Choose the least integer $e$ for which $2^e\ge N^Q$, and let $$q=2^e,\qquad N^Q\le q<2N^Q,\qquad \mathbb K=\mathbb F_q. \tag{4}$$ The support cutoff and moment horizon are $$K=N^\kappa,\qquad T=N^\tau. \tag{5}$$ Here $\mathbb K$ denotes the field and $K$ the integer support cutoff.

Let $a_1,\ldots,a_m\in\mathbb K$ be distinct anchors and $P=\mathbb K\setminus\{a_1,\ldots,a_m\}$. Let $\Theta$ be the set consisting of the global table type and the satisfying local assignment types for each clause. As in the source, $$|\Theta|\le1+8\ell\le9N, \qquad M=|\Theta||P|q.$$

For a desired Euclidean exponent $c$, four asymptotic costs control the retuning: $$\begin{aligned} M&\le40N^{1+2Q}, \qquad\text{(6)}\\ \kappa&>1+2c(1+2Q), \qquad\text{(7)}\\ \tau&>1+5\kappa, \qquad\text{(8)}\\ Q&>1+2\kappa+\tau. \qquad\text{(9)} \end{aligned}$$ The first line is the dense one-hot cost. The second makes $K$ dominate the support discarded from a binary solution of weight $O(M^{2c}R)$. The third provides all shifted moments used by the valuation argument. The fourth keeps the cleared reconstruction degree below the field size. The exact constants needed in addition to these exponent inequalities are recorded in section 5.

3 Encoding Boolean assignments by Reed–Solomon codes

For every table type $\theta\in\Theta$, evaluation point $p\in P$, and value $w\in\mathbb K$, the source construction has a binary coordinate $x_{\theta,p,w}$. Its ordinary and shifted power-sum constraints, expanded in an $\mathbb F_2$-basis of $\mathbb K$, form the same explicit affine system $$Hx=b\qquad\text{over }\mathbb F_2. \tag{10}$$ No coefficient or equation in this system is changed by the retuning.

3.1 Completeness

OpenAI’s Lemma 8 applies verbatim. If $\varphi$ is satisfiable, the one-hot graph of its interpolation polynomial, together with one active local table for each clause, gives a solution of weight $$R=(\ell+1)|P|. \tag{11}$$ Because equation (3) gives $\ell+1\le N$ and $|P|<q$, $$R\le Nq. \tag{12}$$ For the Euclidean reduction, set $r=\lceil\sqrt R\rceil$. Since $R\ge1$, $$r^2\le4R\le4Nq. \tag{13}$$ This exact estimate is used in the finite-$N$ soundness calculation.

3.2 Dimension and construction size

From $|P|<q<2N^Q$ and $|\Theta|\le9N$, $$M=|\Theta||P|q\le40N^{1+2Q}. \tag{14}$$ The source’s row count becomes $$|P|+\ell|P|q+4|\Theta|(T+1)|P|e =O\!\left(N^{1+2Q}+N^{1+Q+\tau}\log N\right). \tag{15}$$ For fixed $Q$ and $\tau$, both the system and the field construction remain deterministic polynomial time. At equation (1), the two exponents in equation (15) are $485$ and $415$, respectively.

4 Algebraic reconstruction of bounded polynomial-moment families

OpenAI’s Lemma 10 is independent of the Boolean encoding. For a family of sets $S(p)\subseteq\mathbb K$ with $|S(p)|\le K$, it reconstructs a separable polynomial over $\mathbb K(X)$ from power sums through degree $T$. We use that lemma exactly as stated.

For a retained evaluation set $P_\theta$, its numerical hypotheses are $$T\ge2K-1,\qquad dT<|P_\theta|,\qquad |P_\theta|-dK(K-1)>2dK^2T. \tag{16}$$ The term $dK(K-1)$ bounds the zeros of the Hankel determinant. The term $2dK^2T$ is the degree range needed after clearing denominators. These are the only places where the retuned values enter Lemma 10’s application. The lemma’s construction of a common splitting field and its root-moment identities are unchanged.

5 Soundness of the nearest-codeword reduction

Suppose that $x\in\mathbb F_2^M$ solves equation (10) and $$\operatorname{wt}(x)\le4M^{2c}R. \tag{17}$$ For each type $\theta$ and point $p$, let $$S_\theta(p)=\{w\in\mathbb K:x_{\theta,p,w}=1\}.$$ The proof follows the five parts of the source’s Section 5.

5.1 Pointwise support sets of a low-weight solution

For each table type separately, retain $$P_\theta=\{p\in P:|S_\theta(p)|\le K\}.$$ Markov’s inequality and equations (12) and (17) give $$|P\setminus P_\theta| \le\frac{4M^{2c}R}{K} \le\frac{4M^{2c}Nq}{K}. \tag{18}$$ Thus the exact sufficient condition $$16M^{2c}N<K \tag{19}$$ makes the discarded set smaller than $q/4$. The sets $P_\theta$ may differ; they are never intersected over all table types.

At the concrete parameters, equation (19) follows from $$16(40N^{485})^{1/15}N<N^{34}. \tag{20}$$ Raising both sides to the fifteenth power reduces this to $$16^{15}\cdot40<N^{10}, \tag{21}$$ which holds already at $N=100$ and remains true for larger $N$.

5.2 Applying the reconstruction lemma

Reserve a second quarter of the field for the anchors and the zeros of the Hankel determinant. It is enough that $$4\bigl(m+dK(K-1)\bigr)<q. \tag{22}$$ Together with equations (18) and (19), this gives $$|P_\theta|-dK(K-1)>q/2. \tag{23}$$ The remaining reconstruction and interpolation requirements follow from $$4dK^2T<q,\qquad 2dT<q,\qquad T\ge2K-1. \tag{24}$$ Indeed, equations (23) and (24) imply all three conditions in equation (16).

For equation (1), using $d,m\le N$ and $q\ge N^{242}$, the exact checks are $$\begin{aligned} 4\bigl(N+N^{69}\bigr)&<N^{242}, \qquad\text{(25)}\\ 4N^{241}&<N^{242}, \qquad\text{(26)}\\ 2N^{173}&<N^{242}, \qquad\text{(27)}\\ N^{172}&\ge2N^{34}-1. \qquad\text{(28)} \end{aligned}$$ All hold for $N\ge100$. Hence Lemma 10 reconstructs the root sets by the same per-table argument as in the source proof and places them in one common splitting field.

5.3 Valuative recovery of local assignments

OpenAI’s Lemma 12 studies, for a reconstructed root $\alpha$ and a clause bit $\beta_i$, $$y=\frac{\alpha-\beta_i}{X-a_i}.$$ If $h\le K$ is the number of roots of the table polynomial, the proof defines $$D_0=dh^2+h,\qquad U_h=h^2D_0+dh^2+1,\qquad z=hU_h+1.$$ The unchanged estimates give $$D_0\le2N^{1+2\kappa},\qquad U_h\le4N^{1+4\kappa},\qquad z+h-1\le5N^{1+5\kappa}. \tag{29}$$ Thus $5N^{1+5\kappa}<T$ supplies every shifted moment required by the valuation argument. At the concrete values, $$5N^{171}<N^{172}=T \tag{30}$$ for $N\ge100$. The conclusion of Lemma 12, that each local root recovers the prescribed bit at the corresponding anchor valuation, is therefore unchanged.

5.4 Clause matching

The source parity argument uses ordinary moments to match every global root to at least one satisfying local root set for each clause. Since a clause has at most eight satisfying local assignments, the Vandermonde system has size at most $$(1+|B_C|)K\le9K.$$ The sufficient condition is $9K<T+1$. At the concrete parameters the stronger inequality $$9N^{34}<N^{172}=T \tag{31}$$ holds. OpenAI’s Lemma 13 therefore applies without alteration.

5.5 Completing soundness and exact constants

The preceding bounds give the retuned form of OpenAI’s Proposition 14.

The exponent inequalities control growth rates; the finite coefficients enter through the quarter-field allocation in equations (19) and (22) and the exact source estimate equation (13). Together they give the coefficient-$16$ condition in equation (20), which equation (21) verifies already at $N=100$. This exact bookkeeping does not change the affine system, reconstruction lemma, valuation argument, or parity lift.

The OpenAI paper states Proposition 14 with coefficient $4$. The imported Lean snapshot exposed coefficient $2$ at one binary wrapper, although its factor-$n^{1/200}$ output theorem only needed coefficient $1$. This is a source/interface discrepancy, not a failure of OpenAI’s final theorem. The retuned formalization carries coefficient $4$ through the explicit and physical binary interfaces so that proposition 2 is available for the Euclidean transfer.

6 Transfer to CVP and complexity

OpenAI’s parity lift maps a consistent affine system $Hx=b$ to an integer lattice $L(B_H)$ and a binary target $u$ with $$\operatorname{dist}_2(u,L(B_H))^2 =\min\{\operatorname{wt}(x):x\in\mathbb F_2^M,\ Hx=b\}. \tag{32}$$ The lattice has rank $n=M$. The preprocessing and inconsistent-system branches use the same fixed one-dimensional instances as the source.

If $\varphi$ is satisfiable, equations (11) and (32) give distance at most $\sqrt R\le r$. If $\varphi$ is unsatisfiable and the distance were at most $M^c r$, then $$\operatorname{dist}_2(u,L(B_H))^2 \le M^{2c}r^2 \le4M^{2c}R.$$ By equation (32), this would give a binary solution excluded by proposition 2. Hence $$\operatorname{dist}_2(u,L(B_H))>M^c r=n^c r,$$ with the strict inequality required by the promise problem.

At the concrete values, the field extension degree is $e=O(\log N)$, the affine system has $M\le40N^{485}$ variables and $O(N^{485})$ rows, and the square parity-lift basis has fixed-polynomial encoding length. Field construction, Reed–Solomon checks, Gaussian elimination, serialization, and basis construction therefore remain deterministic polynomial-time operations. The exponents are large, but none depends on the input.

This proves the concrete case of theorem 1. The binary gap in proposition 2 also gives the following source-parallel consequence.

7 Further consequences and verification

7.1 The retained parameter frontier

Eliminating $\tau$ and $\kappa$ from equations (7), (8), and (9) gives $$Q>2+7\kappa >2+7\bigl(1+2c(1+2Q)\bigr),$$ and therefore $$(1-28c)Q>9+14c. \tag{33}$$ For $c\ge1/28$ and $Q\ge0$, the left side is nonpositive and the right side is positive. Thus the retained strict inequalities are infeasible at and above $1/28$.

Conversely, fix $0\le c<1/28$. For sufficiently large integer $Q$, the interval $$\left[2+2c(1+2Q),\frac{Q-4}{7}\right] \tag{34}$$ contains an integer $\kappa$. Set $\tau=2+5\kappa$. Then $$\kappa>1+2c(1+2Q),\qquad \tau>1+5\kappa, \qquad 1+2\kappa+\tau<Q.$$ These choices leave at least one full power of $N$ in the support, valuation, and reconstruction comparisons. Since $N\ge100$ and $16\cdot40^{2c}<100$ for $c<1/28$, the exact support coefficient is also absorbed. The lower-order anchor, Hankel, interpolation, and parity conditions then follow. This proves theorem 1 for every fixed $c<1/28$.

7.2 FPRD method and provenance

The resource decomposition and frontier calculation are the specific mathematical contribution of FPRD Lab—Finitely Presented Recognition Dynamics. They form a parameter audit of the OpenAI construction, not a new construction. OpenAI supplies the one-hot encoding, moment reconstruction, valuation argument, clause matching, and parity lift. FPRD Lab supplied the resource decomposition, the elimination argument, and the concrete specialization. Exact and formal audits verify these outputs. In the lab’s terminology, this is an algebraic-sewing and resource-compression audit: local proof obligations are retained, while their shared resource coordinates are composed and then eliminated according to the final readout.

Resource-audit procedure.

The analysis is organized as the following reusable procedure.

1. Fix the external readout. State the desired approximation factor in the final dimension, then propagate it backward through every transfer. Here the squared-distance parity lift turns the Euclidean factor $M^c$ into a binary weight scale $M^{2c}$.

2. Expose independent coordinates. Replace the source’s chosen powers by one coordinate for each proof budget. Here $q$ measures the available evaluation field, $K$ bounds each retained support, $T$ is the moment horizon, and $M$ is the external representation size. No relation among their growth rates is assumed at this stage.

3. Extract the source obligations. Read the proof in dependency order and record every quantitative premise that connects two coordinates. Keep leading exponents separate from fixed constants and from losses at the smallest input size.

4. Eliminate and instantiate. Write $q\asymp N^Q$, $K=N^\kappa$, and $T=N^\tau$. Eliminate the internal coordinates to obtain the feasible range for $c$, then choose an integral tuple with explicit slack.

5. Certify the endpoint. Restore the finite constants, check the smallest allowed $N$, and push the tuple through the actual executable construction. Report the verified concrete endpoint separately from the symbolic frontier.

Application to this reduction.

The first step gives the low-weight threshold $4M^{2c}R$ in equation (17). The next two steps extract the leading dependency chain $$M\asymp q^2,\qquad K\gtrsim M^{2c}, \qquad T\gtrsim K^5,\qquad q\gtrsim K^2T.$$ The suppressed powers of $N$ become the constant terms in equations (7), (8), and (9). Eliminating $\kappa$ and $\tau$ makes $(1-28c)Q>9+14c$ visible. It gives the retained range $c<1/28$ and guides the choice $(Q,\kappa,\tau)=(242,34,172)$ at $c=1/30$.

The certification step uses the quarter-field allocation in equations (19) and (22) and the exact radius estimate in equation (13) to obtain the coefficient-$16$ margin. The Lean development checks the complete concrete endpoint. It separately checks the symbolic retained frontier, without claiming one uniformly parameterized executable reduction for every $c<1/28$.

The same elimination also identifies which retained costs control the answer. If a related construction has $$M\asymp q^a,\qquad T\gtrsim K^v,\qquad q\gtrsim K^rT,$$ the same leading-exponent elimination gives $$c<\frac{1}{2a(r+v)}. \tag{35}$$ The present values are $a=2$, $r=2$, and $v=5$. The factor $28$ therefore records three separate costs: squaring in the Euclidean transfer, the dense one-hot $q^2$ representation, and the combined seventh power of $K$ in valuation and reconstruction. This also separates three attack seams. A more economical representation reduces $a$; a sharper valuation lemma reduces $v$; and a lower-degree cleared-reconstruction identity reduces $r$.

FPRD Lab is an Insight Forge Boxlab project (https://gitlab.com/insight-forge/boxlab) that begins with recognition-theoretic constructions and asks how their structural and resource tradeoffs transfer to other settings. Here that lens was applied to the parameter dependencies in the direct GapCVP reduction; no source reconstruction or valuation lemma was changed.

The lab also served as a testing and training bed for Sidecat (https://gitlab.com/sidecat-dev/sidecat), the agent-work system used to coordinate the AI-assisted work and preserve its evidence and publication record. That operational provenance affected the mathematical outcome. The FPRD parameter search produced the $1/30$ specialization and $1/28$ frontier. The retained dependency record, exact arithmetic audit, and independent Lean development established the finite-$N$ margins and verified the complete concrete endpoint.

7.3 Lean verification

The independent formal audit uses OpenAI source commit 94bc0feb6a9f and is published at fork commit 3ac608981eb4 [3]. The bibliography gives the complete immutable fork revision. The complete retuned build reaches the physical integer-target theorem and the two factor-$1/15$ binary endpoints. The frontier module proves natural-number witnesses below $1/28$ and impossibility at and above it.

The principal axiom probes report only propext, Classical.choice, and Quot.sound. The modified proof files contain no sorry, admit, sorryAx, or new axiom declaration. The principal source-to-check correspondence is shown in table 2.

7.4 Limits of the conclusion

The audit establishes that the selected parameters satisfy every numerical hypothesis encountered in the source proof and its executable Lean specialization. It does not replace the source reconstruction and valuation lemmas with an independent proof. The complete formal reduction is presently instantiated only at $c=1/30$; the formal result for arbitrary real $c<1/28$ concerns the retained resource inequalities. A uniformly parameterized Lean version of the complete reduction would narrow this remaining distinction.

The value $1/28$ is correspondingly an unattained supremum of the retained parameter system. It should not be interpreted as an optimal hardness exponent for Euclidean CVP or as an obstruction to a different direct construction.

Reproducibility

The exact integer-arithmetic certificate and its canonical output are published in the FPRD Lab reproduction package [2]. The independent Lean fork records the imported source revision, modified paths, complete build logs, source hashes, and axiom output [3]. These two checks are complementary: the small certificate evaluates the seven concrete finite-$N$ side conditions reported in its output, while Lean checks that the concrete values reach the actual executable reduction and final promises.