All missions

Motivation

A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, computed from a common reference string $\sigma$ that both parties share, without revealing anything beyond the truth of the statement. NIZK proofs were introduced by Blum, Feldman and Micali (STOC 1988) and are a building block of chosen-ciphertext secure encryption, signatures and secure multi-party computation. For a long time every NIZK proof for all of NP was zero-knowledge only computationally: a simulator produced proofs that no efficient adversary could tell apart from real ones.

Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012; conference versions at Eurocrypt 2006 and Crypto 2006) gave the first NIZK argument for all of NP whose zero-knowledge is perfect: real and simulated proofs have exactly the same distribution, so even an unbounded adversary learns nothing. The construction is the Circuit SAT proof of their Figure 3, run on a perfectly hiding key of a homomorphic proof commitment scheme. Its zero-knowledge is Lemma 8 of the paper, and it is the zero-knowledge half of their Theorem 11.

Setting

A homomorphic proof commitment scheme has a message space $M$ (a finite cyclic group with generator $1$, here $\mathbb Z/N$), a randomizer space $R$ and a commitment space $C$, all finite abelian groups, and a commitment function $\mathrm{com}_{ck}(m; r)$. A hiding key generator $K_{\mathrm{hiding}}$ outputs a commitment key $ck$ together with a trapdoor $tk$. The scheme is assumed to have:

1. the homomorphic property, $\mathrm{com}(m_1+m_2; r_1+r_2) = \mathrm{com}(m_1; r_1)\,\mathrm{com}(m_2; r_2)$;
2. perfect trapdoor opening: $\mathrm{Topen}_{tk}(m_1, r_1, m_2)$ returns $r_2$ with $\mathrm{com}(m_2; r_2) = \mathrm{com}(m_1; r_1)$;
3. perfect trapdoor opening indistinguishability: for uniform $r_1$, the opening $\mathrm{Topen}_{tk}(m_1, r_1, m_2)$ is distributed, jointly with $ck$, as a fresh uniform randomizer;
4. perfect witness indistinguishability of a proof $P_{01}(ck, m, r; \rho)$ that a commitment contains $0$ or $1$: if $\mathrm{com}(0; r_0) = \mathrm{com}(1; r_1)$, the proofs made from $(0, r_0)$ and from $(1, r_1)$ have the same law.

A NAND circuit on $n$ wires is a list of gates $(i, j, k)$ and an output wire $\mathrm{out}$; a witness $w \in \{0,1\}^n$ satisfies it, $C(w) = 1$, if $w_k = \neg(w_i \wedge w_j)$ for every gate and $w_{\mathrm{out}} = 1$. The prover $P(\sigma, C, w)$ of Figure 3, with $\sigma = ck$, commits to every wire, $c_i = \mathrm{com}(w_i; r_i)$ with $c_{\mathrm{out}} = \mathrm{com}(1; 0)$, proves that each commitment contains $0$ or $1$, and for each gate proves that $c_i c_j c_k^2\,\mathrm{com}(-2; 0)$ contains $0$ or $1$.

The simulator is $S_1 = K_{\mathrm{hiding}}$, returning $\sigma = ck$ and $\tau = tk$, and $S_2(\sigma, \tau, C)$, which commits to $0$ on every wire except the output wire, and makes all the 0/1 proofs from openings it knows or obtains with the trapdoor. In the zero-knowledge game an adaptive adversary $A$ reads $\sigma$, submits pairs $(C, w)$ to an oracle one at a time, sees each answer before choosing the next, and outputs a bit. The real oracle answers with $P(\sigma, C, w)$, the simulation oracle with $S_2(\sigma, \tau, C)$; both answer failure when $C(w) \neq 1$.

Formalization targets

Goal: Lemma 8, perfect zero-knowledge

For every adaptive adversary $A$,

$$\Pr\big[\sigma \leftarrow S_\sigma : A^{P(\sigma,\cdot,\cdot)}(\sigma) = 1\big] = \Pr\big[(\sigma, \tau) \leftarrow S_1 : A^{S(\sigma,\tau,\cdot,\cdot)}(\sigma) = 1\big],$$

where $S_\sigma$ is $K_{\mathrm{hiding}}$ restricted to its first output.

Milestones, in the order the proof uses them

1. Gate witness (proof of Lemma 8, p. 15): with $c_i, c_j, c_k$ commitments to $0$ and $r'_k = \mathrm{Topen}_{tk}(0, r_k, 1)$,

$$c_i c_j c_k^2\,\mathrm{com}(-2; 0) = \mathrm{com}(0; r_i + r_j + 2r'_k).$$

2. Trapdoor-opened wires: $\mathrm{com}(w_i; \mathrm{Topen}_{tk}(0, r_i, w_i)) = \mathrm{com}(0; r_i)$, and the simulated commitments $(\mathrm{com}(0; r_i))_i$ have the law of the honest commitments $(\mathrm{com}(w_i; r_i))_i$.
3. Witness indistinguishability for two 0/1 openings: 0/1 proofs made from any two openings $(m, r)$, $(m', r')$ of the same commitment, $m, m' \in \{0,1\}$, have the same law.
4. One query: for every hiding key and every $(C, w)$ with $C(w) = 1$, $P(ck, C, w) \overset{d}{=} S_2(ck, tk, C)$.

Significance

Lemma 8 makes the Circuit SAT argument of Section 7 the first perfect NIZK argument for every language in NP. Combined with the computational indistinguishability of binding and hiding keys it also gives the computational zero-knowledge of the proof of Figure 3 (Theorem 6), and it is the template for the perfect zero-knowledge of the universally composable NIZK of the paper's Section 8. The same simulation pattern, commit to $0$ everywhere and use the trapdoor where an opening is needed, recurs in later pairing-based proof systems such as Groth–Sahai proofs.

The result is proved in the paper; to our knowledge it has not been machine-checked. A formal proof fixes the simulator completely, including the cases the paper leaves to the reader, and makes the adaptive multi-query argument explicit: the paper's proof treats one proof at a time and does not spell out why answering many adaptively chosen queries preserves equality of distributions.

Difficulty

The real and simulated proofs never use the same randomizers, so the proof cannot compare outputs value by value; it must compare laws. Two gaps in the printed argument need to be closed. First, witness indistinguishability is assumed only for one opening to $0$ against one opening to $1$, while comparing a simulated gate proof with a real one compares two openings that may carry the same message; the trapdoor supplies the missing intermediate opening. Second, the printed gate recipe gives the gate commitment the message $0$ only when no input of the gate is the output wire; when the output wire is an input, the message is $1$ or $2$, and $2$ has no 0/1 opening, so the simulator must open the gate commitment itself with the trapdoor. The adaptive adversary adds a third point: equality of laws must survive an arbitrary interaction in which later queries depend on earlier answers.

Formalization scope

• The message space is ZMod N with $N \ge 4$ (the paper describes Figure 3 for order at least 4, p. 14); $R$ and $R_{\mathrm{proof}}$ are finite nonempty types, $C$ a commutative group. Key generators and the 0/1 prover's randomness are probability mass functions; the coins are uniform.
• Probability-one properties are stated for every key in the support of $K_{\mathrm{hiding}}$; equalities of probabilities for all adversaries are stated as equalities of laws. Trapdoor opening indistinguishability is the joint law with $ck$, since the adversary does not see $tk$.
• The adversary is a well-founded tree of fair coin tosses and adaptive oracle queries that reads $\sigma$. Quantifying over all such trees is stronger than quantifying over polynomial-time adversaries. No running-time bound is imposed on the simulator.
• The simulator is the specific $S_2$ defined in the mission, a function of $ck$, $tk$, the circuit and fresh coins. A "simulator" that runs the honest prover on the witness would make the statement trivial and is ruled out by this definition. Each gate commitment is opened to $0$ with $\mathrm{Topen}_{tk}$, which covers the output-wire case.
• Out of scope: key indistinguishability and every computational statement (computational soundness of Theorem 11, adaptive culpable soundness, the UC results); the second sentence of Lemma 8 (perfect non-erasure zero-knowledge); the verifier of Figure 3, which zero-knowledge does not involve.
• Reusable beyond this mission: the query-tree adversary with its output law, and the abstract homomorphic proof commitment with its perfect properties. Contributions welcome: proofs of the milestones, and a general lemma that oracles with equal laws give equal output laws to every adaptive adversary.

Selected references

• J. Groth, R. Ostrovsky, A. Sahai, New Techniques for Noninteractive Zero-Knowledge, Journal of the ACM 59(3), Article 11, 2012. https://doi.org/10.1145/2220357.2220358
• J. Groth, R. Ostrovsky, A. Sahai, Perfect Non-interactive Zero Knowledge for NP, EUROCRYPT 2006, LNCS 4004. https://doi.org/10.1007/11761679_21
• J. Groth, R. Ostrovsky, A. Sahai, Non-interactive Zaps and New Techniques for NIZK, CRYPTO 2006, LNCS 4117. https://doi.org/10.1007/11818175_6
• M. Blum, P. Feldman, S. Micali, Non-Interactive Zero-Knowledge and Its Applications, STOC 1988. https://doi.org/10.1145/62212.62222
• U. Feige, D. Lapidot, A. Shamir, Multiple NonInteractive Zero Knowledge Proofs Under General Assumptions, SIAM J. Comput. 29(1), 1999. https://doi.org/10.1137/S0097539792230010
• J. Groth, A. Sahai, Efficient Non-interactive Proof Systems for Bilinear Groups, EUROCRYPT 2008, LNCS 4965. https://doi.org/10.1007/978-3-540-78967-3_24

Motivation

A prophet inequality compares two players facing the same random sequence of rewards $X_1, X_2, \dots, X_n$. The gambler sees the values one at a time and must decide, as each value arrives, whether to stop and collect it; a value passed over is lost. The prophet knows the whole sequence in advance and simply takes its maximum. In 1978 Krengel, Sucheston and Garling showed that when the $X_i$ are independent, non-negative and $\mathbb E[\max_i X_i] < \infty$, the gambler has a stopping rule $\tau$ with

$$2\,\mathbb E[X_\tau] \;\ge\; \mathbb E\big[\max_i X_i\big],$$

and that the factor $2$ cannot be improved. This inequality, labelled (1) in Kleinberg and Weinberg's Matroid Prophet Inequalities (arXiv:1201.4764, STOC 2012), is the starting point of optimal stopping theory's prophet inequalities and, more recently, of a large literature in online algorithms and algorithmic mechanism design, where it is the reason that a single posted price can extract a constant fraction of the optimal welfare or revenue.

Timeline.

• 1977: Krengel and Sucheston prove the inequality with factor 4 in place of 2 (Bull. Amer. Math. Soc. 83).
• 1978: Krengel and Sucheston publish the result attributed to Krengel, Sucheston and Garling, the factor-2 inequality (1) for independent non-negative rewards with $\mathbb E[\max_i X_i] < \infty$; the factor $2$ cannot be improved.
• 1984: Samuel-Cahn shows that a single threshold suffices: stopping at the first value above a threshold $T$ with $\Pr[\max_i X_i > T] = \tfrac12$ (a median of $\max_i X_i$) already achieves the factor $2$ (doi:10.1214/aop/1176993223).
• 2012: Kleinberg and Weinberg, introducing the matroid prophet inequality, give in §3.1 a second single-threshold rule, with threshold $T = \mathbb E[\max_i X_i]/2$, and a half-page proof that it earns at least $T$. This rule and its analysis are the rank-one case of their matroid algorithm.

This mission formalizes that §3.1 result.

Setting

Let $(\Omega, \mathcal F, \mathbb P)$ be a probability space and $n \ge 1$. Let $X_1, \dots, X_n$ be real random variables on $\Omega$ that are independent (as a family), non-negative, and such that the prophet's value $\max_i X_i$ has finite expectation. Define

$$T = \tfrac12\,\mathbb E\big[\max_i X_i\big], \qquad p = \Pr\big[\max_i X_i \ge T\big].$$

The single-threshold rule observes $X_1, X_2, \dots$ in order and stops at the first time $\tau$ with $X_\tau \ge T$, collecting $X_\tau$. If no $X_i$ reaches $T$, the rule accepts nothing and collects $0$. Write $X_\tau$ for the amount collected; it equals $X_{\tau(\omega)}(\omega)$ on the event $\{\max_i X_i \ge T\}$, which has probability $p$, and $0$ off it.

In Lean the variables are X : Fin n → Ω → ℝ with [NeZero n]; $\max_i X_i$ is maxX X, $T$ is thr P X, $p$ is stopProb P X, and $X_\tau$ is reward P X, all in the namespace MatroidProphetKW.RankOne.

Formalization targets

Goal: the half-mean threshold rule

$$\mathbb E[X_\tau] \;\ge\; T \;=\; \tfrac12\,\mathbb E\big[\max_i X_i\big].$$

This is inequality (1) for an explicit rule, which is stronger than (1)'s existence statement. The constant $\tfrac12$ is sharp, so the goal is stated with it.

Milestones (in the order the paper's argument uses them)

1. Tail bound, for every $x > T$:

$$\Pr[X_\tau > x] \;\ge\; (1-p)\sum_{i=1}^n \Pr[X_i > x].$$

2. Comparison with the prophet's tail, for every $x > T$:

$$\Pr[X_\tau > x] \;\ge\; (1-p)\,\Pr\big[\max_i X_i > x\big].$$

3. The prophet's upper tail:

$$\int_T^\infty \Pr\big[\max_i X_i > x\big]\,dx \;\ge\; T.$$

4. The gambler's lower tail:

$$\int_0^T \Pr[X_\tau > x]\,dx \;\ge\; pT.$$

Significance

The result. A threshold that depends on the distributions only through one number, $\mathbb E[\max_i X_i]$, already matches the optimal worst-case guarantee of the best stopping rule. Because it is a single price, the rule translates directly into a posted-price mechanism: a seller who posts the price $T$ to arriving buyers obtains half of the expected maximum value. The same accounting, in which accepted value is charged against the threshold and rejected value against the probability of having accepted nothing, is what Kleinberg and Weinberg generalize to matroids (missions 1 and 2 of this series).

Formalizing it. The result is proved and classical; the work here is to formalize its known proof. No machine-checked proof of the factor-2 prophet inequality is in Mathlib, and none was found among the platform's published theorems in October 2026. A completed development provides the inequality itself, the tail comparisons, and the layer-cake bookkeeping for a stopped reward, all of which are reusable for other single-threshold prophet inequalities (Samuel-Cahn's median rule, $k$-choice and posted-price variants).

Difficulty

The expected reward of the rule is not a function of the marginals of the individual $X_i$ alone in an obvious way: the event that the rule is still running when $X_i$ arrives depends on $X_1, \dots, X_{i-1}$, and the reward is $X_\tau$ at a random index. The natural first attempt, comparing $X_\tau$ and $\max_i X_i$ pointwise, fails, since on a given outcome the rule may stop early at a value just above $T$ while the maximum comes later. The comparison has to be made between distributions, at each level $x$, and it has to use independence to decouple "nothing accepted before time $i$" from "$X_i > x$". The rest is measure-theoretic bookkeeping that is routine on paper and not routine in Lean: expressing expectations of non-negative variables as integrals of tail probabilities, splitting them at $T$, and keeping track of integrability.

Formalization scope

• Probability space. Ω with a MeasurableSpace, P : Measure Ω with [IsProbabilityMeasure P].
• Variables. X : Fin n → Ω → ℝ, [NeZero n]; each X i measurable; iIndepFun X P (mutual independence); 0 ≤ X i ω for all i, ω; Integrable (maxX X) P, which is the paper's $\mathbb E[\max_i X_i] < \infty$.
• Maximum. Finset.sup' over the nonempty index set; no junk supremum.
• Expectations and probabilities. Bochner integrals (∫ ω, … ∂P) and Measure.real probabilities. Tail integrals are Lebesgue integrals of $x \mapsto \Pr[\cdot > x]$ over $(T, \infty)$ and $(0, T]$.
• Weak and strict inequalities are as printed: the rule stops at $X_\tau \ge T$, $p = \Pr[\max_i X_i \ge T]$, tails are $\Pr[\cdot > x]$, for $x > T$.
• The rule may accept nothing. The reward is $0$ when no value reaches $T$; the rule is not forced to stop at $X_n$.

The threshold $T$ is a definition, $\mathbb E[\max_i X_i]/2$, not a free parameter constrained by hypotheses; a formalization in which $T$ is arbitrary and the upper-tail bound is assumed would make the goal a rearrangement of its hypotheses, and is ruled out.

Infrastructure that a complete development needs, and that is welcome as separate contributions: the layer-cake formula $\mathbb E[Y] = \int_0^\infty \Pr[Y > x]\,dx$ for non-negative integrable $Y$ split at a level $T$ (Mathlib has the unsplit form, MeasureTheory.integral_eq_integral_meas_lt); measurability and integrability of the stopped reward (it is dominated by $\max_i X_i$); and the probability of the event "the first $i-1$ values are below $T$ and $X_i > x$" as a product under iIndepFun.

Selected references

• Robert Kleinberg and S. Matthew Weinberg, Matroid Prophet Inequalities, STOC 2012, pp. 123–136; preprint arXiv:1201.4764v1, 2012. https://arxiv.org/abs/1201.4764 (doi:10.1145/2213977.2213991)
• Ulrich Krengel and Louis Sucheston, Semiamarts and finite values, Bulletin of the American Mathematical Society 83, 1977, pp. 745–747.
• Ulrich Krengel and Louis Sucheston, On semiamarts, amarts, and processes with finite value, Advances in Probability and Related Topics 4, 1978, pp. 197–266.
• Ester Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Annals of Probability 12(4), 1984, pp. 1213–1216. https://doi.org/10.1214/aop/1176993223

Motivation

A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, computed from a common reference string $\sigma$ that both parties share, without revealing why the statement is true. NIZK proofs were introduced by Blum, Feldman and Micali (STOC 1988). They are a basic component of chosen-ciphertext secure encryption, signature schemes and secure multi-party computation.

Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012; conference versions at EUROCRYPT 2006 and CRYPTO 2006) built NIZK proofs for all of NP from bilinear groups. The construction rests on one abstraction, the homomorphic proof commitment, and one protocol, the NIZK proof for Circuit SAT of their Figure 3. Theorem 6 says that the Figure 3 protocol works for every homomorphic proof commitment. This mission formalizes the part of Theorem 6 that holds exactly, with no computational assumption.

Setting

A homomorphic proof commitment scheme (Section 3) has a message space $\mathcal M$, a finite cyclic group $(\mathcal M,+,0)$ with generator $1$. It also has a randomizer space $(\mathcal R,+,0)$ and a commitment space $(\mathcal C,\cdot,1)$, both finite abelian groups. It comes with algorithms $(K_{\mathrm{binding}},K_{\mathrm{hiding}},\mathrm{com},\mathrm{Topen},P_{01},V_{01})$:

• $K_{\mathrm{binding}}$ outputs a commitment key $ck$ and an extraction key $xk$; $K_{\mathrm{hiding}}$ outputs $ck$ and a trapdoor key $tk$;
• $\mathrm{com}(m;r)\in\mathcal C$ commits to $m\in\mathcal M$ with randomizer $r\in\mathcal R$;
• $P_{01}(ck,m,r;\rho)$ proves that a commitment contains $0$ or $1$, and $V_{01}(ck,c,\pi)$ checks such a proof;
• $\mathrm{Ext}_{xk}$ recovers a committed bit when the scheme has perfect extractability.

The exact properties used here are the following. The homomorphic property is $\mathrm{com}(m_1+m_2;r_1+r_2)=\mathrm{com}(m_1;r_1)\,\mathrm{com}(m_2;r_2)$ on keys of either mode. Perfect binding says that on binding keys no commitment has openings to two different messages. Perfect completeness of the 0/1 proof says that honest proofs for $(m,r)\in\{0,1\}\times\mathcal R$ are always accepted, on keys of either mode. Perfect soundness of the 0/1 proof says that on binding keys an accepted proof implies $c=\mathrm{com}(m;r)$ for some $(m,r)\in\{0,1\}\times\mathcal R$. Perfect extractability says that on binding keys $\mathrm{Ext}_{xk}(\mathrm{com}(m;r))=m$ for $m\in\{0,1\}$.

A NAND circuit $C$ on wires $1,\dots,n$ is a list of gates $(i,j,k)$, with inputs $i,j$ and output $k$, and an output wire $\mathrm{out}$. An assignment $w$ satisfies it, $C(w)=1$, when $w_k=\neg(w_i\wedge w_j)$ for every gate and $w_{\mathrm{out}}=1$.

The protocol of Figure 3 takes $\sigma=ck$ with $(ck,xk)\leftarrow K_{\mathrm{binding}}$. The prover commits to every wire, $c_i=\mathrm{com}(w_i;r_i)$, with $c_{\mathrm{out}}=\mathrm{com}(1;0)$. It proves with $P_{01}$ that each $c_i$ contains $0$ or $1$. For each gate $(i,j,k)$ it proves that $c_ic_jc_k^2\,\mathrm{com}(-2;0)$ contains $0$ or $1$, using message $w_i+w_j+2w_k-2$ and randomizer $r_i+r_j+2r_k$. The verifier checks $c_{\mathrm{out}}=\mathrm{com}(1;0)$ and every 0/1 proof.

Formalization targets

Goal: Theorem 6, exact part

If $|\mathcal M|\ge 4$ and the scheme has the homomorphic property, perfect binding, and perfectly complete and perfectly sound 0/1 proofs, then

$$\text{perfect completeness}\ \wedge\ \text{perfect soundness}\ \wedge\ \big(\text{perfect extractability}\Rightarrow\text{perfect knowledge extraction}\big).$$

The theorem holds for every scheme with these properties, with no assumption on how the scheme is built.

Milestones

• Lemma 5. For bits $b_0,b_1,b_2$ in a cyclic group of order at least $4$, $b_2=\neg(b_0\wedge b_1)$ iff $b_0+b_1+2b_2-2\in\{0,1\}$. Order $3$ needs the extra condition $b_0+b_1+b_2-1\in\{0,1\}$.
• The gate commitment. $c_0c_1c_2^2\,\mathrm{com}(-2;0)$ commits to $b_0+b_1+2b_2-2$, and on a binding key an accepted 0/1 proof for it forces $b_2=\neg(b_0\wedge b_1)$.
• Perfect completeness (proof of Theorem 6), on keys of either mode.
• Lemma 7. Perfect soundness on binding keys.
• Knowledge extraction (proof of Theorem 6). The wires $w_i=[\mathrm{Ext}_{xk}(c_i)=1]$ of an accepted proof satisfy $C$.

Significance

Theorem 6 is the step from a commitment primitive to NIZK proofs for an NP-complete language. With the subgroup-decision commitment of Section 4 or the decisional-linear commitment of Section 5 it gives Corollaries 9 and 10: perfectly sound NIZK proofs for Circuit SAT with proofs of size $O(|C|k)$. When the common reference string is instead a hiding key, the same protocol becomes the perfect NIZK argument of Theorem 11. Its completeness clause is the hiding-key half of the completeness formalized here.

The result is proved in the paper. Lemma 5 and the soundness of the circuit protocol are left to the reader there or proved in three sentences. No machine-checked proof of this theorem, or of any commitment-based NIZK, was found in Mathlib or in the public Lean libraries searched. This mission states its exact content against an abstract scheme interface. The same interface can then be instantiated by machine-checked versions of the concrete commitments, which are the third and fourth missions of this series.

Difficulty

The argument is short, so the difficulty lies in the bookkeeping. On a binding key the verifier only learns that each commitment opens to some bit. Perfect binding is what identifies the message a gate proof certifies with $b_i+b_j+2b_k-2$, which in turn identifies it with the wire bits. Lemma 5 must then be checked in $\mathbb Z/N\mathbb Z$ rather than in the integers, where $-2$, $-1$ and $2$ must be shown to differ from $0$ and $1$. This is exactly where $N\ge4$ enters: for $N=3$ the all-zero assignment passes every gate check, since $-2=1$. The output wire is handled by the literal check $c_{\mathrm{out}}=\mathrm{com}(1;0)$ together with binding. Completeness needs the prover's convention $r_{\mathrm{out}}=0$ to be used consistently in the gate proofs.

Formalization scope

• The message space is ZMod N. A finite cyclic group with a chosen generator $1$ is this group, and every theorem that needs it assumes 4 ≤ N, the paper's restriction on p. 14.
• The randomizer and commitment spaces are a finite AddCommGroup and a finite CommGroup. Key generators are PMFs. $P_{01}$ takes its randomness as an argument.
• Each perfect property of Section 3 is its own Prop, quantified over the support of the relevant generator. The paper's "for all adversaries, $\Pr[\dots]=1$" (or $=0$) is equivalent for unbounded adversaries.
• Soundness of the 0/1 proof is assumed on binding keys only. Assuming it on hiding keys as well would be inconsistent with a real scheme and is not done.
• Circuits are lists of NAND gates on Fin n with an output wire. No acyclicity is required, so the statements cover every system of NAND constraints.
• The extractor is fixed to the paper's $E_1=K_{\mathrm{binding}}$ and $E_2$, which reads each wire as $[\mathrm{Ext}_{xk}(c_i)=1]$. An existentially quantified, computationally unbounded extractor would turn knowledge extraction into a restatement of soundness, and that trivializing reading is excluded.

Dropped, because they are computational:

• computational zero-knowledge and computational non-erasure zero-knowledge (Theorem 6);
• key indistinguishability;
• the size bounds of Corollaries 9 and 10.

Perfect zero-knowledge on hiding keys (Lemma 8) is the second mission of this series. The definitions of this mission (the scheme interface, NAND circuits, the protocol) are reusable by any formalization of commitment-based proof systems. Proofs of the milestones are welcome in any order.

Selected references

• J. Groth, R. Ostrovsky, A. Sahai, New Techniques for Noninteractive Zero-Knowledge, Journal of the ACM 59(3), Article 11, 2012. https://doi.org/10.1145/2220357.2220358
• J. Groth, R. Ostrovsky, A. Sahai, Perfect Non-interactive Zero Knowledge for NP, EUROCRYPT 2006, LNCS 4004, pp. 339–358. https://doi.org/10.1007/11761679_21
• J. Groth, R. Ostrovsky, A. Sahai, Non-interactive Zaps and New Techniques for NIZK, CRYPTO 2006, LNCS 4117, pp. 97–111. https://doi.org/10.1007/11818175_6
• M. Blum, P. Feldman, S. Micali, Non-interactive zero-knowledge and its applications, STOC 1988, pp. 103–112. https://doi.org/10.1145/62212.62222
• D. Boneh, E.-J. Goh, K. Nissim, Evaluating 2-DNF Formulas on Ciphertexts, TCC 2005, LNCS 3378, pp. 325–341. https://doi.org/10.1007/978-3-540-30576-7_18

Why the penalty parameter matters

Augmented Lagrangian methods solve a constrained problem by minimizing a sequence of penalized subproblems while updating estimates of the Lagrange multipliers. Each subproblem carries a penalty parameter $\rho_k$. When $\rho_k$ grows without bound the subproblems become ill-conditioned and hard to solve, and the method behaves like a plain external penalty method. Avoiding that growth is one of the main reasons for using multiplier updates at all, so conditions under which $\rho_k$ stays bounded matter both in theory and in practice (Bertsekas 1982; Conn, Gould, Toint 1991).

Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18 (2007); HAL hal-01295437) propose an augmented Lagrangian method, Algorithm 3.1, in which only some of the constraints are penalized. Their §5 shows that, under classical local hypotheses at the limit point and a subproblem tolerance tied to the current infeasibility, the penalty parameters remain bounded. This mission formalizes that result for equality-constrained problems (Theorem 5.4), together with the general case (Theorem 5.5) as a companion statement.

Setting

Let $f:\mathbb R^n\to\mathbb R$, $h_1:\mathbb R^n\to\mathbb R^{m_1}$, $g_1:\mathbb R^n\to\mathbb R^{p_1}$, $h_2:\mathbb R^n\to\mathbb R^{m_2}$, $g_2:\mathbb R^n\to\mathbb R^{p_2}$ be continuously differentiable. Problem (2.1) is

$$\text{Minimize } f(x)\ \text{ subject to } h_1(x)=0,\ g_1(x)\le0,\ h_2(x)=0,\ g_2(x)\le0 .$$

The upper-level constraints $h_1,g_1$ are penalized by the PHR augmented Lagrangian

$$L(x,\lambda,\mu,\rho)=f(x)+\frac\rho2\sum_{i=1}^{m_1}\Big([h_1(x)]_i+\frac{\lambda_i}\rho\Big)^2+\frac\rho2\sum_{i=1}^{p_1}\Big([g_1(x)]_i+\frac{\mu_i}\rho\Big)_+^2,$$

while the lower-level constraints $h_2,g_2$ stay in the subproblems.

Algorithm 3.1 fixes $\tau\in[0,1)$, $\gamma>1$, $\rho_1>0$, a box $[\bar\lambda_{\min},\bar\lambda_{\max}]$, a bound $\bar\mu_{\max}\ge0$ and tolerances $\varepsilon_k\to0$. At outer iteration $k\ge1$ it finds $x_k$ and lower-level multipliers $v_k,u_k$ such that $x_k$ is an $\varepsilon_k$-approximate KKT point of minimizing $L(\cdot,\bar\lambda_k,\bar\mu_k,\rho_k)$ over the lower-level set, in the sense of (3.1)–(3.4). It then forms the first-order multiplier estimates

$$\lambda_{k+1}=\bar\lambda_k+\rho_k h_1(x_k),\qquad \mu_{k+1}=\max\{0,\bar\mu_k+\rho_k g_1(x_k)\},$$

and safeguarded estimates $\bar\lambda_{k+1},\bar\mu_{k+1}$, which in §5 are the projections of $\lambda_{k+1},\mu_{k+1}$ on their boxes. Finally it updates the penalty parameter: with $[\sigma_k]_i=\max\{[g_1(x_k)]_i,-[\bar\mu_k]_i/\rho_k\}$,

$$\rho_{k+1}=\begin{cases}\rho_k & \text{if } \max\{\|h_1(x_k)\|_\infty,\|\sigma_k\|_\infty\}\le\tau\max\{\|h_1(x_{k-1})\|_\infty,\|\sigma_{k-1}\|_\infty\},\\ \gamma\rho_k & \text{otherwise.}\end{cases}$$

In §5.1 there are no inequality constraints ($p_1=p_2=0$): problem (5.1), with Lagrangian $L_0(x,\lambda,v)=f(x)+\langle h_1(x),\lambda\rangle+\langle h_2(x),v\rangle$. Assumptions 1–6 at the limit $x_*$ of $\{x_k\}$ are: convergence, feasibility, linear independence of all constraint gradients, $C^2$ near $x_*$, the second-order sufficient condition with multipliers $\lambda_*,v_*$, and $\lambda_*$ in the interior of the safeguard box.

Formalization targets

Goal: Theorem 5.4

Under Assumptions 1–6, $\tau>0$, and $\varepsilon_k\le\eta_k\|h_1(x_k)\|_\infty$ for a sequence $\eta_k\to0$,

$$\sup_k\rho_k<\infty .$$

Milestones, in attack order

1. Proposition 5.1: $\lambda_k\to\lambda_*$, $v_k\to v_*$, and $\bar\lambda_k=\lambda_k$ for $k$ large.
2. Lemma 5.2: there is $\bar\rho>0$ such that for all $\pi\in[0,1/\bar\rho]$

$$\begin{pmatrix}\nabla^2_{xx}L_0(x_*,\lambda_*,v_*)&\nabla h_1(x_*)&\nabla h_2(x_*)\\ \nabla h_1(x_*)^T&-\pi I&0\\ \nabla h_2(x_*)^T&0&0\end{pmatrix}\ \text{is nonsingular.}$$

3. Lemma 5.3: if $\rho_k\ge\bar\rho$ eventually, then for $k$ large

$$\|x_k-x_*\|,\ \|\lambda_{k+1}-\lambda_*\|\le M\max\Big\{\tfrac{\|\bar\lambda_k-\lambda_*\|_\infty}{\rho_k},\|\alpha_k\|,\|\beta_k\|\Big\},$$

with $\alpha_k=\nabla L(x_k,\bar\lambda_k,\rho_k)+\nabla h_2(x_k)v_k$ and $\beta_k=h_2(x_k)$. 4. (5.10): if $\rho_k\to\infty$, then $\|h_1(x_k)\|_\infty\le C\|\lambda_k-\lambda_*\|_\infty/\rho_k$ for $k$ large. 5. Contraction: if $\rho_k\to\infty$, then $\|h_1(x_k)\|_\infty\le (C/\rho_k)\|h_1(x_{k-1})\|_\infty$ for $k$ large.

Companion statements

Theorem 5.5, the general problem (2.1) under Assumptions 7–13 (LICQ, $C^2$, a second-order condition on the tangent subspace of all active constraints, multipliers inside the safeguard boxes, strict complementarity for the active upper-level inequalities), with $\varepsilon_k\le\eta_k\max\{\|h_1(x_k)\|_\infty,\|\sigma_k\|_\infty\}$; and two steps of its proof, (5.13) and (5.14).

Significance

Theorem 5.4 tells a user of the method when it does not degenerate: if the safeguard box contains the true multipliers and the subproblems are solved to a precision proportional to the current infeasibility, then the penalty parameter is eventually constant. The Remark after Theorem 5.5 draws the practical conclusion that the box should be large enough to contain the true multipliers. The result underlies the analysis of the ALGENCAN solver built on Algorithm 3.1.

The results are proved on paper. To our knowledge none of them, nor the PHR augmented Lagrangian method itself, has a machine-checked formalization. A formal proof would also pin down two gaps in the printed statements, recorded under Formalization scope: the case $\tau=0$ and the early iterations in Lemma 5.3. The local analysis (a uniformly nonsingular KKT matrix and implicit-function error bounds for multiplier estimates) is reusable for other augmented Lagrangian and SQP methods.

Difficulty

Without the second-order structure there is no reason for $\rho_k$ to stay bounded: the update test compares consecutive infeasibilities, and nothing in the global theory forces them to decrease geometrically. The local argument has to show that $\|h_1(x_k)\|_\infty$ contracts by a factor of order $1/\rho_k$, which requires error bounds for both $x_k$ and $\lambda_{k+1}$ that hold uniformly as $1/\rho_k$ varies in an interval containing $0$. The uniformity in the perturbation parameter $\pi=1/\rho_k$, around the singular-looking limit $\pi=0$, is the central difficulty. Applying the implicit function theorem at each fixed $\rho$ does not give it.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Constraint maps are families of real functions indexed by Fin m, and problem (5.1) is (2.1) with $p_1=p_2=0$. The norm in (3.1), on $x$ and on $\alpha_k$ is Euclidean. Every $\|\cdot\|_\infty$, and the norms in (3.4), on $\lambda$ and on $\beta_k$, are the sup norm. The paper's norm is arbitrary and the constants absorb the change. A run of Algorithm 3.1 is a predicate on sequences: x 0 is $x_0$, the outer iterations are $k\ge1$, and the three tolerances of Step 2 are kept separate. The gradient in (3.1) is the true gradient of the defined augmented Lagrangian. "Continuous first derivatives" is $C^1$ on $\mathbb R^n$; "continuous second derivatives near $x_*$" is ContDiffAt ℝ 2. Hessians are derivatives of gradients. Every statement that uses a Hessian assumes $C^2$ at $x_*$, so it cannot be a junk value. Assumption 5 is pinned to Fletcher's equality-constrained second-order sufficient condition. Linear independence is that of a family indexed by a sum type, so equal gradients count as dependent.

Added hypotheses, each stated in the item's Formalization Note:

• $\tau>0$ in Theorems 5.4 and 5.5. With $\tau=0$ the theorem is false.
• Lemma 5.3 holds for $k\ge k_1$ instead of every $k$. It is false at early iterations.
• In Proposition 5.1, $\lambda_*,v_*$ are Lagrange multipliers at $x_*$.
• In Theorem 5.5, the multipliers are KKT multipliers of (2.1), and strict complementarity holds for the active lower-level inequalities. Without it the theorem fails when $\tau\gamma<1$.

Statements that would trivialize the goal are excluded. These include a run predicate that no sequence satisfies, merging the three tolerances into $\varepsilon_k$, collapsing gradient families into sets, a junk Hessian, and assuming $\rho_k\to\infty$ or $\rho_k\ge\bar\rho$ in the goal. The last two appear only as milestone hypotheses.

A complete development needs the PHR gradient formula, uniform invertibility of a continuous family of matrices on a compact interval, a quantitative inverse function estimate for $C^1$ maps, and the convergence of multiplier estimates under LICQ. Proofs of any milestone, and reusable lemmas for these pieces, are welcome.

Selected references

• R. Andreani, E. G. Birgin, J. M. Martínez, M. L. Schuverdt, On augmented Lagrangian methods with general lower-level constraints, SIAM J. Optim. 18(4), 2007, 1286–1309. https://doi.org/10.1137/060654797 (HAL hal-01295437v1: https://hal.science/hal-01295437)
• R. Fletcher, Practical Methods of Optimization, 2nd ed., Wiley, 1987. https://doi.org/10.1002/9781118723203
• D. P. Bertsekas, Constrained Optimization and Lagrange Multiplier Methods, Academic Press, 1982. https://doi.org/10.1016/C2013-0-10366-2
• A. R. Conn, N. I. M. Gould, Ph. L. Toint, A globally convergent augmented Lagrangian algorithm for optimization with general constraints and simple bounds, SIAM J. Numer. Anal. 28(2), 1991, 545–572. https://doi.org/10.1137/0728030

Motivation

Augmented Lagrangian methods (the method of multipliers of Hestenes, Powell and Rockafellar) solve a constrained nonlinear program by a sequence of easier subproblems in which some constraints are moved into the objective through a penalty term plus a multiplier estimate. Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18 (2007); preprint HAL hal-01295437) split the constraints into upper-level constraints, which are penalized, and lower-level constraints, which are kept in every subproblem and may be arbitrary (not only bounds). This is the design of the solver ALGENCAN and of its successors.

A practical method usually cannot guarantee that its iterates approach a feasible point: the problem may be infeasible, and even when it is not, a local method may stall. The question this mission formalizes is what a limit point of the method is when the penalty parameter is or is not driven to infinity. The answer, Theorem 4.1 of the paper, states that infeasible limit points are not arbitrary: they are stationary for the problem of minimizing the upper-level infeasibility over the lower-level set, unless a weak constraint qualification fails there.

Setting

The problem is (2.1):

$$\text{Minimize } f(x)\ \text{ subject to }\ h_1(x)=0,\ g_1(x)\le0,\ h_2(x)=0,\ g_2(x)\le0,$$

with $f:\mathbb R^n\to\mathbb R$, $h_1:\mathbb R^n\to\mathbb R^{m_1}$, $g_1:\mathbb R^n\to\mathbb R^{p_1}$, $h_2:\mathbb R^n\to\mathbb R^{m_2}$, $g_2:\mathbb R^n\to\mathbb R^{p_2}$, all continuously differentiable. Write $\Omega_1=\{x: h_1(x)=0,\ g_1(x)\le0\}$ and $\Omega_2=\{x: h_2(x)=0,\ g_2(x)\le0\}$.

The PHR augmented Lagrangian (2.2) with respect to $\Omega_1$ is, for $\rho>0$, $\lambda\in\mathbb R^{m_1}$, $\mu\in\mathbb R^{p_1}_+$,

$$L(x,\lambda,\mu,\rho)=f(x)+\frac\rho2\sum_{i=1}^{m_1}\Big([h_1(x)]_i+\frac{\lambda_i}\rho\Big)^2+\frac\rho2\sum_{i=1}^{p_1}\Big([g_1(x)]_i+\frac{\mu_i}\rho\Big)_+^2 .$$

Algorithm 3.1 has parameters $\tau\in[0,1)$, $\gamma>1$, $\rho_1>0$, boxes $[\bar\lambda_{\min},\bar\lambda_{\max}]$ and $[0,\bar\mu_{\max}]$, and tolerances $\varepsilon_k\ge0$ with $\varepsilon_k\to0$. At outer iteration $k=1,2,\dots$ it finds $x_k$ and lower-level multipliers $v_k$, $u_k\ge0$ satisfying the approximate KKT conditions (3.1)–(3.4) of minimizing $L(\cdot,\bar\lambda_k,\bar\mu_k,\rho_k)$ over $\Omega_2$ to tolerance $\varepsilon_k$; it chooses new safeguarded multipliers $\bar\lambda_{k+1}$, $\bar\mu_{k+1}$ in the boxes; and it keeps $\rho_{k+1}=\rho_k$ when

$$\max\{\|h_1(x_k)\|_\infty,\|\sigma_k\|_\infty\}\le\tau\max\{\|h_1(x_{k-1})\|_\infty,\|\sigma_{k-1}\|_\infty\},\qquad[\sigma_k]_i=\max\Big\{[g_1(x_k)]_i,-\frac{[\bar\mu_k]_i}{\rho_k}\Big\},$$

and sets $\rho_{k+1}=\gamma\rho_k$ otherwise. A run is a sequence produced this way in which the subproblem of Step 2 is always solvable.

A point $x$ is a KKT point of a problem with objective $F$, equalities $H_i$ and inequalities $G_j$ if it is feasible and $\nabla F(x)+\sum_i a_i\nabla H_i(x)+\sum_j b_j\nabla G_j(x)=0$ for some $a$ and some $b\ge0$ vanishing on inactive inequalities. The constant positive linear dependence condition (CPLD, Qi and Wei) holds at $x$ if every nontrivial null combination of gradients of equalities and active inequalities, with nonnegative coefficients on the inequalities, has gradients that remain linearly dependent at every point near $x$. CPLD is weaker than both LICQ and the Mangasarian–Fromovitz condition.

Formalization targets

Goal: Theorem 4.1

Let $\{x_k\}$ be a run and $x_*$ a limit point of it. If $\{\rho_k\}$ is bounded, then $x_*\in\Omega_1\cap\Omega_2$. Otherwise at least one of the following holds:

1. $x_*$ is a KKT point of

$$\text{Minimize }\frac12\Big[\sum_{i=1}^{m_1}[h_1(x)]_i^2+\sum_{i=1}^{p_1}\max\{0,[g_1(x)]_i\}^2\Big]\ \text{ subject to } x\in\Omega_2; \tag{4.1}$$

2. $x_*$ does not satisfy CPLD with respect to the constraints $h_2,g_2$ defining $\Omega_2$.

Milestones

1. Every limit point lies in $\Omega_2$.
2. If $\{\rho_k\}$ is bounded, $\|h_1(x_k)\|_\infty\to0$ and $\|\sigma_k\|_\infty\to0$.
3. If $\{\rho_k\}$ is bounded, every limit point is feasible (the first half of the goal).
4. (4.2): the residual $\delta_k$ of (3.1), with $\nabla L$ written out from (2.2), satisfies $\|\delta_k\|\le\varepsilon_k$ and $\delta_k\to0$.
5. Carathéodory's theorem for cones with free and nonnegative generators, with a linearly independent support, as used for (4.3).

Significance

Theorem 4.1 is the feasibility half of the global convergence theory of the method; Theorem 4.2 of the same paper (a companion mission) shows that feasible limit points satisfying CPLD are KKT points of (2.1). Together they say that the method either finds a stationary point of the original problem or a stationary point of the infeasibility, under a constraint qualification weaker than MFCQ and only at the limit point. Because the lower-level set is arbitrary, the theorem covers the many variants in which bounds, linear constraints or structured sets are kept out of the penalty.

The result is proved in the paper; no machine-checked proof of it is known. Formalizing it requires the gradient of the PHR function, a conic Carathéodory theorem with linear independence (Mathlib contains only the convex-hull version), and the subsequence and normalization arguments of the proof. Each is reusable: milestone 5 is used again, unchanged, in the proof of Theorem 4.2.

Difficulty

The bounded case is elementary. The unbounded case is where the work lies. Dividing the approximate stationarity condition by $\rho_k$ removes the objective and the multiplier estimates, but the lower-level multipliers $v_k,u_k$ divided by $\rho_k$ need not stay bounded, so no limit can be taken directly. The supports of the lower-level combinations must first be reduced to linearly independent ones, uniformly along a subsequence, before the bounded/unbounded dichotomy on the reduced multipliers yields either a KKT point of (4.1) or a nontrivial null combination at $x_*$ whose gradients are independent at points arbitrarily close to $x_*$. Taking limits of the original multipliers without this reduction does not work.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); constraint maps are families of real functions indexed by Fin m. Continuous differentiability "on a sufficiently large and open domain" is read as $C^1$ on all of $\mathbb R^n$. The norm in (3.1) is the Euclidean one; (3.4), Step 4 and the vectors $h_1(x_k)$, $\sigma_k$ use the sup norm. The paper's norm is arbitrary and the results do not depend on the choice. A run is a predicate on sequences indexed by $\mathbb N$: x 0 is the initial point $x_0$, the outer iterations are $k\ge1$, the three subproblem tolerances $\varepsilon_{k,1},\varepsilon_{k,2},\varepsilon_{k,3}$ are kept separate, and $\nabla L$ is the true gradient of the defined function (2.2). "Limit point" is a cluster point of the sequence; "bounded" is boundedness above of $\{\rho_k\}$. KKT and CPLD are defined once for arbitrary finite index types; CPLD carries no feasibility clause, and linear independence is that of a family indexed by a disjoint union, so a repeated gradient counts as dependent.

No hypothesis is added to Theorem 4.1 beyond the $C^1$ reading. Junk values cannot trivialize the statement: the run evaluates (2.2) and $\sigma_k$ only at $\rho_k\ge\rho_1>0$; the gradients are taken of $C^1$ functions; the run is satisfiable; and both alternatives (i) and (ii) can fail at the same point, so the second half of the theorem has content.

Contributions are welcome on every milestone. The gradient computation (4.2) and the conic Carathéodory theorem are self-contained and useful beyond this paper.

Selected references

• R. Andreani, E. G. Birgin, J. M. Martínez, M. L. Schuverdt, On augmented Lagrangian methods with general lower-level constraints, SIAM J. Optim. 18(4), 1286–1309, 2007. https://doi.org/10.1137/060654797 (preprint: https://hal.science/hal-01295437)
• L. Qi, Z. Wei, On the constant positive linear dependence condition and its application to SQP methods, SIAM J. Optim. 10(4), 963–981, 2000. https://doi.org/10.1137/S1052623497326629
• R. Andreani, J. M. Martínez, M. L. Schuverdt, On the relation between constant positive linear dependence condition and quasinormality constraint qualification, J. Optim. Theory Appl. 125, 473–483, 2005. https://doi.org/10.1007/s10957-004-1861-9
• D. P. Bertsekas, Nonlinear Programming, 2nd ed., Athena Scientific, 1999 (Carathéodory's theorem for cones, p. 689).

Motivation

The effective resistance between two vertices of a weighted graph is the voltage difference that appears between them when the graph is viewed as an electrical network, edge weights being conductances, and one unit of current is injected at one vertex and extracted at the other. Effective resistances drive the spectral sparsification algorithm of Spielman and Srivastava (arXiv:0803.0929): sampling each edge with probability proportional to its weight times its effective resistance yields a sparse graph whose Laplacian approximates the original one. They are also used as a distance on graphs in the analysis of social and small-world networks, where they reflect how many short paths connect two vertices.

Computing every effective resistance exactly requires the pseudoinverse of the Laplacian, which costs far more than the size of the graph. Section 4 of the paper shows that all of them can be approximated in nearly linear time: a random projection compresses the relevant vectors to $O(\log n)$ dimensions, and the projected vectors are obtained from $O(\log n)$ calls to a fast approximate Laplacian solver (Spielman–Teng). This mission formalizes the deterministic statement that makes this procedure correct, Lemma 9: approximate solves, at a stated accuracy, do not destroy the approximation that the random projection provides.

Setting

Let $G=(V,E,w)$ be a connected, simple, weighted undirected graph with $n=|V|$ vertices, edge set $E$ and edge weights $w_e>0$. Orient every edge arbitrarily, so that it has a head and a tail. The signed incidence matrix $B\in\mathbb R^{E\times V}$ has $B(e,v)=1$ if $v$ is the head of $e$, $-1$ if $v$ is its tail, and $0$ otherwise. With $W$ the diagonal matrix of weights, the Laplacian is $L=B^{\mathsf T}WB$, a symmetric positive semidefinite matrix whose kernel is spanned by the all-ones vector when $G$ is connected. Its Moore–Penrose pseudoinverse is $L^+=\sum_{\lambda_i\neq 0}\lambda_i^{-1}u_iu_i^{\mathsf T}$, where $u_i$ are orthonormal eigenvectors of $L$ with nonzero eigenvalues $\lambda_i$.

For a vertex $u$ let $\chi_u$ be its indicator vector. The effective resistance between $u$ and $v$ is

$$R_{uv}=(\chi_u-\chi_v)^{\mathsf T}L^+(\chi_u-\chi_v),$$

and $R_e=R_{ab}$ for an edge $e$ with endpoints $a,b$. The $L$-norm of $y\in\mathbb R^V$ is $\|y\|_L=\sqrt{y^{\mathsf T}Ly}$. Let $w_{\min}$ and $w_{\max}$ be the smallest and largest edge weights.

A resistance sketch is a $k\times n$ matrix $Z$ (columns indexed by $V$) with

$$(1-\varepsilon)R_{uv}\le\|Z(\chi_u-\chi_v)\|^2\le(1+\varepsilon)R_{uv}\quad\text{for all }u,v,$$

where $\|\cdot\|$ is the Euclidean norm. In the paper, $Z=QW^{1/2}BL^+$ for a random $\pm1/\sqrt k$ matrix $Q$ with $k=O(\log n/\varepsilon^2)$, and the Johnson–Lindenstrauss lemma makes it a sketch with high probability. Write $z_i$ and $\tilde z_i$ for the $i$-th rows of $Z$ and of an approximation $\widetilde Z$, as vectors in $\mathbb R^V$.

Formalization targets

Goal: Lemma 9 (p. 11)

Let $0<\varepsilon<1$. If $Z$ is a resistance sketch, if every row satisfies

$$\|z_i-\tilde z_i\|_L\le\delta\|z_i\|_L,\tag{4}$$

and if

$$\delta\le\frac{\varepsilon}{3}\sqrt{\frac{2(1-\varepsilon)w_{\min}}{(1+\varepsilon)n^3w_{\max}}},\tag{5}$$

then for every pair $u,v$

$$(1-\varepsilon)^2R_{uv}\le\|\widetilde Z(\chi_u-\chi_v)\|^2\le(1+\varepsilon)^2R_{uv}.$$

The lemma is stated for arbitrary $k$, $Z$ and $\widetilde Z$: nothing about the random projection or the solver enters beyond (4) and the sketch property.

Milestones

• Trace identity (§3, p. 8): $\sum_{e}w_eR_e=n-1$ for a connected graph.
• Proposition 10 (p. 12): $R_{uv}\ge 2/(nw_{\max})$ for distinct vertices $u\neq v$ of a connected simple graph.

Significance

Lemma 9 is the correctness half of the paper's Theorem 2: together with a Johnson–Lindenstrauss lemma and the Spielman–Teng solver it yields a data structure, built in $\widetilde O(m\log r/\varepsilon^2)$ time, that returns any effective resistance to within a factor $(1\pm\varepsilon)^2$ in $O(\log n/\varepsilon^2)$ time. This in turn makes the effective-resistance sampling of the paper's Theorem 1 run in nearly linear time, and the same sketch-and-solve pattern has been reused in later work on Laplacian solvers, graph sparsification and electrical-flow algorithms.

The result is proved in the paper. Formalizing it produces machine-checked statements of three facts that recur throughout spectral graph theory: the trace identity $\sum_e w_eR_e=n-1$ (Foster's theorem in its weighted form), the lower bound on effective resistances by comparison with the complete graph, and the stability of a resistance sketch under relative $L$-norm errors. Neither Mathlib nor this platform states any of them for the linear-algebraic definition of effective resistance used here.

Difficulty

The hypothesis (4) controls the error row by row, in the $L$-norm on $\mathbb R^V$, while the conclusion concerns the columns of $\widetilde Z$ applied to $\chi_u-\chi_v$, in the Euclidean norm on $\mathbb R^k$, and it is a relative bound for every pair at once. A relative bound cannot hold unless $R_{uv}$ is bounded below uniformly over all pairs of distinct vertices, which is where the factors $n^3$, $w_{\min}$ and $w_{\max}$ of (5) come from. Such a lower bound is false for multigraphs, whose parallel edges can make $R_{uv}$ arbitrarily small, and the relation between the $L$-norm of a row and the Euclidean norms of the columns involves every edge of the graph, not only a path between $u$ and $v$.

Proposition 10 is classically derived from Rayleigh's monotonicity law. Its standard formal statement on this platform concerns the probabilistic definition of effective resistance through hitting probabilities of a random walk, which is a different definition from $(\chi_u-\chi_v)^{\mathsf T}L^+(\chi_u-\chi_v)$; no theorem relating the two is available.

Formalization scope

The graph is a structure WGraph V E over finite types $V$ (vertices, $n=$ Fintype.card V) and $E$ (edges), with head, tail : E → V, head e ≠ tail e, weights w : E → ℝ with 0 < w e. Connectivity is that of the underlying simple graph (Mathlib's SimpleGraph.Connected, which includes $V\neq\emptyset$); simplicity means that no two edges join the same unordered pair. Matrices are Mathlib matrices indexed by $E$ and $V$. $L^+$ is the published Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv of $x\mapsto Lx$ on the Euclidean space $\mathbb R^V$, converted back to a matrix; for symmetric $L$ this is the spectral pseudoinverse of §2.2. $\|Z x\|^2$ is the sum of squares of the coordinates, not Lean's sup norm. $n^3$ is the real number $n^3$.

Choices committed to, relative to the page:

• $w_{\min}$, $w_{\max}$ are any reals with $0<w_{\min}\le w_e\le w_{\max}$ for all edges; the exact extremes are an instance, and looser bounds only make (5) and Proposition 10 weaker.
• $\varepsilon$ is assumed to satisfy $0<\varepsilon<1$; the paper gives no range, and for $\varepsilon\ge1$ the square root in (5) has a non-positive argument.
• The graph is assumed simple in Lemma 9 and Proposition 10. Proposition 10 is false for multigraphs (two parallel unit edges give $R=1/2<1=2/(nw_{\max})$), and the proof of Lemma 9 uses it.
• Proposition 10 is stated for $u\neq v$. As printed it claims all $u,v$, which fails at $u=v$ since $R_{uu}=0$.
• The trace identity requires connectivity only.

A trivializing formalization is ruled out: the goal does not assume the intermediate inequality $|\|Zx\|-\|\widetilde Zx\||\le(\varepsilon/3)\|Zx\|$ of the proof, nor a stronger condition on $\delta$ than (5); its hypotheses are satisfiable (for example $\widetilde Z=Z$ with $Z=W^{1/2}BL^+$ and $\delta=0$), and its conclusion is not vacuous for $n\ge2$.

Infrastructure that a complete development needs, and that is reusable beyond this mission: the identity $L^+LL^+=L^+$ and $LL^+$ as the projection onto $\mathbf 1^\perp$ for a connected Laplacian; the trace identity; Loewner-order monotonicity of $R_{uv}$ in the edge weights; and the effective resistances of the complete graph. Contributions of any of these as separate lemmas are welcome. The random projection (Johnson–Lindenstrauss) and the solver's running time are outside this mission.

Selected references

• D. A. Spielman, N. Srivastava, Graph Sparsification by Effective Resistances, arXiv:0803.0929v4, 2009; SIAM J. Comput. 40(6), 2011. https://arxiv.org/abs/0803.0929, https://doi.org/10.1137/080734029
• D. A. Spielman, S.-H. Teng, Nearly-linear time algorithms for preconditioning and solving symmetric, diagonally dominant linear systems, arXiv:cs/0607105. https://arxiv.org/abs/cs/0607105
• D. Achlioptas, Database-friendly random projections: Johnson–Lindenstrauss with binary coins, J. Comput. Syst. Sci. 66(4), 2003. https://doi.org/10.1016/S0022-0000(03)00025-4
• P. G. Doyle, J. L. Snell, Random Walks and Electric Networks, MAA, 1984. https://arxiv.org/abs/math/0001057