Motivation

Wilmott, Howison and Dewynne, The Mathematics of Financial Derivatives: A Student Introduction (1995), Chapter 12, pp. 206–212 (https://doi.org/10.1017/CBO9780511812545.013), examine knock-out and knock-in options, barrier conditions and rebates. This fifth Financial Derivatives mission establishes rigorous finite-binomial first-hit valuation identities supporting those contracts. It continues FD-01 finite state-price restrictions, FD-02 one-period replication, FD-03 full-tree European valuation and FD-04's payoff-level barrier complementarity.

The source's distinctive explicit formulae use continuously monitored Black–Scholes diffusions. The current finite-maturity mission is a derived discrete counterpart, and does not claim to prove those continuous-time formulae. That separate mathematical task will require the Black–Scholes PDE and first-passage/reflection foundations.

Setting

Fix the FD-03 strictly arbitrage-free binomial market with initial price $S_0>0$, stock multipliers $0<d<R<u$ and bank-account growth $R$. Write $q=(R-d)/(u-d)$ for the risk-neutral up weight. A full path $\omega$ consists of $N$ up/down observations, and $S_t(\omega)$ is the stock price after the first $t$ moves.

A monitoring schedule $M\subseteq\{0,\ldots,N\}$ specifies whether inception and maturity are observed. For upper level $B$, touch means $S_t\ge B$ at a monitored date. Define $\tau_B(\omega)$ to be the first observed touch and $N+1$ if none occurs. Lower barriers use $S_t\le B$. Equality is a touch. Discrete observation does not infer a hit between monitoring times.

For any terminal reward $g:\mathbb R\to\mathbb R$, set

$$H_{\rm out}(\omega)=g(S_N(\omega))\mathbf1_{\{\tau_B(\omega)>N\}},\qquad H_{\rm in}(\omega)=g(S_N(\omega))\mathbf1_{\{\tau_B(\omega)\le N\}}.$$

Both settle at maturity. The financial model has no dividends, transaction costs or rebate unless one is specified.

Formalization targets

Absorbing first-hit valuation

Construct an absorbing dynamic value independently from the FD-03 terminal-payoff valuation. It is zero at an already knocked-out node, equals the terminal reward at alive maturity, and otherwise obeys the one-period risk-neutral recursion

$$U_t=\frac{qU_{t+1}^{u}+(1-q)U_{t+1}^{d}}{R}.$$

The root proves that this recursion equals the FD-03 \europeanValue\ of the path-sensitive knock-out payoff tree and the discounted finite-path expectation

$$\boxed{V_{\rm out}=R^{-N}\sum_{\omega}p_q(\omega) g(S_N(\omega))\mathbf1_{\{\tau_B(\omega)>N\}}.}$$

It also establishes the genuine price-level complementary identity

$$\boxed{V_{\rm in}+V_{\rm out}=V_{\rm vanilla}.}$$

The proof derives these from tree induction, price additivity and a correctly constructed first-hit event. Neither the required price equality nor an equivalent martingale/absorbing property may be embedded as an assumption or definition.

First-hit rebates

A fixed cash rebate $Z$ payable at the first hitting date has initial value

$$\sum_{\omega}p_q(\omega)\,R^{-\tau_B(\omega)}Z \mathbf1_{\{\tau_B(\omega)\le N\}}.$$

This is proved by a terminal-equivalent payoff $ZR^{N-\tau_B(\omega)}$ on hit paths, so the existing terminal-claim pricing machinery can be reused. A rebate payable at expiry instead has value $R^{-N}Z\Pr_q(\tau_B\le N)$. A rebated knock-out value decomposes into the zero-rebate knock-out value plus the appropriate rebate claim. The two payment conventions are separate theorem targets.

Milestone architecture

The lower-level targets establish chronological path representation, positive stock evolution, agreement with FD-03's full terminal tree, upper and lower touch predicates, existence and minimality of the earliest monitored hit, and monotonicity of hit events under barrier and monitoring changes.

The valuation branch establishes the full-path knock-in/out payoff trees, their sum as the vanilla tree, the three absorbing recursion cases, the induction identifying absorbing and European values, and a finite-product-probability path-sum identity.

The price-order branch proves nonnegativity and vanilla upper bounds for nonnegative rewards, increasing knock-out value as an upper barrier is raised, and decreasing knock-out value as monitored dates are added. Knock-in comparisons follow by complementarity. Signed rewards remain admissible for linear equalities, but are never used to assert these order bounds.

The rebate branch establishes first-hit terminal equivalence, discounting at the actual hitting date, the distinct expiry-paid rebate, a rebated-price decomposition, and a lower-barrier version. A separate optional advanced branch studies a weighted reflection/counting result under reciprocal up/down multipliers and a lattice-aligned barrier. It must prove the weight correction for $q\ne1/2$ and is not a hypothesis of the general root.

Significance

The mission turns elementary contract triggers into constructive arbitrage-free values under a complete, finite stock market. It supplies reusable first-hit and absorbing-state pricing tools for later path-dependent, American-barrier and diffusion-limit missions. Its capstone is a rigorous theorem for arbitrary observed schedules and payoffs, with explicit assumptions and an honest separation from continuous monitoring. The source's continuous barrier equations and their future extension are described in the Cambridge chapter.

Difficulty

The genuinely nontrivial component is identifying first-hit information across all paths of a recombining stock tree. Different histories with the same current stock can have different activation status. The value recursion must carry that status and its monitoring schedule, and the definition of its output cannot assume equality with the price of the terminal claim. The finite weighted path measure and tree recursion must agree without imposing the capstone identity as a hypothesis.

Formalization scope

The root must quantify over an arbitrary finite horizon, explicit monitoring schedule, initial spot and payoff function. The full path must remain available: histories that recombine at the same terminal stock may have different earlier barrier hits.

Important edge cases are $N=0$, no monitoring, monitoring at inception, exact barrier equality, ties, the first hit at expiry, no hit, signed rewards, $R<1$, and rebates paid either upon hit or at expiry. Stock is positive throughout because $d>0$. A standard knock-out does not reactivate after a hit.

Reuse published and pinned FD-03/FD-04 definitions once their current proposal reviews permit imports. An In review proposal is not proof acceptance. Do not execute Lean locally or treat a new Draft theorem as proved. The core milestone graph should use actual proof imports and remain useful independently of the optional reflection branch.

Selected references

• Wilmott, Howison and Dewynne (1995), The Mathematics of Financial Derivatives, Chapter 12, Barrier Options, pp. 206–212: https://doi.org/10.1017/CBO9780511812545.013.
• Cox, Ross and Rubinstein (1979), Option pricing: A simplified approach: https://doi.org/10.1016/0304-405X(79)90015-1.
• Financial Derivatives Financial Derivatives I–IV, Prove2Me owner proposals inspected 27 October 2026: https://prove2.me/.

Financial Derivatives III: Multi-Period Binomial Replication and Optimal Exercise

Motivation and source

A binomial option-pricing model is more than a numerical approximation: it is a finite complete market in which prices can be derived recursively from self-financing replication. At each node, the one-period stock-and-bank market fixes the value of the two possible continuation payments. Repeating this calculation yields the unique European replication price. When an option can be exercised early, the holder instead chooses between its immediate payment and continued exposure to the market. This creates a finite optimal-stopping problem whose value is determined by the Snell recursion.

This mission builds on Financial Derivatives I (payoff geometry, portfolios and put–call parity) and Financial Derivatives II (two-state arbitrage, unique replication and risk-neutral valuation). It proves the multi-period European and American/Bermudan results without introducing an unproved continuous-time stochastic integral or Black–Scholes formula.

The primary source is Paul Wilmott, Sam Howison and Jeff Dewynne, The Mathematics of Financial Derivatives (1995), Chapter 10, printed pp. 180–194. The European valuation is equation (10.16), printed p. 188; the American exercise recursion is equation (10.17), printed p. 191. The stock tree and related risk-neutral conventions appear in §§10.1–10.3, and the European/American algorithms in Figures 10.4 and 10.7. The dynamic-replication, finite stopping-policy and seller-superhedging equivalences below are rigorous extensions of the source's calculations, not verbatim propositions from the book. DOI.

Repeated binomial market

Fix a finite number of periods $N\in\mathbb N$; an initial stock price $S_0>0$; constant up, down and bank-growth multipliers $u,d,R$ satisfying

$$0<d<R<u.$$

The stock is dividend-free, with one-period outcomes $Su$ and $Sd$ when its current value is $S>0$. A current bank deposit $b$ becomes $Rb$ next period. Fractions, short stock positions and bank borrowing are allowed. There are no transaction costs or position constraints. The stronger assumption $d>0$ is important in a multi-period market: it keeps the stock strictly positive at every descendant node, so the FD-II two-state replication theorem is applicable everywhere.

The unique positive risk-neutral up and down weights are

$$q=\frac{R-d}{u-d},\qquad 1-q=\frac{u-R}{u-d},\qquad 0<q<1.$$

These weights price next-period cashflows. They are derived from the stock and bank prices, and are not assertions about real-world stock-move frequencies. For next-period values $V_u,V_d\in\mathbb R$, define

$$\mathcal B(V_u,V_d)=\frac{qV_u+(1-q)V_d}{R}.$$

At current stock price $S$, a one-period replicating portfolio contains

$$\Delta=\frac{V_u-V_d}{S(u-d)},\qquad b=\frac{uV_d-dV_u}{R(u-d)},$$

so $\Delta S+b=\mathcal B(V_u,V_d)$ and next period's stock and bank holdings deliver the prescribed child values. FD-II provides the exact one-period no-arbitrage and uniqueness justifications; this mission must prove that the assembled strategy remains self-financing across all dates and histories.

European backward induction and dynamic replication

Model all $2^N$ terminal histories by a full binary payoff tree, allowing any signed and path-dependent payoff. At maturity the claim value equals its terminal payment $H$. At earlier nodes the recursion is

$$V_t=\mathcal B(V_{t+1}^{u},V_{t+1}^{d}).$$

Prove that this value equals the discounted sum of terminal payments under the product risk-neutral weights. Prove its linearity and monotonicity. Recursively construct an adapted stock/bank strategy that matches the continuation values at each child and rebalances without cash injection. Show that it replicates every terminal history and has the only possible initial cost. A European claim introduced as a separately traded security preserves no-arbitrage exactly when its quote equals that cost.

When the terminal payoff depends only on the final stock price, all histories with the same up count share a value. At time $t$ and after $k$ up moves,

$$S_{t,k}=S_0u^kd^{t-k}.$$

Prove that the efficient $t+1$-node recombining algorithm implements the same backward recursion as the full tree:

$$V_{t,k}=\frac{qV_{t+1,k+1}+(1-q)V_{t+1,k}}{R}.$$

For path-dependent contracts, retaining the distinct histories is necessary. Recombining solely on the stock level would lose contractual information and is not asserted in that generality.

American and Bermudan exercise

An exercise-reward tree assigns a real immediate payment $G$ at each node and records whether exercise is permitted there. Maturity exercise is mandatory; intermediate exercise is available at every date for an American contract and only at selected dates for a Bermudan contract. A stopping policy must use only the history known at the current node: it can stop when permitted or specify separate future decisions for the two child states.

At maturity the exercise value equals $G_N$. At earlier nodes, let $C_t=\mathcal B(V_{t+1}^{u},V_{t+1}^{d})$ be the continuation value. The Snell recursion is

$$V_t=\begin{cases} \max\{G_t,C_t\},&\text{if exercise is permitted},\\ C_t,&\text{otherwise}. \end{cases}$$

Prove, by finite backward induction, that every admissible stopping policy has discounted value no greater than $V_t$, and construct a policy attaining $V_t$ by comparing exercise with continuation at each node. Thus $V_t$ is the finite optimal-stopping value, including ties, and allowing more exercise dates cannot decrease the holder's value. In particular, an American option with the same maturity payoff is worth at least its European counterpart.

As an independent financial theorem, construct a seller's adapted self-financing superhedge starting with the Snell value, and prove that no lower initial capital covers the payment for every admissible holder exercise policy. The holder's stopping policy is distinct from the writer's stock/bank trading strategy. For a put with immediate payment $(K-S)^+$, the resulting recursion is the book's American-put algorithm. It also applies to calls, arbitrary finite exercise sets and signed rewards under the stated maturity convention.

Main theorem and proof architecture

The capstone, provisionally FinancialDerivatives.FD03.finiteBinomial_pricing_and_optimal_exercise, combines four genuinely proved statements:

1. Every finite signed terminal claim has a unique self-financing European replication price, equal to backward induction, discounted risk-neutral valuation and the unique no-arbitrage quote.
2. American and Bermudan values equal the greatest discounted values of admissible nonanticipating exercise policies, as characterised by the Snell recursion.
3. The seller's minimum superhedging capital equals the Snell value, with a constructed strategy that covers all permitted exercise times.
4. For state-only payoffs, a recombining stock-price algorithm reproduces full-tree values.

The proof graph proceeds through market and stock positivity, one-step valuation, full-tree algebra, finite path sums, local hedge replication, recursive self-financing, recombining rows, exercise-policy upper bounds and attainment, and seller superhedging. Every parent must use the relevant actual accepted helpers, with no capstone conclusion packed into a definition or assumed as a hypothesis.

Scope, boundaries and subsequent missions

The time horizon may be zero, rates may be zero or negative as long as $0<d<R<u$, and European claims may have negative payments. Stock positivity throughout the tree requires $d>0$. At exercise-continuation ties either admissible decision is optimal. Strong no-arbitrage excludes $q=0$ and $q=1$. Statements about American calls never being exercised early need separate dividend and interest assumptions and are not made unconditionally here.

Chapter 10's dividend-yield adjustments (§10.6, pp. 191–193) require distinguishing ex-dividend stock growth from total shareholder return; they are reserved for an explicit bridge to FD-08. CRR-to-Black–Scholes convergence is a separate advanced branch requiring precise asymptotics and a continuous-time pricing foundation. The book's numerical comparisons alone do not establish that theorem. The chapter's exercise connecting binomial and finite-difference methods is allocated to the later numerical-analysis missions.

The mission will reuse published, verified Prove2Me and pinned-Mathlib statements. Its natural-language descriptions, Lean declarations, source ledger, milestone ordering and independent read-backs will be audited before the owner confirms and submits a Draft. A Draft or a locally prepared Lean snippet is not evidence that a definition compiles or a theorem has been proved.

Why the composition is the consensus rule

Every component mission transcribed one layer of Bitcoin Core's validation: the subsidy schedule, compact targets and retargeting, the merkle root, the ledger accounting, median time past and the header rules, the activation heights and flag exceptions, serialization and hashing, the Script interpreter, the signature layer, the SegWit and Taproot dispatch. None of them is a consensus rule on its own. The rule is the way AcceptBlockHeader, CheckBlock, ContextualCheckBlock and ConnectBlock combine them — in which order the tests run, which ledger each transaction sees, where the fees and sigop costs accumulate, what the clock may reject, which historical blocks are exempt, and what state results. This mission writes that composition down, as the executable $C(S,B,t)$ of the umbrella contract, states the declarative $V(S,B,t)$ and $\mathrm{ApplySpec}(S,B)$ independently, and proves the two contract theorems. (validation.cpp, tx_verify.cpp, chainparams.cpp)

The validation path

A chain state is the list of validated headers from the genesis to the tip together with the UTXO set (a ledger of coins: output, creation height, coinbase flag). The genesis state holds the genesis header and an empty ledger, as the source never adds the genesis coinbase. A candidate block is offered with the local clock $t$; the outcome is accept S' undo, invalid, futureTime (BLOCK_TIME_FUTURE, a temporary rejection) or missingPrev (the block does not build on the tip).

Header path (AcceptBlockHeader): proof of work, the parent lookup, then ContextualCheckBlockHeader in source order — nBits against GetNextWorkRequired (the period's first block supplied from the chain), the median-time-past floor, the two-hour ceiling against the clock, the BIP34/66/65 version floors. CheckBlock: merkle root and mutation, size and count limits, exactly one coinbase first, CheckTransaction for every transaction, the legacy sigop bound. ContextualCheckBlock: IsFinalTx against the lock-time cutoff (median time past once CSV is active), the BIP34 height push in the coinbase, CheckWitnessMalleation (the commitment in the last qualifying coinbase output, the 32-byte nonce, or no witness at all), the weight limit. ConnectBlock: the genesis shortcut, the BIP30 scan with IsBIP30Repeat and the BIP34 shortcut, GetBlockScriptFlags with the two exception blocks, and the loop — CheckTxInputs, the fee range, SequenceLocks, GetTransactionSigOpCost against 80,000, CheckInputScripts through the complete VerifyScript (Taproot branch included), UpdateCoins — then the coinbase bound against GetBlockSubsidy. DisconnectBlock spends the block's outputs back and restores the inputs from the undo data in reverse, with the clean flag and the two unspendable-coinbase exceptions.

Every layer below is the published mission's function: coreSubsidy, nextWorkRequired, checkProofOfWork, computeMerkleRoot, medianTimePast, versionOutdated, blockScriptFlags, lockTimeFlags, sequenceLocks, verifyScriptFull. Nothing is re-transcribed.

The specification

$V(S,B,t)$ is a predicate, not a program: a header predicate in the PoW mission's specTarget form with the parent, difficulty, time floor, clock ceiling and version floors; a block predicate; a contextual predicate; and a ledger predicate that quantifies over the transactions in sequence — each spends existing, mature coins of valid value, the inputs cover the outputs, the BIP68 specification satisfiesBIP68 holds, every input script verifies, the fees and sigop costs stay within their bounds, BIP30 freshness holds where the scan applies, and the coinbase is bounded by the fees plus the specification subsidy. $\mathrm{ApplySpec}(S,B)$ extends the headers and folds UpdateCoins over the transactions.

Formalization targets

1. Genesis (genesis_checkBlock): the mainnet genesis block passes CheckBlock, by kernel evaluation.
2. Header path (acceptHeader_iff), time classification (futureTime_iff, validate_clock, futureTime_transient): the future-time rejection is exactly characterized, transient, and the only clock dependence.
3. Layer characterizations (checkTransaction_iff, checkBlock_iff, contextualCheck_iff, checkTxInputs_iff, sequenceLocks_iff, connectLoop_iff, connectBlock_iff): each Boolean stage equals its predicate, the BIP68 one through the published fold_acceptance.
4. History (bip30_history): exactly when the BIP30 scan is skipped.
5. State (connectBlock_apply, apply_spec, reachable_wellFormed, work_increases): the resulting ledger is the fold, reachable states are well formed, chain work strictly increases.
6. Undo (disconnect_connect): the undo data restores the previous ledger, cleanly.
7. Goal (acceptance): $R(S) \Rightarrow (C(S,B,t)\text{ accepts} \iff V(S,B,t))$.

What the result establishes

With the component missions, the umbrella's two contract theorems are now Lean theorems about a concrete, source-linked rendering of the pinned mainnet rules, with no parameter left abstract: hashes are SHA-256d, signatures are secp256k1 ECDSA and BIP340 Schnorr, scripts run through the full interpreter, and the historical exceptions are the source's. The definitions were exercised on the real chain: the genesis block, blocks 1–170 as the header chain, and block 170 — the first transaction between two users — validates end to end against the ledger holding block 9's coinbase, is rejected when its signature is altered or the spent coinbase is immature, is classified futureTime at an early clock, and disconnects back to the original ledger cleanly.

What remains outside: the proof-of-work hardness and signature unforgeability (computational assumptions, not functional correctness), the on-disk and networking layers, and a reorganization across multiple blocks, which is the disconnect theorem applied in sequence.

Where the obvious argument fails

The loop breaks at the first failing transaction and threads four accumulators; its characterization needs the fee total and sigop cost to be non-negative so that running-range tests collapse to the final bound, which in turn needs the block predicate's non-negative outputs — the hypotheses on connectLoop_iff and connectBlock_iff. CheckTxInputs uses nSpendHeight - coin.nHeight with natural subtraction, which happens to agree with the specification form for every coin height. The future-time test sits in the middle of the header chain, so classifying it requires the four earlier tests to pass. DisconnectBlock restores inputs in reverse and spends outputs by exact match, so the identity needs the txids distinct, the outputs fresh and every ledger coin spendable with a positive height — which is where reachability and the BIP30 scan enter.

Formalization scope

Policy is off; fJustCheck is false; assumed-valid shortcuts are not modeled (scripts are always checked). The chain is linear: a header whose parent is not the tip is the missingPrev outcome, as BLOCK_MISSING_PREV is not a validity verdict. Block hashes and byte orders are those of the serialization mission. No Mathlib is required; the development imports only Std.

Selected references

• Bitcoin Core contributors. validation.cpp, consensus/tx_verify.cpp, consensus/tx_check.cpp, coins.cpp, kernel/chainparams.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source
• Pieter Wuille. BIP30: Duplicate transactions, 2012. Specification
• Gavin Andresen. BIP34: Block v2, Height in Coinbase, 2012. Specification
• Thomas Kerin, Mark Friedenbach. BIP113: Median time-past as endpoint for lock-time calculations, 2015. Specification
• Eric Lombrozo, Johnson Lau, Pieter Wuille. BIP141: Segregated Witness, 2015. Specification

Motivation

UK defined benefit pensions may combine salary-related benefits, guaranteed minimum pensions (GMP), underpins, different increase promises, survivor entitlements and payment guarantees. Applying a minimum at retirement can produce different payments from applying it to each later instalment. Likewise, a guarantee payable to an estate cannot automatically extinguish a legally protected survivor benefit. These distinctions affect the expected present value and administration of a scheme's promises. Standard life-contingency methods are developed by Dickson, Hardy and Waters (2020), https://doi.org/10.1017/9781108784184, and Promislow (2015), https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782460.

Setting

The main contract has a finite horizon of calendar-month instalments indexed by $t=0,\ldots,H$. A valid date mapping $D_t$ supplies each instalment's actual Gregorian date. Consecutive mapped dates must follow the next calendar month, using a fixed original payment-day anchor and clamping that day at month end when necessary. A member's actual date of death is represented separately for each mortality scenario, within the interval after their last alive instalment and before the next scheduled instalment.

A finite joint scenario law $p_{zij}\geq0$, with $\sum_{z,i,j}p_{zij}=1$, indexes award information $z$, the member's final alive period $i$, and the survivor's final alive period $j$. The horizon terminal state represents survival to the horizon. No independence among these variables is assumed. A payment due at date $t$ has discount factor $v_t$, and the expected present value is

$$\operatorname{EPV}(C)=\sum_{z,i,j}p_{zij} \sum_{t=0}^{H}v_tC_t(z,i,j).$$

The first ordinary pension tranche offers award-date amounts $A_z$ and $B_z$. An automatic award-date underpin fixes $\max(A_z,B_z)$ and retains the selected alternative's own subsequent increase schedule and linked survivor entitlement. A payment-date floor, $\max(A_zG^A_t,B_zG^B_t)$, is a different promise because it may switch the winning alternative later. A second tranche $C_z$ has a separate increase schedule. Monthly amounts and weekly statutory rates use explicitly different units.

For ordinary non-GMP benefits, a scheduled annual limited price indexation rate with floor $f$ and cap $c$, $f\leq c$, is $r_k=\min(c,\max(f,\pi_k))$, where $\pi_k$ is the relevant price index movement. In this illustrative contract, a first scheduled increase within a year of retirement uses the complete-month fraction of the capped annual rate. Later increases occur on scheduled annual dates. Statutory and contractual rounding, index lookbacks and component eligibility remain distinct.

Formalization targets

Option exercise and indexation

Prove that $\mathbb E[\max(X,Y)]\geq\max(\mathbb E[X],\mathbb E[Y])$ for the same joint law, with a strict example. Distinguish the exercise-date information available to a decision-maker from later mortality or inflation outcomes. Formalise floors, caps, compounding, separately scheduled first increases, and both member and survivor indexation paths.

Statutory GMP and anti-franking

The scheme's statutory pre-1988 GMP has no scheme increase under section 109 of the Pension Schemes Act 1993. Qualifying post-1988 GMP receives the full relevant increase on 6 April following the payable date, then on subsequent eligible 6 April dates, without ordinary first-increase pro-rating. Pre-commencement GMP revaluation is a different process. See sections 109–110: https://www.legislation.gov.uk/ukpga/1993/48/section/109.

For eligible cases under section 87(1) or 87(2), let $R$ be the weekly relevant sum, $\Delta G$ the GMP increase since cessation after the specifically applicable pre-1985 transfer-credit growth disregard, $A$ the appropriate addition and $E$ the later earnings addition. The conditional protected weekly aggregate is

$$M=R+\Delta G+A+E.$$

The later earnings term applies only where the scheme provides qualifying post-cessation employment-related accrual under section 87(4)(d). Eligibility separately excludes employment left before 1 January 1985 and employment ceasing to be contracted-out before that date, as provided in section 87(7). For survivors, section 87(2) uses the prescribed half-member-GMP cessation baseline and the actual member death date. The relevant sum, statutory assumptions for the later earnings addition, dates, transfers and special-case entitlement are externally certified scheme/member inputs. The section 87(3)(a) complete-substitute case, sections 91–92 special circumstances and transitional provisions require separate assessment. See https://www.legislation.gov.uk/ukpga/1993/48/section/87.

A statutory survivor GMP entitlement uses a separately certified payable date no earlier than member death; annual 6 April increases are measured from that date. This entitlement is kept separate from the contractual survivor amount. The comparator with an estate guarantee can displace only scheme-permitted survivor amounts above the protected statutory floor. A positive top-up meets any higher applicable certified statutory minimum without adding the entire GMP a second time.

Above-statutory increase credits

Pensions Act 1995 section 53 permits certain excess pension increases in one tax year to be credited towards specified statutory increases in the immediately following tax year, subject to eligibility and allocation restrictions. Pension-credit-attributable pensions are excluded by subsection (3A). Distinguish actual increments after certified credits from the full deemed statutory increase. A generic credit arithmetic definition does not determine statutory eligibility: https://www.legislation.gov.uk/ukpga/1995/26/section/53.

Joint-life valuation and guarantees

Establish finite joint-law cashflow valuation identities, member/survivor payment boundaries and the distinction between parallel estate-plus-survivor payments and a scheme-permitted replacement arrangement. Show that tranche-by-tranche floors can exceed an underpin applied to the aggregate pension.

Integrated capstone

Reconcile the scenario-by-scenario and separately assembled expected present values of a two-tranche monthly pension with option-linked survivor benefits, scheduled ordinary increases, statutory GMP protections and conditional section 87 floors. Prove that the original award exceeds either first-tranche award, both member and survivor payment-level minima are met and the difference between parallel and replacement guarantees equals only the contractually displaceable survivor surplus. The independent section 53 results are supporting work, rather than an assumed automatic offset within the integrated root.

Significance

The formalisation permits scheme rules and certified statutory inputs to be translated into explicit cashflows, with benefit eligibility, date boundaries and unit conversions inspectable. It also provides reusable finite-state valuation and option identities. The underlying life-contingent valuation identities are already established in Dickson, Hardy and Waters (2020). The combined contractual synthesis is an original derived formalisation target. Its present Lean theorem statements have no accepted machine-checked proofs and are not claimed to occur verbatim in those textbooks.

Difficulty

The maximum operator does not commute with expectation or with aggregation over heterogeneous benefit streams. Award-date decisions must respect their information sets. GMP dates and ordinary increase dates use different event rules; death may occur between payments. Where estate guarantees overlap survivor payments, the amount displaced depends on the precise pension promise and protection of statutory benefits. A simple interchange of finite sums proves a valuation reconciliation only after each contingent entitlement has been defined correctly.

Formalization scope

The Lean development uses finite scenarios, nominal instalment amounts, explicit Gregorian dates, a monthly payment calendar, death-date intervals, deterministic increase schedules and certified legal inputs. Its finite two-life indicators and expectation arithmetic reuse the published Actuarial Mathematics CII definitions ActuarialJointD.alive, onlyY, mass and expect via small award-state, retirement and censoring adapters. These are imported from public CII modules at the matching pinned Mathlib revision; the adapted definitions are checked by a separate Lean compatibility proof before reliance in the integrated capstone. The section 87 protections model specified ordinary cases and exclude stated historical circumstances; they do not determine universal legal entitlement. Section 53 credits are a separate conditional component. Special statutory cases, GMP equalisation, conversions, insurer-specific administration and arbitrary exercise-time information are outside the integrated capstone. The finite identities do not require member and survivor independence. Five additional open F theorem targets extend the proved CII annuity and guarantee identities. They include bounded survivor-state equivalence and award-indexed and actual F survivor valuation identities. Their methods have compiled in a private exact-revision Lean check. Neither automatically establishes the integrated scheme promise, because death-fixed survivor amounts, scheduled increases and statutory minima require separate hypotheses. All principal theorem statements remain open proof obligations until independently accepted by the remote verifier.

Selected references

• Dickson, D. C. M., Hardy, M. R. and Waters, H. R., Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, 2020. https://doi.org/10.1017/9781108784184
• Promislow, S. D., Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015. https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782460
• UK Parliament, Pension Schemes Act 1993, sections 17, 87–92 and 109–110. https://www.legislation.gov.uk/ukpga/1993/48/section/87
• UK Parliament, Pensions Act 1995, sections 51–54. https://www.legislation.gov.uk/ukpga/1995/26/section/53

Financial Derivatives IV: Compound, Chooser and Barrier Option Identities

Motivation

The fourth mission in the financial-derivatives series follows the Cambridge chapter by Paul Wilmott, Sam Howison and Jeff Dewynne, The Mathematics of Financial Derivatives (1995), Chapter 11, Exotic and Path-dependent Options, printed pp. 197–205. In particular, §§11.2–11.4 introduce compound options (options on options), chooser options and barrier options. Chapter 12 gives the fuller treatment of barrier valuation; Chapters 13–15 develop more advanced path-dependent models. This mission establishes exact finite-market identities underpinning the Chapter 11 examples. Its capstone is a derived rigorous formulation of simple-chooser pricing, rather than a claim that the book states it in this formal notation.

The preceding FD-03 mission models a strictly arbitrage-free, dividend-free repeated binomial market as a full binary tree. FD-04 will reuse its definitions for market parameters, the stock tree, the European payoff tree and backward-induction valuation. As of 27 October 2026, FD-03 is in review and its definitions have not yet been confirmed as publicly importable. The corresponding paper mathematics is established, while the new Lean declarations and the unaccepted FD-03 theorems remain open formalisation work. Basic real algebra and finite structures already exist in Mathlib. No unproved FD-03 theorem is treated as an axiom.

Setting

Let the stock start at $S_0>0$, with up multiplier $u$, down multiplier $d$, and gross per-period bank factor $R$ such that $0<d<R<u$. Trading is frictionless, the stock has no dividends, and the same binomial parameters remain fixed at every node. Write $\mathcal V_n[f(S_n);S]$ for the FD-03 backward-induction price of a European payoff after $n$ steps when the stock begins at $S$. The arithmetic discount factor over $m$ periods is $R^{-m}$, which is meaningful even when $R<1$.

For any strike $K\in\mathbb R$ and stock price $S$, put

$$c_K(S)=(S-K)^+,\qquad p_K(S)=(K-S)^+,\qquad K_m=K/R^m.$$

Strikes are normally nonnegative for actual option contracts. The core equalities hold for signed $K$, making the Lean theorem more general without changing the financial interpretation. All contracts settle in the same currency. Valuations are time-zero values; a payoff computed at the choice date still needs to be discounted back to time zero.

Formalization targets

The principal target is an exact simple chooser option pricing formula. Supporting targets cover payoff-level put–call parity, recursive valuation, a finite two-stage valuation identity, compound exercise values and complementary barrier contracts. Each target must have a non-vacuous Lean statement whose conclusion follows from earlier definitions and accepted theorems.

Simple chooser valuation

A simple chooser permits the holder to choose, after $n$ periods, between a European call and European put with the same strike $K$, common final expiry a further $m$ periods later, and the same underlying stock. At the choice date the two option values are

$$C_m(S)=\mathcal V_m[c_K(S_m);S],\qquad P_m(S)=\mathcal V_m[p_K(S_m);S].$$

The chooser pays the more valuable of these two options at that date, so its time-zero price is

$$\operatorname{Chooser}_{n,m}(S_0,K) =\mathcal V_n[\max(C_m(S_n),P_m(S_n));S_0].$$

The put–call parity lemma for the remaining $m$ periods is

$$C_m(S)-P_m(S)=S-\frac{K}{R^m}.$$

Hence the choice-date payoff decomposes as

$$\max\{C_m(S),P_m(S)\} =C_m(S)+\left(\frac{K}{R^m}-S\right)^+.$$

Risk-neutral linearity and the two-stage valuation identity then yield the root goal:

$$\boxed{\operatorname{Chooser}_{n,m}(S_0,K) =C_{n+m}(S_0,K)+P_n(S_0,K/R^m).}$$

Here $C_{n+m}$ expires at final maturity, whereas the added European put $P_n$ expires at the choice date with discounted strike $K/R^m$. The result covers $n=0$, $m=0$, ties at the choice date and negative interest rates compatible with $0<d<R<u$. It assumes identical call and put strikes, expiry and exercise conventions. A general chooser with different strikes or expiries has a different decomposition.

The formal root is FinancialDerivatives.FD04.simpleChooser_pricing_identity. It directly asserts the boxed equality for the concrete FD-03 valuation operator, rather than introducing the equality as a hypothesis or hiding it in a definition.

Compound option exercise

A call-on-call has choice/exercise time after $n$ steps, underlying call strike $K$, underlying expiry another $m$ steps later, and compound strike $L$. Its exercise payoff at stock price $S$ is $[C_m(S)-L]^+$. Define the corresponding time-zero binomial valuation and prove basic positivity, zero-strike reduction (when the underlying call value is nonnegative), and monotonicity as the compound strike increases. Proving a Black–Scholes/Geske closed form requires continuous-time assumptions and is outside this discrete foundational mission.

Barrier monitoring and payoff complementarity

A discretely monitored upper barrier $B$ is touched if at least one observed stock price satisfies $S_t\ge B$. The observation sequence must state explicitly whether spot and maturity are included. On any common path, for terminal call payoff $c_K(S_T)$, define the knock-in payoff as $c_K(S_T)$ when touched and zero otherwise, and define the knock-out payoff with the complementary trigger. Their sum is always the ordinary call payoff. There is no rebate, and the in/out contracts share identical monitoring and terminal settlement rules. This is a payoff identity; the full valuation and diffusion barrier PDE are reserved for later missions.

Significance

Rubinstein's original chooser-option discussion (1991) demonstrates why a chooser can be decomposed into a longer-dated call and a shorter-dated put. This makes the pricing calculation auditable and supplies a compositional theorem for subsequent missions. The compound and barrier branches supply independent contract primitives. Future continuous-time models can reuse the payoff-level decomposition while replacing the finite backward recursion with an appropriate discounted conditional expectation. Cox, Ross and Rubinstein (1979) provides the foundational arbitrage-based binomial valuation framework.

Difficulty

The hard formal steps derive put–call parity from the concrete repeated-binomial recursion, show that two-stage valuation equals pricing directly over the combined horizon, and establish additivity of European prices for arbitrary terminal history trees. The depths n, m and n+m require structural induction and precise indexed-tree rewriting. The main theorem cannot be established by assuming the chooser formula, assuming put–call parity, or defining the chooser price to be its intended decomposition.

Formalization scope

1. Pin FD-03 definition module names and check that they have been published. Keep any unapproved imports as explicit Draft blockers.
2. Publish atomic FD-04 definitions for call/put payoffs, discounted strike, finite European prices, chooser and compound exercise payoffs, and barrier monitoring.
3. Prove terminal payoff parity and the discounted stock/cash parity needed for call–put parity at each node.
4. Prove the chooser's local maximum decomposition, European-value linearity on full binary trees and the two-stage valuation/tower lemma.
5. Prove the root equality without assuming it. Cover the zero-step and tie edge cases.
6. Prove compound-option order identities and barrier in/out complementarity as independent branches.
7. Verify that the principal theorem is selected as the proposal's main item, perform a complete Draft read-back, and inspect compilation diagnostics with the remote Prove2Me compiler once dependent imports have been published. The human owner confirms and submits the proposal.

Zero-step horizons, ties at choice, and negative rates consistent with positive gross growth are included. All chooser options here have identical call and put strikes, expiry dates and exercise conventions. Monitoring for barrier contracts is an explicitly supplied sequence of stock observations; touching the level counts as a hit and zero rebates are required for in/out parity. Continuous-monitoring diffusion barrier pricing and Geske compound-option closed forms belong to later missions.

Selected references

• Wilmott, P., Howison, S. and Dewynne, J. (1995), The Mathematics of Financial Derivatives: A Student Introduction, Cambridge University Press, Chapter 11, pp. 197–205, especially §§11.2–11.4. Cambridge chapter. Book DOI.

• Rubinstein, M. (1991), Chooser Options, University of California, Berkeley research manuscript, 6 February 1991. University-hosted PDF. Original same-strike chooser decomposition.

• Cox, J. C., Ross, S. A. and Rubinstein, M. (1979), Option pricing: A simplified approach, Journal of Financial Economics, 7(3), pp. 229–263. DOI. Finite binomial arbitrage-pricing foundation.

Why Taproot is consensus

Since block 709,632 (BIP341 activation, November 2021) every version-1 witness program with a 32-byte payload is a Taproot output. Spending it means either a key-path spend — one Schnorr signature by the output key — or a script-path spend that reveals a leaf script together with a control block proving that the leaf is committed to by the output key, and then runs the leaf under the Tapscript rules of BIP342. Both paths are evaluated by the version-1 branch of VerifyWitnessProgram, which the published VerifyScript mission left as a parameter (TaprootHandler). This mission supplies that parameter from the source and closes the script-validation layer. (VerifyWitnessProgram, BIP341, BIP342)

The transcription covers the tagged hashes (TapLeaf, TapBranch, TapTweak, TapSighash), the merkle path of a control block, the key tweak check through the x-only tweak-add of libsecp256k1, the BIP341 signature hash with all its hash types and the annex, CheckSchnorrSignature, and the Tapscript interpreter rules: the OP_SUCCESSx scan, MINIMALIF as consensus, OP_CHECKSIGADD, the ban on OP_CHECKMULTISIG, the validation-weight budget, OP_CODESEPARATOR positions, and the absence of an operation count.

The two spending paths

Key path. The witness, after removing an annex (a final element starting with 0x50 when at least two elements are present), is a single element: a 64-byte BIP340 signature under SIGHASH_DEFAULT, or 65 bytes whose last byte is a non-zero hash type. The message is the BIP341 signature hash computed from the transaction, the spent outputs, the input index, the hash type and the annex; the key is the 32-byte program itself.

Script path. The last element is the control block (33 + 32k bytes, k ≤ 128); the one before it is the leaf script; the control byte's low bit is the parity of the output key and its other bits the leaf version. VerifyTaprootCommitment recomputes the merkle root from the leaf hash and the path nodes, hashes it with the internal key into the tweak, and checks that the internal key plus tweak·G has the output key's x-coordinate and the stated parity. Leaf version 0xc0 runs the script under Tapscript with the weight budget |serialized witness| + 50; other leaf versions succeed (upgrade hook).

Tapscript. Builds on the published Script mission's interpreter: each non-signature opcode is the same execOp; OP_CHECKSIG, OP_CHECKSIGVERIFY and OP_CHECKSIGADD go through EvalChecksigTapscript (an empty signature is a clean false, 32-byte keys are checked with BIP340, other key lengths are upgradable and succeed, each passed signature costs 50 weight); OP_IF/OP_NOTIF require [] or [1]; OP_CHECKMULTISIG(VERIFY) fail; OP_SUCCESSx anywhere in the script makes it succeed before execution.

Formalization targets

1. Branch hash symmetry (tapbranch_comm) and merkle paths (merkleRoot_base, merkleRoot_snoc): the merkle root is a left fold of the symmetric branch hash along the control block's nodes.
2. Tapscript rules (opsuccess_accepts, checkmultisig_rejected, minimalif_rejects, sigops_budget, checksig_empty): the five BIP342 rules that differ from legacy script, as universal statements about the transcription.
3. BIP341 sighash guards (sighash_type_invalid, sighash_single_missing).
4. Key path (keypath_handler, keypath_annex, checkSchnorr_iff) culminating in the goal, keypath_correct: a key-path spend verifies iff the witness is a BIP340 signature by the output key of the BIP341 hash under the encoded hash type.
5. Script path (scriptpath_commitment): a verifying script-path spend carries a valid commitment of the revealed leaf to the output key.

What the result establishes

With the Script, Signature and VerifyScript missions, the goal theorem reduces the acceptance of a Taproot key-path spend to one BIP340 verification of one BIP341 hash, for every flag set, transaction and amount. verifyScriptFull is the complete VerifyScript of the source, with no parameter left: every output type that has ever been spendable on mainnet now has its validation rule transcribed in Lean. The script-path theorem fixes the commitment structure that the Tapscript execution sits behind; the Tapscript rule theorems make the BIP342 differences from legacy script facts about the definitions.

Policy flags (DISCOURAGE_*) are off, as in block validation. The definitions were checked by evaluation against the full BIP341 wallet test vectors (script trees, tweaks, control blocks, key-path signature hashes and signatures) and the BIP340 vectors.

Where the obvious argument fails

CheckSchnorrSignature distinguishes three signature lengths and reads the hash type from the last byte: the characterization needs the 65-byte case decomposed as body ++ [b] with dropLast/getLast? reasoning, and the converse direction must rule out a 64-byte body being presented as a 65-byte signature. The merkle step theorem requires the chunking of a control block to commute with appending a node, an induction over the node count with the natural-number division (length − 33)/32. The annex is detected by getLast? on the raw witness but popped by dropLast; the script-path theorem threads the witness through two pops in CScriptWitness order (last element on top) before reaching the commitment check.

Formalization scope

The handler is instantiated for the spent outputs of the transaction (needed by the BIP341 hash); the context is the VerifyScript mission's Ctx. Tapscript opcode positions and OP_CODESEPARATOR are tracked here (the Tapscript sighash commits to the position). No Mathlib is required; the development imports only Std.

A trivializing formalization would define the key path as "a Schnorr signature verifies"; here taprootHandler is the source's control flow, and the key-path statement is a theorem about it.

Selected references

• Bitcoin Core contributors. VerifyWitnessProgram, ExecuteWitnessScript, EvalScript, EvalChecksigTapscript, SignatureHashSchnorr, VerifyTaprootCommitment, src/script/interpreter.cpp; XOnlyPubKey::CheckTapTweak, src/pubkey.cpp; secp256k1_xonly_pubkey_tweak_add_check, src/secp256k1, at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source
• Pieter Wuille, Jonas Nick, Tim Ruffing. BIP340: Schnorr Signatures for secp256k1, 2020. Specification
• Pieter Wuille, Jonas Nick, Anthony Towns. BIP341: Taproot: SegWit version 1 spending rules, 2020. Specification
• Pieter Wuille, Jonas Nick, Anthony Towns. BIP342: Validation of Taproot Scripts, 2020. Specification

Why script dispatch is consensus

EvalScript decides what a script does; VerifyScript decides which scripts run, on what stack, under which signature version, and what counts as success. It is where pay-to-script-hash (BIP16), segregated witness (BIP141) and the hand-off to Taproot live: the output script is evaluated first, then — if it is a witness program — the witness is interpreted, or — if it is P2SH — the redeem script is extracted from the scriptSig and run, possibly revealing a wrapped witness program. Each of these steps carries anti-malleability rules (an empty scriptSig for native witness, exactly one push for wrapped witness, push-only scriptSigs for P2SH, a clean witness stack) and the future-compatibility rule that unknown witness versions succeed. (VerifyScript, BIP16, BIP141)

This mission transcribes VerifyScript, VerifyWitnessProgram for version 0 and the unknown versions, ExecuteWitnessScript, and the script predicates, on top of the published interpreter and signature layer, and proves that the four spending templates that carry the chain's history behave as advertised — P2SH, native P2WPKH, native P2WSH, P2SH-wrapped P2WPKH — and that the malleability and compatibility rules hold as universal statements.

Evaluations, stacks, and the dispatch

A byte-level evaluation parses a script with GetOp, rejects scripts over 10,000 bytes, and runs the Script mission's interpreter with the signature mission's concrete oracle for the given signature version (BASE or WITNESS_V0) and script code. Stacks are top-first; a CScriptWitness lists its elements first to last, the last being the top, so witness stacks are reversed before execution.

VerifyScript runs the scriptSig, keeps a copy of the resulting stack, runs the output script, and requires a true top. With WITNESS, an output that is a witness program (OP_n and one push of 2–40 bytes) must have an empty scriptSig and is handed to VerifyWitnessProgram. With P2SH, an output OP_HASH160 <h> OP_EQUAL requires a push-only scriptSig; the copied stack is restored, its top is the serialized redeem script, which is run on the remainder and must leave a true top; with WITNESS, a redeem script that is a witness program must be the scriptSig's only push and is handed to VerifyWitnessProgram as P2SH-wrapped. Finally, with WITNESS, a non-empty witness that no program consumed fails.

VerifyWitnessProgram for version 0 distinguishes a 32-byte program (P2WSH: the last witness element is the script, its SHA-256 must be the program) from a 20-byte one (P2WPKH: exactly two elements, the implied DUP HASH160 <program> EQUALVERIFY CHECKSIG); ExecuteWitnessScript requires every element within 520 bytes and exactly one true element at the end. Version 1 with a 32-byte program outside P2SH is Taproot, delegated to a handler parameter when the TAPROOT flag is on; pay-to-anchor and every other version/size combination succeed.

Formalization targets

Goal — native P2WPKH is correct

$$\mathrm{verifyScript}([\,],\ \mathtt{OP\_0}\langle h\rangle,\ [sig, pk]) \iff \mathrm{castToBool}(h) \wedge \mathrm{Hash160}(pk) = h \wedge \mathrm{checkSig}_{\mathrm{V0}}(\text{p2pkh}(h), sig, pk)$$

for every 20-byte $h$, every signature and key within the push limit, every transaction, amount and flag set with WITNESS. This is BitcoinVerify.p2wpkh_correct: the most common output type on the network today is correct against the full dispatch, the interpreter and the concrete BIP143 checker. The first conjunct is a genuine finding of the transcription: OP_0 <h> is evaluated as a script before the witness is consulted, so an all-zero program is unspendable.

Supporting milestones

1. Predicates (isPayToScriptHash_iff, isWitnessProgram_iff): the byte tests are exactly the templates.
2. Push-only scriptSigs (parseScript_pushes, isPushOnly_pushes): canonical pushes parse back and are push-only.
3. Malleability rules (native_witness_malleated, witness_unexpected): non-empty scriptSig on a witness program fails; an unconsumed witness fails.
4. Future compatibility (unknown_witness_version): unknown versions succeed exactly when the program is a true script value.
5. P2WSH (p2wsh_correct): the witness script, hashed to the program, runs on the remaining elements and must leave one true element.
6. P2SH (p2sh_correct): hash match and redeem evaluation on the pushed arguments.
7. P2SH-P2WPKH (p2sh_p2wpkh_correct): the wrapped program through the P2SH path.

What the result establishes

The template theorems are two-directional: they say what spends succeed and that nothing else does, for every oracle verdict. Combined with the signature mission they reduce the correctness of the four templates to Hash160 equalities and ECDSA verification of the appropriate sighash. The rule theorems make BIP141's malleability protections and its upgrade hooks universal facts about the transcription rather than test cases.

What is left to the Taproot mission: the version-1 branch (TaprootHandler) and Tapscript. What is policy and off: SIGPUSHONLY, CLEANSTACK, MINIMALIF, DISCOURAGE_*. Known modeling limit inherited from the Script mission: OP_CODESEPARATOR positions are not tracked, so the oracle's script code is the whole executed script (exact for scripts without the opcode).

Status: all statements are open with intentional placeholder proofs. The dispatch has been checked by evaluation against independently signed P2WPKH, P2SH-P2WPKH and legacy P2SH spends and their negative variants.

Where the obvious argument fails

The base evaluation of a witness output is easy to forget: OP_0 <h> must itself evaluate to a true top before the witness is looked at, which produces the castToBool h conjunct and the all-zero exception. The P2SH path reasons about two stacks — the one after the scriptSig (restored and popped) and the one after the output script (only its top matters) — and about the parse of the scriptSig twice (as pushes, and as IsPushOnly). The unknown-version theorem needs the evaluation of OP_n for every $n$ in 1–16 through the interpreter's small-integer branch, with its count and disabled-opcode exemptions. Witness order (last element on top) must be threaded through reverse, dropLast and getLast? consistently.

Formalization scope

Flags are the seven consensus flags of GetBlockScriptFlags. The amount is an integer (negative where unknown, as the source passes for legacy inputs). The Taproot branch is a parameter. No Mathlib is required; the development imports only Std.

A trivializing formalization would define verifyScript by cases on the templates; here it is the source's control flow and the templates are theorems.

Selected references

• Bitcoin Core contributors. VerifyScript, VerifyWitnessProgram, ExecuteWitnessScript, src/script/interpreter.cpp, and CScript predicates, src/script/script.cpp, at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source
• Gavin Andresen. BIP16: Pay to Script Hash, 2012. Specification
• Eric Lombrozo, Johnson Lau, Pieter Wuille. BIP141: Segregated Witness (Consensus layer), 2015. Specification
• Johnson Lau, Pieter Wuille. BIP143, 2016. Specification

The Hlawka inequality compares the norms of three vectors with those of their pairwise sums and total sum. The question is the smallest comparison constant that works in every finite dimension.

This mission records the proved extension of the sharp diagonal Hlawka constant to every real $p\ge12$. It uses the unchanged coordinate norm and cyclic constant from the foundation mission, for arbitrary complex vectors, including unequal and zero norms.

The cutoff-12 goal theorem is already proved on Prove2Me. Sixteen accepted interval proofs cover $[12,16]$ and join the proved cutoff-16 result. The conclusion includes both the inequality and optimality of its constant, uniformly over all finite complex coordinate dimensions.

This is an entry in the sharp diagonal Hlawka campaign, whose conjectured endpoint is $p\ge2$. The cutoff-2 mission remains open; 12 is a proved sufficient cutoff, with no claim that it is optimal. The broader Schatten-norm question for general matrices is described by Audenaert and Kittaneh, §8.2.

A finite-range piece of Dusart's explicit upper bound for the prime counting function: $\pi(x) \le x/(\log x - 1.1)$ for $60184 \le x \le 2\cdot 10^6$. Dusart proved the bound for every $x \ge 60184$ [P. Dusart, Estimates of some functions over primes without R.H., arXiv:1002.0442, Theorem 6.9]. This mission asks only for the finite range, which is a computation over about 148,000 primes and needs no analytic input.

Why it matters: the bound is an input to explicit Goldbach-type results, where it is used to control prime counts in a bounded window. A Lean proof lets those results drop one cited assumption.

Proposed by the Lean Lab, an AI-assisted formalization project on Goldbach-related literature. The statement was written by Claude; the proposer confirmed it against the paper before launch.

Why the signature layer is consensus

A Bitcoin transaction is authorized by signatures, and whether a signature counts is decided by a chain of exact rules: the byte layout the signature must have (strict DER since BIP66), which parts of the transaction the signature commits to (the signature hash, in its legacy and BIP143 forms, with the historical SIGHASH_SINGLE bug), how the public key is parsed, how a possibly non-canonical signature is parsed "laxly", and finally ECDSA verification on secp256k1 — or Schnorr verification for Taproot. Each of these has been the site of a consensus-relevant subtlety: BIP66 was a soft fork to remove OpenSSL's parsing from consensus; the SIGHASH_SINGLE bug lets a signature commit to nothing; high-S normalization is why libsecp256k1 accepts what historical blocks contain. (interpreter.cpp, pubkey.cpp, BIP66, BIP143, BIP340)

This mission transcribes that layer end to end — the encoding checks, FindAndDelete, both signature hashes, CPubKey::Verify with the lax DER parser and normalization, the secp256k1 verification equations for ECDSA and Schnorr, the checker's lock-time methods, and the byte-level script parser — and proves what the rest of validation needs: the strict-DER test is exactly the canonical layout, the signature hashes depend on what they should and nothing else, the checker's outcomes are characterized, and the Script mission's abstract P2PKH theorem instantiates to the concrete cryptography.

Keys, signatures, hashes, and the checker

secp256k1 is the curve $y^2 = x^3 + 7$ over the prime field of order $p$, with group order $n$ and generator $G$. Points are affine pairs or infinity; addition and scalar multiplication are the textbook formulas with Fermat inverses. A public key is parsed as secp256k1_eckey_pubkey_parse: compressed (02/03, square root by $(p+1)/4$ with parity selection), uncompressed (04) or hybrid (06/07), with coordinates below $p$ and on the curve. A signature reaches verification through ecdsa_signature_parse_der_lax, which tolerates long-form lengths and leading zeros, ignores trailing bytes, and substitutes the zero signature on overflow; its S value is normalized to the low half; the message is the 32-byte hash reduced modulo $n$; and secp256k1_ecdsa_sig_verify accepts iff $r, s \in [1, n)$, $R = e s^{-1} G + r s^{-1} Q \ne \infty$ and $R_x \equiv r \pmod n$. Schnorr verification is BIP340 with tagged hashes and lift_x.

The signature hash of input $nIn$ under hash type $t$ is, for legacy scripts, SHA-256d of the CTransactionSignatureSerializer output — version, the inputs (only the signed one under ANYONECANPAY; other inputs' scripts blanked, their sequences zeroed under SINGLE/NONE), the outputs (none under NONE, truncated to $nIn+1$ with blanked others under SINGLE), lock time — followed by $t$ as four bytes, except that SINGLE with no output at $nIn$ yields the constant $1$; for witness v0 it is the BIP143 construction with hashPrevouts, hashSequence, hashOutputs, the script code and the amount.

The encoding checks are IsValidSignatureEncoding (the fourteen BIP66 tests), low-S, the key-shape tests and the hash-type test, assembled by CheckSignatureEncoding/CheckPubKeyEncoding under the flags (DERSIG is the only one mainnet consensus enables). The checker (EvalChecksigPreTapscript) deletes the signature push from the script code (legacy only), applies the encoding checks as script errors, and returns CheckECDSASignature's verdict: a valid key, a non-empty signature whose last byte is the hash type, and CPubKey::Verify on the signature hash. The lock-time checks are CheckLockTime and CheckSequence. The oracle packages all of this, with Core's hashes, into the abstract Oracle of the legacy Script interpreter.

Formalization targets

Goal — the strict-DER characterization

$$\mathrm{IsValidSignatureEncoding}(sig) \iff sig = \mathtt{30}\,L\,\mathtt{02}\,|r|\,r\,\mathtt{02}\,|s|\,s\,ht \text{ with } r, s \text{ minimal positive big-endian integers and } |r|+|s| \le 66.$$

This is BitcoinSig.derEncode_complete together with its converse derEncode_valid: the byte-indexed test of the source is exactly the canonical layout, in both directions. It is the content of BIP66 as a statement about byte strings rather than a procedure.

Supporting milestones

1. SIGHASH_SINGLE bug (sigHash_single_bug): the hash is $1$ when there is no output at the input's index.
2. What signatures commit to (sigHashLegacy_skeleton, sigHashWitnessV0_skeleton): both hashes ignore scriptSigs and witnesses; (sigHashLegacy_anyoneCanPay): with the flag, only the signed input matters.
3. Keys and S values (pubkeyValid_iff, normalizeS_low, overflow_rejected).
4. The checker (checkSig_empty, checkSig_dersig, checkSig_base_iff): an empty signature is a clean false; with DERSIG a malformed one is a script error; the legacy verdict is ECDSA on the legacy sighash of the signature-deleted script code.
5. Byte-level parsing (parseScript_p2pkh): the P2PKH bytes parse to the interpreter's P2PKH instructions.
6. The concrete P2PKH theorem (p2pkh_concrete): the Script mission's p2pkh_correct, instantiated with Core's hashes and checker.

What the result establishes

With this mission the signature-related rules of the pinned source are kernel-checked semantics rather than prose: what shape a signature must have, what it signs, and what accepting it means in terms of the curve equations. The characterization of strict DER removes a class of malleability by construction. The sighash theorems are the facts that transaction malleability arguments and the segregated-witness design rest on. The concrete P2PKH theorem closes the loop the Script mission opened: the template is correct with the real cryptography, modulo nothing but the mathematics of the curve.

What is deliberately not claimed: that the curve operations are constant-time, that the group law holds (the verifier is a function; its correctness as a signature scheme is a cryptographic, not a consensus, property), or anything about OP_CODESEPARATOR positions, which the legacy interpreter of the Script mission does not track (the oracle's script code is the executed script, exact for separator-free scripts). Signature caching, the precomputed-transaction-data caches and the sighash midstate cache are optimizations with the same result and are not modeled.

Status: all statements are open with intentional placeholder proofs. The definitions have been checked by evaluation against the BIP340 test vectors, the BIP143 worked example, independently generated ECDSA signatures, and a reference implementation of the legacy serializer.

Where the obvious argument fails

The strict-DER characterization is byte-index chasing: the source reads sig[4], sig[5 + lenR], sig[lenR + 7], and the proof must relate these to the slices $r$ and $s$ and show the three leading-zero rules are exactly minimality of the big-endian integers. The converse direction needs the cuts at $4$, $4 + |r|$, $6 + |r|$ and the end to reassemble the string. The sighash theorems look definitional but require relating getD on the input list to the projected skeleton under ANYONECANPAY (one input), SINGLE (outputs truncated) and the blanking rules. The checker characterization has to split the signature into body and hash-type byte in both directions.

Formalization scope

Field and scalar arithmetic are on Nat modulo $p$ and $n$, with inverses by Fermat and explicit fuel for exponentiation and scalar multiplication. Byte strings are List (BitVec 8); the transaction type is the serialization mission's. Policy flags (LOW_S, STRICTENC, WITNESS_PUBKEYTYPE, NULLFAIL, CONST_SCRIPTCODE) are carried where they shape the control flow but are off in block validation. Tapscript signature checking (BIP341/342 sighash, OP_CHECKSIGADD) belongs to the Taproot mission.

A trivializing formalization would define the strict-DER test by the layout, or the sighash by what it should depend on; here both are the source's procedures and the layout and dependence are theorems. No Mathlib is required; the development imports only Std.

Selected references

• Bitcoin Core contributors. script/interpreter.cpp, pubkey.cpp, script/script.cpp, and libsecp256k1 eckey_impl.h, ecdsa_impl.h, modules/schnorrsig/main_impl.h at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source
• Pieter Wuille. BIP66: Strict DER signatures, 2015. Specification
• Johnson Lau, Pieter Wuille. BIP143: Transaction Signature Verification for Version 0 Witness Program, 2016. Specification
• Pieter Wuille, Jonas Nick, Tim Ruffing. BIP340: Schnorr Signatures for secp256k1, 2020. Specification
• Certicom Research. SEC 2: Recommended Elliptic Curve Domain Parameters, v2.0, 2010. Standard

Why serialization and hashing are consensus

Every commitment in Bitcoin — a transaction id, a merkle root, a block hash, the proof-of-work target test — is a hash of a byte string, and the byte string is produced by a serializer that every node must implement identically. A node that encoded a CompactSize one byte longer, or read a witness flag differently, would compute different ids for the same transaction and fork from the network. Bitcoin Core's serialization lives in serialize.h (integers, CompactSize, vectors), primitives/transaction.h (the basic and BIP144 extended transaction formats), primitives/block.h (the 80-byte header), and its hashes in crypto/ and hash.h. (serialize.h, transaction.h, sha256.cpp)

This mission transcribes that layer — writers and readers for integers, CompactSize, vectors, transactions, headers and blocks; SHA-256, RIPEMD-160 and SHA-1 as full algorithms; Hash, Hash160, txid, wtxid, the header hash; transaction and block weights; and the mainnet genesis block — and proves the properties the rest of consensus consumes: encodings are canonical and round-trip, the witness-stripped id ignores witnesses, hashes have their sizes, and the transcribed genesis block hashes to the genesis hash of chainparams.cpp.

Bytes, readers, and well-formedness

A writer turns a value into a byte list; a reader consumes a prefix of a byte list and returns the value and the remainder, or none where the source throws. Fixed-width integers are little-endian; signed ones are two's complement. A CompactSize is one byte below $253$, or a marker byte $253$, $254$, $255$ followed by $2$, $4$, $8$ little-endian bytes; the reader rejects an encoding that could have been shorter ("non-canonical") and, in its default range-checked mode, any value above $\mathrm{MAX\_SIZE} = 2^{25}$. A vector is its CompactSize length then its elements; a byte string is its length then its bytes; a uint256 is 32 raw bytes.

A transaction serializes as version vin vout nLockTime, or, when witnesses are allowed and some input carries one, in the extended format: version 0x00 0x01 vin vout witnesses nLockTime, where the 0x00 is an empty dummy vin and 0x01 the flag byte. The reader follows the source's control flow exactly: it reads vin; if that is empty and witnesses are allowed it treats it as the dummy, reads the flag byte and, if non-zero, the real vin and vout; a set witness bit then reads one witness stack per input and rejects a record whose stacks are all empty; any other flag bit rejects. A header is int32 nVersion, previous hash, merkle root, nTime, nBits, nNonce; a block is a header and a transaction vector.

Well-formedness names the field ranges under which the writers are faithful: 32-bit fields below $2^{32}$, hashes of 32 bytes, amounts in $[-2^{63}, 2^{63})$, lengths at most $\mathrm{MAX\_SIZE}$, and — for blocks — every transaction has an input or a witness.

Hashes are the algorithms of crypto/: Merkle–Damgård padding, 64-byte chunks, the SHA-256 schedule and 64 rounds, the two RIPEMD-160 lines, the SHA-1 rounds; Hash is SHA-256 twice and Hash160 is RIPEMD-160 of SHA-256. The txid hashes the witness-stripped serialization; the wtxid the full one; the block hash the 80-byte header. Weight is three times the stripped size plus the full size.

Formalization targets

Goal — blocks round-trip

$$\mathrm{readBlock}(aw, \mathrm{serBlock}(aw, b) ++ r) = \mathrm{some}(\text{(}b\text{ with witnesses iff } aw\text{)},\ r)$$

for every well-formed block $b$, witness mode $aw$ and remainder $r$. This is BitcoinSer.block_roundtrip: deserialization is a left inverse of serialization, in the witness-aware and the legacy reader alike. It is the statement that gives every hash commitment a referent: the bytes a node hashes are exactly the bytes from which every other node recovers the same block.

Supporting milestones

1. Fixed-width integers (leBytes_length, readLE_leBytes): width and round-trip.
2. CompactSize (compactSize_roundtrip, compactSize_canonical, compactSize_range): the writer's output is accepted; only the shortest encoding is ever accepted; read values are bounded.
3. Headers (serHeader_length, header_roundtrip): 80 bytes, round-trip with the signed version.
4. Transactions (tx_roundtrip): round-trip in both formats, with the genuine side condition that the witness-aware reader needs a non-empty vin or a witness.
5. Witness independence (serTx_strip, txid_strip): the stripped serialization and the txid ignore witness data.
6. Weights (weight_no_witness): without witnesses, weight is four times the size.
7. Hash sizes (sha256_length, hash160_length).
8. Genesis (genesis_merkle, genesis_hash): the transcribed genesis coinbase and header hash, by kernel evaluation of the transcribed SHA-256, to the merkle root and block hash recorded in chainparams.cpp.
9. Injectivity (serBlock_injective): distinct well-formed blocks have distinct serializations.

What the result establishes

The round-trip and canonicality theorems make the byte layer of consensus exact: a transaction or block has one encoding, the encoding determines the object, and the identifier hashes are functions of the object alone. The genesis theorems are an end-to-end check against the real chain: the transcriptions of CreateGenesisBlock, the serializers and SHA-256 together reproduce the hard-coded genesis hash, which no transcription error in any of them could survive. The witness-independence theorem is the structural fact behind segregated witness. For the whole-consensus development this mission supplies the concrete hash and serialization semantics that the Merkle, header, proof-of-work and script components took as parameters.

Not modeled: network message framing, CompactSize reading in the chunked allocation loop (semantically the same read), serialization of CBlockIndex/undo data, and the stream exception types (all failures are none).

Status: all statements are open with intentional placeholder proofs. The hash functions have been checked against the standard test vectors and the genesis values by evaluation; the genesis theorems are stated so that the kernel re-checks them.

Where the obvious argument fails

Round-trip looks like unfolding until the transaction reader: because UnserializeTransaction reuses the vin read as the witness dummy, an empty vin is ambiguous, and the honest theorem carries the side condition "an input or a witness". The canonicality theorem is where the three "non-canonical" rejections earn their keep: without them a value would have several encodings and the statement would be false. The signed fields need the two's-complement conversion in both directions. For the genesis theorems the difficulty is not mathematical but computational: the kernel must evaluate nine SHA-256 compressions, which the definitions are written to allow (structural recursion only, no well-founded fixpoints in the evaluated path).

Formalization scope

Bytes are BitVec 8, values are Nat/Int, words are UInt32. Readers return Option (α × Bytes). The writers truncate out-of-range values modulo the width, which the well-formedness predicates exclude; the readers are total. No Mathlib is required; the development imports only Std.

A trivializing formalization would define the readers as inverses of the writers; here each reader follows the source's byte-level control flow, and the round-trips are theorems.

Selected references

• Bitcoin Core contributors. serialize.h, primitives/transaction.h, primitives/block.h, hash.h, crypto/sha256.cpp, crypto/ripemd160.cpp, kernel/chainparams.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source
• Eric Lombrozo, Johnson Lau, Pieter Wuille. BIP141: Segregated Witness and BIP144: Peer Services (transaction serialization with witness), 2015. BIP144
• NIST. FIPS 180-4: Secure Hash Standard, 2015. Standard

Why multiplication improvements need explicit reductions

When a faster multiplication algorithm becomes available, its consequences depend on which problems reduce to multiplication and how the reduction changes input size. A displayed runtime bound alone does not identify this connection. The surrounding computation can also consume the improvement if its cost is omitted or underestimated.

Fourier transforms and bounded integer convolution illustrate two different connections. A complex Fourier transform can be expressed through ordinary complex polynomial multiplication using chirps, following Bluestein's construction. Bounded integer coefficients can instead be packed into binary integers, as in Kronecker substitution. This mission makes the first reduction an explicitly counted arithmetic program and proves the operand-size bound needed by the second. It does not identify binary integer computation with exact complex arithmetic.

Two computational interfaces

A costed oracle returns an answer and a natural-number charge. The general program interface supports returns, explicitly charged work, and adaptive oracle queries. Its substitution theorem preserves answers and sums the query charges with local overhead.

The concrete Fourier interface additionally has explicit instructions for complex multiplication and inversion, each charged one unit. A product instruction takes arrays of lengths $n$ and $2n+1$ and returns their ordinary polynomial product as an array of length $3n+1$, including trailing zero padding. The oracle's charge measures that product call. Array construction, access, index arithmetic, and control operations are uncharged in this arithmetic-operation model. The complex parameter $\rho$ is supplied as input, so root construction is outside the interface.

The binary magnitude length $\ell(z)$ is zero for $z=0$ and is $\lfloor\log_2|z|\rfloor+1$ otherwise. It excludes a sign bit. The integer oracle multiplies signed integers $(u,v)$ with charge bounded by $M(\max\{\ell(u),\ell(v)\})$. Packing and decoding still have explicit charges $E,D$; their implementation in a bit-machine model is outside the proved scope.

Formalization targets

The reusable general theorem states that a correct oracle with nondecreasing bound $T$, at most $k$ calls of size at most $s$, and overhead at most $h$ gives correct execution with cost

$$h+kT(s).$$

Composition preserves the complete answer-and-cost pair. An asymptotic corollary transfers eventual upper bounds on the resulting formula.

The main goal is the concrete Fourier transfer theorem. For every $n\ge0$, nonzero $\rho\in\mathbb C$, and input $x\in\mathbb C^n$, a fixed program returns

$$y_k=\sum_{j=0}^{n-1}x_j(\rho^2)^{jk}$$

with one full polynomial-product call and exactly $6n+7$ additional multiplication or inversion instructions. Consequently, if the oracle cost is at most $P(2n+1)$, then

$$\operatorname{cost}(n)\le P(2n+1)+6n+7.$$

When $\rho^2$ is the desired primitive $n$th root of unity, this is the unnormalised discrete Fourier transform. The identity itself holds for every nonzero $\rho$. The main theorem does not assume that $P$ is monotone or regular.

The Fourier milestones verify middle-coefficient extraction from a full product, generation of $m$ chirp entries in exactly $2m$ instructions, the chirp identity, the exact total cost, and its runtime consequences. For $n\ge1$, the conditions $P(2n+1)\le C P(n)$ and $n\le P(n)$ give the pointwise bound $(C+13)P(n)$. If these conditions hold uniformly with one $C$, a family of these transforms has accounted cost $O(P(n))$.

The integer milestones prove that packing $r$ signed coefficients of magnitude at most $2^p$ in base $2^{3p}$ produces an integer of magnitude length at most $3pr$, for $p\ge1$. For input bound $2^b$, the automatic choice $p=b+\ell(2r)$ satisfies every spacing condition when $r\ge1$. The resulting convolution program is correct and costs at most

$$E+D+M\bigl(3r(b+\ell(2r))\bigr).$$

This applies the existing proved signed Kronecker correctness theorem with a newly justified oracle input size.

What is reusable

The Fourier application no longer relies on arbitrary preparation and decoding labels. Its specific program includes every complex multiplication and inversion used to generate the chirps and scale the arrays, and the interpreter proves their count. A better complex polynomial-product bound can be substituted directly into the main inequality.

The packing application now evaluates an integer multiplication bound at a proved number of magnitude bits. Its logarithmic spacing overhead remains visible. This prevents substituting a length-$r$ coefficient array directly into a runtime bound for $r$-bit integers.

These are formalizations of known reduction principles, with concrete program choices and constants supplied by the companion development. They are not new Fourier or multiplication exponent records. Local Lean proofs accompany every theorem in the strengthened draft. Local verification and accepted platform proof submissions remain distinct statuses.

Where the proof obligations lie

Correct adaptive substitution must preserve subsequent queries, not merely the final numerical bound. Fourier preparation must actually generate chirps by a linear number of instructions; writing a large power in a returned expression would not justify a cheap implementation. Full-product coefficients must match the middle-product identity at every permitted index, and negative exponents must use a nonzero parameter.

Signed packing requires both correctness of balanced-digit decoding and a magnitude bound on the packed operands. A correct encoding alone cannot justify the claimed multiplication cost. Replacing $P(2n+1)$ by $O(P(n))$ also needs a scaling condition; arbitrary runtime functions do not supply one automatically.

Formalization scope and remaining work

The core definitions use terminating inductive programs, natural-number charges, and an explicit eventual big-O predicate. The arithmetic instruction type permits arbitrary mathematical continuations and return values, so it is not a verified compiler from arbitrary functions to circuits. For the concrete Fourier program, preparation and decoding use only its explicit scalar instructions and structural array operations. Its cost result is an arithmetic-operation count, with the oracle cost interpreted in the same unit.

The Fourier theorems include $n=0$; this particular program still performs seven scalar instructions and a product call, returning an empty array. The packing size lemma includes empty lists and cancellation, while convolution requires $r\ge1$. Coefficient bounds include their endpoints and allow negative entries.

The integer result does not prove linear-time bit encoders or decoders. Neither application establishes finite-precision error bounds, root-construction costs, memory costs, or an unrestricted implication from binary integer multiplication to exact complex DFT complexity. Subsequent work can add a verified bit representation and encoding implementation, or a register-based arithmetic compiler. Such additions must justify their costs independently rather than selecting favorable work labels.

Selected references

• L. I. Bluestein, A linear filtering approach to the computation of discrete Fourier transform, IEEE Transactions on Audio and Electroacoustics 18(4), 1970, pp. 451–455. DOI.
• Andrew V. Sutherland, 18.783 Lecture 3: Finite fields and integer arithmetic, MIT course notes, 2019, Section 3.6. Notes.
• Prove2me, IntMul.HvdH.kronMul_eq, proved formal theorem. Statement and proofs.
• General runtime transfer and its Fourier/packing applications, companion proof note and Strengthened transfer results, 24 October 2026, Theorems 1–8. The exact instruction program, accounting constants, and oracle interfaces are this development's formulations of the classical reductions.

Budget pacing in auction markets

Internet advertising markets sell impressions, clicks and conversions one auction at a time, and most advertisers attach a budget to a whole campaign. Bidding one's full value until the budget runs out is suboptimal: the buyer drops out early and misses later auctions that may offer the same value at a lower price. A widely used remedy is multiplicative pacing: the platform shades every bid of buyer $i$ by a common factor, bidding $\alpha_i v_{ij}$ instead of $v_{ij}$, with the pacing multiplier $\alpha_i\in[0,1]$ chosen so that the budget lasts. When every buyer is paced, the multipliers interact through the prices, and the natural question is whether there is a stable profile of multipliers at all.

Conitzer, Kroer, Sodomka and Stier-Moses (arXiv:1706.07151, Operations Research, 2022) study the static game behind this mechanism for second price auctions, define its equilibrium notion and prove that an equilibrium always exists.

Timeline.

• 1952: Debreu (PNAS), Glicksberg (PAMS) and Fan (PNAS) prove that games with compact convex strategy sets and continuous payoffs that are quasiconcave in the player's own strategy have pure-strategy Nash equilibria.
• 2007: Borgs et al. (WWW 2007) study bid-optimization dynamics with budgets in first price auctions, with a similar noise-smoothing of ties.
• 2015–2021: Balseiro, Besbes and Weintraub (Manag. Sci. 2015), Balseiro and Gur (Manag. Sci. 2019) and Balseiro, Kim, Mahdian and Mirrokni (Oper. Res. 2021) analyse budget management in stochastic models, with budgets holding in expectation.
• 2017–2022: Conitzer et al. (arXiv:1706.07151) introduce second price pacing equilibria for deterministic markets and prove their existence (Theorem 1).
• 2021: Chen, Kroer and Kumar (arXiv:2103.13969) show that computing such an equilibrium is PPAD-complete.

The pacing game and its equilibrium

A pacing game has a finite set $N$ of buyers and a finite set $G$ of divisible goods. Buyer $i$ has a valuation $v_{ij}\ge0$ for good $j$ and a budget $B_i>0$. Buyer $i$ picks $\alpha_i\in[0,1]$ and bids $\alpha_i v_{ij}$ on every good; each good is sold in a single-slot second price auction. Write $\operatorname{ho}_{ij}(\alpha)=\max_{k\ne i}\alpha_k v_{kj}$ for the highest bid on $j$ other than $i$'s (it is $0$ when $i$ is the only buyer).

A second price pacing equilibrium (SPPE, Definition 2) is a triple $(\alpha,x,p)$ of multipliers $\alpha\in[0,1]^N$, allocations $x_{ij}\in[0,1]$ and per-unit prices $p_j$ such that, with spend $s_{ij}=p_jx_{ij}$:

1. $\sum_i x_{ij}\le1$, with equality whenever some $v_{ij}>0$;
2. $x_{ij}>0$ implies that $\alpha_iv_{ij}$ is (possibly tied for) the highest bid on $j$;
3. $x_{ij}>0$ implies $p_j=\operatorname{ho}_{ij}(\alpha)$;
4. $\sum_j s_{ij}\le B_i$;
5. $\sum_j s_{ij}<B_i$ implies $\alpha_i=1$ (no unnecessary pacing).

The proof passes through the $(\epsilon,H)$-smoothed pacing game (Definition 3). A reserve bid $2\epsilon$ is added on every good, treated as one more bidder. With $b^*_j$ the highest bid, every bidder within $\epsilon$ of $b^*_j$ receives a share of good $j$ proportional to its distance above $b^*_j-\epsilon$, and buyer $i$ pays $p_{ij}$ per unit, the highest bid other than hers minus $\epsilon$. Each buyer also receives $\alpha_i$ units of an artificial good worth $2\epsilon$ per unit at price $\epsilon$. Her utility is the leftover budget $B_i-\alpha_i\epsilon-\sum_js_{ij}$, multiplied by $H$ when it is negative, plus $2\alpha_i\epsilon+\sum_jx_{ij}v_{ij}$.

Formalization targets

Goal: Theorem 1

$$\text{for every pacing game }(N,G,v\ge0,B>0):\qquad \exists\,(\alpha,x,p)\ \text{an SPPE}.$$

No genericity, no tie assumption and no bound on $|N|$ or $|G|$: one buyer, no buyers and goods nobody values are all covered.

Milestones

1. Continuity (proof of Theorem 2): in the smoothed game, $x_{ij}$, $s_{ij}$ and $u_i$ are continuous on $[0,1]^N$.
2. Quasiconcavity (proof of Theorem 2): with $\alpha_{-i}$ fixed, the total spend $\alpha_i\epsilon+\sum_js_{ij}$ is continuous and strictly increasing in $\alpha_i$; $u_i$ is strictly increasing where the spend is at most $B_i$ and, if $H>M/\epsilon$, strictly decreasing where it is at least $B_i$.
3. Theorem 2: if $\sum_jv_{ij}+2\epsilon\le M$ for all $i$ and $H>M/\epsilon$, the smoothed game has a pure-strategy Nash equilibrium.
4. The four claims of the proof of Theorem 1, for a convergent sequence of smoothed equilibria with $\epsilon^l\to0$, $H^l\to\infty$, $H^l>M/\epsilon^l$ and limit point $(\alpha^*,x^*,p^*,s^*)$: the limit allocation is feasible and goes to highest bidders; $p^*_{ij}=\operatorname{ho}_{ij}(\alpha^*)$ and $s^*_{ij}=x^*_{ij}p^*_{ij}$; $\sum_js^*_{ij}\le B_i$; and $\alpha^*_i<1\Rightarrow\sum_js^*_{ij}=B_i$.

Significance

Theorem 1 makes the SPPE a well-defined solution concept for every instance of the market. The rest of the paper builds on it: SPPE are shown to be best responses (Proposition 2), to refine competitive equilibria of the associated market (§5), and to be the outputs that a mixed-integer program can optimise over; the paper's complexity results (NP-hardness of finding revenue- or welfare-optimal equilibria) presuppose that equilibria exist. The later PPAD-completeness result of Chen, Kroer and Kumar concerns the computation of an object whose existence is this theorem.

The theorem has a published proof; nothing in it has been machine-checked. A formal development needs a pure Nash existence theorem for continuous quasiconcave games, a careful treatment of the smoothed game's continuity, and a compactness-and-limit argument. Each of these is reusable for other smoothing arguments in auction and market design (first price pacing equilibria, throttling equilibria).

Difficulty

The pacing game is discontinuous: a buyer's allocation jumps when her bid crosses another bid, and her utility drops to $-\infty$ when she exceeds her budget. So standard existence theorems do not apply to it, and it is not evident a priori that the game with a fixed tie-breaking rule has a pure Nash equilibrium at all (p. 9). Definition 2 also demands a refinement, no unnecessary pacing, that an arbitrary Nash equilibrium need not satisfy. The obvious fixed-point argument on $\alpha$ alone fails because the allocation is a correspondence, not a function, at ties.

The smoothing removes the discontinuities, but its limit must be controlled: the reserve buyer must win nothing in the limit on goods someone values, the budget penalty $H^l$ must force feasibility, and the artificial good must force every paced buyer to exhaust her budget. Each limit claim uses a different one of these devices.

Formalization scope

• Buyers and goods are arbitrary finite types N, G (Fintype, with DecidableEq N); all quantities are real. The game PacingGame N G carries $v\ge0$ and $B>0$; infinite budgets are outside the model.
• highestOther v α i j is a Finset.sup' over the buyers $k\ne i$ and equals $0$ when there is no other buyer, not a junk value of sSup ∅.
• IsSPPE P α x p has the five conditions of Definition 2 with $\alpha_i,x_{ij}\in[0,1]$. The prices $p$ are one vector shared by the second-price and the budget conditions; they are existentially quantified in the goal.
• Smoothed game: bidders on a good are Option N, with none the reserve bidder bidding $2\epsilon$. Band weights $\max\{0,b_k-(b^*_j-\epsilon)\}$ sum to at least $\epsilon$, so the allocation never divides by zero. The price is per buyer ($p_{ij}$). The utility uses $\varphi_H(y)=y$ for $y\ge0$ and $Hy$ for $y<0$, exactly the paper's two cases.
• Theorem 2's bound $M$ is the hypothesis $\sum_jv_{ij}+2\epsilon\le M$ for every buyer.
• The limit claims assume the sequence itself converges (the paper's passage to a subsequence) and take one $M$ for all $l$. The convergences are Filter.Tendsto in $\mathbb R$ and in $\mathbb R^N$ with the product topology.

A trivializing formalization is ruled out: the full-allocation condition makes $x\equiv0$ fail whenever some $v_{ij}>0$, and the price in the budget condition is the same $p_j$ that the second-price condition pins down, so a zero price is not available to a winner facing a positive competing bid.

Needed infrastructure: a pure Nash equilibrium existence theorem for games with compact convex strategy sets and continuous, own-strategy-quasiconcave payoffs (the Proved platform theorems SocialEquilibrium.Existence.exists_equilibrium_point, Debreu 1952, and FanGlicksberg.kakutani_fan_glicksberg are the natural tools); continuity of finite maxima and quotients with positive denominators; monotonicity arguments for piecewise-linear functions of one variable; and Bolzano–Weierstrass on a bounded subset of $\mathbb R^{N\times G}$. Proofs of any milestone, and alternative routes to Theorem 1, are welcome.

Selected references

• V. Conitzer, C. Kroer, E. Sodomka, N. E. Stier-Moses, Multiplicative Pacing Equilibria in Auction Markets, Operations Research, 2022; arXiv:1706.07151v5. https://arxiv.org/abs/1706.07151
• G. Debreu, A social equilibrium existence theorem, Proc. Natl. Acad. Sci. USA 38(10), 1952. https://doi.org/10.1073/pnas.38.10.886
• I. L. Glicksberg, A further generalization of the Kakutani fixed point theorem, with application to Nash equilibrium points, Proc. Amer. Math. Soc. 3(1), 1952. https://doi.org/10.1090/S0002-9939-1952-0046638-5
• K. Fan, Fixed-point and minimax theorems in locally convex topological linear spaces, Proc. Natl. Acad. Sci. USA 38(2), 1952. https://doi.org/10.1073/pnas.38.2.121
• C. Borgs, J. Chayes, N. Immorlica, K. Jain, O. Etesami, M. Mahdian, Dynamics of bid optimization in online advertisement auctions, WWW 2007. https://doi.org/10.1145/1242572.1242644
• S. R. Balseiro, O. Besbes, G. Y. Weintraub, Repeated auctions with budgets in ad exchanges: Approximations and design, Management Science 61(4), 2015. https://doi.org/10.1287/mnsc.2014.2022
• S. R. Balseiro, Y. Gur, Learning in repeated auctions with budgets: Regret minimization and equilibrium, Management Science 65(9), 2019. https://doi.org/10.1287/mnsc.2018.3174
• S. Balseiro, A. Kim, M. Mahdian, V. Mirrokni, Budget-management strategies in repeated auctions, Operations Research, 2021. https://doi.org/10.1287/opre.2020.2073
• X. Chen, C. Kroer, R. Kumar, The complexity of pacing for second-price auctions, EC 2021; arXiv:2103.13969. https://arxiv.org/abs/2103.13969

Motivation

Firms increasingly observe enough about individual customers to charge them different prices, and regulators, platforms and sellers all ask the same quantitative question: how much more profit can personalization earn than a single posted price? The upper end of that comparison is idealized personalized pricing (first-degree price discrimination), where every customer is charged exactly their valuation. Its profit is an upper bound for every price-discrimination scheme, including feature-based pricing, so a bound on the ratio of idealized personalized profit to single-price profit bounds the value of any personalization at once.

Elmachtoub, Gupta and Hamilton (The Value of Personalized Pricing, Management Science 67(10), 2021; SSRN 3127719) give such bounds in terms of three summary statistics of the valuation distribution, all of which can be estimated from data. Their central result, Theorem 2, is a closed-form bound that is tight for every value of the statistics. The bound is exact rather than asymptotic, and it identifies the markets in which no form of price discrimination can be worth much.

A classical special case is the folklore statement that, with only the support known, the worst case is an equal-revenue (truncated Pareto) distribution. Theorem 2 refines it by also fixing the mean absolute deviation of valuations.

Setting

A seller has per-unit cost $c\ge 0$. A random customer's valuation is a random variable $V$ with law $F$, finite mean $\mu=\mathbb E[V]$, and $V\ge c$ almost surely (customers valuing the product below cost are never served profitably). The purchase probability at price $p$ is

$$\bar F(p)=\mathbb P(V\ge p),$$

which counts the customer who values the product exactly at $p$ as buying. A single price earns $(p-c)\bar F(p)$, and the single-pricing profit is

$$\mathcal R_{SP}(F,c)=\sup_{p}\,(p-c)\bar F(p).$$

Charging each customer their valuation earns the personalized-pricing profit $\mathcal R_{PP}(F,c)=\mu-c$.

The three statistics are the scale $S=\inf\{k\mid \mathbb P(V\le k)=1\}/\mu$ (the essential supremum of $V$ relative to its mean, possibly $+\infty$), the margin $M=1-c/\mu\in(0,1]$, and the coefficient of deviation $D=\mathbb E|V-\mu|/(2\mu)$. With $S_c=(S+M-1)/M$ and $W_{-1}$ the negative real branch of the Lambert $W$ function (the solution $w\le-1$ of $we^w=x$ for $x\in[-1/e,0)$), the regime thresholds are

$$\delta_L=-\frac{M\log S_c}{W_{-1}\!\big(-1/(eS_c)\big)},\qquad \delta_M=\frac{M\log S_c}{1+\log S_c},\qquad \delta_H=\frac{M(S-1)}{S+M-1}.$$

Formalization targets

Goal: Theorem 2

For every law with scale $S>1$, margin $M>0$ and coefficient of deviation $D$,

$$\frac{\mathcal R_{PP}}{\mathcal R_{SP}}\le\begin{cases}\dfrac{-W_{-1}\big((D/M-1)/e\big)}{1-D/M}, & 0\le D\le\delta_L,\\[2mm] \dfrac{M\log S_c}{D}, & \delta_L\le D\le\delta_M,\\[2mm] -W_{-1}\Big(\dfrac{-1}{eS_c(1-D/M)}\Big), & \delta_M\le D\le\delta_H,\end{cases}$$

and for unbounded support the first bound holds for every $D$. Each bound is attained: for every mean, cost, $S>1$ and $D>0$ in a regime there is a law with those statistics for which the regime's bound holds with equality. The goal is stated for a general cost and mean, not only in the standardized case.

Milestones

In the order the proof uses them:

1. Lambert $W_{-1}$ (App. A): the defining equation, $W_{-1}(-1/e)=-1$, the limit at $0^-$, and monotonicity.
2. Lemma 1: the reduction to $c=0$, $\mu=1$, with $S_c$, $M_c=1$, $D_c=D/M$.
3. The Pricing Inequality: $\bar F(x)\le\mathcal R_{SP}(F,0)/x$ for $x>0$.
4. Lemma 3: $D=\int_M^{S+M-1}\bar F(\mu x+c)\,dx=\int_0^M\big(1-\bar F(\mu x+c)\big)\,dx$.
5. Lemma 2: $0\le D\le\delta_H$ and $0\le\delta_L\le\delta_M\le\delta_H$.
6. Eqs. (EC.5), (EC.6) and Lemma EC.1: the three standardized bounds.
7. Lemma EC.2: each regime's bound is the strongest of the three.
8. Lemma EC.3: the explicit tight distributions.

Significance

The theorem turns three estimable numbers into a guarantee. Its reciprocal is the fraction of the personalized-pricing profit that the best single price is certain to earn. When that fraction is close to one (small $D$, or $D$ close to its maximum $\delta_H$), no price-discrimination strategy, however refined its data, can improve much on one price. The paper uses Theorem 2 to bound feature-based pricing (its Theorems 4 and 5), and the tight distributions show that no better bound in these statistics exists.

The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. A complete development yields a formal treatment of single-price revenue for general valuation laws (atoms and unbounded support included), the integral representations of mean absolute deviation, and a usable negative Lambert branch, which neither Mathlib nor the platform currently provides (only the principal branch $W_0$ exists on the platform).

Difficulty

The upper bounds rest on bounding the purchase probability pointwise inside an integral representation of $D$ and solving the resulting transcendental inequality through $W_{-1}$. Each step is elementary on paper, but the formal statement has no slack. $\mathcal R_{SP}$ is a supremum that need not be attained when support is unbounded. $\bar F$ counts atoms, so the tight laws sit on atoms at their optimal prices. Every application of $W_{-1}$ must stay in $[-1/e,0)$, and the regimes meet at their endpoints, where two bounds coincide.

Tightness is the harder half. It needs genuine probability measures with prescribed cCDFs, mean, scale and deviation, and an exact computation of their single-price profit. Two printed details had to be corrected, and those corrections must be respected. At $D=0$ no law has scale $S>1$, so tightness is stated for $D>0$. The high-heterogeneity cCDF of Lemma EC.3 must be left-continuous at $S$, so it keeps an atom at the top of the support.

Formalization scope

All declarations live in the namespace ValuePersPricing.Deviation.

• Laws and standing assumptions. A valuation law is a measure ν : Measure ℝ. Market ν c bundles the standing assumptions: probability measure, $0\le c$, $V\ge c$ almost surely, and integrability of $v$. The margin condition $M>0$ is the hypothesis c < mean ν.
• Profits. $\bar F(p)$ is (ν (Ici p)).toReal. $\mathcal R_{SP}$ is the real supremum over all real prices; it is not assumed attained, bounded by an extra hypothesis, or positive. Under Market the profits are bounded by $\mu-c$, so the supremum is the true one.
• Scale. The scale is the predicate IsScale ν S: $S\mu$ is the essential supremum. Unbounded ν is the case $S=\infty$.
• Ratios. Every ratio bound is stated multiplicatively, $\mathcal R_{PP}\le B\,\mathcal R_{SP}$, and tightness as $\mathcal R_{PP}=B\,\mathcal R_{SP}$. A quotient with a zero denominator would make the bound trivially true, and the product form rules this out.
• Lambert branch. lambertWm1 is defined by choice, with a junk value off $[-1/e,0)$ that no statement reaches.
• Standardized lemmas. Lemmas EC.1–EC.3 and Eqs. (EC.5), (EC.6) are stated for $c=0$, $\mu=1$, as in the paper. The goal is stated for general $(\mu,c)$, and the regime thresholds and bounds are written in $(S,M,D)$ exactly as printed.

A complete development needs the layer-cake (tail-integral) formula for expectations, the change of variables in interval integrals, pushforwards of measures under affine maps, and analytic facts about $x\mapsto xe^x$ on $(-\infty,-1]$. The Lambert $W_{-1}$ facts and the tail-integral representations of mean absolute deviation are reusable beyond this mission. Contributions are welcome at every milestone. In particular, the $W_{-1}$ milestone and Lemma 3 are independent entry points, and the explicit measures of Lemma EC.3 can be built without the upper-bound half.

Selected references

• A. N. Elmachtoub, V. Gupta, M. L. Hamilton, The Value of Personalized Pricing, Management Science 67(10), 2021. SSRN review version: https://ssrn.com/abstract=3127719
• R. M. Corless, G. H. Gonnet, D. E. G. Hare, D. J. Jeffrey, D. E. Knuth, On the Lambert W function, Advances in Computational Mathematics 5, 1996. https://doi.org/10.1007/BF02124750
• J. D. Hartline, V. Mirrokni, M. Sundararajan, Optimal marketing strategies over social networks, WWW 2008. https://doi.org/10.1145/1367497.1367524
• R. E. Barlow, A. W. Marshall, F. Proschan, Properties of probability distributions with monotone hazard rate, Annals of Mathematical Statistics 34(2), 1963. https://doi.org/10.1214/aoms/1177704142