All missions

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

Motivation

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

Setting

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

Target

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

Significance

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

Difficulty

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

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

Formalization scope

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

Selected references

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

The claim

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

What is proved

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

What this rests on and what it does not say

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

The claim

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

What is proved

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

What this rests on and what it does not say

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

The claim

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

What is proved

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

What this rests on and what it does not say

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

The claim

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

What is proved

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

What this rests on and what it does not say

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

The claim

A Lightning commitment transaction carries one output per in-flight payment: an offered HTLC (the local node pays if the remote reveals the preimage, or recovers the funds after the timeout) or a received HTLC (the local node claims with the preimage before expiry, else the remote takes the funds back). BOLT #3 gives each a witness script with three branches (revocation, preimage, timeout), and the channel's security rests on those three being the only ways to spend. The to_local mission proved this for the balance output; this mission proves it for both HTLC scripts, against the script interpreter as transcribed from Bitcoin Core.

What is proved

• The opcodes (cltv_step, multisig_two): OP_CHECKLOCKTIMEVERIFY passes exactly under CltvPasses; a 2-of-2 OP_CHECKMULTISIG passes iff each signature verifies for its key in order.
• Each path in closed form (offered_revocation, offered_preimage, offered_timeout, received_revocation, received_success, received_timeout): on the BOLT #3 witness shapes the interpreter leaves exactly the expected check, including the NULLDUMMY condition on the multisig dummy.
• The spending conditions, for any witness (offered_spends_iff, received_spends_iff): over an arbitrary stack, the witness-v0 success condition holds iff one of the three paths' conditions holds. Two facts the interpreter forces that the BOLT text leaves implicit: the inner selector is "is the top element 32 bytes long", not "is it empty"; and every non-revocation path requires the top element not to hash to the revocation hash, because OP_DUP OP_HASH160 … OP_EQUAL hashes whatever is on top.
• The outputs under VerifyScript (parseScript_offered, parseScript_received, offered_p2wsh_spend, received_p2wsh_spend, the goal): the byte forms parse as intended, and the pay-to-witness-script-hash outputs are spent exactly by the three paths, with the spending transaction's own signature checker and lock-time check.
• The lock time (cltv_concrete, checkLockTime_iff): with the CLTV flag active the check is Core's CheckLockTime, which for a block-height expiry is "nLockTime is a height at least the expiry and the input is not final".

What this rests on and what it does not say

The two 20-byte hashes are parameters, not tied to any key or preimage; signature checks stay at the level of the signature mission's checker. The HTLC-success and HTLC-timeout transactions themselves (second-stage, with their own to_local-style scripts) and the anchor-output variants of the scripts are not modelled, nor is the protocol-level argument about who holds which key when. (BOLT #3, interpreter.cpp)

The claim

A Lightning commitment transaction pays the local node's balance to a to_local output whose witness script (BOLT #3) reads

OP_IF <revocationpubkey> OP_ELSE <to_self_delay> OP_CHECKSEQUENCEVERIFY OP_DROP <local_delayedpubkey> OP_ENDIF OP_CHECKSIG

The channel's security rests on two claims about this script: the counterparty can spend it at any time with the revocation key, and the local node can spend it with its delayed key only after to_self_delay blocks, and nobody can spend it any other way. This mission proves both, and the "no other way", against the script interpreter as the script, signature and verification missions transcribed it from Bitcoin Core.

What is proved

• The interpreter run (eval_cons, csv_step, serialize_length): the script on any stack b :: tl of admissible size fails unless tl is a single element, and otherwise leaves the result of the selected signature check; the OP_CHECKSEQUENCEVERIFY step passes exactly under CsvPasses.
• The spending conditions (spends_iff): for any stack whatsoever, the witness-v0 success condition (one element left, and true) holds iff the stack is [b, sig] and either b is true and sig verifies for the revocation key, or b is false, the sequence check passes, and sig verifies for the delayed key.
• The output (parseScript_toLocal, p2wsh_spend, the goal): the byte form of the script parses as intended, and VerifyScript accepts a witness for the pay-to-witness-script-hash output exactly when the witness is [sig, b, script] and the selected branch's conditions hold for the spending transaction's own signature checker and sequence check.
• The delay (csv_concrete, checkSequence_iff, lightning_delay): with the CHECKSEQUENCEVERIFY flag active, the sequence check is Core's CheckSequence, which for a 16-bit delay and a flag-free nSequence (as Lightning sets it) is exactly "version ≥ 2 and nSequence ≥ to_self_delay".

What this rests on and what it does not say

The signature checks are the signature mission's checkSigPreTapscript with the witness-v0 sighash; nothing here says who holds the keys or how they are derived (BOLT #3's key derivation and the revocation secret are outside the script). The P2WSH program must be a true value, which VerifyScript requires of every witness program and which is a fact about one SHA-256 output the model cannot evaluate symbolically. MINIMALIF is policy, so under consensus any true selector opens the revocation branch; the relative lock time itself (whether the spending transaction may enter a block) is the block mission's BIP68 check, not the script's. (BOLT #3, interpreter.cpp)

The claim

"Bitcoin is secure as long as honest miners hold the majority of the hashrate" is the informal reading of Garay, Kiayias and Leonardos's backbone analysis: in a synchronous network, if the adversary finds fewer blocks than there are uniquely successful honest rounds over every long enough window, then honest chains grow (chain growth), agree on all but their last blocks (common prefix), and contain honest blocks regularly (chain quality). This mission states the synchronous model and proves these three properties from that combinatorial hypothesis.

What is proved

• The model: executions with honest parties, a rushing adversary, maxvalid adoption, and valid chains in which every block sits on exactly the chain its creator extended (the hash-chain abstraction).
• Chain growth (chain_growth, chain_growth_self): between rounds $r$ and $s$ every honest chain grows by at least the number of successful rounds in between.
• Common prefix (uniquely_successful_height, common_prefix_private, common_prefix_rounds, common_prefix, the goal): a uniquely successful round pins the honest block at its height; a private fork that stays adversarial for a window loses; hence the chains of any two honest parties agree once the last $2λ$ blocks are dropped.
• Chain quality (chain_quality): any $λ$ consecutive blocks of an honest chain contain an honest block.
• The bridge to Core (chainWork_const_bits): at constant difficulty the block mission's chainWork is the block count times one block's proof, so "longest" and "most work" coincide in this regime.

What this rests on and what it does not say

Nothing probabilistic is proved: Typical (adversarial blocks in every window of length $≥ λ$ strictly fewer than the uniquely successful rounds strictly inside it) is assumed, where the paper derives it from Chernoff bounds and honest majority. The constants are $k = 2λ$ and $ℓ = λ$ rather than the paper's $2λf$; only the weak form of chain quality is proved. The model is synchronous with one honest block per party per round, no explicit message layer, and static difficulty. (ePrint 2014/765)

Motivation

Philippe Flajolet and Robert Sedgewick's Analytic Combinatorics is the standard reference for counting discrete structures exactly and asymptotically. Its methods are used throughout the analysis of algorithms, random structures and enumerative combinatorics. This mission collects formally verified versions of the book's chapter-level results in one connected development.

Setting

A combinatorial class is a set of objects with a size such that each size has finitely many objects. Its generating function records how many objects have each size: the ordinary generating function $C(z)=\sum_n c_n z^n$ for unlabelled classes and the exponential generating function $\sum_n c_n z^n/n!$ for labelled ones. The symbolic method translates constructions on classes (disjoint union, product, sequence, set, cycle, pointing) into equations between generating functions. For example, if a class has counting series $C(z)$ and no size-zero objects, the series $S(z)$ for ordered sequences of its objects satisfies

$$S(z)\,(1-C(z))=1.$$

Lagrange inversion recovers the coefficients of implicitly defined series. Singularity analysis and the saddle-point method turn the analytic behaviour of a generating function into asymptotic estimates for its coefficients, and the same machinery gives limit laws for parameters of random structures.

Formalization targets

Goal

The goal is the ordered-sequence identity above for a class with finitely many objects of each size and none of size zero, stated for formal power series over $\mathbb Q$. The sequence class includes the empty sequence of size zero.

Milestones

The 132 milestones are the remaining results, listed in the order of the book's chapters. Counts per chapter, goal included:

Book chapter	Topic	Results
I	Ordinary generating functions, the symbolic method, Pólya enumeration, Lagrange inversion	21
II	Exponential generating functions, labelled structures, random mappings	15
III	Bivariate generating functions, moments and variance of parameters	7
IV and VI	Complex analysis, coefficient transfer and singularity analysis	10
V	Rational and meromorphic functions, continued fractions	8
VII	Applications of singularity analysis to trees and lattice-path classes	16
VIII	Saddle-point estimates and integer-partition asymptotics	50
IX	Limit laws for parameters of random structures	6

The total is 133 results.

Significance

The results are classical; the book proves them. This mission adds machine-checked proofs: every listed result has a Lean 4 proof accepted on the platform against a fixed Mathlib revision. Formalizing them pins down hypotheses that informal statements leave implicit: which objects a series counts, which convergence and nonvanishing conditions an estimate needs, and which limits are taken.

Difficulty

Informal treatments identify a generating function with "the" counting sequence of a construction; a formal statement must fix the finite type of objects being counted and the exact construction, so the symbolic-method results here are stated against explicit finite object types. Analytic estimates cannot be read off formal series: they need the analyticity domain, the behaviour near the dominant singularity and explicit error terms. Several saddle-point estimates require uniform local and tail bounds that informal arguments state only loosely; where the source assumes such bounds, the statements here keep them as hypotheses.

Formalization scope

Formal power-series identities are stated coefficientwise and do not require analytic convergence. Analytic estimates and probability limits keep their convergence, nonvanishing, parameter and measurability conditions. Results that the source proves under explicit assumptions remain conditional on those assumptions. Some results import supporting lemmas that are proved as separate theorems of the mission.

The mission covers 133 chapter-level results of the source development. It does not claim that every theorem of the book is formalized; coverage is exactly the verified declarations in the mission. Further results, sharper variants and alternative proofs are welcome as additional theorems.

Selected references

• Philippe Flajolet and Robert Sedgewick, Analytic Combinatorics, Cambridge University Press, 2009. Author-hosted book.
• AnalyticCombinatorics source repository, the immutable source revision formalized here.

Motivation

Atlases I–IV certified four-dimensional vacuum and Einstein–Maxwell metrics on a registered coordinate definition layer. Atlas VI extends the certificate notion to total dimension $5=4+1$ and asks two concrete questions: inside one explicit static ansatz, exactly when is the five-dimensional Einstein–Maxwell certificate satisfied; and for the cohomogeneity-one equal-spin ansatz, is the full system of field equations equivalent to a finite set of radial equations.

Setting

Total dimension $5$, signature $(-,+,+,+,+)$, $\Lambda=0$, coupling $G_{ab}=2S_{ab}$ with $E_{ab}=R_{ab}-\tfrac12 g_{ab}R-2S_{ab}$. VI-01: $g=-f\,dv^2+2\,dv\,dr+r^2[du^2/(4u(1-u))+u\,d\varphi^2+(1-u)\,d\psi^2]$, $f=1-\mu/r^2+\beta/r^4$, $A=-Q/(2r^2)\,dv$, on $\{r>0,\ 0<u<1\}$ for all real $\mu,\beta,Q$. VI-02: $g=-B\,dt^2+D\,dr^2+A[du^2/(4u(1-u))+u(1-u)(d\varphi-d\psi)^2]+H(\sigma-W\,dt)^2$, $\sigma=u\,d\varphi+(1-u)\,d\psi$, $\mathcal A=\Phi\,dt+\Psi\,\sigma$, $F=d\mathcal A$, radial data $C^\infty$ on an open $R$ with $B,D,A,H\neq0$ (ESData).

Formalization targets

• Goal: under ESData, $R\neq\emptyset$ and $A>0$, $H>0$, $BD>0$ on $R$, the Einstein–Maxwell certificate on $\{x_1\in R,\ 0<u<1\}$ holds iff the five reduced Einstein and two reduced Maxwell radial equations hold on $R$.
• VI-01: certificate iff $3\beta=Q^2$; Ricci-flat certificate iff $\beta=0$; explicit counterexample at $(1,1,1)$.
• VI-02: pointwise completeness of the seven reduced equations; fixed certified instances MP01 (VacuumCertificate, and EMCertificateD with $F=0$), MP02 (EMCertificateD with $F=0$ only, via the reduced system; no VacuumCertificate statement) and ST03 (static charged EMCertificateD); refutations NW01 ($\neg$ VacuumCertificate) and NQ14 ($\neg$ EMCertificateD).

Significance

A machine-checked reduction of a five-dimensional Einstein–Maxwell system to seven radial equations, with explicit domains and hypotheses, usable as a certificate checker for equal-spin candidates; the VI-01 criterion derives the charge normalisation.

Difficulty

All curvature data are explicit closed forms generated as CAS hints and re-proved in Lean component by component (Christoffel, derivative, Ricci and Einstein–Maxwell tables); the reduction needs frame reconstruction lemmas for every residual component.

Formalization scope (what is NOT claimed)

• EF5 is one fixed explicit static ansatz (f = 1 − μ/r² + β/r⁴, A = −Q/(2r²) dv); cert_iff (3β = Q²) is a criterion inside that ansatz, not a classification of five-dimensional black holes.
• EF5.vacuum_cert and EF5.vacuum_cert_iff conclude EMCertificateD with F = faraday5 0 (= 0); the literal VacuumCertificate (Ricci-flat) iff is EF5.vacuumCertificate_iff.
• ESData asks only: R open, the seven radial functions C^∞ on R, and B, D, A, H nonvanishing on R — no field equation. The Goal additionally assumes R.Nonempty and A > 0, H > 0, B·D > 0 on R. No B > 0, D > 0, connectedness, exterior-only or q ≠ 0 hypothesis is assumed or claimed.
• ReducedSystem consists of FIVE Einstein (redE_tt, redE_tσ, redE_rr, redE_uu, redE_σσ) and TWO Maxwell (redJ_t, redJ_σ) radial equations; F = d𝒜 by definition supplies closedness. It is not the VI-03 six-state CAS system.
• MP01 and MP02 are two specified certified parameter instances (μ = 3, a = 1/2 and μ = 5 with rotation constant −2/3), not a certified arbitrary-parameter Myers–Perry theorem. ST03 is one fixed static charged instance (μ = 2, Q = 1, β = 1/3).
• Each candidate domain is exactly esDomain {r | 0 < r ∧ rX r ≠ 0} with the listed exclusion polynomial rX; no horizon or axis (u ∈ {0,1}) regularity is claimed.
• NW01 refutes VacuumCertificate (¬ Ricci-flat certificate); NQ14 refutes EMCertificateD. They are ordinary theorems with negated conclusions, not disproofs of positive targets.
• B3 coordinate certificates on the registered local layer (PHYSICS_BOUNDARY §N, §O), not Mathlib-only or manifold results. No new exact charged-rotating solution, global event horizon, uniqueness, gauge equivalence or static ↔ EF coordinate bridge is claimed.
• Supplementary Python/CAS/search evidence (VI-01 per-run instances, PS00/PS02 pilot replays, VI-03 CAS) is outside this release and is not a formally verified search algorithm. EF5/Certificate.lean conditional assemblers are excluded.

Selected references

• R. C. Myers, M. J. Perry, Ann. Phys. 172 (1986) 304 — family name of MP01/MP02/NW01 (not accessed; see LITERATURE_CHECK.md).
• F. R. Tangherlini, Nuovo Cimento 27 (1963) 636 — family name of EF5/ST03 (not accessed; normalisation derived in Lean).
• Exact Vacuum / Spacetime Atlas I, II, IV (the author's earlier releases; bundles and nodes reused unchanged).

The claim

A transaction's identifier is the hash of its serialization without witnesses, and that serialization still contains every scriptSig. Before SegWit, anyone could take a valid transaction, re-encode a signature inside a scriptSig (a different DER length byte, a negated S value, an extra push), and broadcast a transaction that was equally valid and had a different txid. Any protocol that referred to an unconfirmed transaction by its txid — a refund signed against a funding transaction, which is how payment channels start — could be broken this way. BIP141 fixed it by moving signatures into the witness, which the txid does not hash, and by requiring the scriptSig of a native witness spend to be empty.

This mission proves that the fix does what it claims, against the published VerifyScript and CheckInputScripts: for a transaction whose inputs spend native witness programs and whose scripts verify, the txid is a function of the sender's intent — version, prevouts, sequence numbers, outputs, lock time — and of nothing else.

What is proved

• native_scriptSig_empty — under CheckInputScripts with WITNESS, every input spending a native witness program has an empty scriptSig (SCRIPT_ERR_WITNESS_MALLEATED, lifted from the VerifyScript mission's native_witness_malleated).
• txid_of_intent — for such a transaction, txid tx = txid (ofIntent (intentOf tx)): the identifier of the canonical transaction with empty scriptSigs and witnesses.
• txid_determined (goal) — two transactions with the same intent, both verifying against the same ledger, with native witness-program inputs, have the same txid.
• p2sh_wrapped_scriptSig — for a P2SH output spent with witness data, VerifyScript succeeds only if the scriptSig is exactly the single push of the witness program it evaluates to (SCRIPT_ERR_WITNESS_MALLEATED_P2SH); the scriptSig of a wrapped spend is determined by the redeem script.

What this rests on

The serialization mission's txid_strip (the txid ignores witnesses), the VerifyScript mission's native_witness_malleated, and the block mission's CheckInputScripts. The statements are about the executable VerifyScript; no assumption about hash functions or signatures is needed, because the theorems say nothing about whether a valid spend exists, only that its identifier is fixed once it does. (interpreter.cpp, transaction.h, BIP141)

The claim

"There will only ever be 21 million bitcoin" is the most repeated statement about the system, and it is usually justified by the subsidy schedule alone: fifty coins, halved every 210,000 blocks, summing to just under 21 million. The schedule is proved in the subsidy mission (BitcoinSubsidy.issuance_total). But the schedule is a bound on what a coinbase may create; whether the chain's spendable supply stays within it depends on the whole validation path — that every non-coinbase transaction spends at least what it creates, that no input is spent twice, that the coinbase is bounded by the subsidy plus the fees actually collected, and that these checks run against the right ledger at every step. The inflation bug CVE-2018-17144 was a failure of exactly this composition, not of the schedule.

This mission states the bound as a property of every chain state reachable from the genesis under the block mission's validate, and proves it.

What is proved

With totalValue u the sum of the values of the coins of a ledger and issued n the subsidy GetBlockSubsidy has issued to a chain of n blocks:

• update_bound — UpdateCoins raises the total by at most the value created and lowers it by the value spent (ledger arithmetic on a distinct-key ledger).
• values_in_range — every coin of a reachable state has a value in [0, MAX_MONEY], because coins only enter as outputs that passed CheckTransaction.
• block_supply — one accepted block raises the total by at most GetBlockSubsidy(height): the coinbase bound of ConnectBlock against the fees, through the acceptance theorem and ApplySpec of the block mission.
• supply_bound (goal) — on every reachable state, totalValue S.utxo + genesisSubsidy ≤ issued S.nextHeight.
• supply_lt_maxMoney — hence totalValue S.utxo < MAX_MONEY on every reachable state.

The genesis subsidy appears on the left because the source never adds the genesis coinbase to the UTXO set (ConnectBlock's genesis shortcut), so it is issued but unspendable; the inequality is exact at the genesis state.

What this rests on

The block mission's acceptance (the executable validation accepts iff the declarative specification holds), apply_spec (the resulting state is ApplySpec), reachable_wellFormed (distinct ledger keys), and the subsidy mission's core_eq_spec and issuance_bound. Nothing about the rules is re-transcribed here; the mission adds the quantities and the induction. (validation.cpp, tx_verify.cpp, coins.cpp)

Why the script interpreter is the heart of consensus

Every Bitcoin transaction input is authorized by running a small stack program: the input's scriptSig followed by the spent output's scriptPubKey, on the same stack, and the spend is valid when the program leaves a true value on top. Nearly every historical consensus failure in Bitcoin touched this interpreter — the disabled opcodes (CVE-2010-5137), the concatenation bug that let any output be spent (CVE-2010-5141), the overflow in numeric opcodes that prompted the four-byte limit, the CHECKMULTISIG off-by-one that consumes an extra element. Bitcoin Core's EvalScript is 800 lines of C++ with a switch over a hundred opcodes, and VerifyScript wraps it with the pay-to-script-hash and witness-program rules. (interpreter.cpp, script.h)

This mission transcribes the legacy execution path (SigVersion::BASE) — the number representation CScriptNum, the truth test CastToBool, the full non-push opcode table of EvalScript with its resource limits, and VerifyScript for output scripts that are neither pay-to-script-hash nor witness programs — and proves the properties the rest of validation relies on: that script numbers round-trip and are minimal, that truth is "nonzero as a number", that the resource limits and the disabled-opcode rule behave as stated, and that the two classic payment templates do exactly what they are meant to.

Numbers, truth, and the machine

A byte is an 8-bit word and a stack element is a list of bytes. A script number is a little-endian magnitude whose last byte's top bit is the sign: $\mathrm{setVch}(v)$ reads it, $\mathrm{serialize}(n)$ writes the shortest such encoding (appending a sign byte when the magnitude's top bit is already set), and the CScriptNum constructor rejects encodings longer than four bytes (five for the lock-time opcodes) and, under MINIMALDATA, non-minimal ones. $\mathrm{castToBool}(v)$ is true when some byte is nonzero, except that a negative zero (0x80 after zero bytes) is false.

A script is the sequence of instructions GetOp yields: a data push carrying its bytes, or a non-push opcode. The interpreter's state is the main stack, the alt stack, the condition stack vfExec, and nOpCount; stacks are lists with the top first. One step on a push checks the 520-byte element limit and pushes when all conditions are true; on an opcode it counts it against the 201-operation limit (only opcodes above OP_16 count, as in the source: OP_1NEGATE, OP_RESERVED and the small-integer pushes are exempt), rejects the fifteen disabled opcodes regardless of execution state, and when executing (or for IF/NOTIF/ELSE/ENDIF always) runs the opcode's case — pushes of small integers, flow control, the stack-manipulation family, EQUAL, the numeric family on four-byte operands, WITHIN, the hash opcodes, CODESEPARATOR, CHECKSIG, CHECKMULTISIG with its key-count accounting, the NOPs, and CHECKLOCKTIMEVERIFY/CHECKSEQUENCEVERIFY when their flags are set — then checks the 1000-element stack limit. Hashes, the lock-time checks, and the signature check (with its encoding rules and FindAndDelete) are an abstract oracle, exactly the role of BaseSignatureChecker and the hash primitives in the source. Running a script steps through it and fails on an unbalanced conditional; verifying evaluates scriptSig then scriptPubKey and requires a non-empty stack with a true top.

Formalization targets

Goal — pay-to-public-key-hash does what it says

$$\mathrm{verifyScriptPlain}\big([\langle sig\rangle, \langle pk\rangle],\ \mathtt{DUP\ HASH160}\ \langle h\rangle\ \mathtt{EQUALVERIFY\ CHECKSIG}\big) = \mathtt{true} \iff \mathrm{hash160}(pk) = h \;\wedge\; \mathrm{checkSig}(sig, pk) = \mathrm{some}\ \mathtt{true},$$

for all signatures, keys and hashes within the 520-byte element limit, every flag setting and every oracle. This is BitcoinScript.p2pkh_correct: the template that carries most of Bitcoin's history is correct against the transcribed interpreter, in both directions, with the signature check and hash left abstract. It is the weakest stable statement, since it fixes nothing about the oracle.

Supporting milestones

1. Round-trip (serialize_roundtrip): $\mathrm{setVch}(\mathrm{serialize}(n)) = n$ for every integer.
2. Minimality (serialize_minimal): the serializer's output always passes the minimal-encoding test; (toNum_serialize): a serialized number of at most four bytes is accepted by the strict constructor and reads back as itself.
3. Truth is nonzero (castToBool_iff): $\mathrm{castToBool}(v) \iff \mathrm{setVch}(v) \ne 0$, for every byte string, including both encodings of zero.
4. Pushes (eval_pushes): a push-only script within the element and stack limits leaves exactly its pushes, top-first.
5. Disabled opcodes (disabled_fails): a script containing any of the fifteen disabled opcodes fails from every state, executed or not.
6. Operation limit (op_count_fails): a script with more than 201 counted opcodes (non-push opcodes above OP_16) never succeeds.
7. Pay-to-public-key (p2pk_correct): $\langle sig\rangle$ against $\langle pk\rangle\ \mathtt{CHECKSIG}$ succeeds iff the oracle accepts the signature.

What the result establishes

The goal and milestones give kernel-checked semantics for the pieces of the legacy interpreter that every later layer consumes. The number theorems fix what CScriptNum means on the wire and show the interpreter's own outputs are always minimal — which is why MINIMALDATA can be a policy rule. The truth theorem is what makes VERIFY, IF and the final check well-defined on arbitrary byte strings. The limit and disabled-opcode theorems are the denial-of-service and CVE-2010-5137 defences, stated as universal properties of the transcription rather than of test cases. And the template theorems are the first end-to-end statements that a real Bitcoin spending condition is enforced by the code, modulo the cryptography.

What is deliberately abstract: hash functions, the signature check with its DER/strict-encoding rules and FindAndDelete, and the lock-time checks. These are oracle fields, so every theorem holds for every oracle; instantiating them is the work of the hash, sighash and signature layers. Not modeled: byte-level script parsing (GetOp, MAX_SCRIPT_SIZE), pay-to-script-hash and witness programs in VerifyScript, SegWit v0 and Tapscript execution, and the policy flags (MINIMALDATA, NULLFAIL, CONST_SCRIPTCODE, DISCOURAGE_UPGRADABLE_NOPS, MINIMALIF), which are fixed to off as in block validation.

Status: all statements are open with intentional placeholder proofs. The opcode table has been checked by evaluation against the source's documented stack effects (x1 x2 x3 -- x2 x3 x1 and the like) and the CVE-2010-5137 and limit behaviours; nothing about compiled Bitcoin Core is claimed.

Where the obvious argument fails

The number round-trip looks like bookkeeping until the sign byte: when the magnitude's top byte already has bit 7 set, the serializer appends a whole byte for the sign, and the reader must then see a cleared top bit on that extra byte while the magnitude is unchanged. The proof splits on this case and on the sign, and needs the precise effect of |= 0x80 and & 0x7f on bytes below 128. Minimality has the matching trap: the serializer never emits a trailing zero magnitude byte, which is what makes its output pass the test.

For the templates, the naive approach is to compute. It works, but only after the interpreter's resource checks are discharged on every step — the element size on each push, the op count on each opcode, the stack size after each step — which is why the template theorems carry element-size hypotheses and why the push lemma is stated with its limits. For the op-count theorem the trap is CHECKMULTISIG, which adds its key count to nOpCount mid-execution; the invariant has to allow that increase while keeping it under the limit.

Formalization scope

Bytes are BitVec 8; numbers are Int with natAbs for the magnitude; bit tests are the source's masks (& 0x80, & 0x7f, | 0x80) read through toNat. Stacks are Lists, top first; the stacktop(-k) indexing of the source becomes position $k-1$. Scripts are List Instr. execOp is one if-chain mirroring the switch; step performs the per-iteration checks in the source's order; run is the loop plus the final conditional check; evalScript returns the main stack. Flags carries CHECKLOCKTIMEVERIFY, CHECKSEQUENCEVERIFY and NULLDUMMY; fRequireMinimal is false. The oracle's checkSig returns none where an encoding check fails the whole script and some b for the signature verdict.

A trivializing formalization would define verifyScriptPlain on the two templates directly, or let the oracle see the script; the interpreter is the full opcode table and the oracle sees only the stack elements it is handed. Restricting the templates to canonical sizes beyond the 520-byte limit is out of scope.

No Mathlib is required; the development imports only Std. Proofs in any order are welcome; lemmas about individual opcodes' stack effects are reusable for every later script theorem.

Selected references

• Bitcoin Core contributors. EvalScript, VerifyScript, CastToBool, EvalChecksigPreTapscript, src/script/interpreter.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source
• Bitcoin Core contributors. CScriptNum, opcode table, MAX_SCRIPT_ELEMENT_SIZE, MAX_OPS_PER_SCRIPT, MAX_STACK_SIZE, MAX_PUBKEYS_PER_MULTISIG, src/script/script.h, and GetScriptOp, src/script/script.cpp, same revision. Source
• Pieter Wuille. BIP62: Dealing with malleability (rules 3–6, minimal data and numbers), 2014. Specification
• Satoshi Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System, 2008, section 2. Paper

Why the header clock matters

Bitcoin has no trusted clock. A block's timestamp is chosen by its miner, so the consensus rules constrain it from two sides: it must exceed the median time past of the previous eleven blocks (time-too-old), and it must not run more than two hours ahead of the validating node's own clock (time-too-new). The median, rather than the previous block's time, is what makes the rule robust to a few manipulated timestamps, and since BIP113 the same median is the clock against which time-based lock-times are evaluated. The remaining contextual header rules fix the required difficulty bits and refuse block versions that predate the BIP34, BIP66 and BIP65 soft forks once those are active. (GetMedianTimePast, ContextualCheckBlockHeader, CMainParams)

One property of this design is used everywhere but stated nowhere in the code: along any chain that obeys time-too-old, the median time past never decreases. It is what makes a time-based lock, once satisfied, stay satisfied. This mission transcribes the median and the contextual rules and proves that property.

The median, the window, and the rules

A chain of ancestors is represented by the list of its block times, most recent first. The window is the first eleven entries (nMedianTimeSpan), or all of them for a shorter chain. The median time past sorts the window and takes the element at index $\lfloor |w| / 2 \rfloor$; for an even-length window this is the upper of the two middle elements, as the source's pbegin[(pend - pbegin) / 2]. For an empty chain the model returns $0$, a case the source never queries.

A header carries a version, a time and nBits. For a buried deployment, DeploymentActiveAfter(prev) holds when $\mathrm{prev.height} + 1$ reaches the activation height: $227{,}931$ for BIP34, $363{,}725$ for BIP66, $388{,}381$ for BIP65. The version floor rejects a version below 2, 3 or 4 when the corresponding deployment is active. The contextual check of a header against its predecessor requires: nBits equals the required work (supplied by the caller, as GetNextWorkRequired computes it in the proof-of-work development); the time strictly exceeds the predecessor's median time past; the time is at most the local clock plus $7{,}200$ seconds; and the version is not outdated. Mainnet has enforce_BIP94 = false, so the testnet timewarp rule is absent.

Formalization targets

Goal — median time past is non-decreasing along a valid chain

For a chain of block times $t_0, t_1, \dots$ (most recent first) in which every block satisfies time-too-old against its predecessor — $\mathrm{MTP}(t_{i+1}, t_{i+2}, \dots) < t_i$ for every $i$ — the median time past of every suffix is at most that of every shorter suffix:

$$i \le j \;\Longrightarrow\; \mathrm{MTP}(\text{drop}_j) \le \mathrm{MTP}(\text{drop}_i).$$

This is BitcoinHeader.mtp_mono_chain. It is the clock-monotonicity that BIP113 and BIP68 time locks rely on.

Supporting milestones

1. Window membership (mtp_mem_window, mtp_mem): for a non-empty chain the median is one of the window's times, hence one of the chain's.
2. Bounds (mtp_bounds): the median lies between any lower and upper bound of the window.
3. Only eleven matter (mtp_take): the median of a chain equals the median of its first eleven times.
4. One step (mtp_mono): if $\mathrm{MTP}(c) < t$ then $\mathrm{MTP}(c) \le \mathrm{MTP}(t :: c)$. The heart of the goal, by a counting argument on the sorted window.
5. Version floor (versionOutdated_iff): the rejection condition as a disjunction of height thresholds.
6. The contextual check (contextualCheck_iff): acceptance as a conjunction of the four rules.
7. Floors after activation (version_floor): an accepted header has version at least 2, 3, 4 after the respective heights.

What the result establishes

The goal is a kernel-checked statement about the transcribed median: appending blocks that pass time-too-old can only move the median forward. Together with the characterization of the contextual check it gives the exact semantics of Bitcoin's block clock: bounded from below by a non-decreasing median, from above by local time plus two hours.

Formalizing adds the general proof of a fact usually argued by example. The argument is a counting one: the median of a window of $n$ sorted times is the smallest value with at least $n - \lfloor n/2 \rfloor$ window elements at or above it; appending a time above the old median and dropping at most one old element keeps that count high enough, including when the window is still growing in the first ten blocks of a chain.

Not in scope, and stated as such: the computation of the required nBits (the proof-of-work mission), the local-clock model behind NodeClock::now(), checkpoints, minimum chain work, and the CheckBlockHeader proof-of-work test itself. Status: all statements are open with intentional placeholder proofs.

Where the obvious argument fails

The naive argument — "the new time is larger than the median, so the median cannot fall" — overlooks that the window also loses its oldest element, which may have been one of the elements above the median. The proof must show that losing one such element and gaining one keeps at least $n - \lfloor n/2 \rfloor$ elements at or above the old median. A second subtlety is the growing window: for the first ten blocks the window length increases by one and the median index may move, so the count required changes from $n - \lfloor n/2 \rfloor$ to $(n+1) - \lfloor (n+1)/2 \rfloor$; the two cases are not the same inequality. The even-length convention (upper middle) is what makes the bookkeeping close.

Formalization scope

Times are Int, as int64_t block times. The window is List.take 11, the sort is List.mergeSort on ≤, and the median is getD (length / 2) 0. The required nBits is a parameter of the check. Heights are Nat. enforce_BIP94, checkpoints and minimum chain work are not modeled.

A trivializing formalization would define the median as the previous block's time, or sort with a different index convention; the definitions follow the source's sort-and-index. Assuming the chain's times are themselves sorted is ruled out: the goal assumes only the time-too-old rule.

No Mathlib is required; the development imports only Std. The counting lemmas on sorted lists are reusable for any later median-based rule.

Selected references

• Bitcoin Core contributors. CBlockIndex::GetMedianTimePast, src/chain.h at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source
• Bitcoin Core contributors. ContextualCheckBlockHeader, src/validation.cpp, same revision. Source
• Bitcoin Core contributors. DeploymentActiveAfter, src/deploymentstatus.h, and CMainParams activation heights, src/kernel/chainparams.cpp, same revision. Source
• Thomas Kerin, Mark Friedenbach. BIP113: Median time-past as endpoint for lock-time calculations, 2015. Specification
• Gavin Andresen. BIP34: Block v2, Height in Coinbase, 2012; Pieter Wuille. BIP66: Strict DER signatures, 2015; Peter Todd. BIP65: OP_CHECKLOCKTIMEVERIFY, 2014. BIPs

Why relative lock-time matters

Bitcoin nodes must agree on whether a transaction may spend its inputs yet. Since 2016 that decision includes relative lock-time: an input may declare that the output it spends must have been confirmed for a minimum number of blocks or a minimum elapsed time before it becomes spendable. The rule is defined by BIP68 and enforced on mainnet by three helper functions in Bitcoin Core: CalculateSequenceLocks, EvaluateSequenceLocks, and SequenceLocks (pinned source). Payment channels, atomic swaps, and vault constructions depend on this rule to enforce dispute windows; a node that decodes a sequence word differently from its peers can accept or reject a block the rest of the network treats the other way.

The specification is short and the implementation is about seventy lines, yet the two are written in different languages. BIP68 speaks of bits, masks, and elapsed delays; the implementation folds inputs into two signed thresholds compared against the candidate height and its ancestor's median time. Whether these agree, for every 32-bit sequence word and every input list, is the question this mission settles. Absolute lock-time (nLockTime) already has a Lean treatment in btc-verified, whose consensus documentation lists BIP68 as outstanding work.

Sequence words, inputs, and contexts

An input is a pair $(s, c)$: an unsigned 32-bit sequence word $s$ and the coin height $c \in \mathbb N$ of the output being spent. A context is a pair $(H, M)$: the candidate block height $H \in \mathbb N$ and a total function $M : \mathbb N \to \mathbb N$ giving the median time past of each ancestor height. Write $h^- = \max(h-1, 0)$; natural-number subtraction in Lean truncates at zero and realizes this directly.

Three fields of $s$ matter. The disable bit $D$ is bit 31. The type bit $T$ is bit 22: set means a time-based lock, clear means a height-based lock. The delay $d = s \bmod 65536$ is the low sixteen bits; for a time lock it denotes $512d$ seconds. Enforcement $E$ holds when the transaction version is at least 2 and bit 0 of the validation flags is set.

The declarative model (BIP68_Model) expresses these as arithmetic on $s$ viewed as a natural number: $D \iff \lfloor s / 2^{31} \rfloor = 1$, $T \iff \lfloor s / 2^{22} \rfloor \bmod 2 = 1$. A single input is satisfied when

$$D \ \lor\ \begin{cases} M(c^-) + 512d \le M(H^-), & T,\\ c + d \le H, & \neg T.\end{cases}$$

A transaction satisfies BIP68 when $\neg E$ or every input is satisfied. The model also fixes the expected height list: each input's coin height, replaced by $0$ exactly when $E$ holds and $D$ is set.

The Core transcription (BIP68_Core) uses bit-vector masks 0x80000000, 0x00400000, 0x0000ffff and a left shift by 9. An accumulator holds two signed thresholds $(a, b)$ and a reversed height list, starting at $(-1, -1, [\,])$. Each enabled, non-disabled input updates $b \leftarrow \max(b,\ M(c^-) + 512d - 1)$ for a time lock or $a \leftarrow \max(a,\ c + d - 1)$ for a height lock. Evaluation succeeds when $a < H$ and $b < M(H^-)$. When $E$ is false, the fold is skipped and the original heights are returned.

Formalization targets

Goal — helper correctness

Under the admissible domain ($0 < H \le 2^{31}-1$, every $c \le H$, every $M(h) \le 2^{63}-1$ for $h \le H$) and the no-overflow condition (for every enforced, non-disabled input, the sum selected by $T$ fits its signed destination before the subtraction of one),

$$\mathrm{sequenceLocks}(v, f, H, M, I) = \mathrm{true} \iff \mathrm{satisfiesBIP68}(v, f, H, M, I),$$

and the height list returned by the fold equals the expected height list. This is BitcoinBIP68.core_correct.

Supporting milestones

1. Decoding (decode_sequence): for every 32-bit word, the mask tests agree with the quotient-and-remainder tests, the masked delay equals $d$, and the shifted seconds equal $512d$. No hypothesis on unused bits.
2. Fold acceptance (fold_acceptance): for any starting accumulator, evaluating the fold succeeds iff evaluating the starting accumulator succeeds and every input is satisfied. No range or monotonicity assumptions.
3. Height vector (height_vector): the returned list has the original length and order, with zeroes exactly at enforced, disabled inputs, including repeated entries and the empty list.
4. Threshold bounds (calculated_bounds): under admissibility and no-overflow, $-1 \le a \le 2^{31}-1$ and $-1 \le b \le 2^{63}-1$, preserving the $-1$ sentinel.

What the result establishes

The goal is a kernel-checked statement that a Lean transcription of the pinned Core helpers decides exactly the BIP68 spending condition on the admissible domain, and that its side effect on the per-input height list is the one BIP68 describes. Both directions matter: a lock the implementation accepts is one the specification accepts, and a lock the specification accepts is one the implementation accepts.

Formalizing it adds three things beyond the prose specification. It makes the overflow preconditions explicit, which BIP68 leaves implicit and Core leaves to callers. It separates the bit-level decoding (a bv_decide-style fact) from the aggregation logic (an induction over the input list), so each can be audited on its own. And it produces reusable definitions — Input, Context, the admissibility and overflow predicates — for a later whole-block validation development in which the caller obligations (supplying coin heights, ancestor clocks, activation flags, and coinbase exclusion) are discharged.

Status: the statements compile with intentional sorry placeholders and have independent read-backs. Differential checks ran 2,014 cases against extracted Core helper bodies; these test the transcription, not the theorems. No proof of any statement is claimed.

Where the obvious argument fails

The natural first idea is to prove core_correct by unfolding everything and calling a decision procedure. It fails because the two sides live in different arithmetic. The implementation computes thresholds in signed integers after subtracting one; the specification compares unsigned sums with $\le$. The equivalence $a < H \iff \max_i (c_i + d_i - 1) < H$ holds only because the $-1$ sentinel is below every admissible height and because each $c_i + d_i - 1$ is formed without wrap-around. Both facts need the admissibility and no-overflow hypotheses, and the proof must thread them through the fold.

A second trap is the disabled input. In the model, a disabled input is satisfied unconditionally; in the fold, it leaves both thresholds unchanged but still appends $0$ to the height list only when enforcement is on. height_vector records this asymmetry; a proof that treats disabled inputs as absent gets the height list wrong.

A third is the median-time function. $M$ is arbitrary: not monotone, not bounded outside $[0, H]$. The theorems are stated for this weaker model deliberately, so any proof that assumes a well-formed chain is proving a different statement.

Formalization scope

The development commits to the following conventions, all fixed in BIP68_Model and BIP68_Core. Sequence words, versions, and flags are BitVec 32. Heights and times are Nat in the model and Int in the accumulator. $h - 1$ on Nat truncates at zero, matching max(h-1, 0) in the source. Input lists are finite Lists; the empty list is in scope. The predicates specEnabled, specDisabled, and specTimeBased are Prop with decidability instances; the Core-side tests are Bool. Admissibility and no-overflow are the only hypotheses on core_correct; fold_acceptance and height_vector carry none.

A trivializing formalization would define satisfiesBIP68 by calling sequenceLocks; the model is written independently from the BIP text and must stay that way. Weakening the no-overflow hypothesis to a vacuous one, or restricting to nonempty lists, is out of scope.

Dependencies: Lean 4 core and Std only; no Mathlib. The two definitions are published first and imported by every theorem. Proofs of the four milestones in any order are welcome, as are lemmas on coreStep reusable by the goal. Out of scope: the C++-to-Lean correspondence (documented, not proved), coinbase exclusion, activation selection, and block-level composition, which belong to a separate whole-consensus mission that will import these results.

Selected references

• Mark Friedenbach, BtcDrak, Nicolas Dorier, kinoshitajona. BIP68: Relative lock-time using consensus-enforced sequence numbers, Bitcoin Improvement Proposals, 2015. Specification
• Bitcoin Core contributors. CalculateSequenceLocks, EvaluateSequenceLocks, SequenceLocks, src/consensus/tx_verify.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source
• Bitcoin Core contributors. Mainnet validation and parameters, same revision. validation.cpp, chainparams.cpp
• ProofOfKeags contributors. btc-verified: absolute lock-time in Lean 4, revision 2fdeb40c. LockTime.lean, consensus coverage
• Lean FRO. Bitvectors, Lean Language Reference. Documentation

Why the Merkle root and its mutation check matter

A Bitcoin block header commits to its transactions through a single 32-byte Merkle root: the transaction hashes are paired and hashed, the results paired and hashed again, until one hash remains. Every node recomputes this root from the block body and rejects the block if it does not match the header. Bitcoin's construction has a quirk that later became a vulnerability: when a level has an odd number of hashes, the last one is duplicated before pairing. Consequently the transaction lists $[1,2,3,4,5,6]$ and $[1,2,3,4,5,6,5,6]$ have the same root, and an attacker could relay the second, invalid, block with the first block's header; a node that marked that header permanently invalid would then reject the genuine block (CVE-2012-2459). Bitcoin Core defends by detecting, at every level, two equal adjacent hashes in an aligned pair and treating the block as having a bad root. (ComputeMerkleRoot and the comment above it.)

This mission transcribes that loop and proves that the defence does what its comment claims for the general form of the construction: duplicating any aligned block of $2^k$ trailing leaves preserves the root and is detected, at the level where that block has collapsed to one node.

The loop, as a function on lists

Hashes are an arbitrary type $H$ with decidable equality; the pairwise hash is an abstract $c : H \times H \to H$ (in the source, SHA256D64 on the two concatenated hashes), and the zero hash returned for an empty list is an abstract $z$. The three operations are, for a list of hashes $\ell$:

• pairUp$(\ell)$: $c$ applied to successive aligned pairs; an odd trailing element $a$ contributes $c(a, a)$. This is hashes.push_back(hashes.back()) followed by the pairwise hashing.
• hasEqualPair$(\ell)$: true when some aligned pair $(\ell_{2i}, \ell_{2i+1})$ with $2i + 1 < |\ell|$ consists of equal hashes. The duplicated trailing element is not tested: the check runs before the duplication.
• rootLoop$(\ell, m)$: while $|\ell| > 1$, replace $m$ by $m \lor \mathrm{hasEqualPair}(\ell)$ and $\ell$ by $\mathrm{pairUp}(\ell)$; on exit return the single remaining hash (or $z$ if the list is empty) together with $m$.

computeMerkleRoot$(\ell) = \mathrm{rootLoop}(\ell, \mathtt{false})$ returns the pair (root, mutated), exactly as ComputeMerkleRoot(hashes, &mutated).

Formalization targets

Goal — duplication of an aligned block is root-preserving and detected

For every $k$, every non-empty prefix $\ell$ whose length is a multiple of $2^{k+1}$, and every block $t$ of exactly $2^k$ hashes,

$$\mathrm{root}(\ell \mathbin{+\!\!+} t) = \mathrm{root}(\ell \mathbin{+\!\!+} t \mathbin{+\!\!+} t) \qquad\text{and}\qquad \mathrm{mutated}(\ell \mathbin{+\!\!+} t \mathbin{+\!\!+} t) = \mathtt{true}.$$

This is BitcoinMerkle.dup_block. The alignment hypotheses are what make $t$ collapse to a single node at level $k$, where the duplicate then sits in an aligned pair; $\ell \ne [\,]$ is needed because a list of one hash is its own root while a list of two is not. With $k = 0$ it is the classic duplicated-last-transaction case; with $k = 1$ it is the $[1,\dots,6,5,6]$ example of the source comment.

Supporting milestones

1. Base cases (root_nil, root_single, root_pair): the empty list gives $(z, \mathtt{false})$; one hash gives $(a, \mathtt{false})$; two give $(c(a,b),\ a = b)$.
2. Flag independence (rootLoop_fst): the root does not depend on the incoming flag.
3. Flag is sticky (rootLoop_sticky): once set, the flag stays set through the remaining levels.
4. One level distributes over an even split (pairUp_append_even, hasEqualPair_append_even): for $|\ell|$ even, $\mathrm{pairUp}(\ell \mathbin{+\!\!+} r) = \mathrm{pairUp}(\ell) \mathbin{+\!\!+} \mathrm{pairUp}(r)$ and likewise for the pair test.
5. Leaf-level case (dup_leaf): the goal at $k = 0$, stated directly.

What the result establishes

The goal is a kernel-checked statement about the transcribed loop: for the entire family of duplications that CVE-2012-2459 is built on, the root is unchanged and the mutation flag is raised. Together with the base cases it fixes the exact semantics of the odd-level rule and of the check, including the fact that the self-pairing of a duplicated trailing element is never itself flagged.

What the result does not say is also worth stating. It does not claim that every root collision is detected; that would require assumptions on the hash function (the source comment says "assuming no double-SHA256 collisions"), and $c$ is here an arbitrary function. Nor does it claim anything about the byte-level SHA256D64 or about transaction serialization; those belong to the hash and serialization layer. What formalizing adds is the general $k$ statement with its precise alignment conditions, which the source states only by example.

Status: all statements are open with intentional placeholder proofs. Nothing about compiled Bitcoin Core is claimed.

Where the obvious argument fails

The natural first attempt is to compute both sides for small lists and generalize. It fails on the $k$-level statement because the two lists differ in length by $2^k$ and go through $k$ levels before the duplicate appears as a pair. The argument has to track two facts through the loop at once: that the root is insensitive to the flag (so the two runs can be compared level by level with different flags), and that the flag, once raised at level $k$, survives to the end. Both are separate milestones for that reason.

The alignment hypotheses are the second trap. Without $2^{k+1} \mid |\ell|$ the block $t$ straddles a pair boundary and its two copies do not collapse to equal nodes; without $|t| = 2^k$ the copies collapse at different levels. The theorem is false without them, and the base case $\ell = [\,]$ shows that non-emptiness is needed too.

Formalization scope

$H$ is a type parameter with DecidableEq; $c$ and $z$ are parameters. Lists are Lean Lists, so pairUp and hasEqualPair are structurally recursive, and rootLoop is defined by well-founded recursion on the list length with the lemma $|\mathrm{pairUp}(\ell)| = \lceil |\ell| / 2 \rceil$ supplied in the definition file to justify termination. Equality in hasEqualPair is decide (a = b) on $H$, matching hashes[pos] == hashes[pos + 1] on uint256. The mutated pointer being null in the source (as in BlockWitnessMerkleRoot) only suppresses the output; the model always computes the flag.

A trivializing formalization would restrict $H$ to a type with a trivial hash or define the root by a different, non-duplicating rule; the definitions are fixed to the source's loop. Out of scope: MerkleComputation (Merkle branches), BlockMerkleRoot's leaf extraction, the witness root's zero coinbase leaf, and any collision-resistance assumption on $c$.

No Mathlib is required; the development imports only Std. Proofs of milestones in any order are welcome, and the distribution lemmas are reusable by any later Merkle-branch work.

Selected references

• Bitcoin Core contributors. ComputeMerkleRoot, src/consensus/merkle.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48, lines 16–73 including the CVE-2012-2459 comment. Source
• Forrest Voight. CVE-2012-2459: Bitcoin block Merkle root duplication, 2012. Advisory
• Satoshi Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System, 2008, section 7. Paper

Why the issuance schedule matters

Every Bitcoin block may create new coins through its coinbase transaction, and the amount it may create is fixed by consensus: a block subsidy that starts at fifty bitcoin and halves every 210,000 blocks, plus the fees of the block's other transactions. The schedule is the mechanism behind the often-quoted cap of twenty-one million bitcoin, yet the cap appears nowhere in the code as a rule. What the code enforces is the per-block subsidy, computed by GetBlockSubsidy in validation.cpp, and the check in ConnectBlock that the coinbase pays no more than fees plus subsidy. The cap is a consequence, and the only place a number near it appears is MAX_MONEY, a sanity bound on individual amounts whose comment says explicitly that it is "not the total money supply". (GetBlockSubsidy, amount.h, CMainParams)

This mission makes the consequence a theorem about the pinned implementation: the sum of the subsidies of all blocks, at every height the chain can reach, is strictly below MAX_MONEY, and in fact equals a specific constant once the subsidy reaches zero. It is the arithmetic core of the ledger-supply results that a whole-consensus development will need, and it is small enough to be verified completely.

The subsidy function and its schedule

Amounts are counted in satoshi. One bitcoin is $\mathrm{COIN} = 10^8$ satoshi and $\mathrm{MAX\_MONEY} = 21{,}000{,}000 \cdot \mathrm{COIN}$. The mainnet halving interval is $I = 210{,}000$ blocks.

The Core subsidy at height $h \in \mathbb N$ is the transcription of GetBlockSubsidy: with $k = \lfloor h / I \rfloor$ the number of halvings, the subsidy is $0$ if $k \ge 64$, and otherwise $(50 \cdot \mathrm{COIN}) \gg k$, the right shift of the initial subsidy by $k$ bits. Heights are nonnegative integers in the source, and the shift acts on the nonnegative value $50 \cdot \mathrm{COIN}$, so natural numbers represent both exactly. The explicit halvings >= 64 branch exists because a shift by 64 or more is undefined in C++.

The declarative schedule is $\mathrm{specSubsidy}(h) = \lfloor 50 \cdot \mathrm{COIN} \,/\, 2^{\lfloor h/I \rfloor} \rfloor$: fifty bitcoin, halved once per interval with the remainder discarded.

Issuance below height $n$ is the running sum of Core subsidies, $\mathrm{issuedBelow}(0) = 0$ and $\mathrm{issuedBelow}(n+1) = \mathrm{issuedBelow}(n) + \mathrm{coreSubsidy}(n)$. The interval sum $\mathrm{intervalSum}(m) = \sum_{j < m} \lfloor 50 \cdot \mathrm{COIN} / 2^j \rfloor$ collects one subsidy per interval. The zero height is $33 I = 6{,}930{,}000$.

Formalization targets

Goal — issuance below the cap

$$\forall n,\quad \mathrm{issuedBelow}(n) < \mathrm{MAX\_MONEY}.$$

This is the weakest stable statement: it survives any refinement of the constants below and is what a supply argument downstream consumes. It is BitcoinSubsidy.issuance_bound.

Supporting milestones

1. Core equals schedule (core_eq_spec): $\mathrm{coreSubsidy}(h) = \mathrm{specSubsidy}(h)$ for every $h$, including heights where the 64 branch fires.
2. Amount range (subsidy_le_maxMoney): $\mathrm{coreSubsidy}(h) \le \mathrm{MAX\_MONEY}$, so the subsidy is always a valid amount.
3. Monotone decrease (subsidy_antitone): $h_1 \le h_2 \implies \mathrm{coreSubsidy}(h_2) \le \mathrm{coreSubsidy}(h_1)$.
4. Halving step (subsidy_halving): $\mathrm{coreSubsidy}(h + I) = \lfloor \mathrm{coreSubsidy}(h) / 2 \rfloor$.
5. Exact extinction (subsidy_zero_iff): $\mathrm{coreSubsidy}(h) = 0 \iff h \ge 33 I$. The subsidy is one satoshi throughout the thirty-third interval and zero from the thirty-fourth on.
6. Exact total (issuance_total): $\mathrm{issuedBelow}(33 I) = 2{,}099{,}999{,}997{,}690{,}000$ satoshi.
7. Bounded by the total (issuance_le_total): $\mathrm{issuedBelow}(n) \le 2{,}099{,}999{,}997{,}690{,}000$ for every $n$.

What the result establishes

The goal is a kernel-checked statement that the implemented subsidy schedule can never issue MAX_MONEY or more in total, for any chain length, and the milestones pin down the exact figure: $20{,}999{,}999.9769$ bitcoin, $2{,}310{,}000$ satoshi short of twenty-one million because of the floor in each halving. Milestones 1 and 5 record two facts about the implementation worth having on the record: the halvings >= 64 guard is never the reason the subsidy is zero (division already gives zero from 33 halvings), and the subsidy is exactly one satoshi for the 210,000 blocks of the thirty-third interval.

What formalizing adds is separation of the arithmetic from the accounting. The supply bound on an actual ledger needs more than this: fees move value without creating it, unclaimed coinbase value is never issued, and outputs can be made unspendable. Those are statements about the UTXO transition and belong to a separate mission; this one supplies the exact upper bound they will cite.

Status: every statement is open with an intentional placeholder proof. The constants and the shift are checked against the pinned source; nothing about compiled Bitcoin Core is claimed.

Where the obvious argument fails

The naive proof of the goal is to evaluate the sum: unfold issuedBelow at $6{,}930{,}000$ and compute. The kernel cannot do that in reasonable time, and the statement is for every $n$, not one. The argument has to be structural: within an interval the subsidy is constant, so the sum over the first $m$ intervals is $I \cdot \mathrm{intervalSum}(m)$; past the zero height every term vanishes, so the sum is stable; and for $n$ below the zero height the sum is bounded by monotonicity. Only the thirty-three-term interval sum is evaluated by computation.

A second trap is the shift. $(50 \cdot \mathrm{COIN}) \gg k$ equals $\lfloor 50 \cdot \mathrm{COIN} / 2^k \rfloor$ only because the value is nonnegative; the schedule theorem is what licenses replacing the bitwise operation with division everywhere else.

Formalization scope

Heights, amounts and counts are Nat. coreSubsidy uses Lean's >>> on Nat, which is exact division by $2^k$. issuedBelow and intervalSum are structurally recursive, so proofs about them are inductions on the height or the interval count. No Mathlib is required; the development imports only Std.

A trivializing formalization would define issuedBelow through specSubsidy and prove the bound about the schedule alone; the definition is fixed on coreSubsidy so that the result is about the transcription. Weakening the goal to a bound at one fixed height is out of scope.

Out of scope: the coinbase check GetValueOut() > blockReward in ConnectBlock, fee accounting, and the UTXO set. Those take this mission's definitions as inputs. Proofs of the milestones in any order are welcome, as are reusable lemmas on issuedBelow.

Selected references

• Bitcoin Core contributors. GetBlockSubsidy, src/validation.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source
• Bitcoin Core contributors. COIN, MAX_MONEY, MoneyRange, src/consensus/amount.h, same revision. Source
• Bitcoin Core contributors. CMainParams::nSubsidyHalvingInterval, src/kernel/chainparams.cpp, same revision. Source
• Bitcoin Core contributors. Coinbase amount check in Chainstate::ConnectBlock, src/validation.cpp, same revision. Source
• Satoshi Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System, 2008. Paper

Why rule activation is part of consensus

Bitcoin's consensus rules are not a single ruleset but a history of them. Each soft fork — P2SH, strict DER signatures (BIP66), CHECKLOCKTIMEVERIFY (BIP65), sequence locks (BIP68/112/113), SegWit with NULLDUMMY (BIP141/147), Taproot — began enforcing at a particular block height, and a node validating the chain from genesis must apply to each block exactly the rules in force at its height. Bitcoin Core implements this with buried deployments: fixed activation heights in CMainParams, consulted by DeploymentActiveAt, and a function GetBlockScriptFlags that assembles the script-verification flags for a block. Two historical blocks are special-cased by hash: one that violated P2SH before the rule was enforced, and one that violated Taproot rules before activation; for these the flag set is replaced. (GetBlockScriptFlags, deploymentstatus.h, CMainParams)

A whole-chain correctness statement needs this table to be exact: which rules apply at which height, and precisely how the two exceptions deviate. This mission transcribes it and proves its structural properties: rules are only ever added as height increases, in a fixed order, and the exceptions only ever remove rules.

Deployments, heights, and flags

A buried deployment is one of HEIGHTINCB (BIP34), CLTV (BIP65), DERSIG (BIP66), CSV, SEGWIT, with mainnet heights $227{,}931$, $388{,}381$, $363{,}725$, $419{,}328$, $481{,}824$. It is active at a block when the block's height is at least that height, and active after a previous block when the previous height plus one is.

A flag set records which of P2SH, WITNESS, TAPROOT, DERSIG, CHECKLOCKTIMEVERIFY, CHECKSEQUENCEVERIFY, NULLDUMMY are enforced. The base is P2SH | WITNESS | TAPROOT for an ordinary block, NONE for the BIP16 exception block, and P2SH | WITNESS for the Taproot exception block. GetBlockScriptFlags adds DERSIG, CHECKLOCKTIMEVERIFY, CHECKSEQUENCEVERIFY and NULLDUMMY to the base when DERSIG, CLTV, CSV and SEGWIT respectively are active at the block's height. Flag sets are compared by inclusion: every rule enforced by the first is enforced by the second. Separately, ConnectBlock sets LOCKTIME_VERIFY_SEQUENCE for BIP68 exactly when CSV is active.

Formalization targets

Goal — soft forks only add rules

$$h_1 \le h_2 \;\Longrightarrow\; \mathrm{blockScriptFlags}(h_1) \subseteq \mathrm{blockScriptFlags}(h_2)$$

for ordinary (non-exception) blocks. This is BitcoinActivation.flags_mono: at no height is a script rule enforced that a later height would not enforce. It is the weakest statement that makes "the rules in force at height $h$" a well-ordered notion.

Supporting milestones

1. Activation is monotone (activeAt_mono); after is at of the next height (activeAfter_eq).
2. Before BIP66 (flags_before_bip66): only the base P2SH | WITNESS | TAPROOT.
3. From SegWit on (flags_after_segwit): every flag.
4. Order of activation (flags_order): CHECKLOCKTIMEVERIFY implies DERSIG, CHECKSEQUENCEVERIFY implies CHECKLOCKTIMEVERIFY, NULLDUMMY implies CHECKSEQUENCEVERIFY.
5. The BIP16 exception (bip16_exception): no flags at all at its height (170,060, before BIP66).
6. The Taproot exception (taproot_exception): every flag except TAPROOT at its height (692,261, after SegWit).
7. Exceptions only remove (exception_le): at any height, an exception's flags are included in the default's.
8. Sequence-lock flag (lockTimeFlags_eq): LOCKTIME_VERIFY_SEQUENCE exactly from height $419{,}328$.

What the result establishes

The goal and milestones pin down, as kernel-checked facts, the exact ruleset function of the pinned implementation: which script rules apply at every mainnet height, that the function is monotone and that its four height-dependent rules switch on in a fixed order, and that the two hash-keyed exceptions are the only departures and only ever relax. For the whole-consensus development this is the "historical rule selection" input: a block at height $h$ is validated against $\mathrm{blockScriptFlags}(h)$, and these theorems are what a composition proof cites when it reasons about rules across heights.

Status: all statements are open with intentional placeholder proofs. The exception blocks are identified by their hashes in the source; the model names them and states their flags at any height in the relevant range, so no claim about a specific hash is made.

Where the obvious argument fails

There is little depth here by design; the point is exactness. The trap is the exceptions: P2SH, WITNESS and TAPROOT are not height-gated at all in the pinned source (they are "always on except for the two violating blocks"), so a formalization that gates them by their historical activation heights would be wrong for the pinned revision. Likewise the height-dependent flags are OR-ed onto the exception's base, so the Taproot exception block does enforce DERSIG, CLTV, CSV and NULLDUMMY.

Formalization scope

Heights are Nat; flag sets are a structure of seven Booleans; inclusion is pointwise implication. Versionbits deployments (DEPLOYMENT_TESTDUMMY, the historical Taproot signalling) are not modeled, since the pinned source consults no versionbits state for mainnet consensus flags. The exception table is modeled as a three-valued classification of a block rather than a hash lookup; the hash-to-block correspondence is a serialization matter.

A trivializing formalization would define the flags directly as a monotone function of height, dropping the exceptions; the definition follows the source's base-then-OR structure with the exception table.

No Mathlib is required; the development imports only Std.

Selected references

• Bitcoin Core contributors. GetBlockScriptFlags, src/validation.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48, lines 2249–2288. Source
• Bitcoin Core contributors. DeploymentActiveAt, DeploymentActiveAfter, src/deploymentstatus.h; BuriedDeployment, DeploymentHeight, src/consensus/params.h; CMainParams, src/kernel/chainparams.cpp, same revision. Source
• Bitcoin Core contributors. LOCKTIME_VERIFY_SEQUENCE, src/consensus/consensus.h, same revision. Source
• Bitcoin Improvement Proposals 16, 34, 65, 66, 68, 112, 113, 141, 147, 341, 342, collection at revision 100ba872c808946155b1eeb8c4568058f2eea0a7. Collection

Why the difficulty arithmetic matters

A Bitcoin block header is valid only if its hash, read as a 256-bit number, is at most a target encoded in the header's 32-bit nBits field, and only if that nBits is the one the consensus rules require at that height. Every 2016 blocks the required target is recomputed from the time the previous 2016 blocks took, so that blocks keep arriving roughly every ten minutes. Three pieces of arithmetic carry the whole rule: the lossy compact encoding between a 32-bit word and a 256-bit target (arith_uint256::SetCompact and GetCompact), the retarget computation with its clamped timespan and cap (CalculateNextWorkRequired), and the transition check that a header's claimed difficulty change is within the permitted range (PermittedDifficultyTransition), which Bitcoin Core uses to reject headers cheaply before it has the full chain. (pow.cpp, arith_uint256.cpp, CMainParams)

These functions are short but intricate: the encoding has sign and overflow flags, a mantissa that must be re-normalized when its top bit is set, and a rounding step that discards low bits; the retarget multiplies inside 256 bits where a carry would be lost. A disagreement in any of them splits the network. This mission states what the pinned implementation computes and proves that its own pieces are consistent: the retarget never produces a target the transition check rejects.

Targets, compact words, and the retarget

A compact word $c$ is a 32-bit value with size $S = \lfloor c / 2^{24} \rfloor$ (the top byte) and mantissa $W = c \bmod 2^{23}$ (the low 23 bits; bit 23 is the sign). Its exact value is $\mathrm{specTarget}(c) = W \cdot 256^{S-3}$ when $S > 3$ and $\lfloor W / 256^{3-S} \rfloor$ otherwise. SetCompact computes the same quantity but inside a 256-bit register, so its result is $\mathrm{setCompact}(c) = (W \ll 8(S-3)) \bmod 2^{256}$ for $S > 3$. It also reports negative ($W \ne 0$ and bit 23 set) and overflow ($W \ne 0$ and $S > 34$, or $W > 255$ and $S > 33$, or $W > 65535$ and $S > 32$).

GetCompact encodes a 256-bit value $v$: with $b$ the bit length of $v$ and $S = \lceil b / 8 \rceil$, the mantissa is $v$ shifted to its top three bytes (shifted left into three bytes when $S \le 3$); if bit 23 of that mantissa is set, the mantissa is divided by 256 and $S$ incremented; the word is mantissa $\lor (S \ll 24)$. Because only three bytes survive, $\mathrm{setCompact}(\mathrm{getCompact}(v))$ is $v$ rounded down.

Mainnet parameters: $\mathrm{powLimit} = 2^{224} - 1$, target timespan $T = 1{,}209{,}600$ seconds, spacing $600$ seconds, interval $2016$ blocks; minimum-difficulty blocks, no-retargeting, and BIP94 are all off.

DeriveTarget rejects a word that is negative, zero, overflowing, or above $\mathrm{powLimit}$; proof of work holds when the hash is at most the derived target. CalculateNextWorkRequired takes the last target $t_{\text{old}}$ and the signed elapsed time $a$ of the period, clamps it to $[T/4,\ 4T]$, computes $(t_{\text{old}} \cdot a \bmod 2^{256}) / T$, caps at $\mathrm{powLimit}$, and re-encodes with GetCompact. PermittedDifficultyTransition at a retarget height decodes the claimed new word and requires it to lie between the re-encoded caps of $t_{\text{old}} \cdot (T/4) / T$ and $t_{\text{old}} \cdot 4T / T$; off a retarget height it requires the word to be unchanged. GetNextWorkRequired returns the last word off a retarget height and calls the retarget on one.

Formalization targets

Goal — the retarget passes its own transition check

$$\forall h, c_{\text{old}}, t_{\text{last}}, t_{\text{first}}:\quad h \equiv 0 \pmod{2016}\ \wedge\ \mathrm{setCompact}(c_{\text{old}}) \le \mathrm{powLimit} \ \Longrightarrow\ \mathrm{permittedTransition}\big(h,\ c_{\text{old}},\ \mathrm{calculateNextWork}(c_{\text{old}}, t_{\text{last}}, t_{\text{first}})\big) = \mathtt{true}.$$

The hypothesis on $c_{\text{old}}$ holds for every target DeriveTarget accepts, hence for every block on a valid chain. This is BitcoinPow.nextWork_permitted. It is the weakest stable statement: it says only that the two functions are consistent, without fixing the rounding constants that make them so.

Supporting milestones

1. Overflow is exact (overflow_iff): the overflow flag is set iff $\mathrm{specTarget}(c) \ge 2^{256}$.
2. Decoding is exact without overflow (setCompact_eq_spec): if the flag is clear, $\mathrm{setCompact}(c) = \mathrm{specTarget}(c)$.
3. Proof of work (checkProofOfWork_iff): acceptance iff the word is non-negative, non-overflowing, positive, at most $\mathrm{powLimit}$, and $\mathrm{hash} \le \mathrm{specTarget}(c)$.
4. Rounding down (getCompact_le): $\mathrm{setCompact}(\mathrm{getCompact}(v)) \le v$ for $v < 2^{256}$.
5. Encoding is valid (getCompact_valid): GetCompact never produces a negative or overflowing word.
6. Rounding is monotone (round_mono): $v \le w < 2^{256} \implies \mathrm{setCompact}(\mathrm{getCompact}(v)) \le \mathrm{setCompact}(\mathrm{getCompact}(w))$.
7. Clamp (clamp_bounds): the clamped timespan lies in $[T/4, 4T]$ for every signed input.
8. Cap (nextWork_le_powLimit): the next target decodes to at most $\mathrm{powLimit}$, for every input.
9. Off-boundary (nextWork_off_boundary): off a retarget height the required word is the last word, and that transition is permitted.

What the result establishes

The goal is a kernel-checked consistency property of the pinned implementation: whatever the last target and the two block times, a block carrying the required nBits is never rejected by the cheap header-chain check. Milestones 1–3 give an exact mathematical reading of what nBits means on the wire, including when the implementation refuses it. Milestones 4–6 characterize the lossy re-encoding: it rounds down, keeps the top bit, and is order-preserving, which is the property the transition check silently relies on when it compares re-encoded bounds against a decoded value.

Formalizing adds two things to the C++. It makes the 256-bit wrap-around explicit: the retarget's multiplication is proved not to wrap only under the bound on the previous target, and the overflow flag is proved to be exactly the "does not fit" condition rather than an approximation. And it isolates the rounding as a function of the top-bit position, which is what the monotonicity argument needs and what the source never states.

Status: all statements are open with intentional placeholder proofs. Nothing about compiled Bitcoin Core is claimed; the value-level model of arith_uint256 (a natural number below $2^{256}$, shifts and products reduced modulo $2^{256}$, exact division) is the documented correspondence.

Where the obvious argument fails

The naive proof of the goal is to unfold both functions and compare. It fails at the re-encoding: the new word is $\mathrm{getCompact}(x)$ and the check compares $\mathrm{setCompact}(\mathrm{getCompact}(x))$ against $\mathrm{setCompact}(\mathrm{getCompact}(y))$ for the two bounds $y$. These are not $x$ and $y$; they are $x$ and $y$ with low bits cleared, and how many bits are cleared depends on the bit length of each. The argument needs that the rounding map is monotone across different bit lengths, which holds because the rounded value always retains the top bit — a value with fewer bits is below the top bit of any value with more.

A second trap is the mantissa normalization. When the top three bytes have bit 23 set, GetCompact shifts by a further byte, so the number of discarded bits is not a function of the size byte alone; the case split in the proofs is on the bit position modulo 8.

A third is nActualTimespan, a signed 64-bit difference that can be negative when timestamps go backwards. The clamp is stated on signed integers and the conversion to a natural number happens after it.

Formalization scope

arith_uint256 values are Nat below width = 2 ^ 256; <<= and *= reduce modulo width, /= is Nat division, bits() is Nat.log2 + 1 with 0 for zero, and GetLow64 is % 2 ^ 64. The uint32_t assignment in GetCompact is % 2 ^ 32. Compact words are BitVec 32; their fields are read through toNat. Block times are Int; the clamped timespan is converted with Int.toNat after clamping. Hashes enter checkProofOfWork already as natural numbers; the byte-order correspondence of UintToArith256 is a serialization matter outside this mission. fPowAllowMinDifficultyBlocks, fPowNoRetargeting, enforce_BIP94, and the fuzz-determinism shortcut are fixed to their mainnet values and not modeled as parameters.

A trivializing formalization would define permittedTransition by calling calculateNextWork; both are transcribed independently from the source. Assuming the previous target is already a GetCompact output, which would make rounding exact, is also ruled out: the goal assumes only the powLimit bound.

No Mathlib is required; the development imports only Std. Proofs of milestones in any order are welcome, and lemmas on the rounding map are reusable by any later header-validation work.

Selected references

• Bitcoin Core contributors. GetNextWorkRequired, CalculateNextWorkRequired, PermittedDifficultyTransition, DeriveTarget, CheckProofOfWorkImpl, src/pow.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source
• Bitcoin Core contributors. arith_uint256::SetCompact, arith_uint256::GetCompact, base_uint::operator<<=, operator*=, operator/=, bits, src/arith_uint256.cpp and .h, same revision. Source
• Bitcoin Core contributors. CMainParams proof-of-work parameters, src/kernel/chainparams.cpp, same revision. Source
• Satoshi Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System, 2008, section 4. Paper

Why value accounting matters

Bitcoin's ledger is a set of unspent transaction outputs: every coin that exists is an output of some transaction that no later transaction has spent. A transaction consumes outputs and creates new ones; the rule that it may not create value — that its outputs total at most its inputs — is what makes the supply finite, and the one exception, the coinbase transaction of each block, may create at most the block subsidy plus the fees the block's other transactions paid. Bitcoin Core enforces this through a handful of functions: CheckTransaction rejects negative or overflowing output values (CVE-2010-5139) and duplicate inputs (CVE-2018-17144); CheckTxInputs requires every input to be an existing, mature coin and computes the fee; UpdateCoins spends the inputs and adds the outputs; ConnectBlock accumulates the fees and rejects a coinbase that pays more than fees plus subsidy, after a BIP30 check that no output of the block already exists as an unspent coin. (tx_check.cpp, tx_verify.cpp, coins.cpp, validation.cpp)

Each of these checks has been the site of a real inflation bug. This mission transcribes them and proves the ledger-level consequence: starting from an empty ledger, after any sequence of accepted blocks the total value of all unspent outputs is at most the sum of the block subsidies.

Coins, transactions, and the view

Amounts are integers in satoshi; MoneyRange is $0 \le v \le \mathrm{MAX\_MONEY} = 2.1 \times 10^{15}$. Transaction ids form an arbitrary type $T$ with decidable equality. An outpoint is a pair (txid, index). A coin is an output value together with its creation height, its coinbase flag, and whether its script is unspendable (the only script property the accounting reads: AddCoin never stores an unspendable output). A transaction has a txid, a list of input outpoints, a list of outputs, and a coinbase flag standing for IsCoinBase(). The UTXO set is a list of (outpoint, coin) entries with pairwise distinct outpoints; getCoin looks an outpoint up, spendCoin removes it, addCoin inserts (replacing any entry with the same outpoint, as possible_overwrite permits), and totalValue sums the stored values.

The transcribed rules: checkTransaction (non-empty inputs and outputs, the output-value loop with its running MoneyRange test, no duplicate inputs); checkTxInputs (all inputs present, coinbase inputs mature by COINBASE_MATURITY = 100, each input value and the running nValueIn in range, nValueIn \ge GetValueOut(), fee in range); updateCoins (spend inputs unless coinbase, add outputs); bip30Ok; checkBlockTxs (first transaction coinbase, others not, all passing checkTransaction); connectLoop (per-transaction fee accumulation with the running MoneyRange test, then updateCoins); connectBlock (the above, then GetValueOut(coinbase) \le nFees + subsidy(height)); and connectChain, which connects blocks at consecutive heights. The subsidy is a parameter $s : \mathbb N \to \mathbb Z$.

Formalization targets

Goal — the ledger never holds more than the subsidies issued

$$\mathrm{connectChain}_s([\,],\ h_0,\ B_1 \cdots B_n) = \mathrm{some}(U) \;\Longrightarrow\; \mathrm{totalValue}(U) \le \sum_{i<n} s(h_0 + i),$$

for every subsidy function $s$, starting height $h_0$, and sequence of blocks whose transactions have pairwise distinct txids within each block. This is BitcoinUtxo.ledger_bound. It is the weakest stable statement: the subsidy schedule is a parameter, so the result survives any change to it, and composing with the subsidy mission's bound gives the twenty-one-million cap as a corollary.

Supporting milestones

1. Output checks (checkTransaction_outputs): an accepted transaction has distinct inputs and every output value in $[0, \mathrm{MAX\_MONEY}]$.
2. The fee (checkTxInputs_some): CheckTxInputs returns exactly $\mathrm{valueIn} - \mathrm{valueOut}$, in range, with every input present.
3. Spending one coin (totalValue_spend): removing a present coin lowers the total by exactly its value.
4. Adding a fresh coin (totalValue_add_fresh): adding at a fresh outpoint raises the total by the value, or by nothing if unspendable.
5. Spending the inputs (totalValue_spendInputs): spending distinct, present inputs lowers the total by $\mathrm{valueIn}$.
6. Transaction conservation (tx_conservation): an accepted ordinary transaction with fresh outputs lowers the ledger by at least its fee.
7. Coinbase (coinbase_bound): a coinbase with fresh outputs raises the ledger by at most its output value.
8. Block (block_bound): an accepted block raises the ledger by at most $s(h)$ and keeps outpoints distinct.
9. Chain (chain_bound): the same, summed over consecutive blocks, from any ledger.

What the result establishes

The goal is a kernel-checked statement that the transcribed rules, applied from genesis, cannot put more value into the ledger than the subsidy schedule allows, for any transactions whatsoever: fees only move value, unspendable outputs only destroy it, and the coinbase is bounded by fees plus subsidy. The milestones give the exact per-transaction accounting the proof rests on, including the role of each historical fix: the MoneyRange loop (milestone 1), the duplicate-input rejection (milestones 5 and 6 need distinct inputs), and the BIP30 check (milestones 6 to 8 need fresh outputs).

Three hypotheses are the honest boundary of the result. Distinct txids within a block stand for the collision-freedom of transaction hashes, which an abstract id type cannot provide. The BIP30 check is modeled as enforced, which is true at every mainnet height except the two historical duplicate-coinbase blocks. And the genesis coinbase, which Bitcoin Core never connects to the UTXO set, is simply not among the blocks.

Status: every statement is open with an intentional placeholder proof. Nothing about compiled Bitcoin Core is claimed.

Where the obvious argument fails

The naive argument — "inputs exceed outputs, so value cannot grow" — fails at three places that the actual code guards. Without distinct inputs, a transaction that lists the same outpoint twice would be credited its value twice while the view removes it once (CVE-2018-17144); the accounting lemma for spending needs Nodup. Without the BIP30 check, an output could overwrite an existing unspent coin and silently destroy or replace its value; the lemma for adding a coin needs the outpoint fresh, and freshness must be carried through the block from the initial view, which is where distinct txids enter. And the output values must be known non-negative before any sum is bounded, which is exactly what the MoneyRange loop supplies.

The fee is a second trap: CheckTxInputs computes it with signed arithmetic and tests it separately, so the proof must recover the identity $\text{fee} = \mathrm{valueIn} - \mathrm{valueOut}$ from the loop rather than assume it.

Formalization scope

Amounts are Int; heights are Nat, and the maturity test uses truncated subtraction, which rejects a spend below the coin's height as the signed source does. The UTXO set is a keyed list; keysNodup is the map invariant and is proved preserved. Serialization-size, script-length, null-prevout and script-validity rules are not modeled; the coinbase flag is a field. The BIP30 enforcement flag, fEnforceBIP30, is fixed to its post-exception mainnet value.

A trivializing formalization would define connectBlock so that it fails whenever value would grow; every rule is transcribed from its source function. Restricting to blocks with no unspendable outputs or to transactions with a single input is out of scope.

No Mathlib is required; the development imports only Std. The composition with the subsidy mission's BitcoinSubsidy.issuance_bound, giving the absolute cap, is the intended follow-up theorem.

Selected references

• Bitcoin Core contributors. CheckTransaction, src/consensus/tx_check.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source
• Bitcoin Core contributors. Consensus::CheckTxInputs, src/consensus/tx_verify.cpp, same revision. Source
• Bitcoin Core contributors. CCoinsViewCache::AddCoin, SpendCoin, HaveInputs, AddCoins, src/coins.cpp, same revision. Source
• Bitcoin Core contributors. UpdateCoins, BIP30 check and fee accounting in Chainstate::ConnectBlock, src/validation.cpp, same revision. Source
• Pieter Wuille. BIP30: Duplicate transactions, 2012. Specification
• Satoshi Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System, 2008, sections 2 and 9. Paper

A smaller formalized bound for sums of primes

The Odd Goldbach campaign asks how many prime summands suffice to represent every odd integer greater than one, while tracking bounds supported by formal proofs. This mission supplies the bound 23. Its starting point is the accepted 25-prime formalization, which uses the elementary Schnirelmann–Mann method and explicit sieve estimates. The improvement concerns the constants in that formalized development. It does not assert a new mathematical solution of the three-prime problem.

An explicit bound is useful here because it turns a qualitative additive-basis statement into a theorem with a precise, auditable conclusion. Each improvement must still cover every allowed input, including the smallest odd integers. The campaign statement fixes that common standard, so a smaller displayed value has the same mathematical meaning as the earlier bound.

Integers, prime summands, and counting functions

A prime is a natural number greater than one with no positive divisors other than one and itself. A representation is a finite multiset of primes: order does not matter, and the same prime may occur more than once. Both the sum and the number of summands count multiplicities. In particular, the prime 2 is allowed in the mission's conclusion.

The supporting two-prime counting function counts integers representable as a sum of two odd primes. An integer with several such representations is counted once. For a natural number $n$, write $R(n)$ for the number of representable integers in the interval from zero through $n$. The formalization uses the existing shared representation function and tests whether that function is positive; it does not replace the represented set with a more convenient surrogate.

The finite sieve input uses a set $Q$ of 1000 odd primes, each at most 7927. For a positive difference $d$, its weight is

$$K(d)=\prod_{p\mid d,\ p>2}\frac{p-1}{p-2},$$

where the product runs over distinct odd prime divisors. The finite certificate counts each unordered pair of distinct entries once, using the condition $b<a$.

Formalization targets

The goal is

$$\forall n\in\mathbb N,\quad n>1\ \text{and }n\text{ odd}\ \Longrightarrow\ \exists s,\quad |s|\le23,\quad \sum_{p\in s}p=n,$$

where every member of the multiset $s$ is prime. This is exactly the campaign template specialized to 23. There is no unspecified lower threshold and no additional arithmetic hypothesis on $n$.

The supporting finite milestone establishes

$$|Q|=1000,\qquad \sum_{a,b\in Q,\ b<a}K(a-b)\le867861.$$

The two counting milestones establish

$$R(n)\ge\frac{100n}{2199}$$

on the respective ranges $20\le\log n\le300$ and $\exp(300)\le n$. Natural logarithms and real exponentials are used throughout. The boundary at $\log n=300$ is included in both estimates; no gap between the ranges is intended or permitted.

What the formalization contributes

The mission improves the previously formalized constant from 25 to 23 while retaining the shared mathematical definitions. Its reusable outputs are the explicit finite sieve certificate and the two counting estimates. These can support later work without requiring another author to repeat the finite prime-weight computation or reconstruct the same numerical bounds.

The finite certificate is published with a closed dependency frontier. The medium-range, large-range, and goal records carry their own verification status and dependency graphs. A verified reduction and a theorem with every dependency proved are distinct statuses. Campaign attestation additionally requires review of the mission and the numeric value established by its goal.

The difficulty of preserving explicit constants

The central difficulty is retaining enough quantitative information across the finite sieve input, the two counting ranges, the density comparison, and the small-value transition. An asymptotic estimate alone would leave unboundedly many inputs outside the theorem's scope. A numerical calculation performed outside the proof assistant would also leave the crucial finite certificate unsupported.

Large exact computations pose a separate formalization constraint: a correct proof can exceed the verification service's per-file time limit. The finite computation is therefore organized into genuine mathematical subclaims with independently checked statements. Their combination is a short list-sum argument; a successful helper submission is not substituted for the final endpoint.

Formalization scope and conventions

The development uses Lean 4.33.1 and the campaign's pinned Mathlib environment. Natural numbers encode inputs and prime summands; real numbers encode logarithms, densities, and analytic inequalities. Finite sets are used for the sieve shifts and counted integers, while the final representation is a multiset. The distinction matters: shift primes are distinct, but final summands may repeat.

The existing Schnirelmann definitions, Mann basis theorem, sieve constants, prime-pair estimate, and two Riesel–Vaughan interval estimates remain shared dependencies. The submitted proofs introduce no new axiom, admitted proof, weakened quantifier, or external computation oracle. Local interface files are only mirrors of platform declarations; complete dependency closure is checked on the platform separately from local compilation.

Further contributions may sharpen these explicit estimates or reuse the finite and counting certificates. The stable objects for such work are their published statements and definitions. Any future lower campaign value must still satisfy the full quantified goal.

Selected references

• H. Riesel and R. C. Vaughan, On sums of primes, Arkiv för Matematik 21 (1983). Article scan.
• Prove2Me, Every odd number greater than 1 is the sum of at most 25 primes, accepted formalization, 2026. Theorem and proof dependencies.
• Prove2Me, Odd numbers as sums of primes, campaign template and attested bounds. Campaign.

Motivation

Atlas IV certified the Kerr–Newman background as an exact Einstein–Maxwell solution and proved that its linearised operators $L_E, L_J, L_H$ are the true first variations of the nonlinear residuals. Atlas III proved, for frozen Kerr–Newman radiation systems taken from Hintz (arXiv:2609.33661v1), the local equivalence of systems (1) and (7). Atlas V connects the two: under an explicit phantom gauge and single-mode conditions, IV's linearised equations imply III's systems.

Setting

Boyer–Lindquist coordinates $x=(t,r,\theta,\varphi)$, Atlas signature $(-,+,+,+)$; parameters $p$ with $M>0$, $Q\neq0$, $a^2+Q^2<M^2$ ($a=0$ allowed); exterior $U_p=\{r>r_+,\ 0<\theta<\pi\}$ and $\mathrm{dom}=\{x:(r,\theta)\in U_p\}$. The Kinnersley frame $(l,n,m,\bar m)$ with $q=r+ia\cos\theta$, complex-bilinear contractions (no conjugation), NP spin coefficients and Weyl/Faraday scalars are registered local coordinate definitions; Riemann and Weyl come from Atlas II's curvature. A complex tangent $\tau=(\tau_R,\tau_I)$ is a pair of real first-order tangents $(h,f,B)$ of metric, field and frame, each $C^\infty$, with antisymmetric $f$, the frame reality pattern ($l,n$ real, $\bar m=\overline{m}$) and the first-order Gram relation.

Formalization targets

Goal (atlasV03_main): if $\tau$ is such a tangent on $\mathrm{dom}$, IV's linearised residuals of the complexified tangent vanish, the complex phantom gauge $\delta\Phi_0^{\mathbb C}=\delta\Phi_2^{\mathbb C}=0$ holds on $\mathrm{dom}$, and the scaled radiative variables of both branches are single modes $e^{-i\omega t+im\varphi}\times$(amplitude in $(r,\theta)$) with real $\omega,m$, then III's positive and negative systems (1) hold on $U_p$, and (via III) systems (7).

Milestones: the frame/Faraday/mode bridges (V-01), the frame curvature bridge, the background $\Psi_2$ and the sourced NP Bianchi identity (V-02), the kinematic realisation and the Ricci source formula through IV's $L_E$, and the four per-branch statements (V-03).

Significance

The radiation systems of Atlas III are no longer free-standing: each of the eight frozen residuals res1a–d, res1aN–dN is derived in Lean from a linearised Newman–Penrose identity of an actual metric/field/frame perturbation, with sources written through IV's certified operators. Divisions are only by $P$, $q$, $\bar q$, $\sqrt2$, $\Sigma$, $\Delta$, $\sin\theta$ (nonzero on the exterior) and, in res1d/res1dN, by $\Phi_1=Q/(2\bar q^2)$ using $Q\neq0$; never by $\omega$, $m$ or $F_\pm$.

Difficulty

The frame varies with the perturbation; the curvature bridge needs the $-c\,\Omega$ commutator term; the complex gauge is a condition on the complex combination and may not be split into real parts; sources appear under frame derivatives and must be shown to vanish on an open set; amplitude regularity has to be derived, not assumed.

Formalization scope

Lean 4 with Mathlib (0df444a3…), autoImplicit off; smoothness is ContDiffOn ℝ ∞ ($C^\infty$, not analytic). Pinned Mathlib has no Lorentzian Levi-Civita connection, Ricci tensor or Newman–Penrose objects; the coordinate definitions are a registered local definition layer (B3 policy), reused unchanged from Atlas I–IV and extended in V (registry §K–§M). This is a forward source derivation under the chosen gauge and single-mode conditions, not a two-way reconstruction; no gauge reachability, mode completeness, spectrum, stability, global flow or new exact solution is claimed; zero_instance only shows the hypothesis bundle is non-empty.

Selected references

• P. Hintz, Perturbations of Kerr–Newman black holes: separation and mode stability, arXiv:2609.33661 (v1 archived locally). https://arxiv.org/abs/2609.33661
• Z. Mark, H. Yang, A. Zimmerman, Y. Chen, arXiv:1409.5800 (v1 LaTeX e-print read locally; appendix equation numbers not verified). https://arxiv.org/abs/1409.5800
• S. Chandrasekhar, The Mathematical Theory of Black Holes (not obtained; the NP identities used were derived independently and are marked so).
• Exact Vacuum Atlas III and Exact Spacetime Atlas IV (the author's earlier releases; nodes and bundles reused unchanged).