All missions

Chapter One of Jim Hefferon's Linear Algebra develops Gauss's method and asks what row reduction actually preserves. The answer arrives as the Linear Combination Lemma: row operations change the rows of a matrix but never the subspace those rows span, and that invariant is complete. The goal theorem is that completeness — two matrices are row equivalent exactly when they have the same row space — which is what makes reduced echelon form a genuine canonical form. The milestones are the two results the chapter builds on the way: that row operations leave a system's solution set alone, and that a solution set is always one particular solution translated by the solutions of the associated homogeneous system.

Where should one look for the optimum of a linear programming problem? Chapter 1 of Bertsimas–Tsitsiklis suggests that optima "tend to occur at corners" of the feasible polyhedron; §§2.5–2.6 turn this intuition into theorems. Not every polyhedron has a corner — a halfspace in $\mathbb{R}^n$ ($n > 1$) has none — and the exact dividing line is the presence of an infinite line: a nonempty polyhedron

has an extreme point if and only if it does not contain a line, if and only if $n$ of the vectors $a_1, \dots, a_m$ are linearly independent (Theorem 2.6). In particular every nonempty bounded polyhedron and every nonempty standard-form polyhedron has a basic feasible solution (Corollary 2.2). The capstone, Theorem 2.8, is the sharpest form of the corner principle: if $P$ has at least one extreme point, then for any cost vector $c$ either the optimal cost is $-\infty$, or there is an extreme point of $P$ that is optimal — existence of an optimal solution comes for free once the cost is bounded below. Its companion Theorem 2.7 places an optimal extreme point under the weaker assumption that an optimal solution exists, and Corollary 2.3 — the fundamental theorem of linear programming — concludes that every feasible LP either has optimal cost $-\infty$ or attains an optimal solution, in stark contrast with nonlinear problems such as minimizing $1/x$ over $x \ge 1$. These results license the extreme-point search that the simplex method (Mission IV) performs.

Beneath Exp3, Exp4 and their relatives lies one algorithm: minimize past losses plus a convex regularizer. Chapters 26–28 of Lattimore–Szepesvári develop this unifying view. For a Legendre potential $F$ with Bregman divergence $D_F$, both mirror descent and follow-the-regularised-leader satisfy the master bound $R_n(a) \le \frac{F(a) - F(a_1)}{\eta} + \frac{1}{\eta}\sum_t D_F(a_t, \tilde a_{t+1})$; the negentropy potential on the simplex recovers Exp3 exactly. The goal theorem is the payoff for adversarial linear bandits: FTRL on the unit ball with the self-concordant-flavoured potential $F(a) = -\log(1-\|a\|) - \|a\|$ achieves $R_n \le 2\sqrt{3nd\log n}$ — improving the $\sqrt{d}$ factor over the Exp3-style approach of Chapter 27 and matching the $\Omega(d\sqrt{n})$ lower bound of Mission XI up to logarithms.

Real decisions come with context: a news site chooses an article for a particular user. Competing with the single best arm is then meaningless; the right benchmark is the best mapping from contexts to arms, or more generally the best of $M$ expert policies. Chapter 18 of Lattimore–Szepesvári formalizes this via Exp4 — exponential weighting over experts, fed by the importance-weighted estimator of Mission V. The goal theorem: with learning rate $\eta = \sqrt{2\log(M)/(nk)}$, Exp4 satisfies $R_n \le \sqrt{2nk\log M}$ against the best of $M$ experts. Since $M$ enters only logarithmically, the learner can compete with exponentially large policy classes — the conceptual gateway from bandits to reinforcement learning with function approximation.

Formalize sample-path stability for a continuous-time, unit-rate, infinite-buffer single-server queue. Starting from cumulative arriving service work, define the reflected transient workload, the workload constructed from the infinite past, long-run offered load, and two-time stationarity. Prove that subcritical load forces finite-time coupling and consequently that every finite initial workload converges in its two-time finite-dimensional distributions to the stationary workload law.

Formalize sample-path Little's Law for deterministic continuous-time queueing trajectories, decomposed into area, sojourn, arrival-rate, boundary, and squeeze lemmas.

First raised for two variables by Ludwig Kraus in 1884 and stated in full generality by Ott-Heinrich Keller in 1939, the Jacobian conjecture asks something that sounds almost like freshman calculus: if a polynomial map from complex n-space to itself has a Jacobian determinant equal to a nonzero constant, must it be invertible by another polynomial map? That constant-Jacobian condition is precisely the algebraic shadow of the inverse function theorem, yet producing a polynomial — not merely analytic — inverse has resisted every attack for over eighty years. Shreeram Abhyankar championed the problem because it can be stated 'using little beyond a knowledge of calculus,' and Stephen Smale placed it sixteenth on his 1998 list of problems for the new century. Its notoriety is sharpened by a graveyard of published 'proofs' that later collapsed. Deep reductions exist — Bass, Connell, and Wright showed in 1982 that the general case reduces to maps of degree three — and the problem is equivalent, through work of Tsuchimoto, Belov-Kanel, and Kontsevich, to the Dixmier conjecture on the Weyl algebra. A formal statement anchors this famously slippery problem so that progress can be verified rather than merely believed.

This completed mission proves a deterministic classical polynomial-time $1/2$ approximation to the Quantum Max-Cut optimum. Compute total edge weight $W$ and a greedy maximum-edge matching of weight $g$, then return the exact rational estimate $v=(W+3g)/2$.

The proof establishes $v\le\mathrm{OPT}(G)\le W+2g\le2v$ and certifies the concrete classical Turing-machine computation, including parsing, exact rational arithmetic, and output encoding. Empty graphs and zero weights are included.

The mathematical ingredients are published in Anshu, Gosset, and Morenz, TQC 2020, Lemma 5 / Eq. (9) and Eq. (25). This is a derived numerical construction from those ingredients. Accepted Lean proof.

This completed mission proves existence of a classical polynomial-time numerical $0.498$ approximation to Quantum Max-Cut. Every returned rational estimate is at most the unrestricted optimum, and its expectation is at least $0.498\,\mathrm{OPT}(G)$.

The accepted proof uses the verified deterministic $1/2$ construction and monotonicity. The historical $0.498$ benchmark is Gharibian–Parekh, APPROX/RANDOM 2019, Theorem 6; the verified construction here uses published star and matching estimates from Anshu, Gosset, and Morenz, TQC 2020, Lemma 5 and Eq. (25).

Accepted Lean proof. Polynomial bit complexity, exact rational output, and empty or zero-weight graphs are included.

This completed foundation proves a deterministic classical polynomial-time numerical estimator for Quantum Max-Cut. If $W$ is total edge weight, the algorithm returns the exact rational $v=W/2$.

The verified guarantee is $0\le v\le\mathrm{OPT}(G)$ and $v\ge\mathrm{OPT}(G)/4$, for all nonnegative rational weights, including empty graphs and zero weights. Its proof includes the campaign's actual input/output encodings and polynomial-time Turing-machine certificate.

Accepted Lean proof. The Quantum Max-Cut normalization is the published $I-\mathrm{SWAP}$ convention of Anshu, Gosset, and Morenz, TQC 2020.

A verified starting point for Quantum Max-Cut

Quantum Max-Cut is an optimization problem for a system of interacting qubits. An input graph specifies which pairs interact and the nonnegative weight of each interaction. The task is to prepare a quantum state with high energy relative to the maximum permitted by quantum mechanics. This makes approximation algorithms a way to compare feasible state preparations with an optimum that can require complicated entanglement.

A campaign tracking approximation ratios needs both a stable common statement and an actual proved starting value. This mission supplies the foundation at ratio $1/4$. The value is a basic mathematical baseline, not a new approximation record. Stronger mathematical results are known: Gharibian and Parekh obtained 0.498, and Parekh and Thompson obtained a product-state guarantee of $1/2$. More recent work gives an efficient 0.614 guarantee. These are literature targets for further formalization. Their numerical values are separate from the campaign's machine-checked record.

Inputs, states, and energy

The input has vertices $\{0,\ldots,n-1\}$ and a nonnegative rational weight $w_{ij}$ on every unordered pair $i<j$. A zero weight represents an absent edge. The Hamiltonian convention is

The operator $\mathrm{SWAP}_{ij}$ exchanges two qubits, and $X,Y,Z$ are the Pauli matrices. In this normalization, a singlet on a unit-weight edge has energy $2$, and an antiparallel computational-basis pair has energy $1$. The Hamiltonian convention of Anshu, Gosset, and Morenz, Eq. (5) agrees with this convention.

A state is represented by complex amplitudes on bitstrings, normalized by the sum of their squared absolute values. Its energy is a finite sum of squared differences under swaps of bit coordinates. Preparation circuits can contain ancillary qubits. The graph occupies the first $n$ output wires; every other wire is retained, and the Hamiltonian acts only on graph wires. This describes expected energy on the graph even when the graph qubits are entangled with ancillas.

Formalization target

The goal is the existential algorithmic statement

Here $\mathrm{OPT}(G)$ is the maximum energy over all normalized quantum states on the graph. The formal statement avoids introducing a separate optimum: it requires the output energy to be at least one quarter of the energy of every normalized complex comparison state.

One algorithm and a single polynomial runtime bound must work for every input graph. The generated circuit may depend on that graph but cannot depend on the comparison state used to test the guarantee. Empty vertex sets and zero-weight graphs are included. The claim is about expected output energy, with all ancillary wires retained; it does not select a favorable measurement outcome.

What the foundation establishes

A local Lean 4.33.1 development now proves this complete existential statement, including an explicit uniform classical circuit generator and its polynomial-time Turing-machine certificate. The proof's axiom check lists only Lean's standard axioms. Acceptance by the platform's proof verifier remains a separate publication step. The local proof must not be reported as an accepted platform result before that step succeeds.

This foundation establishes a usable point from which stronger ratios can be pursued without changing the meanings of input size, allowed preparation, or approximation. The $1/2$ mission is the next open challenge under the same definitions. Its mathematical feasibility does not supply an accepted Lean proof of its energy and runtime obligations. Later campaign entries can target further improvements while importing the common model unchanged.

Why the full statement requires care

A performance estimate for a quantum state does not establish a polynomial-time approximation algorithm. The complete claim also requires a uniform finite computation that generates the state-preparation circuit. A concise circuit description is insufficient when its parameters or gate list could require an unbounded search.

The input and output representations therefore contribute to the mathematical content. They must charge for vertex count, register width, individual gates, and rational input bit lengths. The physical comparison is also unrestricted: the reference state may be entangled across the entire graph. A proof against only a chosen output family would assert a different approximation guarantee.

Formalization scope

The foundation uses Lean 4.33.1 with the selected Mathlib revision. Inputs have nonnegative rational weights. Rational numerators and denominators use fixed self-delimiting binary encodings. The graph order, output-register width, and gate wire indices use unary encodings. Every gate is explicitly listed. Unary wire indices introduce only polynomial overhead because register width is already charged in unary.

An algorithm is a uniform classical polynomial-time generator of finite H/T/CNOT circuits, followed by execution of the generated circuit. Every wire starts in the all-zero state. CNOT requires distinct control and target wires. Mathlib's explicit Turing-machine predicate supplies the runtime meaning; efficiency is not a freely assumed label.

The ratio $1/4$ is exact in this fixed gate model. The local proof uses exact allowed gates and does not require a gate-synthesis error allowance. In general, an ideal arbitrary-real-rotation algorithm needs its own connection to this preparation model. The shared definition bundle contains no approximation axiom or unproved supporting theorem. The separate proof establishes the state-energy, finite computation, and runtime obligations for this starting value.

Selected references

• Direct Lean development, theorem $\mathrm{QuantumMaxCut.exists\_quarter\_approximation}$, checked with Lean 4.33.1 and the campaign's selected Mathlib environment.
• Sevag Gharibian and Ojas Parekh, Almost Optimal Classical Approximation Algorithms for a Quantum Generalization of Max-Cut, APPROX/RANDOM 2019. Paper.
• Anurag Anshu, David Gosset, and Karen Morenz, Beyond product state approximations for a quantum analogue of Max Cut, TQC 2020. Paper.
• Ojas Parekh and Kevin Thompson, An Optimal Product-State Approximation for 2-Local Quantum Hamiltonians with Positive Terms, 2022, revised 2026. Paper.
• Ainesh Bakshi, Arpon Basu, Pravesh Kothari, and Anqi Li, Sharp Bounds on the Eigenvalues of Kikuchi Graphs and Applications to Quantum Max Cut, 2026, Theorem 1.3. Paper.

Motivation

A seller offering several substitutable products must decide whether to charge one common price or a different price for each product. Customers may compare every product's net utility, or they may buy the cheapest product that they can afford. The second behavior is min-buying: a customer checks whether each product's valuation covers its price and selects the cheapest acceptable product. The distinction changes how inexpensive products divert purchases from expensive ones. Cui, Hamilton, Lamperski, and Ganjizadeh Tari study the resulting value of uniform pricing in symmetric and asymmetric valuation environments. The source for this mission is the September 27, 2026 manuscript, including its electronic companion.

Setting

There are $n\ge1$ products. A customer has a nonnegative random valuation vector $V=(V_1,\ldots,V_n)$. A feasible price vector $p=(p_1,\ldots,p_n)$ has nonnegative coordinates. The customer's payment is the smallest $p_i$ among products satisfying $V_i\ge p_i$, or zero if there is no acceptable product. Equal prices create no payment ambiguity. This defines expected differentiated-pricing revenue $R_{\mathrm{DP}}(p)$ and uniform-pricing revenue $R_{\mathrm{UP}}(q)=R_{\mathrm{DP}}(q,\ldots,q)$.

The optimal revenues are $R_{\mathrm{DP}}$ and $R_{\mathrm{UP}}$. The source explicitly assumes that these optima are finite, attained, and that $R_{\mathrm{UP}}>0$. The formal model records those conditions. It does not impose finite expected valuations: fixed finite prices have bounded payments even for valuation laws with infinite first moments. General joint probability measures describe dependent valuations; product measures describe independent valuations.

A law is exchangeable when permuting its product coordinates leaves it unchanged. It is affiliated when it has a joint density or probability mass function $f$ satisfying $f(v)f(w)\le f(v\vee w)f(v\wedge w)$ for every pair of valuation vectors. A nonnegative marginal law is regular when its revenue-quantile curve is concave. Regularity uses interior quantiles, with endpoint conventions stated explicitly; it is not replaced by the stronger monotone-hazard-rate condition.

Formalization targets

Goal: Theorem 4, the exact tight regular-distribution guarantee

For independent, absolutely continuous regular valuation distributions, the target is

The constant is defined exactly. Let $A(0)=0$ and $A(x)=-\log(1-x^2)/x$ for $0<x<1$, and let $c$ solve

Then $x^\star$ is the unique point in $(0,1)$ with $x^\star c(x^\star)=1$. The main target includes this nondegenerate root characterization, the universal guarantee, and sharpness: for every $\varepsilon>0$ there is a finite independent continuous regular instance with $R_{\mathrm{DP}}/R_{\mathrm{UP}}>1/x^\star-\varepsilon$. The number of products can vary with $\varepsilon$. The manuscript's decimal $x^\star\approx0.6986$ is explanatory; no decimal is substituted for the exact constant. These are the two conclusions of Theorem 4, p.17.

Symmetric-market results

Theorems 1 and 2, pp.10 and 13, assert $R_{\mathrm{DP}}=R_{\mathrm{UP}}$ for IID valuations and for exchangeable affiliated valuations, respectively. Supporting targets state the stronger policy comparison proved in the manuscript: every price vector is dominated by a uniform price selected from that vector. Theorem 3, p.15, gives an exchangeable nonnegative valuation law for every positive $n$ such that

This last construction is discrete and does not carry a density assumption.

Supporting targets

The milestone list includes the independent-revenue identities, the affiliated conditional-threshold comparison, Lemmas 1–4 on triangular and canonical distributions, Lemmas EC.1–EC.2 on rejection probabilities and continuous approximation, and the analytic properties used to specify the exact constant. Additional interface targets identify the concrete triangular probability laws and connect the canonical continuation formulas to actual min-buying revenues. All main results and numbered supporting lemmas of the source are represented in this one mission.

Significance

The symmetric results specify settings where charging different prices gives no revenue advantage. The asymmetric result gives an exact worst-case guarantee and establishes that a better universal fraction cannot hold throughout the stated regular class. The exchangeable lower bound distinguishes symmetry alone from symmetry combined with affiliation. These interpretations follow from the paper's statements and comparisons in Sections 3–4.

The formalization makes the customer payment rule, probability classes, optimization assumptions, and sharpness quantifiers explicit. It also separates an ODE-defined constant from its numerical approximation. The current deliverable consists of locally compiled definitions and open theorem statements, with independent blind read-backs. Statement compilation is not a proof of a theorem; completed Lean proofs are the mission's remaining work.

Mathematical difficulties

Atomic cap distributions require inclusive purchasing and strict rejection probabilities. Substituting a right-continuous CDF for strict rejection at a cap would change the revenue. Affiliation must be used in its density-or-mass-function meaning; the conditional-tail comparison is a theorem to establish. Discrete order statistics can contain ties and need the corresponding multiplicity treatment. The tightness claim must ultimately hold for continuous regular distributions, although several intermediate extremal distributions have atoms. The continuous approximation lemma is therefore part of the target list.

The exact constant requires existence, uniqueness, and maximum properties of its concrete integral benchmark. Those properties are separate conclusions, not hypotheses of the market model. The canonical continuation value is revenue from the designated cap prices; it is not defined to equal the optimal differentiated revenue.

Formalization scope

Valuation and price vectors are real functions on a finite index type. Joint laws are probability measures; no finite support or moment restriction is inserted into the general pricing theorems. The original continuous-market conventions and positive attained optimum conditions are explicit where used. Atomic triangular laws and the exchangeable lower-bound witness have their appropriate separate scopes. Prices are optimized over all nonnegative real vectors, with no fixed ordering imposed on the feasible set; sorted order is required only in formulas that use it.

Regularity is concavity of $qF^{-1}(1-q)$ for $0<q<1$, avoiding undefined endpoint quantiles. For a nonnegative curve this is equivalent to concavity of its zero-endpoint extension. Affiliation covers both a Lebesgue density and a probability mass function on real-valued vectors. The ODE benchmark is an explicit integrating-factor integral; the main goal proves that its root is unique and lies strictly between zero and one. No desired revenue comparison or extremal bound is assumed inside a definition.

Reusable components include the min-buying payment model, strict-rejection identities, quantile regularity, exchangeability and affiliation, triangular laws, and finite-to-continuous comparison. Proofs of these components and of the paper's complete targets are welcome. All code targets Lean 4.33.1 and the pinned Mathlib environment.

Selected references

• Titing Cui, Michael L. Hamilton, Jourdain Lamperski, and Kasra Ganjizadeh Tari, Unit-Demand Pricing for Min-Buying Customers, September 27, 2026 manuscript. SSRN / DOI.

Motivation

A seller can often predict a customer's willingness to pay from observed features, yet may be limited to a small number of prices. The decisions are then coupled: the seller must choose both the customer groups and the price assigned to each group. Grouping customers first and optimizing prices afterward does not generally solve the joint problem. Cui and Hamilton study this joint optimization in Optimal Feature-Based Market Segmentation and Pricing, using the structure of a regression model with a common prediction error.

The central question is when that statistical structure makes optimal segmentation tractable. The main positive result is Theorem 2. The companion results describe hardness without the additional shape condition, approximation by greedy price-menu selection, and the value of allowing more segments. The source for the page-specific formalization is the October 22, 2025, 60-page manuscript available under SSRN 4151103.

Setting

Let $M=\mu(X)\ge0$ denote a predicted valuation and let $E$ denote a mean-zero error independent of the observed features. Realized valuation is $V=M+E$. The general model uses separate probability laws $\nu$ for $M$ and $\eta$ for $E$, with finite first moments. Independence is represented by the shared location family: every customer with predicted value $x$ has valuation law $x+E$.

The inclusive survival function is $S(t)=\Pr(E\ge t)$. At nonnegative price $p$, expected customer revenue is $r(x,p)=pS(p-x)$. Inclusive survival is essential when the error distribution has atoms. A finite price menu $P$ earns

For a fixed menu, assigning every customer to a revenue-maximizing menu price optimizes its segmentation. Write $R_k=\sup_{|P|\le k}F(P)$, $R_\infty=\int\sup_{p\ge0}r(x,p)\,d\nu(x)$, and $R_k^0$ for the same finite-menu problem with zero error. The MHR condition is encoded for density-bearing error laws by log-concavity of survival on its positive domain, the formulation used in the proof of Lemma 2(b). This permits bounded support and zero purchase probabilities.

Formalization targets

Goal: Theorem 2, optimal computation

For $n$ distinct, sorted predicted values with positive probability masses, independent mean-zero MHR error, and a primitive oracle that returns an optimal block price and its attained revenue, construct a globally optimal policy with at most $k$ contiguous index blocks. Its revenue must equal the specified Bellman recurrence, and the reconstructed policy must dominate every assignment of types to $k$ arbitrary nonnegative prices. If each nonempty block-oracle call costs at most $m$, the specified memoized schedule has

The draft states an explicit upper bound $5n^2(k+m)$ for oracle charges, Bellman candidate evaluations, and backtracking. This is an oracle-operation model for already sorted data; it is not a bit-complexity assertion about evaluating arbitrary real probabilities.

Companion results

Theorem 1 asserts NP-hardness even with finitely supported independent mean-zero noise of polynomial support size. Its target uses an explicit binary encoding of rational input data and polynomial-time finite Turing-machine reductions; $k$ is part of the input. Remark 2 targets normalized, monotone, submodular menu revenue and the greedy guarantee

A separate finite-support target shows that nonnegative realized valuations, together with zero, suffice as candidate prices. Theorem 4 states

for any finite almost-sure prediction bounds $L\le M\le U$. Theorem 5 states diminishing increments,

under MHR error. These two targets retain general prediction distributions. Theorem 3 includes almost-sure nonnegative realized valuations. Corollary 2 uses this same setting and includes the factor two confirmed by the author during review.

Significance

Theorem 2 replaces a search over arbitrary segmentations with an optimal interval policy and a quadratic-size block table. The performance results explain how a small menu approaches feature-based personalized pricing and when the incremental value of another segment diminishes. The hardness and approximation targets delineate what remains possible when the MHR restriction is removed.

The draft makes ties, atoms, support endpoints, optimizer attainment, and computational costs explicit. Generic proofs of monotone finite-menu assignment under a TP2 revenue condition and Bellman optimality have been checked locally in the pinned Lean environment. The full paper theorems remain open formal proof obligations; well-formed statements are not completed proofs.

Mathematical difficulties and author-confirmed corrections

The interval argument needs an attaining assignment that is monotone despite ties and all-zero revenue rows. Division by survival probabilities would exclude legitimate bounded-support cases. The complexity claim also needs the block oracle's attained revenue, not merely its price. The hardness target requires an actual polynomial-time reduction and careful centering of the constructed error while preserving nonnegative predicted means.

The author confirmed two corrections on October 30, 2026. Theorem 3 now explicitly assumes $V=M+E\ge0$ almost surely. Corollary 2 now includes the factor two:

Corollary 2 retains the same nonnegative realized-valuation setting used in the corrected Theorem 3. Both results are definitive milestone targets in this draft. Two earlier draft records are retained as clearly labeled superseded copies, with their mathematical statements corrected as well; they are not milestones. The nonnegative-valuation assumption supports the proof's bound $R_\epsilon(x)\le x$. For Corollary 2, minimizing $2j\sigma/k+(\mathbb E[M]+\sigma)/j$ gives the corrected factor two. Formal proofs must still handle conditional truncation, boundary atoms, and zero variance.

Formalization scope

General revenue targets use probability measures on the real line, nonnegative integrable predictions, and integrable mean-zero error. The finite computational model uses strictly increasing predicted values and positive weights summing to one. At most $k$ price slots are allowed; repeated cuts represent unused slots. Index intervals include every type, including the largest support point. Least optimal prices implement a deterministic tie convention; no interior first-order condition or uniqueness assumption is imposed.

The definition layer contains no proof placeholders or new axioms. Real suprema and infima are defined from the feasible economic objects; their attainment and boundedness must be proved where needed. The MHR-to-TP2 bridge is a theorem target, not an assumption that deletes the analytic content. The Bellman recurrence, its partition relation, and its charged evaluation schedule are separate objects. The goal connects that recurrence to the original unrestricted assignment problem and an actual feasible reconstruction.

The general model, the rational binary-input hardness model, and the discrete candidate-price model are explicit interfaces. Their connecting lemmas, optimizer existence, the analytic MHR argument, interval-to-DP reconstruction, and the source's companion results remain available proof obligations. The optional derivative refinement of Lemma 1 and appendix extension/necessity theorems are outside this first proposal. Every uploaded item includes an independent read-back for comparison with its intended mathematical content.

Selected references

• Titing Cui and Michael L. Hamilton, Optimal Feature-Based Market Segmentation and Pricing, Operations Research 74(3), 1354–1370 (2026). DOI. Page citations refer to the October 22, 2025 manuscript, SSRN 4151103.
• Adrien Saumard and Jon A. Wellner, Log-concavity and strong log-concavity: a review, Statistics Surveys 8, 45–114 (2014), Section 11, cited in the source's proof of Lemma 2(b). DOI.

The claim

MuSig2 (BIP327) lets $n$ signers produce one BIP340 Schnorr signature for an aggregate key, indistinguishable on chain from a single-signer Taproot spend; FROST does the same for a threshold of signers. The correctness claim is that partial signatures which each pass their partial check combine into a signature that the ordinary Schnorr verifier accepts. Earlier this was judged infeasible here: the signature mission's secp256k1 is an executable transcription without a proof of the group law. This mission supplies that proof, by connecting the executable curve to Mathlib's elliptic-curve group, and then proves MuSig2 correctness end to end against the executable schnorrVerify, and FROST correctness in the group.

What is proved

• The bridge (toPoint_padd, valid_padd, tp_padd, valid_pmul, tp_pmul, toPoint_pneg, eq_of_tp_eq, padd_comm, padd_assoc, pmul_add, pmul_padd, pmul_pmul, tp_G): the executable point addition, negation and scalar ladder are Mathlib's group operations on $y^2 = x^3 + 7$ over $\mathbb{F}_p$; hence they are associative, commutative and linear.
• The group (n_prime, n_nsmul_Gpt, nsmul_Gpt_mem, addOrderOf_Gpt): $p$ and $n$ are prime (Lucas–Pratt certificates checked by the kernel) and the generator has order exactly $n$.
• Encodings (cpoint_spec, cpoint_cbytes): compressed points parse to reduced curve points and round-trip.
• MuSig2 (musig2_partialSigAgg, musig2_sign_partialSigVerify, musig2_correct, musig2_partialSigAgg_secp256k1, partialSigAgg_schnorrVerify, the goal): the aggregation algebra in any module and on secp256k1, and the end-to-end statement that BIP327's PartialSigAgg of partial signatures that pass PartialSigVerifyInternal is a signature schnorrVerify accepts for the aggregate x-only key, with key aggregation coefficients, plain and x-only tweaks, and the parity negations of the BIP.
• FROST (lagrange_interpolate_zero, frost_partialSigAgg, frost_sign_partialVerify, frost_correct, frost_correct_secp256k1): Lagrange interpolation at 0 and the aggregation of shares into a Schnorr signature for the group key, in any ZMod n-module and on secp256k1.

What this rests on and what it does not say

Correctness only, not security: nothing is claimed about unforgeability or the hardness of discrete logarithms. The end-to-end theorem assumes each signer key has order dividing $n$ (true of every secp256k1 point because the group has prime order, but proving $\#E(\mathbb{F}_p) = n$ needs point counting; for keys of the form $dG$ it is discharged by nsmul_Gpt_mem), and that the aggregate nonce is not the point at infinity, where BIP327 substitutes $G$ and honest partial signatures no longer combine. FROST is proved in the group only: there is no executable FROST transcription. (BIP327, RFC 9591)

The claim

Miniscript is the structured subset of Bitcoin Script that wallets use to write and analyse spending policies: each fragment has a fixed translation to Script, a type that says what it does to the stack, and a satisfaction table that says which witnesses make it succeed. The claim that makes it trustworthy is compiler correctness: a well-typed Miniscript compiles to a script that the consensus interpreter accepts on exactly the witnesses the satisfaction table describes. This mission proves the soundness half of that claim against the script interpreter transcribed from Bitcoin Core.

What is proved

• Sequential execution (runSeq_append, run_eq_runSeq, evalScript_eq_runSeq, compile_skip): the interpreter's loop composes, and a well-typed fragment inside a non-executing branch is inert.
• The type system (sem_consumes, goodVal_of_sem, goodVal_of_semW, sem_V_nil, sem_K_shape, typeOf_sound): the semantics respects the types and the z/o modifiers, B and W fragments leave valid script numbers, and the decidable checker is sound.
• Compiler soundness (sem_sound, semW_sound, sat_sound, dsat_sound, satV_sound, sat_spends, the goal): for every well-typed fragment over 23 constructors (all hash and time-lock leaves, pk_k, pk_h, multi, the and/or combinators, the seven wrappers), a satisfying witness makes the compiled script leave a true value above the untouched stack, a dissatisfaction leaves the empty element, a V satisfaction leaves nothing; and a satisfaction of a top-level B spends.
• Resources (compile_length, opsIn_compile_le): script size and counted opcodes are bounded by syntactic measures, which carry the theorems' operation and stack hypotheses.

What this rests on and what it does not say

Soundness only: the converse ("nothing else succeeds") and the malleability analysis (the s, f, e properties, non-malleable satisfactions) are not proved. thresh is not in the fragment set, and v: appends an explicit OP_VERIFY instead of folding into a preceding *VERIFY opcode, which changes script bytes but not behaviour. The signature checks are the abstract oracle's. (Miniscript, miniscript.h)

The claim

The backbone mission proved chain growth, common prefix and chain quality for every typical execution: one in which, on every window of at least $\lambda$ rounds, the adversary finds fewer blocks than there are uniquely successful honest rounds. Garay, Kiayias and Leonardos show that under honest majority executions are typical except with probability exponentially small in $\lambda$. This mission proves that half: the random mining process, its expectations, Hoeffding concentration per window, the union bound, and the end-to-end statement that every consequence of typicality holds with probability at least $1 - (L+1)^2 e^{-\text{rate}(\lambda+1)}$, against any adversary strategy.

What is proved

• The process (iIndepFun_rounds, map_eval_P): independent rounds, each a product of independent Bernoulli($p$) queries, $n$ honest and $t$ adversarial.
• Expectations and honest majority (integral_round*, expect_X, expect_Y, expect_Z, expect_Y_sub_expect_Z, margin_ge_of_honest_majority, expect_Z_add_le_expect_Y, expect_Z_lt_expect_Y): $E[Y] = np(1-p)^{n-1}$, $E[Z] = tp$, $E[X] = 1-(1-p)^n$, and with $t \le (1-\delta)n$ and $np \le \delta/2$ the margin $E[Y] - E[Z]$ is at least $\delta p n/2$.
• Concentration (sets_hoeffding, window_bound, window_bound_rate): a window of $k$ rounds fails the typicality inequality with probability at most $e^{-\text{rate}(k+1)}$.
• Typicality (typicalOn_failure_le_of_window, typicalOn_failure_le, typicalOn_prob_ge, typical_toExecution_iff, typicalTrunc_failure_le): on a horizon of $L$ rounds, typicality fails with probability at most $(L+1)^2 e^{-\text{rate}(\lambda+1)}$, independently of the network and of the adversary's chain choices.
• End to end (backbone_failure_le, backbone_prob_ge, the goal): any property implied by legality and typicality, in particular the backbone mission's common prefix, chain growth and chain quality, holds for every adversary strategy with that probability.

What this rests on and what it does not say

The bound is Hoeffding's, with each round's difference ranging over $t+1$ values, not the paper's multiplicative Chernoff bounds (absent from Mathlib), so the rate is weak when $t$ is large and $p$ small; the window conditions $4tp \le (\lambda-3)\,\text{margin}$, $\lambda \ge 2$ are sufficient conditions chosen for clean statements. The execution is frozen after the horizon (party 0 mines alone, the adversary finds nothing) so that the deterministic theorems apply to infinite executions. The paper's separate bounds on $X$ are not proved; the deterministic layer does not need them. The common-prefix instance is a one-line composition left out of the public theorems because a split file cannot import another mission's solution. (ePrint 2014/765)

The claim

At the pinned revision, Bitcoin Core's cluster mempool replaced BIP125 rule 3 ("the replacement's feerate must exceed every conflict's") with a single check: the replacement must strictly improve the feerate diagram of the affected clusters. The replace-by-fee mission had to take rule 3 from v29.0 for that reason. This mission transcribes the actual check (FeeFrac, CompareChunks, ImprovesFeerateDiagram), proves that Core's sweep computes the mathematical comparison of the two diagrams, and connects it to the existing no-free-relay theorems.

What is proved

• The arithmetic (byRatio_eq_compare_ratio, byRatio_lt_iff, div_round_down_eq_floor, div_round_up_eq_ceil, mulFallback_value, divFallback_eq_div, evaluateFeeDown_eq_floor, evaluateFeeUp_eq_ceil, getFee_eq_evaluateFeeUp): Core's cross-multiplied comparison is the comparison of exact ratios; its divisions round as named on both code paths; the replacement mission's GetFee is EvaluateFeeUp.
• The diagram (diagram_at_zero, diagram_total, diagram_concave): starts at the origin, ends at the total fee, and is concave for chunkings with non-increasing feerates.
• The check (compare_chunks_sound, improvesFeerateDiagram_iff): CompareChunks returns greater, less, equivalent or unordered exactly according to the pointwise comparison of the two piecewise-linear functions; ImprovesFeerateDiagram is "strictly better".
• What it guarantees (improves_total_fee, improves_total_fee_not_strict, no_free_relay_diagram, the goal): a strict improvement never lowers the total fee but need not raise it, and together with PaysForRBF the replacement adds at least the incremental relay fee: no free relay holds under the pinned revision's actual rules.

Vectors

All eleven CompareChunks cases of Core's rbf_tests.cpp, the FeeFrac arithmetic cases of feefrac_tests.cpp (including the fast-path thresholds and issue #32294), and hand-computed diagrams agree (tests/FeerateDiagramVectors.lean).

What this rests on and what it does not say

The chunk lists are input: the linearization of the affected clusters (txmempool.cpp, txgraph.cpp) is not modelled, nor which transactions belong to the clusters; no_free_relay_diagram relates the diagrams to a Replacement by a hypothesis on total fees. Fees and sizes are unbounded integers. (feefrac.cpp, rbf.cpp)

The claim

Eyal and Sirer's relative revenue is computed from the stationary distribution of their Markov chain, and the threshold result is read as "a pool above the threshold earns more than its share over time". The selfish-mining missions proved the formula for the stationary distribution, its uniqueness, and the threshold as statements about that distribution. This mission proves the time statement: started from no lead (or from any distribution), the chain's time-averaged occupation converges to the stationary distribution, the pool's realized revenue share converges to the paper's formula, and above the threshold it eventually exceeds the pool's hashrate.

What is proved

• The chain over time (the five dist_* step equations, dist_mass, dist_summable_lead, dist_nonneg, isDist_dist, isDist_distN, dist_stationary, distN_stationary, isDist_delta, le_one_of_isDist, distN_mix): one step of the chain as an operator on distributions, preserving distributions, with the stationary distribution as a fixed point.
• Tightness (distN_zero_lead_le, distN_delta_lead_le): from any start, the probability of a long private lead is bounded geometrically, uniformly in time.
• Cesàro convergence (cesaro_delta_tendsto, cesaro_zero_tendsto, cesaro_tendsto): the average occupation of every state over the first $n$ steps converges to the stationary distribution, from any initial distribution. The proof uses the uniqueness mission: limit points are invariant with mass 1.
• Revenue over time (avgPoolGain_eq, avgOthersGain_eq, avgPoolGain_tendsto, avgOthersGain_tendsto, avgRelativeRevenue_tendsto, the goal; avgRelativeRevenue_eventually_gt): the time-averaged revenues converge to the paper's rates and the realized share to the relative revenue; above $(1-\gamma)/(3-2\gamma)$ the pool's realized share eventually exceeds $\alpha$.
• Renewal structure (firstReturn_zero, last_exit, renewal_equation): the last-exit decomposition and the renewal equation for returns to zero, with an aperiodic return-time distribution.

What this rests on and what it does not say

Convergence is in Cesàro mean, which is what a long-run revenue share needs. Pointwise convergence of the $n$-step distributions (which holds, the chain being aperiodic) is not proved; the renewal equation is the first step towards it. "Revenue" is the expected number of credited blocks; almost-sure convergence of the realized share along a single run is not stated. (arXiv:1311.0243)

The claim

The script mission's interpreter, reviewed twice and tested against Core's 994 vectors, is exact except at two documented limits: L1, the signature script code does not restart after an executed OP_CODESEPARATOR (a handful of historical transactions), and L10, OP_CHECKMULTISIG deletes only the checked signature from the script code instead of all of them (constructed test cases). Those nine vectors disagreed. This mission closes both limits with a second interpreter that tracks Core's pbegincodehash and performs Core's FindAndDeletes itself, and proves that the two interpreters agree wherever the limits do not bite, so that every published theorem about verifyScript carries over unchanged to the exact rule.

What is proved

• The script code (stepV2_codesep, stepV2_keeps, codesep_tracks): after an executed OP_CODESEPARATOR at byte position $p$ the script code is the script from $p+1$; nothing else changes it.
• The deletions (checksig_deletes_one, fadAll_base, fadAll_witness, multisigSigs_eq, multisig_deletes_all): OP_CHECKSIG checks against the code with its own signature deleted; OP_CHECKMULTISIG against the code with all its signatures deleted, before any check, in SigVersion::BASE only.
• Equivalence outside the limits (legacyOracle_eq, annotate_parse, annotate_suffix, annotate_op_suffix, stepV2_agree, eval_agree, evalBytes_agree, runOk_of_static, runOk_witness, evalOk_of_static, evalOk_witness, verify_agree, the goal): under the side condition that no executed OP_CODESEPARATOR and no multisig self-signature push occurs (statically implied by the absence of the two opcodes; in witness v0 only the separator matters), verifyScriptV2 = verifyScript.

Vectors

verifyScriptV2 agrees with Core on all 793 script tests and all 201 transaction tests of the pinned revision; the nine cases that disagreed with the published interpreter (seven L1, two L10) now agree, and no previously agreeing case changed (tests/CoreV2*.lean, REVIEW_V2.md).

What this rests on and what it does not say

The side condition for L10 is semantic (it depends on the signatures actually on the stack), so EvalOk is stated along the run, with static sufficient conditions. Policy flags (CONST_SCRIPTCODE and the rest) remain off as in the published model; the Taproot handler is unchanged. (interpreter.cpp)

The claim

Lightning's security against a counterparty who broadcasts an old, revoked commitment transaction rests on the penalty: the honest party, who holds the revocation secret for that commitment, can take every output at once, while the cheater can take nothing before to_self_delay blocks. The script missions proved what each commitment output's script enforces; this mission puts the pieces together at the script level, output by output, in both directions.

What is proved

• Completeness (to_local_penalty_sig, to_local_penalty, the four HTLC penalty theorems, revoked_commitment_penalty, the goal): if the oracle accepts a signature for the revocation key, every penalisable output of the commitment transaction (to_local, offered and received HTLCs, legacy and anchors forms) has a witness VerifyScript accepts, with no delay and no condition on the spending transaction. to_remote_honest_only and the two anchor theorems state the facts for the outputs that have no revocation path.
• Safety (to_local_cheater_delayed, cheater_delay_in_tx_terms, cheater_delay_any_sequence, cheater_needs_delay, the four *_cheater_no_revocation theorems, htlc_cheater_one_block_anchors, received_cheater_height): if the oracle accepts no signature for the revocation key and knows no other preimage of its hash, every spend the cheater can make takes a non-revocation path: the balance only after to_self_delay (version 2, nSequence ≥ to_self_delay), the HTLCs only by preimage, success or timeout, with the one-block delay in the anchors form and the expiry bound for timeouts.
• The race (penalty_any_block): the penalty transaction is final in any block, so the honest party wins whenever it confirms within the delay.

What this rests on and what it does not say

The hypotheses are unforgeability stated on the oracle for one key (NoRevocationSig) and second-preimage resistance of hash160 for the revocation hash (NoRevHashPreimage); there is no model of key derivation (BOLT #3's per-commitment secrets), no signing oracle, no ECDSA security proof, and no network or fee model. The BIP68 consequence of nSequence ≥ to_self_delay (the cheater's transaction cannot enter a block within the delay) is stated in transaction terms, not composed with the block mission's sequence-lock check. The legacy (P2WPKH) to_remote has no published theorem and is not covered. (BOLT #5)

This mission formalizes K. Juschenko and N. Monod, Cantor systems, piecewise translations and simple amenable groups, Ann. of Math. (2) 178 (2013) 775–787, doi:10.4007/annals.2013.178.2.7. Page numbers are those of the journal.

Motivation

The topological full group $[[T]]$ of a Cantor system $(T, C)$ is the group of homeomorphisms of $C$ given piecewise by powers of $T$, on open pieces. Matui showed that for minimal $T$ its commutator subgroup is simple, and finitely generated exactly when $(T, C)$ is a minimal subshift. Grigorchuk and Medynets conjectured that $[[T]]$ is amenable. Juschenko and Monod proved the conjecture (Theorem A). Together with Matui's results this gave the first examples of infinite, finitely generated, simple, amenable groups (Corollary B); in the paper's words, “Until now, no example of a finitely generated simple group that is amenable (and infinite) was known.”

Setting

• A Cantor space is a nonempty compact metrizable totally disconnected space without isolated points; $T$ is minimal when no closed set $S$ with $T(S) = S$ other than $\emptyset$ and $C$ exists.
• $W(\mathbf Z)$ is the group of permutations $g$ of $\mathbf Z$ with $|g|_{\rm w} = \sup_j |g(j) - j|$ finite.
• $f_n(x) = \exp\big(-n\sum_j x_je^{-|j|/n}\big)$ on the Bernoulli space $\{0,1\}^{\mathbf Z}$ with the symmetric Bernoulli measure.
• A mean on a set is a finitely additive probability measure on all its subsets; a group is amenable when it carries a left-invariant one.
• The definitions are in the bundle JuschenkoMonod, which reuses $W(\mathbf Z)$ (IntervalExchange.wobbling ℤ), the topological full group (CantorSystems.topologicalFullGroup), amenability (Garrido.IsAmenable) and local finiteness (Chou.IsLocallyFinite) from published bundles.

Target

Theorem A (p. 776): the topological full group of any minimal Cantor system is amenable.

Significance

Theorem A is the first amenability proof for a class of groups that contains finitely generated infinite simple groups. Its method, a family of almost invariant densities on the Bernoulli space, became the starting point of extensive amenability (Juschenko, Matte Bon, Monod and de la Salle), which also yields amenability of interval exchange groups of low rank. The milestones also state the cited results that Corollary B combines with Theorem A: Matui's simplicity theorem and finite generation criterion, and Matui's uncountable family of pairwise non-isomorphic examples.

Difficulty

The analytic core (§2) is elementary but delicate: Theorem 2.1 shows that the densities $f_n$ are almost invariant under each piecewise translation, through a signed series $F_n(g)$ controlled by Abel summation. §3 converts this into Theorem C, an invariant mean on finite subsets of $\mathbf Z$ concentrated on the sets containing $0$, by Fourier analysis on $\mathscr P_{\rm f}(X)$ and the Reiter criterion. §4 embeds $[[T]]$ into $W(\mathbf Z)$ and shows the relevant stabilisers are locally finite, by the ubiquitous pattern property. The amenability of $[[T]]$ is then assembled from two general facts: an action with an invariant mean and amenable stabilisers forces amenability of the group (Lemma 3.2), and for a subgroup of $W(\mathbf Z)$ it suffices that the stabilisers of the sets $E \triangle \mathbf N$ are amenable (Proposition 3.3). The external results on topological full groups (Matui, Giordano–Putnam–Skau, Elek–Monod) are substantial papers of their own; the Elek–Monod example shows that the one-dimensional structure is essential, since Theorem A fails for minimal $\mathbf Z^2$-systems.

The definitions follow the paper closely, with a few encodings worth knowing. $\{0,1\}^X$ is the type of functions X → Fin 2 with the product of uniform measures. The lamplighter $\mathscr P_{\rm f}(X) \rtimes G$ acts on finite subsets by $E \mapsto F \triangle gE$. Means are finitely additive probability measures on all subsets, as in the bundle Garrido_Amenability. The net of almost invariant vectors in Lemma 3.1 is stated with finite sets of group elements and tolerances $\varepsilon$. Where a reading was needed — the range of $n$ in §2, how the constants of Lemma 2.6 depend on $|g|_{\rm w}$, the size of Matui's family — the milestone's Formalization note says which was taken.

Formalization scope

Every numbered result is a milestone, with the unnumbered steps the proofs use: the inequality (2.ii), the remark after Theorem C, the finiteness of $\mathbf N \triangle g(\mathbf N)$, and the homomorphism $\pi_p$. The cited results stated as external milestones are Matui's simplicity theorem, finite generation criterion and uncountable family, the Giordano–Putnam–Skau classification, and the Elek–Monod $\mathbf Z^2$-system. Left out: Schreier's remark on free subgroups of $W(\mathbf Z)$ and the Grigorchuk–Medynets local embeddability theorem (motivation only), the local finiteness of forward-orbit stabilisers via Putnam's AF-algebras (context for Lemma 4.1, which the paper reproves), and Matui's theorem that the groups are never finitely presented.

Selected references

• K. Juschenko and N. Monod, Cantor systems, piecewise translations and simple amenable groups, Ann. of Math. 178 (2013) 775–787, https://doi.org/10.4007/annals.2013.178.2.7.
• H. Matui, Some remarks on topological full groups of Cantor minimal systems, Internat. J. Math. 17 (2006) 231–251, https://doi.org/10.1142/S0129167X06003448.
• T. Giordano, I. F. Putnam and C. F. Skau, Full groups of Cantor minimal systems, Israel J. Math. 111 (1999) 285–320, https://doi.org/10.1007/BF02810689.
• G. Elek and N. Monod, On the topological full group of a minimal Cantor $\mathbf Z^2$-system, Proc. Amer. Math. Soc. 141 (2013) 3549–3552, https://doi.org/10.1090/S0002-9939-2013-11654-0.
• R. I. Grigorchuk and K. Medynets, On algebraic properties of topological full groups, Sb. Math. 205 (2014) 843–861, https://doi.org/10.1070/SM2014v205n06ABEH004400.
• K. Juschenko, N. Matte Bon, N. Monod and M. de la Salle, Extensive amenability and an application to interval exchanges, Ergodic Theory Dynam. Systems 38 (2018) 195–219, https://doi.org/10.1017/etds.2016.32.

The claim

The selfish-mining mission took the stationary distribution of Eyal and Sirer's equation (7) as a definition and proved it is invariant with total mass 1. That leaves a gap a careful reader will point out: the revenue analysis is only meaningful if the chain has no other stationary distribution. This mission closes it: every nonnegative, lead-summable, mass-one function that is invariant under one step of the chain is the paper's distribution.

What is proved

• Stationarity (stationary_isStationary): the paper's distribution satisfies the predicate.
• Balance for any stationary π (balance_zero_of, balance_tie_of, balance_one_of, balance_two_of, balance_lead_of): the five balance identities follow from invariance alone, for every $\alpha$ and $\gamma$.
• Geometric form (geometric_of_isStationary): on the lead states every stationary distribution is geometric with ratio $\alpha/(1-\alpha)$; the recurrence's constant mode is excluded by summability.
• Uniqueness (stationary_unique, the goal): every stationary distribution equals stationary α state by state.

What this rests on and what it does not say

The hypotheses $0 < \alpha < 1/2$ are essential: for $\alpha \ge 1/2$ the chain is not positive recurrent and no such distribution exists. Nonnegativity of $\pi$ is in the predicate for faithfulness to the notion of a distribution but is not needed by the proof. No limit theorem is proved: that the chain converges to this distribution from any start, or that time averages of the revenue process converge to the stationary rates, remains outside the formalization. (arXiv:1311.0243)

The claim

The HTLC mission proved which witnesses spend a received HTLC output under the script interpreter, and that its timeout path runs through OP_CHECKLOCKTIMEVERIFY <cltv_expiry>. That is a statement about one script evaluation. The claim Lightning actually needs is one block higher: no block can contain a non-revocation spend of a received HTLC by the timeout path before the expiry height. This mission composes the script result with the block mission's finality rule (IsFinalTx, required by ContextualCheckBlock for every transaction in a block) to state exactly that, and the same bound for a pre-signed HTLC-timeout transaction whose lock time is the expiry.

What is proved

• Finality of height-locked transactions (isFinalTx_height): with a nonzero lock time below the threshold and an input that is not SEQUENCE_FINAL, a transaction is final at height $h$ iff its lock time is below $h$.
• Pre-signed HTLC-timeout transactions (presigned_timeout_height): lock time cltv_expiry means acceptance only in a block above the expiry.
• Received HTLC, timeout path (received_spend_height, the goal): a two-element witness accepted by VerifyScript for a received HTLC output, in a transaction final at height $h$, is a revocation spend or has cltv_expiry < h.

What this rests on and what it does not say

The composition uses only published theorems: received_p2wsh_spend, cltv_concrete, checkLockTime_iff (HTLC mission) and the block mission's isFinalTx. It does not say that a transaction final at a height is in a block at that height, which is the block mission's ContextualCheckBlock characterization, nor anything about the offered HTLC's timeout path beyond the pre-signed transaction's own lock time (there the bound rests on the remote node signing only a transaction with that lock time, a key-level fact outside the script). Time-based expiries (lock times at or above the threshold) are excluded by hypothesis; BOLT #3 uses heights. (BOLT #3, tx_verify.cpp)

The claim

A Lightning channel's funds sit in the funding transaction's output, a pay-to-witness-script-hash of the 2-of-2 script 2 <pubkey1> <pubkey2> 2 OP_CHECKMULTISIG. Everything else in the protocol (commitment transactions, penalties, HTLCs) rests on one fact about this output: it moves only with both parties' signatures. This mission proves that fact against the script interpreter as transcribed from Bitcoin Core, and completes the on-chain script set of a channel begun by the to_local, HTLC and anchor missions.

What is proved

• The script on its witness (funding_witness): the 2-of-2 loop's verdict, with the NULLDUMMY condition on the dummy element.
• The spending condition, for any witness (funding_spends_iff): the witness-v0 success condition holds iff the stack is exactly [sig2, sig1, dummy] with each signature valid for its key in order; no other shape succeeds.
• The output under VerifyScript (parseScript_funding, funding_p2wsh_spend, the goal): the byte form parses as intended, and VerifyScript accepts a witness for the P2WSH output exactly when it is dummy sig1 sig2 with both signatures valid for the spending transaction's own checker.

What this rests on and what it does not say

The signature checks are the signature mission's checker with the witness-v0 sighash; which transaction the signatures commit to (a commitment transaction, a mutual close) is a matter of what was signed, outside the script. BOLT #3's lexicographic ordering of the two keys is not a script-level condition and is not stated. (BOLT #3, interpreter.cpp)

The claim

Modern Lightning channels use option_anchors: the remote balance and both HTLC kinds carry a one-block OP_CHECKSEQUENCEVERIFY so that a commitment transaction's outputs cannot be spent in the same block it confirms in, and each side gets an anchor output that it can spend at any time to bump the fee, and that anyone can sweep after 16 blocks so that anchors do not litter the UTXO set. This mission proves what those scripts enforce, against the script interpreter as transcribed from Bitcoin Core, completing the BOLT #3 commitment-transaction script set begun by the to_local and HTLC missions.

What is proved

• to_remote (to_remote_eval, to_remote_spends_iff, parseScript_toRemote, to_remote_p2wsh_spend): spendable by the remote key, only after the one-block delay, and by nothing else.
• Anchor (anchor_eval, anchor_holder, anchor_anyone, anchor_spends_iff, parseScript_anchor, anchor_p2wsh_spend, anchor_anyone_concrete, anchor_anyone_delay): the funding-key holder spends at any time; a clean-false signature (the empty signature) spends exactly after the 16-block delay; under the concrete checker, the empty-signature witness verifies iff the spending transaction is version 2 or later with nSequence ≥ 16. A signature the checker rejects outright fails the script.
• HTLCs with anchors (the six path theorems, the two spends_iff, the two parse theorems, the two p2wsh_spend): the HTLC mission's three paths each, with the one-block delay added to every non-revocation path and the revocation path unchanged.

What this rests on and what it does not say

The signature checks stay at the level of the signature mission's checker; the 20-byte hashes are parameters. anchor_anyone_concrete holds under consensus flags: under the policy flag WITNESS_PUBKEYTYPE an uncompressed funding key would make the empty-signature path fail, which is not modelled. With the CHECKSEQUENCEVERIFY flag off (pre-BIP112 blocks) the anchor is spendable by anyone at once; the activation mission fixes the flag on for every current height. The HTLC-success and HTLC-timeout second-stage transactions pay to the to_local script, already covered. (BOLT #3, interpreter.cpp)