Motivation

AdaBoost (Freund and Schapire, 1997) combines many weak classifiers $f_m(x) \in \{-1, 1\}$ into a weighted vote $\operatorname{sign}\big(\sum_m c_m f_m(x)\big)$. At each round it fits a classifier to a reweighted training sample, sets $c_m = \log((1 - \mathrm{err}_m)/\mathrm{err}_m)$ from the weighted error $\mathrm{err}_m$, and multiplies the weights of the misclassified points by $e^{c_m}$. The algorithm was introduced as a procedure for boosting the accuracy of weak learners in the PAC sense, and its good test performance was at first not explained by any statistical model.

Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) recast boosting as stagewise fitting of an additive model by minimizing the exponential criterion $J(F) = E(e^{-yF(x)})$. Their Lemma 1 shows that $J$ is minimized at half the log-odds, so an additive $F$ fitted this way estimates a logistic regression model. Result 1 of that paper, the subject of this mission, shows that Discrete AdaBoost is exactly such a fitting procedure: in its population version, each round is a Newton-like step on $J$ followed by an exact line search, and the resulting reweighting is AdaBoost's. This view underlies gradient boosting, LogitBoost and the loss-function analysis of boosting in later work.

Setting

Let $X$ be a measurable space of features and let $\nu$ be a probability law of the pair $(x, y)$ on $X \times \{-1, 1\}$. The conditional law of $y$ given $x$ is the disintegration $\nu(\cdot \mid x)$, and $E(\cdot \mid x)$ is the integral against it. A current estimate is a measurable $F : X \to \mathbb R$, and the exponential criterion is

$$J(F) = E\big(e^{-yF(x)}\big) \in [0, \infty].$$

With weight $w(x, y) = e^{-yF(x)}$, the weighted conditional expectation and the weighted expectation are

$$E_w[g(x, y) \mid x] = \frac{E[w(x, y) g(x, y) \mid x]}{E[w(x, y) \mid x]}, \qquad E_w[g(x, y)] = \frac{E[w(x, y) g(x, y)]}{E[w(x, y)]}.$$

A classifier is a measurable $f : X \to \{-1, 1\}$; its weighted error is $\mathrm{err} = E_w[1_{[y \neq f(x)]}]$. The paper's candidate update is $F \leftarrow F + cf$ with

$$f(x) = \begin{cases} 1, & E_w(y \mid x) > 0, \\ -1, & \text{otherwise}, \end{cases} \qquad (18) \qquad\qquad c = \frac12 \log\frac{1 - \mathrm{err}}{\mathrm{err}}. \qquad (20)$$

Algorithm 1 (p. 338) uses $c_m = \log((1 - \mathrm{err})/\mathrm{err}) = 2c$ and the update $w \leftarrow w \exp(c_m 1_{[y \neq f(x)]})$ followed by renormalization.

Formalization targets

Goal: Result 1 (p. 346)

For $F$ measurable with $J(F) < \infty$:

1. for every $c > 0$ and every $x$, the classifier (18) minimizes the quadratic approximation $E_w(1 - ycs + c^2/2 \mid x)$ over $s \in \{-1, 1\}$;
2. for every classifier $f$ with $0 < \mathrm{err} < 1$, the coefficient $c$ of (20) satisfies

$$J(F + cf) \le J(F + c'f) \qquad \text{for all } c' \in \mathbb R;$$

3. for every classifier $f$, every $x$ and $y$,

$$e^{-yF(x)} e^{-cf(x)y} = e^{-c} \cdot e^{-yF(x)} \exp\Big(\log\frac{1 - \mathrm{err}}{\mathrm{err}}\, 1_{[y \neq f(x)]}\Big),$$

so the population reweighting coincides with Algorithm 1's after renormalization.

Milestones

• the second-order expansion of $E_w(e^{-cys} \mid x)$ in $c$ (proof of Result 1, p. 346);
• (17)–(18): for $c > 0$, (16) is maximization of $E_w[yf(x)]$, solved by (18) (p. 347);
• (19): $-E_w[yf(x)] = E_w[(y - f(x))^2]/2 - 1$ (p. 347);
• (20): $c = \frac12\log((1-\mathrm{err})/\mathrm{err})$ is the unique minimizer of $E_w e^{-cyf(x)}$ (p. 347);
• $-yf(x) = 2 \times 1_{[y \neq f(x)]} - 1$ and the weight identity (p. 347);
• Corollary 2 (p. 348), referenced from the platform in its sample form;
• (21)–(22): the first-order condition of the line search (p. 348).

Significance

The result. Result 1 turns AdaBoost from a combinatorial reweighting scheme into an optimization method with a known objective. It identifies the population quantity the algorithm estimates (via Lemma 1, half the log-odds), explains the specific constant $\log((1-\mathrm{err})/\mathrm{err})$ as an exact line search, explains why the weights of misclassified points are inflated by $(1-\mathrm{err})/\mathrm{err}$, and shows that a weak learner worse than chance is used with reversed sign. It is the template for the other population results of the paper (Real AdaBoost, LogitBoost, Gentle AdaBoost) and for later functional-gradient views of boosting.

Formalizing it. The result is proved on paper; it has not been machine-checked. The paper's argument is stated informally ("≈", "arg min", "Newton-like"); this mission fixes each claim as a precise statement about measures on $X \times \{-1, 1\}$. The sample version of Corollary 2 is already proved on the platform (UnderstandingML.adaboost_reweighted_error) and is reused; everything else is new.

Difficulty

Each step is elementary on its own; the work is in carrying the population statements through measure theory. The weighted expectations are ratios of integrals that are meaningful only under integrability of $e^{-yF(x)}$, and the line-search claim compares $J(F + c'f)$ for all real $c'$, all of which must be shown finite before they can be compared as real numbers. The pointwise claim (16)–(18) uses the conditional law of $y$ given $x$, which exists only as a disintegration kernel; passing from it to the unconditional (17) requires the disintegration identity and measurability of (18) in $x$. The tempting shortcut of treating $J(F + cf)$ as its quadratic approximation does not prove the line-search claim: (20) is the exact minimizer of $J$, not of the approximation.

Formalization scope

Labels are Booleans, with $y = 1$ for true and $y = -1$ for false. $J$ is a lower Lebesgue integral in $[0, \infty]$ and is compared there; $E_w$ and $E_w(\cdot \mid x)$ are ratios of Bochner integrals, the conditional one against ν.condKernel x. Disclosed additions, each needed for the page's formulas to be defined: $F$ and $f$ measurable, $J(F) < \infty$, and $0 < \mathrm{err} < 1$ wherever $\log((1-\mathrm{err})/\mathrm{err})$ is used. No condition $\mathrm{err} < 1/2$ is imposed. Ties $E_w(y \mid x) = 0$ go to $-1$, as printed. The "≈" of the expansion is read as "second-order Taylor polynomial in $c$", and derivatives are stated with HasDerivAt.

Trivializing formalizations are excluded: $J$ is not defined by a conditional formula or as a Bochner integral (which would return $0$ on non-integrable weights and make every step optimal), the logarithm is never applied outside its domain, and the class of $f$ stays $\{-1, 1\}$-valued (over real-valued $f$ the Newton step is Gentle AdaBoost's, a different result).

Everything is in the namespace AddLogReg.Discrete, with one definitions file (Setting) holding $J$, $E_w$, the classifier (18), $\mathrm{err}$ and the coefficient (20). Reusable pieces are lemmas on disintegrations of laws on $X \times \mathrm{Bool}$ and on weighted expectations. Proofs of any milestone are welcome independently.

Selected references

• J. Friedman, T. Hastie and R. Tibshirani, Additive logistic regression: a statistical view of boosting, Ann. Statist. 28(2):337–407, 2000. https://doi.org/10.1214/aos/1016218223
• Y. Freund and R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, J. Comput. System Sci. 55(1):119–139, 1997. https://doi.org/10.1006/jcss.1997.1504
• R. E. Schapire and Y. Singer, Improved boosting algorithms using confidence-rated predictions, Machine Learning 37:297–336, 1999. https://doi.org/10.1023/A:1007614523901

Motivation

Retailers accept large volumes of returned merchandise, and a common default is the full refund: a buyer who is unhappy with a product brings it back and gets the whole price back. Many consumers only learn how much they value a product after they have it at home — clothes that do not fit, a gadget that does not suit the buyer's needs. A returns policy therefore plays two roles at once. It raises the buyer's willingness to pay before purchase, and after purchase it decides which units stay with consumers and which go back to the seller to be salvaged.

Xuanming Su's paper Consumer Returns Policies and Supply Chain Performance (SSRN 1020451; published in Manufacturing & Service Operations Management 11(4), 2009, doi:10.1287/msom.1080.0240) puts this effect into a newsvendor model with random demand. The earlier literature it builds on, notably Che (1996) and Davis, Gerstner and Hagerty (1995), asked whether a seller should offer full refunds or no returns at all. Su's model makes the refund amount a separate decision variable. The answer it gives is closed-form and sharp: the optimal refund equals the salvage value. This mission formalizes Sections 3–4 of the paper: the single-seller model, the full-refund benchmark, and the optimal partial refund.

Setting

A seller stocks a quantity $q \ge 0$ before a selling season at unit cost $c$. Unsold and returned units are salvaged at value $s$. Market demand is a nonnegative random variable $X$ with law $D$, distribution function $F$ and $\bar F = 1 - F$. Each consumer who buys learns a valuation $V$ after purchase. Valuations are i.i.d. with law $\nu$ and finite mean $\mu = EV$, and the standing assumption is $\mu > c > s \ge 0$.

The seller chooses a price $p$, a quantity $q$ and a refund $r$. Once a consumer has bought, they keep the product if $V \ge r$ and return it otherwise. The keep and return probabilities are

$$\bar G(r) = \mathbb P(V \ge r), \qquad G(r) = \mathbb P(V < r).$$

Before purchase a consumer's expected utility from buying is $E\max(V, r)$, so this is the reservation price. Every consumer buys if $p \le E\max(V, r)$ and nobody buys otherwise (the demand rule (6)). With $E\min(X, q)$ the expected sales of a stock $q$, the seller's expected profit (7)–(8) is

$$\Pi(p,q,r) = \big[(p-s)\bar G(r) + (p-r)G(r)\big]\,E\min(X,q) - (c-s)q \quad\text{if } p \le E\max(V,r),$$

and $-(c-s)q$ otherwise. Two special cases serve as benchmarks. Under full refunds ($r = p$) every consumer buys and the profit is $\Pi_{\text{full}}(p,q) = (p-s)\bar G(p)E\min(X,q) - (c-s)q$, from (1)–(2). Under no returns the price is $\mu$ and the profit is $\Pi_{\text{no}}(q) = (\mu - s)E\min(X,q) - (c-s)q$, from (3). Social welfare (12)–(13) is the sum of consumer surplus and seller profit, $SW(p,q,r) = \int_{[r,\infty)}(v-s)\,d\nu(v)\cdot E\min(X,q) - (c-s)q$, again subject to the demand rule.

Formalization targets

Goal: Proposition 2 (p. 11)

With $p^* = E\max(V,s)$, $r^* = s$ and any $q^*$ satisfying

$$\bar F(q^*) = \frac{c-s}{E\max(V,s) - s},$$

the triple $(p^*, q^*, r^*)$ maximizes $\Pi$ over all prices, all refunds and all quantities $q \ge 0$:

$$\Pi(p,q,r) \le \Pi(p^*, q^*, r^*).$$

Milestones

1. The reservation price splits as $E\max(V,r) = rG(r) + \int_{[r,\infty)} v\,d\nu$, which is the step (28)→(29) of the proof (p. 26).
2. At $p = E\max(V,r)$ the per-unit margin $(p-s)\bar G(r) + (p-r)G(r)$ equals $\int_{[r,\infty)}(v-s)\,d\nu$, displays (27)–(30), p. 26.
3. This integral is maximized at $r = s$ (p. 26).
4. Hence $(E\max(V,s), s)$ maximizes the margin subject to $p \le E\max(V,r)$, the first step of the proof (p. 26).
5. The newsvendor critical fractile, a reference to a proved platform theorem (p. 26).
6. Proposition 1(i) (p. 9): under full refunds, $p^* \in \arg\max_p (p-s)\bar G(p)$ with $\bar F(q^*) = (c-s)/((p^*-s)\bar G(p^*))$ is optimal.
7. Proposition 1(ii) at $s = 0$ (p. 26): with nonnegative valuations, no returns beats every full-refund policy.
8. Corollary 1 (p. 12): the inequality $(p-s)\bar G(p) \le E\max(V,s) - s$ (p. 26), and its consequence that partial refunds earn at least the full-refund profit and, for strictly increasing $F$, stock at least as much.
9. Corollary 2 (p. 13): the triple of Proposition 2 also maximizes social welfare.

Significance

The result separates two things that a full refund ties together: the price and the refund. Setting $r = s$ sends every unit back to its more valuable use. Consumers who value the product above its salvage value keep it, and the rest return it to be salvaged. The price $E\max(V,s)$ then extracts the whole expected surplus. Consequences follow directly. Partial refunds dominate both full refunds and no returns (Corollary 1). They raise the stocking quantity, which benefits an upstream manufacturer paid per unit ordered. With valuation uncertainty resolved only after purchase, the monopoly outcome is welfare-maximizing (Corollary 2). Section 5 of the paper, formalized in the companion mission, uses Proposition 2's triple as the first-best target that supply chain contracts must implement.

The results are proved on paper with short arguments in Appendix A of the paper. None of them has a machine-checked proof. The mission's contribution is a formal model of consumer returns with the demand rule built in, plus checked versions of Propositions 1–2 and Corollaries 1–2 for general valuation laws (with atoms), not only densities.

Difficulty

The paper's proof treats the problem as separable: first maximize the margin over $(p, r)$, then solve a newsvendor problem in $q$. Two steps that are routine on paper need care. First, the margin bound must hold over the whole constrained region $p \le E\max(V, r)$, including refunds above the price and negative prices. It rests on comparing $\int_{[r,\infty)}(v-s)\,d\nu$ with $\int_{[s,\infty)}(v-s)\,d\nu$, which needs the closed half-line convention to hold up at atoms of $\nu$. Second, the newsvendor step must be done for a demand law that may have atoms, where $\bar F$ has no inverse. Without the demand rule the problem is not separable at all: formula (8) alone is unbounded in $p$. Without nonnegativity of demand and quantity it is unbounded in the other direction.

Formalization scope

Lean represents all prices, refunds, costs, quantities and profits as real numbers. The valuation law is a probability measure ν on ℝ with integrable identity, so a density is not required. The demand law is a probability measure D on ℝ with D (Set.Iio 0) = 0. $\bar G(r)$ is (ν (Set.Ici r)).toReal and $G(r)$ is (ν (Set.Iio r)).toReal, following the page's tie rule (keep iff $V \ge r$). $E\min(X,q)$ is SupplyChainTheory.expSales D q from the published module SupplyChainTheory_contracts, and $\bar F$ is 1 - ProbabilityTheory.cdf D. Printed page numbers equal PDF page numbers throughout the source.

Committed conventions and readings:

• Demand rule inside the objectives. Profit and welfare are zero-demand cash flows when $p > E\max(V,r)$.
• Nonnegativity. Stocking quantities range over $q \ge 0$ and demand is nonnegative. Both are the page's words ("stocking quantity", "a mass of infinitesimal consumers"), and without them the profit is unbounded.
• Salvage value. $0 \le s$, as on p. 26.
• Optimality, not uniqueness. Every optimum is stated as optimality of the page's closed-form triple. Uniqueness fails when $\nu$ has gaps: if $\nu$ puts no mass on $[s, r)$, the refund $r$ is optimal too.
• No continuity of $F$ for the goal. The goal assumes no continuity of $F$. Existence of $q^*$ is not claimed.
• Corollary 1, quantity part. The quantity comparison assumes $F$ strictly increasing on $[0,\infty)$, which the proof's $\bar F^{-1}$ presumes. Without it the statement is false.
• Proposition 1(ii) at $s = 0$. This case assumes nonnegative valuations. The "sufficiently low" form of Proposition 1(ii) is not formalized.

A trivializing formalization is ruled out: $p^*$ and $r^*$ are the explicit values $E\max(V,s)$ and $s$, not an argmax chosen by Classical.choose. The maximization ranges over all $(p, r)$ and all $q \ge 0$, not a set restricted to $r = s$. The returned-units cash flow $(p - r + s)G(r)$ appears in the profit.

The newsvendor step reuses the proved platform theorem SupplyChainTheory.chain_optimal_fractile. The other pieces needed are elementary lemmas on integrals over half-lines and the concavity of $q \mapsto E\min(X,q)$. They are reusable for any newsvendor-type model. Proofs of any milestone, and a general-law newsvendor optimality lemma that does not need a continuous $F$, are welcome.

Selected references

• X. Su, Consumer Returns Policies and Supply Chain Performance, SSRN working paper 1020451, version of August 2008. https://ssrn.com/abstract=1020451 — published in Manufacturing & Service Operations Management 11(4), 2009. https://doi.org/10.1287/msom.1080.0240
• Y.-K. Che, Customer Return Policies for Experience Goods, Journal of Industrial Economics 44(1), 1996. https://doi.org/10.2307/2950560
• S. Davis, E. Gerstner, M. Hagerty, Money Back Guarantees in Retailing: Matching Products to Consumer Tastes, Journal of Retailing 71(1), 1995. https://doi.org/10.1016/0022-4359(95)90010-1

Motivation

The log-Sobolev constant $\alpha$ of a finite Markov chain controls how fast the chain forgets its starting point in relative entropy and in $\ell^2$, and it gives sharper mixing-time bounds than the spectral gap $\lambda$ when the stationary distribution has very small atoms. Diaconis and Saloff-Coste (Ann. Appl. Probab. 6 (1996)) made this constant a standard tool for finite chains. A practical obstacle runs through their paper: $\alpha$ is defined by a nonlinear variational problem, and exact values are known for very few chains. Lower bounds on $\alpha$ for a complicated chain are usually obtained by comparison with a simple chain whose constant is known exactly.

The Appendix of that paper computes such a reference value. For the chain that forgets its state in one step, $K(x,y)=\pi(y)$, it determines $\alpha$ in closed form for every positive $\pi$, and with it the log-Sobolev constant of every chain on two points and of the random walk on the complete graph.

Timeline. Rothaus's work on log-Sobolev inequalities (references [38–40] of the paper) studied the constant through its minimizers, the approach the Appendix follows. Diaconis and Saloff-Coste (1996) give the formula $\alpha=(1-2\pi_*)/\log(1/\pi_*-1)$, and note that Higuchi and Yoshida independently found the asymmetric two-point value.

Setting

Let $\mathcal X$ be a finite set and $K$ a Markov kernel on it: $K(x,y)\ge0$ and $\sum_y K(x,y)=1$. Let $\pi$ be an invariant probability, $\sum_x\pi(x)K(x,y)=\pi(y)$, with $\pi(x)>0$ for every $x$. Functions on $\mathcal X$ are real. Write $Kf(x)=\sum_yK(x,y)f(y)$, $\langle f,g\rangle=\sum_x f(x)g(x)\pi(x)$, $\|f\|_2^2=\langle f,f\rangle$, $E_\pi f=\sum_x f(x)\pi(x)$ and $\mathrm{Var}_\pi(f)=\|f-E_\pi f\|_2^2$.

The Dirichlet form is $\mathcal E(f,g)=\langle (I-K)f,g\rangle$. The entropy functional is

$$\mathcal L(f)=\sum_{x\in\mathcal X}|f(x)|^2\log\frac{|f(x)|^2}{\|f\|_2^2}\,\pi(x),$$

which is nonnegative and vanishes exactly when $|f|$ is constant. The spectral gap and the log-Sobolev constant are

$$\lambda=\inf\Big\{\frac{\mathcal E(f,f)}{\mathrm{Var}_\pi(f)}:\mathrm{Var}_\pi(f)\ne0\Big\},\qquad \alpha=\inf\Big\{\frac{\mathcal E(f,f)}{\mathcal L(f)}:\mathcal L(f)\ne0\Big\}.$$

Equivalently, $1/\alpha$ is the best constant $C$ in $\mathcal L(f)\le C\,\mathcal E(f,f)$.

The chain of the mission is $K(x,y)=\pi(y)$: at each step it draws a fresh point from $\pi$, ignoring its current state. Its invariant measure is $\pi$, and $\pi_*=\min_{\mathcal X}\pi$ is its smallest atom. In Lean the objects are dirichlet, entL, gap, logSobolev, indepChain and piMin in the namespace LogSobolevMC.TwoPoint.

Formalization targets

Goal: Theorem A.1

For a positive probability $\pi$ on $\mathcal X$ with $\pi_*<1/2$, the chain $K(x,y)=\pi(y)$ has

$$\alpha=\frac{1-2\pi_*}{\log(1/\pi_*-1)},$$

and in particular, for $\pi\equiv1/|\mathcal X|$ with $|\mathcal X|\ge3$, $\alpha=(1-2/|\mathcal X|)/\log(|\mathcal X|-1)$. The goal is an equality, so it contains both a log-Sobolev inequality with this constant and the existence of functions that make it sharp.

Milestones

1. Lemma 3.1: $2\alpha\le\lambda$ for every chain.
2. $\mathcal E(|f|,|f|)\le\mathcal E(f,f)$ (proof of Theorem A.1).
3. Either $\alpha=\lambda/2$, or the infimum is attained at a nonconstant nonnegative function (proof of Theorem A.1).
4. (A.3): a positive minimizer $u$ of a reversible chain satisfies $2u\log u-2u\log\|u\|_2-\alpha^{-1}(I-K)u=0$.
5. (A.1): the explicit pair $a=\log[(1-\theta)/\theta]/(1-2\theta)$, $s=(1-2\theta)/(2\theta(1-\theta))$ solves the two-equation system of the proof of Theorem A.2.
6. Theorem A.2: the two-point chain with both rows $(\theta,1-\theta)$, $0<\theta\le1/2$, has $\alpha(\theta)=(1-2\theta)/\log[(1-\theta)/\theta]$, with the limit value $1/2$ at $\theta=1/2$.

Consequences

Corollary A.3 (every two-point chain), Corollary A.4 ($\alpha(K)\ge(1-2\pi_*)\lambda(K)/\log[1/\pi_*-1]$ for every finite chain) and Corollary A.5 (the complete graph, $\alpha=(|\mathcal X|-2)/((|\mathcal X|-1)\log(|\mathcal X|-1))$, and $\alpha=1/(2\log2)$ on $\mathbb Z_3$).

Significance

The result. Theorem A.1 is one of the few exact log-Sobolev constants known for a whole family of chains. Since this chain has $\lambda=1$, the formula shows that $\alpha$ can be smaller than $\lambda/2$ by a factor of order $\log(1/\pi_*)$, which answers the question on p. 715 of how far $2\alpha$ and $\lambda$ can be apart. Corollary A.4 turns this into a general tool: any spectral gap bound gives a log-Sobolev bound, losing only a factor $\log(1/\pi_*-1)/(1-2\pi_*)$. Corollary A.3 settles every chain on two points, and Corollary A.5 gives the complete graph, a frequent reference chain for comparison arguments.

Formalizing it. These results are proved in the paper. To our knowledge none of them, nor the log-Sobolev constant of a finite Markov chain itself, has a machine-checked formalization. The mission produces the definitions of $\mathcal E$, $\mathcal L$, $\lambda$ and $\alpha$ for finite chains, and exact values that later comparison arguments can cite.

Difficulty

The upper bound $\alpha\le(1-2\pi_*)/\log(1/\pi_*-1)$ needs only a good test function. The lower bound is the hard part: it is a statement about every function on $\mathcal X$, and $\mathcal L$ is neither quadratic nor convex. The obvious route, comparing with the spectral gap, loses exactly the logarithmic factor the theorem is about. Reducing to two-valued functions requires the infimum to be attained and analysed through its minimizers. The two-point problem that remains is a one-parameter inequality $l(s)\le a\,e(s)$ on an interval. The authors describe its solution as a calculus exercise that depended on numerical guessing, and it has removable singularities at $\theta=1/2$.

Formalization scope

$\mathcal X$ is a Fintype with decidable equality. $K$ is a Matrix V V ℝ and $\pi$ a function V → ℝ. Stochasticity, invariance, distributions and reversibility are the published MarkovMixing predicates (IsStochastic, IsStationary, IsDist, DetailedBalance) from mm_basic, and $\mathrm{Var}_\pi$ is MarkovMixing.distVar from mm_lower. Positivity of $\pi$ is a hypothesis throughout, as in §2.1. The infima $\lambda$ and $\alpha$ are Lean sInfs over exactly the sets of (2.4) and (3.1). $\mathcal E$ is the bilinear form $\langle (I-K)f,g\rangle$. $\lambda$ is the variational gap, not the eigenvalue-based MarkovMixing.spectralGap, which agrees with it only for reversible chains.

Disclosed additions, all at removable singularities of the printed formulas: $\pi_*<1/2$ in Theorem A.1 (and $|\mathcal X|\ge3$ in its uniform case); the explicit limit value $1/2$ at $\theta=1/2$ in Theorem A.2; strict $\pi(0)<\pi(1)$ in Corollary A.3; and $|\mathcal X|\ge3$ in Corollary A.5. In (A.3), reversibility, positivity of $u$ and $\alpha>0$ are added. Irreducibility is not assumed anywhere.

Trivializing formalizations are ruled out. A closed form evaluated at $0/0$ would be Lean's value $0$, so each such case is excluded or replaced by its limit. Real.log of a nonpositive number and an sInf over an empty or unbounded set do not occur under the stated hypotheses. Dropping the positivity or invariance of $\pi$, or replacing $\lambda$ by the eigenvalue gap, would change the statements. Stating the goal for two points only, or assuming the minimizer is two-valued, would state a step of the proof.

Contributions welcome: the general facts $\mathcal L\ge0$, $\mathcal E(f,f)=\tfrac12\sum_{x,y}(f(x)-f(y))^2K(x,y)\pi(x)$ and the existence of minimizers are reusable for every log-Sobolev development on finite spaces. The two-point calculus of Theorem A.2 is self-contained real analysis.

Selected references

• P. Diaconis and L. Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Ann. Appl. Probab. 6(3):695–750, 1996. https://doi.org/10.1214/aoap/1034968224
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, AMS, 2009 (source of the MarkovMixing definitions used here). https://doi.org/10.1090/mbk/058

Motivation

The Metropolis algorithm turns a simple random walk into a Markov chain with a prescribed stationary distribution, by accepting or rejecting the walk's proposals. It is the basic tool of Markov chain Monte Carlo, and the practical question it raises is quantitative: how many steps are needed before the chain's distribution is close to the target? For most chains used in practice there is no rigorous answer.

Diaconis and Saloff-Coste (Ann. Appl. Probab. 6 (1996) 695–750) developed logarithmic Sobolev inequalities for finite Markov chains as a tool for exactly this question. Their first illustration, stated as Theorem 1.1 in the introduction, is the Metropolis chain for the binomial distribution: a one-dimensional chain for which the spectral gap gives a bound of order $n^2$ steps, while the log-Sobolev constant gives the correct order $n\log n$. This mission formalizes that theorem and the chain of results the paper uses to prove it: the log-Sobolev constant of a product chain, of the hypercube walk, of the Ehrenfest chain, a comparison principle, and a discrete-time convergence bound.

Setting

Let $\mathcal X$ be a finite set. A Markov kernel $K$ on $\mathcal X$ is a matrix with $K(x,y)\ge 0$ and $\sum_y K(x,y)=1$; $K^l(x,\cdot)$, written $K^l_x$, is the law of the chain after $l$ steps from $x$. A probability $\pi$ on $\mathcal X$ is invariant if $\sum_x\pi(x)K(x,y)=\pi(y)$; throughout, $\pi$ charges every point. $(K,\pi)$ is reversible if $\pi(x)K(x,y)=\pi(y)K(y,x)$.

For real functions $f,g$ on $\mathcal X$ write $\langle f,g\rangle=\sum_x f(x)g(x)\pi(x)$, $\|f\|_2=\langle f,f\rangle^{1/2}$, $Ef=\sum_x f(x)\pi(x)$ and $\operatorname{Var}(f)=\|f-Ef\|_2^2$. The Dirichlet form is $\mathcal E(f,g)=\langle (I-K)f,g\rangle$, and

$$\mathcal L(f)=\sum_x |f(x)|^2\log\frac{|f(x)|^2}{\|f\|_2^2}\,\pi(x).$$

The spectral gap and the log-Sobolev constant are

$$\lambda=\inf\Big\{\frac{\mathcal E(f,f)}{\operatorname{Var}(f)}:\operatorname{Var}(f)\neq0\Big\},\qquad \alpha=\inf\Big\{\frac{\mathcal E(f,f)}{\mathcal L(f)}:\mathcal L(f)\neq0\Big\}.$$

For reversible $K$, $\beta_{\min}$ is the smallest eigenvalue of $K$. The total variation distance is $\|\mu-\nu\|_{TV}=\max_{A\subseteq\mathcal X}|\mu(A)-\nu(A)|$.

The chain of the goal lives on $\mathcal X=\{0,1,\dots,n\}$, $n\ge1$, with the binomial distribution $\pi(x)=2^{-n}\binom nx$. The base chain is the nearest-neighbour walk $K(x,x\pm1)=1/2$ for $1\le x\le n-1$, holding with probability $1/2$ at $0$ and at $n$. The Metropolis chain $M$ accepts a proposed move $x\to y\neq x$ with probability $\min\{1,\pi(y)/\pi(x)\}$, so $M(x,y)=K(x,y)\min\{1,\pi(y)/\pi(x)\}$ for $y\ne x$, and $M(x,x)=1-\sum_{y\ne x}M(x,y)$. Explicitly, $M(x,x+1)=\frac12$ for $x\le (n-1)/2$ and $M(x,x+1)=\frac{n-x}{2(x+1)}$ above, symmetrically for $x-1$; this is the kernel (1.9) of the paper.

Two auxiliary chains appear in the proof: the hypercube walk on $\{-1,1\}^n$, which flips a uniformly chosen coordinate, and the Ehrenfest chain $P(x,x+1)=(n-x)/n$, $P(x,x-1)=x/n$ on $\{0,\dots,n\}$, which records the number of coordinates equal to $1$.

Formalization targets

Goal: Theorem 1.1 (upper bound)

For every $n\ge1$, every starting point $x$, every $c>0$ and every integer $l$,

$$\|M^l_x-\pi\|_{TV}\le e^{1-c}\qquad\text{whenever } l\ge\frac n2(\log n+2c).$$

The goal is stated about the explicit chain (1.9) only; it fixes the constants as printed.

Milestones

1. Example 1.1, (1.9). The Metropolis construction gives the six-case kernel (1.9), and $\pi(x)M(x,y)=\pi(y)M(y,x)$.
2. Example 3.1. The two-point chain on $\{-1,1\}$ has $\pi\equiv1/2$, $\lambda=2$ and $\alpha=\lambda/2=1$.
3. Lemma 3.2. The product chain (2.9) of $d$ chains, with the product measure (2.10), has $\lambda=\frac1d\min_i\lambda_i$ and $\alpha=\frac1d\min_i\alpha_i$.
4. Example 3.2. The hypercube walk is that product of two-point chains and has $\alpha=\lambda/2=1/n$.
5. Lemma 3.1. $2\alpha\le\lambda$ for every chain.
6. Lemma 3.3. If $\mathcal E'\le A\mathcal E$ and $a\pi\le\pi'$ with $A,a>0$, then $\lambda'\le\frac Aa\lambda$ and $\alpha'\le\frac Aa\alpha$.
7. Example 3.3. The Ehrenfest chain is the projection of the hypercube walk, with $\lambda=2/n$ and $\alpha(P)=1/n$; $\frac12P(x,y)\le M(x,y)\le P(x,y)$ for $x\ne y$, so $\mathcal E_M\le\mathcal E_P\le2\mathcal E_M$; hence $\frac1n\le\lambda(M)\le\frac2n$ and $\frac1{2n}\le\alpha(M)\le\frac1n$.
8. Corollary 3.8. For reversible $(K,\pi)$ and $\pi(x)\le1/e$, with $\lambda_*=\min\{\lambda,1+\beta_{\min}\}$, $\|K^m_x/\pi-1\|_2\le(1+2e^2)^{1/2}e^{-c}$ for $m\ge\frac1{4\alpha}\log\log\frac1{\pi(x)}+\frac c{\lambda_*}+1$.
9. Example 3.4. $M(x,x)\ge2/(n+3)$, $\beta_{\min}\ge-1+4/(n+3)$, and $\|M^l_x/\pi-1\|_2\le(1+2e^2)^{1/2}e^{-c}$ for $l\ge\frac n2(\log n+2c)+1$.

Significance

The theorem shows that the Metropolis chain for the binomial distribution mixes in $\frac n2\log n+O(n)$ steps, matching the lower bound of order $n\log n$ quoted in the paper's converse. The spectral gap $\lambda(M)\asymp1/n$ together with $\pi_*=2^{-n}$ only yields order $n^2$; the improvement comes from replacing $\log(1/\pi_*)$ by $\log\log(1/\pi_*)$, which is what the log-Sobolev constant buys. The intermediate results are reusable on their own: the tensorization of $\lambda$ and $\alpha$ (Lemma 3.2), the comparison principle (Lemma 3.3) and the discrete-time bound (Corollary 3.8) apply to any finite chain, and the exact log-Sobolev constants of the two-point chain, the hypercube and the Ehrenfest chain are standard inputs elsewhere.

All results are proved in the paper (the gap $\lambda=2/n$ of the Ehrenfest chain is quoted there as known). To our knowledge none of them is machine-checked: there is no log-Sobolev constant of a Markov chain in Mathlib or on the platform. The work is to formalize the known proofs.

Difficulty

The natural first idea is to bound the distance to stationarity by the spectral gap: $\|K^l_x/\pi-1\|_2^2\le\pi(x)^{-1}\beta^{2l}$. With $\pi(x)$ as small as $2^{-n}$ and $1-\beta\asymp 1/n$, this needs $l$ of order $n^2$, so no amount of care with this argument reaches the theorem. The proof instead goes through the log-Sobolev constant, which is hard to compute even for simple chains: the paper obtains $\alpha(M)$ only through a sequence of exact computations (two points, products, a projection) followed by a comparison. Each step involves the nonlinear functional $\mathcal L$, whose tensorization and behaviour under comparison of measures are less elementary than those of the variance. The passage from continuous to discrete time also needs control of $\beta_{\min}$, since a chain with eigenvalue near $-1$ does not converge.

Formalization scope

The state space $\{0,\dots,n\}$ is Fin (n + 1), $\{-1,1\}$ is Fin 2 ($0\mapsto-1$, $1\mapsto1$), and $\{-1,1\}^n$ is Fin n → Fin 2. Kernels are real matrices Matrix V V ℝ; stochasticity, invariance, irreducibility, reversibility (detailed balance), total variation, the rows $K^l_x$, the product chain (2.9) and the generic Metropolis rule are the published MarkovMixing definitions (mm_basic, mm_mixing, mm_continuous, mm_mcmc). Functions are real valued. Time $l$ is a natural number and thresholds are compared in $\mathbb R$.

$\lambda$, $\alpha$ and $\beta_{\min}$ are defined variationally as real infima (sInf). $\beta_{\min}$ is the minimum of the Rayleigh quotient $\langle Kf,f\rangle/\langle f,f\rangle$, which is the smallest eigenvalue for reversible chains. The eigenvalue-based MarkovMixing.spectralGap is not used, since it equals $\lambda$ only for reversible chains. Two hypotheses are added where Lean's conventions would otherwise falsify a statement: Lemma 3.2 assumes every factor has at least two points (Lean evaluates the infimum over an empty set as $0$, the paper as $+\infty$), and Corollary 3.8 assumes $1+\beta_{\min}>0$ (Lean evaluates $c/0$ as $0$, the paper as $+\infty$). Lemmas 3.1 and 3.3 are stated without the section's irreducibility assumption, which they do not need.

A trivializing formalization is ruled out: the goal mentions only the explicit chain $M$, the binomial distribution, $M^l_x$ and total variation, not a chain assumed to have $\alpha\ge1/(2n)$; positivity and invariance of $\pi$ are never dropped; and no statement relies on a junk value of sInf, Real.log or division. The converse half of Theorem 1.1, $\max_x\|M^l_x-\pi\|_{TV}\ge\frac14+o(1)$ for $l\le\frac n8\log n$, is asymptotic and proved in the paper only by citation; it is not part of the mission. The second statement of Corollary 3.8 (the uniform bound on $|k^{2n}(x,y)-1|$) is also left out.

A complete development needs the semigroup $H_t=e^{-t(I-K)}$ and the hypercontractivity theorem of the paper (Theorem 3.5) on the way to Corollary 3.8, a spectral decomposition of reversible kernels, and the entropy inequalities behind Lemmas 3.2 and 3.3. The general results (Lemmas 3.1–3.3, Corollary 3.8) are reusable beyond this mission. Contributions to any milestone, and alternative routes to the goal, are welcome.

Selected references

• P. Diaconis and L. Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Ann. Appl. Probab. 6(3) (1996), 695–750. https://doi.org/10.1214/aoap/1034968224
• P. Diaconis and L. Saloff-Coste, What do we know about the Metropolis algorithm?, J. Comput. System Sci. 57 (1998), 20–36 (reference [18] of the paper, in its preprint form). https://doi.org/10.1006/jcss.1998.1576
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, AMS, 2009 (source of the published MarkovMixing definitions). https://doi.org/10.1090/mbk/058

Motivation

Biometric readings, typed passphrases and physical measurements are secrets that are never reproduced exactly: a second reading $w'$ of the same fingerprint differs from the enrolled reading $w$ in a few positions. Dodis, Ostrovsky, Reyzin and Smith (arXiv:cs/0602007, SIAM J. Comput. 38(1), 2008) introduced the secure sketch, public helper data that lets anyone holding a nearby $w'$ recover $w$ while leaking as little as possible about $w$, and the fuzzy extractor, which in addition turns $w$ into a nearly uniform key. Their constructions for the Hamming, set-difference and edit metrics are the standard reference for this primitive in cryptography.

A construction is judged by its entropy loss: how much min-entropy of the secret the published sketch destroys. To call a construction optimal one needs a lower bound on that loss which holds for every sketch, whatever its algorithm. Appendix C of the paper supplies such a bound from coding theory. It shows that, for uniformly distributed inputs, the code-offset sketch for the Hamming metric and the set-difference sketches lose no more entropy than any sketch must. This mission formalizes that bound, Lemma C.1.

Setting

A metric space is a finite set $\mathcal M$ with an integer-valued distance $\mathrm{dis}$; the paper also requires $\mathrm{dis}(x,y)=0$ exactly when $x=y$, symmetry, and the triangle inequality (§2.1, p. 7). Random variables are identified with their laws; logarithms are base 2.

The min-entropy of a random variable $A$ is $\mathbf H_\infty(A) = -\log \max_a \Pr[A=a]$. For a pair $(A,B)$ the average min-entropy is

$$\tilde{\mathbf H}_\infty(A\mid B) = -\log \mathbb E_{b\leftarrow B}\Big[\max_a \Pr[A=a\mid B=b]\Big],$$

the negative logarithm of the probability that an adversary who sees $B$ guesses $A$.

An $(\mathcal M,m,\tilde m,t)$-secure sketch (Definition 3, p. 11) is a pair of randomized procedures: $\mathsf{SS}$ maps $w\in\mathcal M$ to a string $s$, and $\mathsf{Rec}$ maps $(w',s)$ back to $\mathcal M$. Correctness: if $\mathrm{dis}(w,w')\le t$ then $\mathsf{Rec}(w',\mathsf{SS}(w))=w$. Security: for every distribution $W$ on $\mathcal M$ with $\mathbf H_\infty(W)\ge m$, one has $\tilde{\mathbf H}_\infty(W\mid \mathsf{SS}(W))\ge\tilde m$.

An $(\mathcal M,K,t)$-code (§2.2, p. 8) is a set $C\subseteq\mathcal M$ of $K$ points such that every ball $\{c : \mathrm{dis}(w,c)\le t\}$ around a point $w\in\mathcal M$ contains at most one codeword. For $S\subseteq\mathcal M$, $K(\mathcal M,t,S)$ is the largest $K$ for which an $(\mathcal M,K,t)$-code lies inside $S$, and $K(\mathcal M,t)=K(\mathcal M,t,\mathcal M)$. Finally (Appendix C, p. 40)

$$L(\mathcal M,t,m) = \log\Big(\min_{|S|=2^m} K(\mathcal M,t,S)\Big),$$

the worst case, over all sets $S$ of $2^m$ points, of the largest $t$-error-correcting code inside $S$.

In the Lean development these are minEntropy, avgMinEntropy, IsSecureSketch, IsCode, K dis t S and L dis t N hN, in the namespace FuzzyExtractors.LowerBound.

Formalization targets

Goal: Lemma C.1

If $(\mathsf{SS},\mathsf{Rec})$ is an $(\mathcal M,m,m',t)$-secure sketch and $2^m=N$ is a natural number with $N\le|\mathcal M|$, then

$$m' \le L(\mathcal M,t,m).$$

The bound fixes no particular metric and no particular sketch; it is stated for every finite integer-valued metric and every sketch, with an arbitrary type of sketch values.

Milestones

The proof in Appendix C has three steps, each a milestone. For $W$ uniform on a set $S$ of $2^m$ points:

1. some sketch value $v$ has $\Pr[\mathsf{SS}(W)=v]>0$ and $\mathbf H_\infty(W\mid\mathsf{SS}(W)=v)\ge m'$;
2. the set $T$ of points of $S$ that can produce $v$ has $|T|\ge 2^{m'}$;
3. under the correctness property alone, $T$ is an $(\mathcal M,|T|,t)$-code.

A fourth milestone is the lemma's second sentence: when $m=\log|\mathcal M|$,

$$m' \le \log K(\mathcal M,t).$$

Significance

The result. Lemma C.1 converts any secure sketch into a code: the residual entropy $m'$ of the sketch can be no larger than the logarithm of the best $t$-error-correcting code inside a worst-case set of $2^m$ points. For uniform inputs it says $m'\le\log K(\mathcal M,t)$, so the entropy loss is at least $\log|\mathcal M|-\log K(\mathcal M,t)$. The code-offset construction built from an optimal code attains that loss, which is how the paper certifies its Hamming and set-difference constructions as optimal for uniform passwords. The companion Lemma C.2 gives the analogous bound for fuzzy extractors, up to a $-\log(1-\varepsilon)$ term. Lower bounds of this shape are what separate an efficient construction from a provably best one.

Formalizing it. The lemma has a complete, short proof in the paper; it has no machine-checked proof that we know of. The mission produces a checked version of the bound for arbitrary finite integer metrics and arbitrary randomized sketches, together with reusable definitions of min-entropy and average min-entropy on probability mass functions, of secure sketches, and of $t$-error-correcting codes in a general finite metric space.

Difficulty

The combinatorial core, that the preimage set of one sketch value is a code, is immediate from correctness. The work lies in the probabilistic bookkeeping. One must pass from an average bound on guessing probability to a single good sketch value, which requires handling sketch values of probability zero and an infinite (possibly uncountable) space of sketch outputs. One must then pass from "$\Pr[W=w\mid v]\le 2^{-m'}$ for all $w$" to "at least $2^{m'}$ points carry positive probability", and compute the min-entropy of a uniform distribution exactly. Finally the bound must be transferred to the minimum over all sets of size $2^m$, a finite but large family. A first idea, to reason only about deterministic sketches, does not suffice: Definition 3 allows randomized $\mathsf{SS}$ and $\mathsf{Rec}$, and the statement quantifies over them.

Formalization scope

Laws are Mathlib PMFs; randomized procedures are maps into PMF. The sketch value type V is arbitrary, standing in for $\{0,1\}^*$. Average min-entropy is written in the equivalent joint form $-\log\sum_b\max_a\Pr[A=a\wedge B=b]$, which avoids conditioning on null events. "Min-entropy $m$" is read as $\mathbf H_\infty(W)\ge m$, and $m, m'$ are real numbers. $\mathsf{Rec}$ is randomized and correctness asks that it return $w$ with probability one for every possible sketch value of $w$.

The explicit choices:

• $L(\mathcal M,t,m)$ is defined only when $2^m$ is a natural number $N\le|\mathcal M|$ (otherwise the minimum ranges over no sets); the goal takes such an $N$ with $(N:\mathbb R)=2^m$. The printed $K(n,t,S)$ inside the minimum is read as $K(\mathcal M,t,S)$, and the printed $L(\mathcal M,t,n)$ as $L(\mathcal M,t,\log|\mathcal M|)$.
• The code-bound statements explicitly assume all metric axioms from §2.1: zero distance exactly for equal points, symmetry, and the triangle inequality. Symmetry is used because the ball condition of a code measures $\mathrm{dis}(w',c)$, while correctness is stated for $\mathrm{dis}(c,w')$. The second-sentence milestone also assumes $\mathcal M$ nonempty, which the paper leaves implicit.
• The hypothesis is the worst-case secure sketch of Definition 3, not the average-case one of Definition 4, which would weaken the lemma.
• Definition 3's efficiency requirement is dropped; no complexity theory is formalized, and no placeholder predicate replaces it.

Two trivializing formalizations are ruled out: $K(\mathcal M,t,S)$ is the largest size of a code in $S$, not a count of codes; and a code is defined by the ball condition, not by "distinct codewords are at distance greater than $t$", which is weaker in the absence of the triangle inequality.

Needed infrastructure: the min-entropy of a uniform PMF on a finset, the averaging argument over a tsum of ENNReal values, and monotonicity of Finset.inf'. The min-entropy and code definitions are reusable by every other mission of this paper. Contributions are welcome on any milestone, in any order.

Selected references

• Y. Dodis, R. Ostrovsky, L. Reyzin, A. Smith, Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data, SIAM J. Comput. 38(1):97–139, 2008. arXiv:cs/0602007v4. https://arxiv.org/abs/cs/0602007 — DOI https://doi.org/10.1137/060651380
• A. Juels, M. Wattenberg, A Fuzzy Commitment Scheme, ACM CCS 1999. https://doi.org/10.1145/319709.319714
• R. Renner, S. Wolf, Simple and Tight Bounds for Information Reconciliation and Privacy Amplification, ASIACRYPT 2005. https://doi.org/10.1007/11593447_11

Motivation

Linear programming algorithms often compute a solution to an auxiliary problem before extracting a solution to the original primal and dual pair. For a homogeneous self-dual formulation, the extraction requires a positive scaling coordinate. If that coordinate vanishes, the same auxiliary solution may instead describe infeasibility or unboundedness. Ye, Todd, and Mizuno introduced a homogeneous self-dual linear program that can start from arbitrary positive primal and dual slack vectors, even when the original programs have no known feasible point (Ye–Todd–Mizuno 1994).

Their Theorem 3 concerns strictly self-complementary optimal solutions of the auxiliary program. Theorem 9 addresses a different question: under a regularity assumption on the original programs, does a general optimal solution of the auxiliary program still have a positive scaling coordinate? The distinction matters because optimality alone does not require every complementary pair to have a positive member. This mission formalizes the statement of Theorem 9 and the numbered identities that frame it.

Setting

Fix a real matrix $A\in\mathbb R^{m\times n}$, a right-hand side $b\in\mathbb R^m$, and a cost vector $c\in\mathbb R^n$. The primal linear program (LP) minimizes $c^Tx$ subject to $Ax=b$ and $x\ge0$. Its dual (LD) maximizes $b^Ty$ subject to $A^Ty\le c$; $y\in\mathbb R^m$ is unrestricted. The dual slack is $s=c-A^Ty$.

An interior feasible point of (LP) is an $x$ with $Ax=b$ and every $x_j>0$. An interior feasible point of (LD) is a $y$ with every component of $c-A^Ty$ positive. “Interior” here is the paper's strict coordinatewise feasibility condition, not the topological interior of an equality-constrained set in ambient space. The existence of such a point implies ordinary feasibility for the corresponding program.

The paper builds an auxiliary program (HLP) from initial vectors $x^0>0$, $s^0>0$, and $y^0$. It uses the derived data

$$\bar b=b-Ax^0,\qquad \bar c=c-A^Ty^0-s^0,\qquad \bar z=c^Tx^0+1-b^Ty^0.$$

A point is a tuple $(y,x,\tau,\theta,s,\kappa)$ with $x,s,\tau,\kappa\ge0$ and free $y,\theta$. Its equality constraints are

$$\begin{aligned} Ax-b\tau+\bar b\theta&=0,\\ s&=-A^Ty+c\tau-\bar c\theta,\\ \kappa&=b^Ty-c^Tx+\bar z\theta,\\ -\bar b^Ty+\bar c^Tx-\bar z\tau&=-(x^0)^Ts^0-1. \end{aligned}$$

The objective is to minimize $((x^0)^Ts^0+1)\theta$. A feasible point is optimal when no feasible point has a smaller objective. The paper calls an optimal point self-complementary, whether or not its complementary pairs satisfy strict inequalities (p. 57, after Theorem 2(v)). After introducing the general construction, the paper fixes $y^0=0$ and $x^0=s^0=e$, the all-ones vector. That is the instance used in Theorem 9.

Formalization targets

Goal: Theorem 9

If both (LP) and (LD) have interior feasible points, then every self-complementary solution $w^*=(y^*,x^*,\tau^*,\theta^*,s^*,\kappa^*)$ of this fixed (HLP) satisfies

$$\tau^*>0.$$

The theorem quantifies over every optimal point, including those that are not strictly self-complementary. The printed tuple writes $\theta^*=0$; Theorem 2(iv) entails that fact from optimality, so it is not an extra hypothesis in the goal (Theorem 9, p. 64).

Supporting targets

Theorem 2(iv) states that (HLP) has zero optimal value and, for every feasible point under arbitrary positive initial $x^0,s^0$, satisfies

$$((x^0)^Ts^0+1)\theta=x^Ts+\tau\kappa.$$

Corollary 4 states that a positive $\kappa$ at an optimum under the fixed initialization entails infeasibility of (LP) or (LD). Equation (9) states the corresponding normalization identity

$$e^Tx+e^Ts+\tau+\kappa-(n+1)\theta=n+1.$$

These are separate milestone statements, each tied to its index and page in the paper (Theorem 2(iv), p. 57; equation (9), p. 58; Corollary 4, p. 59).

Significance

Theorem 9 says that the auxiliary model does not lose its positive scale at any optimum when the primal and dual programs are both strictly feasible. With $\tau^*>0$, the homogeneous primal and dual variables can be divided by $\tau^*$ to recover solutions in the original scale. The result applies even when the auxiliary optimum lacks strict complementarity; that is the additional coverage beyond the strictly self-complementary case of Theorem 3 (Ye–Todd–Mizuno 1994, pp. 58 and 64).

The mathematical result was proved in 1994. This mission's remaining work is a machine-checked proof of the stated regularity result and its supporting claims in the paper's specific (HLP) model. The definitions of the homogeneous feasible set, its slacks, and its optimality relation are reusable for the other results in the same paper. The full algorithm and complexity estimate belong to the other missions in this series.

Difficulty

The optimality condition controls the objective, and Theorem 2(iv) identifies that objective with a sum of complementarity terms. Those facts alone permit $\tau^*=0$; they do not force the scaling coordinate to be positive. Theorem 3's assertion for a strictly self-complementary point cannot be applied to an arbitrary optimal point, because its strict support condition may fail. The challenge is to use interior feasibility of both original programs to exclude all zero-scale optima while retaining the full set of HLP optima in the quantifier.

Formalization scope

The Lean model uses finite-dimensional real vectors indexed by Fin m and Fin n, a real matrix $A$, and a six-field HLP point in the paper's order $(y,x,\tau,\theta,s,\kappa)$. The standard-form primal and dual feasible sets are reused from a published LP definition with the same minimization and maximization orientation. Paper-specific interior predicates and the homogeneous program are defined locally. Slack fields in an HLP point are constrained to equal their formulas, so they cannot be chosen independently to make a statement true.

The model first defines (HLP) for general $x^0,y^0,s^0$ and then substitutes the paper's choice (7). It treats self-complementarity as objective minimization over the whole feasible set. Defining it by $\theta=0$ or by a complementarity equation would erase the content of Theorem 2(iv). The objective and normalization constants are exact, including the $n+1$ in the fixed instance. No real supremum or infimum is used to define optimality; it is a direct comparison against every feasible point.

The dimensions $m,n$ may be zero. Empty coordinatewise inequalities then have their usual vacuous meaning, but the equations remain in force. In particular the prescribed point $(0,e,1,1,e,1)$ is strictly feasible for every $A,b,c$, as a separate sorry-free local verification checks. This excludes an empty-feasible-set reading of the HLP definitions. Contributions proving the three numbered milestones, the goal, or reusable finite-dimensional LP lemmas are within scope.

Selected references

• Yinyu Ye, Michael J. Todd, and Shinji Mizuno, An $O(\sqrt nL)$-Iteration Homogeneous and Self-Dual Linear Programming Algorithm, Mathematics of Operations Research 19(1), 53–67, 1994. DOI 10.1287/moor.19.1.53.