LP hardness of approximation for polynomial-time solvable problems

Contributed by Sebastian Pokutta
Published 2026-10-20 · last changed in 29ff25c
License: CC BY 4.0

@misc{lemmata:2610.00004,
  title        = {LP hardness of approximation for polynomial-time solvable problems},
  author       = {Sebastian Pokutta},
  howpublished = {Lemmata Repository, lemmata:2610.00004, \url{https://lemmata.iol.berlin/abs/2610.00004}},
  year         = {2026},
  url          = {https://lemmata.iol.berlin/abs/2610.00004},
  note         = {Version a9429cb9cbf5; formal statements checked in Lean 4}
}

Polynomial-time optimization does not imply the existence of a small LP formulation. This contribution gives approximation-preserving reductions for four problems: minimum-cost perfect matching, minimum-cost $T$ -join, minimum odd cut, and minimum-cost odd-red bipartite perfect matching. Each problem admits an exact polynomial-time algorithm. Nevertheless, shifted matching matrices yield strong lower bounds on a common LP formulation supporting all objectives.

We give the four applications together with the factorization argument that underlies them. The Lean development includes the actual graph and matching domains, objective sums, attaining solutions, and reductions. The published matching-matrix rank bound is an explicit theorem hypothesis. For parity matching, Lean also proves the new finite extension of the rectangle argument, from explicitly stated hypotheses describing the Jia–Svensson–Yuan partition framework. No external theorem is introduced as a Lean axiom.

For every fixed $\alpha>1$ , the implications are as follows. Here $n$ is the number of vertices in the first three rows and the number of vertices in each bipartition class in the last row.

Problem	Restricted objectives	Lower bound on LP size	Nonnegative-rank lower bound used
Minimum-cost perfect matching	Strictly positive metric costs on $K_n$	$2^{\Omega_\alpha(n)}$	Shifted ordinary matching matrix
Minimum-cost $T$ -join	$T=V(K_n)$ , the same metric costs	$2^{\Omega_\alpha(n)}$	Shifted ordinary matching matrix
Minimum odd cut	Weights in $\{0,1\}$ on $K_n$	$2^{\Omega_\alpha(n)}$	Transpose of the shifted ordinary matching matrix
Minimum-cost odd-red bipartite perfect matching	Positive costs on a fixed two-colored complete bipartite multigraph	$2^{\Omega_\alpha(n)}$	Shifted parity-matching matrix

The first three applications use the exponential nonnegative-rank bound for the shifted odd-cut versus perfect-matching matrix proved by Braun and Pokutta. The fourth uses a different matrix, from Jia, Svensson, and Yuan. Their published exact bound alone does not give the shift needed for a fixed-factor approximation. Below we prove the required extension; Lean checks its new construction, charging estimate, and finite rank consequence, while their partition and entropy assertions remain explicit hypotheses.

Formulations and source matrices¶

Fix a set $I$ of instances, a set $X$ of solutions, and objective values $v(i,x)$ . An $\alpha$ -approximate formulation for this minimization problem has one polyhedron $P$ , with $m$ inequalities, a realization $z_x\in P$ for every solution, and an affine objective $\ell_i$ for each instance such that

\ell_i(z_x)=v(i,x),\qquad \inf_{z\in P}\ell_i(z)\ge \frac{\operatorname{OPT}(i)}{\alpha}.

(1)

Both $P$ and the realization $x\mapsto z_x$ are independent of the instance. The encoding is otherwise arbitrary. Equations can be removed by parametrizing their affine solution space and do not count toward $m$ . The lower bounds concern this model, which allows arbitrary extended formulations. They do not bound the running time of an algorithm. For the usual rational-input model, it suffices to use a fixed rational approximation factor: hardness for any rational factor larger than a given real $\alpha$ also rules out an $\alpha$ -approximate formulation. The resulting cost families have rational entries of polynomial encoding length.

Write $r_+(S)$ for the nonnegative rank of a real matrix $S$ : the least number of nonnegative rank-one summands, or $\infty$ if no finite factorization exists. The Lean definition is shared with the spanning-tree contribution.

For even $n$ , let $\mathcal U_n$ be the odd subsets of $[n]$ and let $\mathcal M_n$ be the perfect matchings of $K_n$ . Set

q_n(U,M)=|\delta(U)\cap M|, \qquad Q_{n,r}(U,M)=q_n(U,M)-r.

(2)

The theorem of Braun and Pokutta used here states that

r_+(Q_{n,r})=2^{\Omega_r(n)} \quad\text{for every fixed }0<r<1.

(3)

In Section 2.2.3 and the proof of Theorem 3.1 of Braun and Pokutta, the relevant submatrix has entries $(q_n-1+\beta)/2$ for fixed $0<\beta<1$ . Taking $\beta=1-r$ and rescaling gives the stated nonnegative-rank bound. Rothvoss’s exact matching bound corresponds to $r=1$ ; it is not by itself a bound for $r<1$ .

We use the formulation-complexity factorization theorem in its usual affine Farkas form, as in Braun, Pokutta, and Zink and Braun, Pokutta, and Roy. For precision, the formalization starts from the certificate data: if $P=\{z:s_l(z)\ge0,\ 1\le l\le m\}$ and $\beta_i$ is the claimed objective bound, it assumes nonnegative coefficients $y_{il},\kappa_i$ with

\ell_i(z)-\beta_i =\sum_{l=1}^m y_{il}s_l(z)+\kappa_i \quad\text{for all }z.

(4)

The Lean structure CertifiedLP contains the inequalities, feasible realizations, exact objective values, and this identity. The existence of these certificates from validity on a finite-dimensional polyhedron is the external affine Farkas theorem.

In each application below, $L$ is a nonnegative integer. A source bound $L\le r_+(S)$ therefore gives $L\le m+1$ . Substituting an exponential source bound gives the corresponding exponential lower bound on formulation size.

Minimum-cost perfect matching¶

Let $n\ge2$ be even, put $H=n/2$ , and fix $\alpha>1$ . For $U\in\mathcal U_n$ give the edges of $K_n$ costs

c^U_e=1+\lambda\,\mathbf1[e\in\delta(U)], \qquad \lambda=(\alpha-1)n=2(\alpha-1)H.

(6)

In particular, $c^U$ is a strictly positive metric. It is also a tree metric: attach each vertex to its side’s center by an edge of length $1/2$ , and join the centers by an edge of length $\lambda$ .

Applying the bound $r_+(Q_{n,r})=2^{\Omega_r(n)}$ of Braun and Pokutta with $r=1/(2\alpha)$ gives $m=2^{\Omega_\alpha(n)}$ for every fixed $\alpha>1$ , although weighted perfect matching is polynomial-time solvable. The costs are 1 and $1+(\alpha-1)n$ . Thus their aspect ratio grows with $n$ ; this is not a bounded-aspect-ratio claim.

Minimum-cost $T$ -join¶

Again let $n\ge2$ be even and take $T=V(K_n)$ . A $T$ -join is an edge set $J$ whose odd-degree vertex set is $T$ . Use the same costs $c^U$ .

Thus minimum-cost $T$ -join has formulation size $2^{\Omega_\alpha(n)}$ already for $T=V(K_n)$ and these positive metric costs. Minimum-cost $T$ -join is polynomial-time solvable, for example through shortest-path distances and minimum-weight perfect matching on $T$ .

Minimum odd cut¶

Let $n\ge2$ be even. The solutions are now odd subsets $U$ of $[n]$ . Each perfect matching $M$ specifies an objective with edge weights $w^M_e=\mathbf1[e\in M]$ . The cost of the cut is $q_n(U,M)$ .

The resulting bound is $2^{\Omega_\alpha(n)}$ for fixed $\alpha>1$ . Polynomial-time solvability is supplied by the odd-cut algorithm of Padberg and Rao.

Minimum-cost odd-red bipartite perfect matching¶

Let $G_n$ have left vertices $u_1,\ldots,u_n$ and right vertices $v_1,\ldots,v_n$ , with one red and one blue edge between each opposite pair. A feasible solution is a perfect matching with an odd number of red edges. Equivalently, it is a permutation $\sigma$ of $[n]$ together with a Boolean color for each edge $(u_i,v_{\sigma(i)})$ , with odd total red count. This is the concrete Lean solution type ParityMatching.

Rows are Boolean labelings $a$ of the $2n$ vertices such that the number of labels equal to one is congruent to $n$ modulo two. Call an edge a violation if it is blue with equal endpoint labels or red with unequal endpoint labels. Let $t_n(a,M)$ count the violations in $M$ and put

P_{n,r}(a,M)=t_n(a,M)-r.

(9)

The nonnegative-rank bound needed for this application is

r_+(P_{n,r})=2^{\Omega_r(n)} \quad\text{for fixed }0<r<1.

(10)

The mathematical proof of this separate shifted parity-matching assertion is given in Theorem 7. The original reduction accepts this rank bound as a hypothesis. The additional Lean theorem Corollary 4 instead derives a finite lower bound from explicit partition and probability-comparison hypotheses. The argument extends the rectangle estimates of Jia, Svensson, and Yuan; their exact bound at $r=1$ alone would not suffice, and the ordinary matching bound of Braun and Pokutta concerns a different matrix.

Applying Theorem 7 gives $2^{\Omega_\alpha(n)}$ inequalities for every fixed $\alpha>1$ on a host with $2n$ vertices and $2n^2$ colored edges. All costs are positive and at most $1+2(\alpha-1)n$ . No metric restriction is asserted here. The weighted odd-red problem is deterministically polynomial-time solvable; see the discussion of weighted parity matching in Jia, Svensson, and Yuan, Section 1. The condition is an odd red count, rather than an exactly prescribed red count.

The common reduction mechanism¶

The preceding arguments use simple scaling, restriction, and transposition. The accompanying library also proves the more general reduction used in Affine reductions for LPs and SDPs and Strong reductions for extended formulations.

The maps $f$ and $g$ are independent. Dependence on both indices may occur in $A$ and $B$ , and its nonnegative factorization size is accounted for in the inequality.

Bounded additive baselines¶

Objective reversal¶

The same contribution retains the near-exact objective-reversal transfer. This auxiliary result is not needed for the four fixed-factor applications above.

Interpreting $o_i$ as the source maximum requires the corresponding upper bound and an attaining solution. The library proves optimum transfer from those additional hypotheses; the corollary does not silently assume them.

Source bound for the shifted parity matrix¶

This section proves the additional rank bound for odd-red bipartite matching. The new extension is formalized in Lean, conditional on explicit assertions from the earlier partition framework. These assertions include the small- and bad-triple estimates, Equations (4.5)–(4.6), and the permutation lemma, Lemma 4.4, of Jia, Svensson, and Yuan, Sections 4.2–4.6. Their entropy proofs and the complete outside-partition construction are not formalized here. The one-violation construction, its admissibility, the new charging estimate, conversion to finite rank bounds, numerical parameter choice, and padding are proved in Lean. The precise conditional statements appear at the end of this section.

Write $L$ for a vertex labeling and $E_L$ for its violating edges; thus $t(L,M)=t_n(L,M)=|M\cap E_L|$ and $P_{n,r}(L,M)=t(L,M)-r$ . Fix a sufficiently large integer $k$ , let $h=4k+3$ , and first take $n=4k(2s+1)+3$ , where $s$ tends to infinity. A partition consists of ordered blocks $A_1,\ldots,A_s,B_1,\ldots,B_s$ of $4k$ vertex pairs each, and an unordered core $C$ of $h$ pairs. On an ordered block $D$ , define $M_A(D)$ by the red edges $(u_i,v_{2k+i})$ and $(u_{2k+i},v_i)$ for $1\le i\le2k$ . Let $L_B(D)$ assign one to both endpoints at positions $1,\ldots,k,2k+1,\ldots,3k$ , and zero at the other positions. These matching and labeling choices have no violations.

Outside the core, fix $M_A$ on every $A$ -block and choose any labeling consistent with it; fix $L_B$ on every $B$ -block and choose any matching consistent with it. All such choices have the required even parities outside $C$ : consistency gives equal labels on each fixed red edge, and the red-count parity of a consistent matching is the number of pairs minus the number of labels equal to one. For a fixed rectangle $\mathcal R=\mathcal L\times\mathcal M$ , write $p_M(J)$ and $p_L(K)$ for the respective probabilities of membership in its factors when the core matching is $J$ , or the core labeling is $K$ , and the permitted outside completions are sampled uniformly. The two completions are independent.

Lemma 5 (A finite rectangle inequality for parity matchings)

For $0<\varepsilon<1/3$ , sufficiently large $k$ , and sufficiently large $s$ , there are probability distributions $\mu_3,\mu_h,\nu_1$ supported on $t=3,h,1$ , respectively, such that every rectangle satisfies

\mu_3(\mathcal R)\le A\mu_h(\mathcal R)+B\nu_1(\mathcal R)+E_s,

(16)

where

p=\binom{2k+3}{3},\qquad A=\frac{10k(1+\varepsilon)^2}{(1-\varepsilon)p},\qquad B=\frac{3(1+\varepsilon)^6}{1-\varepsilon},\qquad E_s=\frac{2^{-\delta s}+2^{-\zeta s}}{1-\varepsilon}.

(17)

Here $\delta,\zeta>0$ depend only on $k,\varepsilon$ .

Proof (of Lemma 5)

Sample the partition uniformly and order its core uniformly as $C=F\sqcup D_2$ , with $|F|=2k+3$ and $|D_2|=2k$ . Fix the family of bijections from JSY Lemma 4.4. For $H\in\binom F3$ , use the bijection indexed by the positions of $H$ in $F$ to order $F\setminus H$ as $D_{1,H}$ , and put $D_H=D_{1,H}\sqcup D_2$ . The family has the following property: in every family of at least $10k$ triples, there are $H,H'$ and $i,j\in H'\setminus H$ lying in opposite halves of $D_{1,H}$ .

Let $J_{3,H}$ be red identity edges on $H$ and $M_A(D_H)$ elsewhere. Let $K_{3,H}$ assign $(1,0)$ to each pair in $H$ and equal $L_B(D_H)$ elsewhere. Their only violations are the three edges on $H$ . Set $g_H=p_M(J_{3,H})p_L(K_{3,H})$ . Averaging over the partition, the ordered core, and uniform $H$ defines $\mu_3(\mathcal R)$ . This is JSY’s alternative sampling of their three-violation distribution: conditional on $H$ , the order of the remaining pairs is uniform, regardless of the fixed bijection used to order $D_{1,H}$ .

Let $J_h$ consist of all red identity edges on $C$ . Let $K_h$ label the pairs in $F$ by $(1,0)$ and those in $D_2$ by $(0,1)$ . Set $w=p_M(J_h)p_L(K_h)$ . These completions do not depend on $H$ , have $h$ violations, and their average defines $\mu_h(\mathcal R)$ .

Use JSY’s good, small, and bad classification. Goodness means that, for each factor separately, replacing its canonical completion on $D_H$ by any permitted completion changes its positive membership probability by at most a factor $1+\varepsilon$ . For the matching factor, permitted means consistent with $L_B(D_H)$ ; for the labeling factor it means consistent with $M_A(D_H)$ . Both $J_h$ and $K_h$ are permitted replacements. Consequently every good triple satisfies

g_H\le(1+\varepsilon)^2w.

(18)

The imported small- and bad-triple estimates are

\mathrm{Small}\le2^{-\delta s},\qquad \mathrm{Bad}\le\varepsilon\mu_3(\mathcal R)+2^{-\zeta s}.

(19)

They hold for arbitrary rectangles: their proofs use slice densities, entropy, and block exchanges, without excluding one-violation entries. That exclusion is used in JSY’s good-triple contradiction, which we now replace by a quantitative estimate.

To make the use of the bad-triple estimate precise, on the labeling side fix the labels on $H$ and all $B$ -blocks. Let $X=\prod_{i=0}^{s}X_i$ be the product of allowed labelings on $D=A_0$ and the $A$ -blocks, and let $Y\subseteq X$ be the full set of completions belonging to the rectangle’s labeling factor. A nonsmall canonical slice in coordinate $j$ gives $|Y|/|X|\ge2^{-\delta s}/|X_j|$ . The alphabet sizes depend only on $k$ , so this satisfies the entropy lemma’s density hypothesis after adjusting $\delta$ . At an unbiased coordinate, every slice density lies within a factor $1+\varepsilon/3$ of $|Y|/|X|$ ; any two therefore lie within a factor $1+\varepsilon$ . The block-exchange argument gives the stated bad-triple bound, and the matching side is identical. Here $Y$ is the full product-space subset, rather than a single fixed-coordinate slice. No exclusion of one-violation entries is involved.

Define $\nu_1$ independently of the rectangle. Conditional on the partition and ordered core, choose $H'\in\binom F3$ uniformly and then an unordered pair $\{i,j\}\subset H'$ uniformly. Define $J'$ by red identity edges on $C\setminus\{i,j\}$ and the two blue edges $(u_i,v_j),(u_j,v_i)$ . Define $K'$ to be one at every core vertex except the three right vertices belonging to $H'$ . The core has $h-2$ red edges and $2h-3$ labels equal to one; both numbers are odd. Its only violation is the unchanged red identity edge at the third element of $H'$ . Complete outside as before. This defines a probability distribution supported on $t=1$ , using $3p$ equally weighted core indices.

Fix the partition and ordered core, and let $\mathcal G$ be the family of good triples. Call $H'\in\mathcal G$ regular if some $H\in\mathcal G$ has $i,j\in H'\setminus H$ in opposite halves of $D_{1,H}$ . There are fewer than $10k$ exceptional triples: otherwise the permutation lemma, applied to that exceptional subfamily, would produce a regular member.

For each regular $H'$ , select one witness $H$ and pair $\{i,j\}$ . The corresponding $J'$ agrees with $J_{3,H}$ on $H$ . On $D_H$ , its red identity edges are consistent with $L_B(D_H)$ ; the two blue edges are also consistent because $i,j$ have opposite $L_B(D_H)$ labels. Thus $J'$ is a permitted matching replacement for $H$ . The labeling $K'$ agrees with $K_{3,H'}$ on $H'$ and is identically one on $D_{H'}$ . Since $M_A(D_{H'})$ is entirely red, $K'$ is a permitted labeling replacement for $H'$ . Comparison through the respective canonical completions gives

p_M(J')\ge\frac{p_M(J_h)}{(1+\varepsilon)^2}, \qquad p_L(K')\ge\frac{p_L(K_h)}{(1+\varepsilon)^2}.

(20)

Different regular $H'$ give distinct indices $(H',\{i,j\})$ in the sampling experiment defining $\nu_1$ . Therefore

\nu_1(\mathcal R\mid T,C) \ge\frac{|\mathcal G_{\rm reg}|\,w}{3p(1+\varepsilon)^4}.

(21)

Adding the at most $10k$ exceptional contributions yields

\frac1p\sum_{H\in\mathcal G}g_H \le\frac{10k(1+\varepsilon)^2}{p}w +3(1+\varepsilon)^6\nu_1(\mathcal R\mid T,C).

(22)

Average this inequality, add the small- and bad-triple contributions, and divide by $1-\varepsilon$ .

Proof (of Theorem 7)

Set $W=\mu_3-A\mu_h-B\nu_1$ . Its value on each rectangle indicator is at most $E_s$ . On the matrix $P_{n,r}=t-r$ , its value is

\langle W,P_{n,r}\rangle =(3-r)-A(h-r)-B(1-r) =2r-A(h-r)-(B-3)(1-r).

(24)

Choose $\varepsilon=r/100$ and $k\ge400/r$ , also sufficiently large for the permutation lemma. The formal parameter estimates give $A(4k+3)\le r/10$ and $B-3\le r/4$ ; hence the displayed value is greater than $3r/2$ .

For completeness, if a finite signed matrix $W$ has value at most $E$ on every rectangle indicator, then any nonnegative matrix $S$ satisfies

r_+(S)\ge\frac{\langle W,S\rangle}{E\|S\|_\infty}

(25)

whenever the numerator and $E$ are positive. Normalize a nonzero nonnegative rank-one summand $ab^{\mathsf T}$ by the maxima of its two factors. The resulting factors lie in unit cubes. Maximizing a linear functional in each factor in turn shows that their signed pairing is at most the largest rectangle weight. The original summand therefore contributes at most $E\|a\|_\infty\|b\|_\infty$ . Since each summand of a nonnegative factorization is entrywise at most $S$ , this is at most $E\|S\|_\infty$ . Summing proves the inequality. This finite argument, including empty index sets and zero factors, is formalized in Lean.

Here $0\le P_{n,r}\le n$ , while $E_s$ is exponentially small in $s$ and $s=\Theta_r(n)$ . This proves the lower bound for $n=4k(2s+1)+3$ . For arbitrary sufficiently large $n$ , take the largest such $n_0\le n$ and add blue identity matching edges with endpoint labels $(1,0)$ . They add no violations, preserve odd red parity, and change the label parity by precisely $n-n_0$ . Thus $P_{n_0,r}$ occurs as a submatrix of $P_{n,r}$ , with $n-n_0<8k$ . The bound follows for all sufficiently large $n$ .

Formal statements for the extension¶

The finite statements below specify exactly which part of the preceding argument Lean proves. They use the same costs and violation matrices as the four applications.

For clarity, call the following the finite partition hypotheses. There is a finite set of partitions with nonnegative averaging weights and a finite set of $p$ triples. Each partition specifies its good triples, canonical and high-violation completions, and nonnegative row and column membership probabilities. The following assertions are supplied:

Every family of at least $K$ good triples contains the witness pair guaranteed by the permutation-family property.
For a good triple, the probability of every permitted completion is within a factor $c=1+\varepsilon$ of its canonical probability. Permitted matchings agree with the red identity matching on that triple and are consistent with the complementary labeling. Permitted labelings have the canonical values on the triple and are consistent with the complementary matching.
The high completions are permitted. The old canonical matchings and labelings have the block properties described above; the witness relation gives two opposite labels outside the witness triple.
The averages of the high-completion probabilities and the new one-violation sample probabilities equal the respective rectangle masses. The three-violation mass is covered by the good, small, and bad contributions, with $\mathrm{Small}\le e_s$ and $\mathrm{Bad}\le\varepsilon\mu_3(\mathcal R)+e_b$ .

These are explicit fields of ConcreteJSYRectangleData. Its new matching and labeling are the concrete core constructions, not arbitrary replacement objects. Lean proves that they are permitted and derives their probability comparisons from the generic goodness condition. The sampling identities, permutation-family assertion, and small-/bad-triple estimates remain hypotheses; their proofs in the earlier framework are outside this formalization.

Theorem 10 (Finite shifted-rank bound)

Let $\mu_3,\mu_h,\nu_1$ be probability matrices supported on $t=3,h,1$ , respectively, where $h=4k+3$ . Assume the finite partition hypotheses for every rectangle, with $K=10k$ , $p=\binom{2k+3}{3}$ , $\varepsilon=r/100$ , $0<r\le1$ , and $k\ge400/r$ . Suppose $e_s,e_b\ge0$ and $t(i,j)-r\le U$ , where $U\ge0$ . Set $E=(e_s+e_b)/(1-r/100)$ . For every $L\in\mathbb N$ ,

(L-1)EU\le\frac{3r}{2} \quad\Longrightarrow\quad L\le r_+(t-r).

(29)

Here $L-1$ is subtraction in the real numbers.

Scope of the formalization¶

The four final Lean theorems use actual combinatorial solutions. Perfect matchings are finite simple graphs of degree one, $V$ -joins are finite simple graphs with all degrees odd, odd cuts are odd finite vertex subsets, and colored bipartite matchings are permutations with edge colors. Edge counts and objective sums are defined on these objects.

The formal proofs include the one-crossing matching construction, degree-sum arguments, the singleton odd-cut optimum, the parity identity and one-violation matching construction, all four exact optimum calculations, and the transfers to $L\le m+1$ . The metric property is proved for the actual cost function. The first three applications use a graph with $n$ vertices; the parity application uses a multigraph with $2n$ vertices.

The remaining external hypotheses and results are:

the ordinary matching-matrix nonnegative-rank theorem of Braun and Pokutta;
for the new parity extension, the permutation-family property, generic good-completion comparisons, sampling identities, and small-/bad-triple estimates of the Jia–Svensson–Yuan framework; the full-graph completion maps are required to preserve the core violation count;
the existence of affine Farkas certificates, provided as data in CertifiedLP;
the cited polynomial-time algorithms, whose running times are not formalized here.

The original four transfer theorems remain available with an assumed source rank bound. The additional parity theorem instead derives that rank bound, in finite quantitative form, from the displayed partition hypotheses. The mathematical exponential statement also uses the exponential decay in the external small-/bad-triple estimates. The Lean development does not formalize the earlier paper in its entirety.

All four applications can be imported from one module:

Main.lean

/-
The four application theorems concern concrete combinatorial domains and
actual edge costs. Each concludes L ≤ m + 1 from an explicit shifted
nonnegative-rank lower bound and a formulation with affine certificates.
The parity extension below derives the rank bound from explicit JSY
partition and entropy hypotheses. General Farkas certificate existence
and the earlier source theorems remain external.
-/
export Matching (matching_lp_lower_bound oddCut_lp_lower_bound)
export Joins (vjoin_lp_lower_bound)
export Parity (parity_matching_lp_lower_bound)
export ParityExtension (parity_lp_lower_bound_from_jsy)

Formal verification

✓ kernel-checked (Lean v4.35.0) Theorem 1 — Lemmata.LPHardnessInP.Formulation.certified_slack_factorization (source)
✓ kernel-checked (Lean v4.35.0) Lemma 1 — Lemmata.LPHardnessInP.Matching.matching_minimum (source)
✓ kernel-checked (Lean v4.35.0) Theorem 2 — Lemmata.LPHardnessInP.Matching.matching_lp_lower_bound (source)
✓ kernel-checked (Lean v4.35.0) Proposition 1 — Lemmata.LPHardnessInP.CostTransfer.cut_metric_properties (source)
✓ kernel-checked (Lean v4.35.0) Lemma 2 — Lemmata.LPHardnessInP.Joins.vjoin_minimum (source)
✓ kernel-checked (Lean v4.35.0) Theorem 3 — Lemmata.LPHardnessInP.Joins.vjoin_lp_lower_bound (source)
✓ kernel-checked (Lean v4.35.0) Lemma 3 — Lemmata.LPHardnessInP.Matching.oddCut_minimum (source)
✓ kernel-checked (Lean v4.35.0) Theorem 4 — Lemmata.LPHardnessInP.Matching.oddCut_lp_lower_bound (source)
✓ kernel-checked (Lean v4.35.0) Lemma 4 — Lemmata.LPHardnessInP.Parity.matchingCost_minimum (source)
✓ kernel-checked (Lean v4.35.0) Theorem 5 — Lemmata.LPHardnessInP.Parity.parity_matching_lp_lower_bound (source)
✓ kernel-checked (Lean v4.35.0) Theorem 6 — Lemmata.LPHardnessInP.RankReduction.factorization_reduction (source)
✓ kernel-checked (Lean v4.35.0) Corollary 1 — Lemmata.LPHardnessInP.Formulation.certified_reduction_rank_lower_bound (source)
✓ kernel-checked (Lean v4.35.0) Proposition 2 — Lemmata.LPHardnessInP.RankReduction.rank_transpose (source)
✓ kernel-checked (Lean v4.35.0) Proposition 3 — Lemmata.LPHardnessInP.RankReduction.rank_rowScale_eq (source)
✓ kernel-checked (Lean v4.35.0) Corollary 2 — Lemmata.LPHardnessInP.Formulation.bounded_baseline_lp_lower_bound (source)
✓ kernel-checked (Lean v4.35.0) Corollary 3 — Lemmata.LPHardnessInP.Formulation.near_exact_reversal_lp_lower_bound (source)
✓ kernel-checked (Lean v4.35.0) Proposition 4 — Lemmata.LPHardnessInP.ParityExtension.coreProbability_supported (source)
✓ kernel-checked (Lean v4.35.0) Theorem 8 — Lemmata.LPHardnessInP.ParityExtension.ConcreteJSYRectangleData.corruption_bound (source)
✓ kernel-checked (Lean v4.35.0) Theorem 9 — Lemmata.LPHardnessInP.ParityExtension.pairing_factorization_le (source)
✓ kernel-checked (Lean v4.35.0) Proposition 5 — Lemmata.LPHardnessInP.ParityExtension.calibrated_witness_gap (source)
✓ kernel-checked (Lean v4.35.0) Theorem 10 — Lemmata.LPHardnessInP.ParityExtension.calibrated_shifted_rank_from_jsy (source)
✓ kernel-checked (Lean v4.35.0) Corollary 4 — Lemmata.LPHardnessInP.ParityExtension.parity_lp_lower_bound_from_jsy (source)
✓ kernel-checked (Lean v4.35.0) Proposition 6 — Lemmata.LPHardnessInP.ParityExtension.shifted_rank_mono (source)

Checked at commit a9429cb9cbf5. The formal statement is machine-checked; that it matches the prose is checked by review. What “checked” means.

AI use. The exposition and Lean formalization were developed with OpenAI Codex. The published matching rank theorem, the earlier parity partition and entropy assertions, and affine Farkas certificate existence remain external. The new parity extension is formalized conditionally on precise hypotheses; no custom axioms are introduced.

Acknowledgements. Research reported in this paper was partially supported by the Berlin Mathematics Research Center MATH $^+$ (EXC-2046/2, project ID 390685689), funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) under Germany’s Excellence Strategy. This work has been partially supported by OpenAI’s Academic Researchers program.

References¶

Padberg, M. W., & Rao, M. R. (1982). Odd Minimum Cut-Sets and b-Matchings. Mathematics of Operations Research, 7(1), 67–80. 10.1287/moor.7.1.67