All missions

Partitions and generating functions

A partition of a nonnegative integer is a way to express it as a sum of positive integers, with the order of the summands ignored. For example, the partitions of 4 are 4, 3+1, 2+2, 2+1+1, and 1+1+1+1. If $p(n)$ denotes their number, then $p(4)=5$ and $p(0)=1$, with the empty partition counted once. Although this definition is elementary, the values of $p(n)$ obey identities and divisibility laws that are difficult to see from lists of partitions.

A generating function records a sequence as coefficients of a power series. For partitions it is $P(X)=\sum_{n\geq0}p(n)X^n$. Product and series identities give different descriptions of the same coefficients, connecting counting problems with algebra and complex analysis. Hei-Chi Chan's An Invitation to q-Series develops these connections through Jacobi's product identity, the Rogers–Ramanujan identities, and Ramanujan's partition congruences. This collection imports the proved statements in the accompanying Lean development, with Ramanujan's partition identity as its main result.

Formal series and convergent products

A formal power series over a ring $R$ is a sequence of coefficients written as $\sum_{n\geq0}a_nX^n$; equality means equality of every coefficient. Multiplication uses the finite sum $[X^n](FG)=\sum_{k=0}^n a_kb_{n-k}$. The symbol $X$ is an indeterminate, so a formal identity requires no choice of a numerical value for $X$ and no analytic convergence assumption.

Write $E(X)=\prod_{m\geq1}(1-X^m)$. This formal product is well defined because, for a fixed degree $n$, factors with $m>n$ do not change its coefficient. Euler's partition identity states that $P(X)E(X)=1$. Substituting $X^d$ for $X$ multiplies every exponent by the positive integer $d$; in particular, $E(X^5)=\prod_{m\geq1}(1-X^{5m})$.

The analytic results use a complex number $q$ in place of the formal variable. Their finite product notation is $(a;q)_N=\prod_{j=0}^{N-1}(1-aq^j)$, and $(a;q)_\infty$ denotes the corresponding infinite product when it converges. Conditions such as $|q|<1$, $q\ne0$, and the nonvanishing of other parameters are part of the individual statements. The formal and analytic settings remain distinct throughout the collection.

The main identity and accompanying results

The main theorem identifies the generating function for partition numbers whose indices are 4 modulo 5. In $\mathbb Q[[X]]$, it asserts the unconditional identity

$$\sum_{n\geq0}p(5n+4)X^n=5E(X^5)^5P(X)^6.$$

Since $P(X)E(X)=1$, this is the usual expression $5E(X^5)^5/E(X)^6$. The inverse exists because $E(X)$ has constant coefficient 1. The displayed equality concerns the whole infinite series, rather than a fixed number of initial coefficients.

The associated milestones include Euler's pentagonal identity, Jacobi's triple product, the two Rogers–Ramanujan identities, and the partition congruences

$$p(5n+4)\equiv0\pmod5,\qquad p(7n+5)\equiv0\pmod7,\qquad p(11n+6)\equiv0\pmod{11}$$

for every natural number $n$. Additional milestones record formal identities involving the Rogers–Ramanujan quotient and the parity of Ramanujan's tau coefficients. Each reference retains its own hypotheses and coefficient ring; the collection does not treat identities over different rings as interchangeable.

What the collection provides

The partition identity gives an exact generating function for an infinite arithmetic progression of partition numbers. The three congruences likewise apply to all indices in their stated progressions. Their scope is therefore different from the numerical partition and tau values that also appear in the library. Both kinds of result are included, with their ranges stated explicitly.

The source development supplies Lean proofs of these known mathematical results. The imported collection makes their definitions, statements, and supporting lemmas available in one compatible environment for subsequent work on partition identities and Ramanujan notebook formulas. Its reusable components include finite product algebra, coefficient extraction, substitutions in formal series, and the links between analytic products and formal coefficient identities.

Why the representation matters

Agreement of many initial coefficients cannot establish equality of two arbitrary infinite series. A formalization must account for every coefficient and justify any infinite product or sum used to define it. In an analytic statement, moving between a limit and a sum or product also requires convergence under the stated parameter conditions. These obligations remain present even when the final displayed identity is short.

Division presents a separate issue. A quotient of formal series needs an invertible denominator, while analytic quotients need the relevant complex values to be nonzero. Residue-class extraction introduces another distinction: retaining terms of degree $5n+r$ and replacing their exponents by $n$ is different from leaving those exponents unchanged. The imported definitions specify the convention used by each theorem.

Formalization scope

The main result uses rational formal power series and the ordinary partition-counting function. Supporting statements use integers, commutative coefficient rings, finite residue fields, or complex analysis as required by their types. The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The mathematical source is pinned to revision 5df34b280b6a9c4a68ab09105b4e5d3c7bbe88d1; compatibility adaptations are recorded with the imported items.

This is a collection of the source's proved results, including auxiliary and conditional lemmas. It does not assert that every statement discussed in the book has been formalized. In particular, the continued-fraction convergence discussion, the closed-form special value at $e^{-2\pi}$, the general core-partition characterization, and the full modularity and multiplicativity theory of the tau function must not be inferred from the narrower entries provided here. A definition of a proposed value is kept distinct from a theorem evaluating a function at that value.

The referenced theorem statements are fixed to the audited import. Further work can reuse these results to formalize additional identities or supply separate, stronger theorems. Conditional reductions remain conditional in their titles and statements, and finite computations retain their explicit bounds.

Selected references

Hei-Chi Chan, An Invitation to q-Series: From Jacobi's Triple Product Identity to Ramanujan's Most Beautiful Identity, World Scientific, 2011. DOI: 10.1142/8129.

Xiang Huang, Lean formalization of An Invitation to q-Series, source revision 5df34b280b6a9c4a68ab09105b4e5d3c7bbe88d1. Pinned source repository.

Comparing classification problems

A classification problem specifies when two objects should count as equivalent. Descriptive set theory compares such problems by asking whether an assignment of invariants transforms one equivalence relation into another. Requiring that assignment to be Borel measurable prevents arbitrary choices from obscuring the topological complexity of classification. A universal relation for a class would provide one common target for every classification problem in that class.

This mission asks for a Lean formalization of Theorem 1.1 of Ruijun Wang, There is no universal $F_\sigma$ equivalence relation, arXiv:2610.31052v1. The paper proves a negative answer for equivalence relations whose graphs are countable unions of closed sets. The requested mission category is OpenProblem; the open task is the formalization of this known paper theorem, rather than a claim that the mathematical question remains unanswered.

The historical comparison is with the smaller class of relations whose graphs are countable unions of compact sets. Rosendal proved a universality theorem for that class and asked whether its bounded-difference benchmark also captures all $F_\sigma$ relations. The source introduction and bibliography identify Proposition 19 and Problem 28 of his paper as the relevant result and question. The timeline is: Rosendal's compact-cover universality result and question in 2005; the question's subsequent appearance in the descriptive-set-theory literature cited in Wang's introduction; and Wang's 22 October 2026 preprint giving the stronger nonuniversality theorem targeted here.

Spaces, relations, and measurable reductions

A Polish space is a topological space admitting a complete separable metric compatible with its topology. An equivalence relation $F$ on a space $Y$ is reflexive, symmetric, and transitive. Its graph is the subset of $Y\times Y$ consisting of pairs $(y,y')$ with $yFy'$. A set is $F_\sigma$ when it is a countable union of closed sets. For relations this condition refers to the graph in the product topology.

Given equivalence relations $E$ on $X$ and $F$ on $Y$, a reduction is a function $f:X\to Y$ satisfying

$$\forall x,x'\in X,\qquad xEx'\ \Longleftrightarrow\ f(x)Ff(x').$$

No injectivity on points is required. A Borel measurable reduction has Borel preimages of open sets. A Baire measurable reduction has preimages of open sets with the Baire property: each such preimage differs from an open set by a meager set. A meager set is a countable union of nowhere dense sets. These conventions follow Sections 2.1–2.3 of the source.

The domain of the main construction is the real Hilbert space $\ell_2$ of square-summable real sequences, with its norm topology. For a real linear subspace $H\subseteq\ell_2$, its coset equivalence relation is

$$xE_Hx'\quad\Longleftrightarrow\quad x-x'\in H.$$

The subspace need not be closed, complete, or Polish in its inherited topology. If $H$ is $F_\sigma$, its coset graph is also $F_\sigma$ because subtraction is continuous.

Formalization targets

The main goal is the full existence assertion of Theorem 1.1:

$$\begin{gathered} \text{for every Polish }Y\text{ and every }F_\sigma\text{ equivalence relation }F\text{ on }Y,\\ \exists\text{ a real linear subspace }H\subseteq\ell_2\text{ such that}\\ H\text{ is }F_\sigma,\quad E_H\text{ is }F_\sigma,\quad E_H\not\leq_{\mathrm{Baire}}F. \end{gathered}$$

The last clause excludes every Baire measurable reduction, with no auxiliary assumptions on its range or on the constructed subspace.

Two supporting targets accompany the goal. Lemma 2.4 says that a Baire measurable map from a Polish space to a second-countable space is continuous on some comeager $G_\delta$ subset of its domain. Here $G_\delta$ means a countable intersection of open sets, and comeager means that the complement is meager. The second target is the final clause of Theorem 1.1: no $F_\sigma$ equivalence relation on a Polish space is universal under Borel reducibility for all $F_\sigma$ equivalence relations on Polish spaces. Their exact declarations share the same definitions as the main target.

What completing the mission establishes

The result rules out a single $F_\sigma$ relation as a common Borel classification target for this entire class. Its main clause supplies an obstruction already among coset relations of real linear subspaces of one fixed Hilbert space. Thus the obstruction does not require varying the source among arbitrary Polish spaces or arbitrary kinds of equivalence relations.

The mathematical result is proved in the cited preprint. This draft supplies definitions and open Lean statements. Completing the mission means proving the submitted statements against those definitions using the supported Lean and Mathlib environment. Local compilation checks that the statements are well formed; the present sorry proof bodies do not constitute formal proofs. A completed development would also expose reusable interfaces for descriptive-set-theoretic reductions and coset relations.

Where the difficulty lies

An $F_\sigma$ graph has a closed cover, but those closed pieces need not themselves be equivalence relations. In particular, composing two pairs belonging to one piece need not stay in that piece. A proof cannot assume transitivity at each closed approximation merely because the union is transitive. Likewise, the compact-cover universality result does not automatically extend to arbitrary closed covers in noncompact Polish spaces. The source distinguishes these issues explicitly in its treatment of a fixed target.

The target also quantifies over Baire measurable reductions, which can be discontinuous on the ambient space. A proof limited to continuous maps would leave a weaker theorem. The continuity-on-a-comeager-set milestone records the precise regularity available without adding continuity as a hypothesis to the main goal.

Formalization scope

The shared namespace is NoUniversalFSigma. Real $\ell_2$ is Mathlib's lp (fun _ : ℕ => ℝ) 2; linear subspaces are Submodule ℝ RealL2, and equivalence relations are Setoid. The definition of $F_\sigma$ uses a sequence indexed by all natural numbers, including zero. Baire measurability uses Mathlib's Baire-property predicate on open preimages. Borel measurability refers explicitly to the Borel sigma algebra of the given topology, so an arbitrary measurable-space instance cannot change the assertion.

The main theorem permits targets in any universe and includes empty targets. The nonuniversality target quantifies over ordinary Type Polish source and target spaces, sufficient for the usual presentations of Polish classification problems. Its universal quantifier includes $\ell_2$ itself. Neither target assumes a chosen closed cover, a rank bound, or the desired obstruction. Restricting the source to a finite-dimensional space, requiring the subspace to be closed, or excluding only continuous reductions does not meet the goal.

Contributions may develop the source's intermediate constructions and the necessary category, Hilbert-space, and ordinal machinery, or give another proof of the same statements. The supporting declarations can be reused independently; the acceptance boundary remains the stated quantifiers and conclusions without additional hypotheses.

Selected references

• Ruijun Wang, There is no universal $F_\sigma$ equivalence relation, arXiv preprint arXiv:2610.31052v1, 2026. Version and source; full text. Main target: Theorem 1.1; preparatory target: Lemma 2.4; definitions: Sections 2.1–2.3.
• Christian Rosendal, Cofinal families of Borel equivalence relations and quasiorders, Journal of Symbolic Logic 70(4), 1325–1340, 2005, Proposition 19 and Problem 28. Published paper. These are historical context, not additional unformalized assumptions of the goal.

Overview

This project gives a completed Lean 4/mathlib formalization of the main theorem of A uniform bound of five for Diophantine tuples in imaginary quadratic integer rings by Zrinka Franušić and Tomislav Pejković.

A Diophantine tuple, or $D(1)$-tuple, in a commutative ring with identity is a finite set of nonzero elements such that $ab+1$ is a square in the ring whenever $a$ and $b$ are distinct elements of the set. The theorem gives a uniform upper bound of five for such tuples in the full rings of integers of all imaginary quadratic number fields.

Mathematical setting

Let $K$ be an imaginary quadratic number field, that is, an extension of $\mathbb Q$ of degree two that admits no embedding into $\mathbb R$. Let $\mathcal O_K$ denote its full ring of integers, consisting of the elements of $K$ that are integral over $\mathbb Z$.

A finite set $S\subseteq\mathcal O_K\setminus\{0\}$ is a $D(1)$-tuple if

$$\forall a,b\in S,\quad a\ne b\ \Longrightarrow\ \exists r\in\mathcal O_K,\quad r^2=ab+1.$$

The value $ab+1=0$ is allowed, with $r=0$. Requiring the square roots to lie in $K$ instead of $\mathcal O_K$ gives the same notion, since $\mathcal O_K$ is integrally closed in $K$.

Main theorem

For every imaginary quadratic number field $K$ and every $D(1)$-tuple $S$ in $\mathcal O_K$,

$$|S|\le 5.$$

Equivalently, $\mathcal O_K$ contains no $D(1)$-tuple with six elements.

Adžaga established a uniform bound of $42$. Cipu and Fujita established bounds of $24$ in 2024 and $22$ in 2026. Whether a $D(1)$-tuple with five elements exists in the ring of integers of any imaginary quadratic field remains an open question (Dujella, Problem 1.11).

Scope

The theorem concerns the full ring of integers in every case. In particular, for a positive squarefree integer $d\equiv3\pmod4$, it applies to $K=\mathbb Q(\sqrt{-d})$, whose ring of integers strictly contains $\mathbb Z[\sqrt{-d}]$. No further hypotheses are imposed on the entries.

Lean formalization

The formalization is complete. The main theorem has status Proved on Prove2Me. The formalization was completed on 24 October 2026. The Lean source repository contains the full source code and instructions for reproducing the verification.

The theorem card displays the formal statement with a by sorry placeholder; the accepted proof is stored separately and can be followed through its dependency graph.

The Lean 4 development D1Bound5 uses mathlib's full ring of integers 𝓞 K. Its main declaration is D1Bound5.main_statement, whose type is D1Bound5.MainStatement.

The proposition D1Bound5.MainStatement quantifies over types K with instances Field K, NumberField K and NumberField.IsTotallyComplex K, subject to Module.finrank ℚ K = 2, and over finite sets A : Finset (𝓞 K). It asserts A.card ≤ 5 whenever D1Bound5.IsD1 A holds. The definition D1Bound5.IsD1 requires every member to be nonzero and, for distinct members x and y, a witness r in the same ring satisfying r * r = x * y + 1.

Reference and source code

Zrinka Franušić and Tomislav Pejković, A uniform bound of five for Diophantine tuples in imaginary quadratic integer rings, preprint, 15 October 2026.

Lean formalization

Motivation

Linearised Einstein–Maxwell equations around charged black-hole backgrounds are the starting point of perturbation theory for the Reissner–Nordström and Kerr–Newman families (Newman et al., 1965; see e.g. Giorgi, arXiv:2002.07228). Every such analysis silently uses two facts: that the backgrounds solve the coupled equations, and that the linearised operator is the derivative of the nonlinear residual. In a proof assistant neither is free. This mission records machine-checked certificates for the two backgrounds and an off-shell theorem identifying explicit linearised operators with true derivatives.

Setting

Coordinates on an open set $U\subseteq\mathbb R^4$ are $x=(x^0,x^1,x^2,x^3)$. A metric field $g$ and an inverse field $g^{-1}$ are $4\times4$ arrays of real functions with $g^{-1}g=1$ on $U$; a two-form field $F$ is an array $F_{ab}$. With the coordinate partial derivatives $\partial_a$, Christoffel symbols $\Gamma^a_{bc}$ and Ricci tensor $R_{ab}$ built from $g$ and the given $g^{-1}$, the three residuals are

$$E_{ab}=R_{ab}-\tfrac12 g_{ab}R-2S_{ab},\quad S_{ab}=F_{ac}g^{cd}F_{bd}-\tfrac14 g_{ab}F_{cd}F^{cd},$$ $$J^b=\partial_aF^{ab}+\Gamma^a_{ak}F^{kb}+\Gamma^b_{ak}F^{ak},\qquad H_{abc}=\partial_aF_{bc}+\partial_bF_{ca}+\partial_cF_{ab}.$$

An Einstein–Maxwell certificate on $U$ records: $U$ open and nonempty, $g$ symmetric, $g^{-1}$ a true inverse, all components $C^\infty$, $F$ antisymmetric, $g$ Lorentzian, and $E=0$, $J=0$, $H=0$ on $U$. A family $(g_\varepsilon,g^{-1}_\varepsilon,F_\varepsilon)$ on an open $W\subseteq\mathbb R\times\mathbb R^4$ is admissible (FamilyData) when $(\varepsilon,y)\mapsto g_\varepsilon(y),F_\varepsilon(y)$ are jointly $C^\infty$ and $g^{-1}_\varepsilon g_\varepsilon=1$ on $W$; no symmetry, signature, antisymmetry or field equation is assumed. Its tangent $(h,f)$ is the $\varepsilon$-derivative at $0$.

Formalization targets

Goal

For every admissible family with tangent $(h,f)$ and every $x$ with $(0,x)\in W$,

$$\frac{d}{d\varepsilon}\Big|_0E_{ab}(g_\varepsilon,g^{-1}_\varepsilon,F_\varepsilon)(x)=LE_{ab}(g_0,g^{-1}_0,F_0;h,f)(x),$$

and likewise $\frac{d}{d\varepsilon}|_0J^b=LJ^b$, $\frac{d}{d\varepsilon}|_0H_{abc}=LH_{abc}(f)$, where $LE$, $LJ$, $LH$ are explicit finite expressions in the background, $h$, $f$ and their first and second coordinate derivatives. The statement is off shell.

Milestones

The twelve milestones above: the two background certificates and two parameter specialisations; realisation of arbitrary directions and linearity; covariance and certificate transport; parameter tangents of both families; coordinate and potential gauge directions; and one direction on which $LE$ does not vanish.

Significance

The goal makes the linearised operators usable without trusting a hand derivation: any statement about $LE,LJ,LH$ is a statement about true derivatives of the registered residuals. The background certificates cover every real parameter in the stated domains (Kerr–Newman for $M>0$ and all real $a,Q$), and the parameter-tangent and gauge milestones check the operator against the expected zero directions, while milestone 12 rules out a trivially vanishing operator. The background solutions are classical; what is new here is their machine-checked form and the off-shell derivative theorem in this coordinate setting.

Difficulty

The residuals involve the inverse metric and second derivatives of the metric. Differentiating in $\varepsilon$ requires interchanging $\partial_\varepsilon$ with coordinate derivatives and differentiating the inverse family; pointwise differentiability in $\varepsilon$ is not enough, and an operator merely named "derivative" would make the goal vacuous.

Formalization scope

Lean 4 with Mathlib (0df444a3…), autoImplicit off; smoothness is ContDiffOn ℝ ∞ ($C^\infty$, not analytic). The pinned Mathlib has no Lorentzian Levi-Civita connection or Ricci tensor, so the coordinate definitions (partial derivative, Christoffel symbols, Ricci tensor, residuals) are a registered local definition layer from the earlier Atlas releases, reused unchanged. The operators $LE,LJ,LH$ are independently specified using finite sums and coordinate derivatives; they are not defined as parameter derivatives of the nonlinear residuals. The goal proves that these expressions equal the genuine parameter derivatives. Not included: nonlinear integrability of tangents, new exact solutions, Newman–Penrose reductions, stability, gauge classification, horizons or global structure. The coordinate family $x\mapsto x+\varepsilon\xi(x)$ used for the gauge milestone is a local family of coordinate maps, not a flow of $\xi$.

Selected references

• T. Müller, F. Grave, Catalogue of Spacetimes, arXiv:0904.4184 (v3 used locally). https://arxiv.org/abs/0904.4184
• E. Giorgi, arXiv:2002.07228 (Kerr–Newman in Boyer–Lindquist form; review-provided, not opened by the executor). https://arxiv.org/abs/2002.07228
• E. T. Newman, E. Couch, K. Chinnapared, A. Exton, A. Prakash, R. Torrence, Metric of a rotating, charged mass, J. Math. Phys. 6 (1965) 918 (link not re-opened this round).
• H. Reissner, Ann. Phys. 355 (1916) 106; G. Nordström, Proc. KNAW 20 (1918) 1238 (historical attribution; not transcribed).

Motivation

Sequential packing matters when an item's size is known statistically before placement but revealed only afterward. A connection request has uncertain bandwidth, a shipment has uncertain final weight, and a virtual machine has uncertain resource use. In each example, exceeding capacity can have a separate cost from opening another container. Perez-Salazar, Singh, and Toriello formulate this as adaptive bin packing with overflow and analyze policies that respond to observed sizes without seeing future outcomes (paper, §1.1–1.2).

The paper's i.i.d. result gives a fixed numerical guarantee for a simple online rule, even against the best adaptive policy that knows how many items will arrive. This mission formalizes that theorem and the policy comparisons on which its statement depends. The source is the pinned preprint arXiv:2007.11532v2; all page and result numbers below refer to that version.

Setting

There are $n$ items with independent, nonnegative random sizes $X_1,\ldots,X_n$. Each bin has unit capacity. Before placing item $i$, a policy knows its distribution and the realized sizes and assignments of earlier items, but it does not know $X_i$. Its choice is irrevocable. A bin becomes unavailable after its accumulated load becomes strictly greater than one. Opening a bin costs one, and breaking a bin adds penalty $C\ge1$. A policy here is deterministic, nonanticipative, measurable, and feasible: it never puts an item into an already overflowed bin (paper, §1.2 and §3.1).

Let $N_P$ count bins opened by policy $P$, and let $O_P$ count bins whose final load exceeds one. The policy's objective is

$$\operatorname{cost}(P)=\mathbb E[N_P]+C\,\mathbb E[O_P].$$

For a bin with current load $S$, placing item $i$ incurs overflow risk $p_i(S)=\Pr(X_i+S>1)$. The risk of a bin is the sum of these quantities over items assigned to it. A policy is risk-budgeted at level $r$ if every bin's risk is at most $r$. These terms are properties of the realized history before each assignment, not substitutes for the actual count $O_P$.

Budgeted Greedy, the paper's Algorithm 1, uses risk budget $\gamma/C$ with $\gamma\ge1$. At a round it considers an opened bin if its load is at most one and the new item's risk would keep total risk within the budget. It uses an eligible bin if one exists and opens a new bin otherwise. The paper leaves ties arbitrary; the formal rule chooses the lowest indexed eligible bin. When an item has $\Pr(X_i>1)>\gamma/C$, it cannot fit the budget even in a fresh bin. The algorithm still opens a new bin for it, so a separate heavy-item case is needed in the performance theorem (paper, §3.2 and Theorem 4.4).

Formalization targets

The central target is Theorem 4.4, also stated in Theorem 1.2. For i.i.d. nonnegative items and $\gamma=\sqrt2$, Budgeted Greedy is an admissible policy and, for every admissible policy $P$,

$$\operatorname{cost}(\mathrm{BG}_{\sqrt2}) \le (3+2\sqrt2)\operatorname{cost}(P).$$

The comparison with every $P$ is deliberate. The paper explains that an exact minimizer need not exist for continuous distributions; its notation $\operatorname{Opt}$ includes arbitrarily good approximations. The universal inequality therefore expresses the same guarantee without presuming that an optimum is attained (paper, p. 8 and Theorem 4.4).

The milestone list follows the paper's stated intermediate results. Proposition 3.1 identifies expected broken-bin count with expected accumulated risk. Lemma 3.4 and Corollary 3.5 turn the risk budget into an expected cost bound. Theorem 4.1 states that every policy has a controlled-cost counterpart that isolates high-risk items and budgets every other bin. Lemma 4.3 compares the expected bin openings of Budgeted Greedy with all budgeted policies for i.i.d. items. The heavy-item estimates are taken directly from the proof of Theorem 4.4. An initial milestone states that the online algorithm actually induces a policy (paper, pp. 4, 8–14).

Significance

The theorem supplies an explicit bound for an online packing algorithm when overflow has a monetary penalty. Its comparator may adapt to past observations and know the finite horizon, so the guarantee concerns a strong benchmark rather than a fixed packing plan. The structural milestones are also useful separately: the risk identity describes how individual placement probabilities account for broken bins, while Theorem 4.1 connects arbitrary policies to the risk-budgeted class (paper, Theorem 1.1, Proposition 3.1, Theorem 1.2).

The mathematical result is proved in the cited paper. This mission supplies Lean statements and definitions but does not claim machine-checked proofs of the milestones or the goal. A completed development would give a reusable interface for adaptive bin assignments, product laws for independent sizes, measurable policy costs, and per-bin risk accounting. Those definitions could support later statements about other distributions or packing rules from the same paper.

Difficulty

An item's overflow event is revealed after its bin has been chosen, while the bin choice can depend on all earlier sizes. Consequently, multiplying an unconditional overflow probability by a simple occupancy count does not directly give the cost: the assignment and current load are random. The risk identity must account for this dependence. The comparison with an arbitrary adaptive policy is harder because that policy can interleave work across bins, whereas Budgeted Greedy follows a narrower budget rule. The i.i.d. assumption supports the expected-opening comparison, but does not make the random policy histories disappear (paper, §§3–4).

Formalization scope

Items and bins are Fin n, indexed from zero. This provides at most $n$ bins, enough for a sequence of $n$ items. The item laws form a product probability measure on real-valued outcome vectors; nonnegativity is a separate support hypothesis. In the i.i.d. statements every coordinate uses one law $\nu$. A bin breaks at load $>1$, not at equality. The algorithm's risk test uses the exact real probability of $X_i>1-S$. All costs are integrals of the bin-opening and bin-breaking counts, rather than definitions in terms of risk.

The model makes policy measurability explicit so these real integrals do not acquire Lean's default value for nonintegrable or nonmeasurable inputs. Policy feasibility is required on every outcome vector, including vectors outside the nonnegative support; this is a chosen extension of the paper's reachable-history convention. The model also fixes a lowest-index tie break. Algorithm 1 line 3 omits the load-at-most-one test stated in its preceding prose; the formal algorithm includes it. Lemma 4.3 is stated under $\Pr(X_1>1)\le\gamma/C$, the condition needed for Budgeted Greedy itself to be budgeted and the case in which the paper uses that lemma. These choices are disclosed in the item descriptions and moderation notes (paper, pp. 9–10, 13–14).

The representation must retain the two actual random counts $N_P$ and $O_P$; defining cost from the risk sum would erase Proposition 3.1's content. The finite indexing, product measure, measurable sets, and Bochner integrals use Mathlib. Useful contributions include proofs of policy measurability, the per-bin expectation identity, the risk-budget comparisons, and the final approximation bound.

Selected references

• S. Perez-Salazar, M. Singh, and A. Toriello, Adaptive Bin Packing with Overflow, Mathematics of Operations Research, 2022. Formalization source: arXiv:2007.11532v2, pp. 2–14 and 33–35.

Motivation

Linear perturbations of a rotating, charged black hole are governed, after a mode decomposition, by a coupled first-order system for the linearised Weyl and Maxwell quantities. For the uncharged Kerr solution these equations decouple into the Teukolsky equation, and mode stability was proved by Whiting (1989) through an integral transform. For the charged Kerr–Newman family the Weyl and Maxwell perturbations stay coupled, and no separation of variables was available for decades; Giorgi (2020, arXiv:2002.07228) obtained coupled Teukolsky-type and Regge–Wheeler-type systems but not a separated form. Hintz (2026, arXiv:2609.33661) found a matrix integrating factor that removes the same-chirality coefficient A from the first-order derivatives and makes the remaining coefficient matrix split into a radial and an angular part; from this he derives separation of variables and mode stability for subextremal Kerr–Newman black holes. The algebraic core of that derivation is a chain of explicit, local, coordinate-level transformations between first-order systems on the exterior region. This mission formalises that chain.

Prior formalised material on this platform: the Boyer–Lindquist Kerr vacuum certificate and the Exact Vacuum Atlas I/II coordinate certificates and transports (same author, same environment). None of them touch perturbation theory; this mission starts a new, independent layer and does not depend on them.

Setting

Fix subextremal Kerr–Newman parameters $M>0$, $a\in\mathbb R$, $Q\neq 0$ with $a^2+Q^2<M^2$ (Lean: Hintz2026.SubextremalKN). Put $\Delta(r)=r^2-2Mr+a^2+Q^2$, $r_+=M+\sqrt{M^2-a^2-Q^2}$, and work on the open set

$$U=\{(r,\theta)\in\mathbb R^2:\ r>r_+,\ 0<\theta<\pi\}$$

(Lean: U p, with x 0 = r, x 1 = θ). Write $\bar\rho=r+ia\cos\theta$, $\bar\rho^*=r-ia\cos\theta$. Fix a frequency $\omega\in\mathbb R$ and an azimuthal number $m$ (kept real in Lean; integrality is not used by any statement here), and put $K=-(r^2+a^2)\omega+am$, $\hat Q=-a\omega\sin\theta+m/\sin\theta$.

The first-order operators of the Newman–Penrose formalism in these coordinates are, for a label $j$,

$$\mathcal D_j=\partial_r+\tfrac{iK}{\Delta}+j\tfrac{\Delta'}{\Delta},\qquad \mathcal L_j=\partial_\theta+\hat Q+j\cot\theta,$$

with daggers $\mathcal D_j^\dagger,\mathcal L_j^\dagger$ obtained by $K\mapsto -K$, $\hat Q\mapsto-\hat Q$. Partial derivatives are coordinate-slice derivatives (Lean: cpd), and all fields are complex-valued functions on $\mathbb R^2$ that are $C^\infty$ on $U$.

System (1) (positive spin) is the system (1a)–(1d) of Hintz for the four rescaled mode quantities $(\psi_2,\psi_1,k,s)$; the negative-spin system is obtained from it by the replacement rules stated in the paper (Lean: res1a–res1d, res1aN–res1dN, each the difference "left side minus right side"). The chiral variables (3) are

$$y_\pm^{(+)}=\Delta^{5/4}\sqrt{\sin\theta}\begin{pmatrix}\psi_2\pm i\Delta^{-1/2}\psi_1\\ -2Q(k\pm i\Delta^{-1/2}s)\end{pmatrix},\qquad y_\pm^{(-)}=\Delta^{-3/4}\sqrt{\sin\theta}\begin{pmatrix}\psi_{-2}\mp i\Delta^{1/2}\psi_{-1}\\ 2Q(n\mp i\Delta^{1/2}\ell)\end{pmatrix}.$$

System (4) is $(\sqrt\Delta\,\partial_r\mp i\partial_\theta\mp A)y_\pm=(c^{(\varsigma)}I\mp B^{(\varsigma)})y_\mp$ with the explicit $2\times2$ matrices $A$, $B^{(\varsigma)}$ and scalar $c^{(\varsigma)}$ of the paper (Lean: A, Bmat, cscalar; $\varsigma=\pm1$ is the spin label). The integrating factor is the matrix $X(r,\theta)$ of equation (5), with $\det X=Q^2-M^2$, and system (7) is

$$(\sqrt\Delta\,\partial_r-i\partial_\theta)z_+=C\,z_-,\qquad(\sqrt\Delta\,\partial_r+i\partial_\theta)z_-=\operatorname{adj}(C)\,z_+,$$

for $z_+=\operatorname{adj}(X)y_+$, $z_-=X^*y_-$ and $C=\det X\cdot X^{-1}(cI-B)(X^*)^{-1}$. The paper's separation statement is that $C=R(r)+i\Theta(\theta)$ with four explicit coefficient functions $R_0,R_1,\Theta_0,\Theta_1$.

Formalization targets

Goal — local equivalence of the original and the transformed systems

$$\text{for all }C^\infty\text{ fields and all }x\in U:\qquad \text{(1) holds at }x\iff\text{(7) holds at }x\text{ for }(z_+,z_-)=T(\psi),$$

for both spins (Lean: Hintz2026.main_pos, Hintz2026.main_neg, with the on-$U$ forms main_pos_on_U, main_neg_on_U). The composite transformation is explicitly invertible on $U$: first recover $y_+=(Q^2-M^2)^{-1}Xz_+$ and $y_-=(X^*)^{-1}z_-$, then apply the inverse chiral map invPos or invNeg. The goal leaves the frequency and azimuthal parameters free, assumes nothing beyond subextremality and $C^\infty$ regularity on $U$, and does not assert anything at the horizon or at infinity.

Milestones

1. The matrix integrating factor: $(\sqrt\Delta\partial_r-i\partial_\theta)X=AX$ and the companion equation for $(X^*)^{-1}$ (Dminus_X_eq_AX, Dplus_XstarInv_eq).
2. Residual identities and solution correspondence for the integrating factor (Dm_Xv_sub_AXv, Dp_Yv_add_AYv, Dm_zero_iff_Xv_residual_zero_on_U, …).
3. The coefficient separation $C=R(r)+i\Theta(\theta)$ verified entrywise against the paper's four coefficients (Cmat_eq_Csep), and $\operatorname{adj}C=R^{\mathsf T}-i\Theta$.
4. Local equivalence (4) ⟺ (7) for arbitrary $C^\infty$ fields (system4_iff_system7).
5. The eight chiralisation identities expressing the residuals of (4) for the chiral variables as an explicit invertible combination of the residuals of (1), for both spins (ident_*, identN_*), and the equivalence (1) ⟺ (4) (sys1_iff_sys4_pos, sys1_iff_sys4_neg).

Significance

The chain (1)→(4)→(7) is the step on which the rest of Hintz's argument rests: once $C$ is known to separate, the angular operator can be diagonalised and the radial problem reduces to a scalar second-order equation, which is where the mode-stability argument lives. The transformations are algebraic but far from trivial to check by hand — each entry of $C$ is a rational-trigonometric expression in $r$, $\theta$, $\omega$, $m$ and the three parameters, and the cancellation of all mixed $(r,\theta)$ terms is the content of the separation claim.

Everything in this mission is already proved in the paper. What the mission adds is a machine-checked verification of the explicit coefficient data and of the transformation identities for arbitrary $C^\infty$ fields, with the regularity and domain hypotheses made explicit. All targets listed here already carry accepted proofs on this platform; the mission records them as a public, reviewable dependency tree. Not formalised here: the derivation of (1) from the Einstein–Maxwell equations, the angular eigenvalue problem, the radial reduction, the Whiting-type transform, and mode stability itself.

Difficulty

The naive approach — substituting the chiral variables into (4) and comparing with (1) term by term — produces hundreds of rational terms with half-integer powers of $\Delta$ and of $\sin\theta$. The first-order terms match by construction; the difficulty is that the zeroth-order terms only match after using $\sqrt\Delta^{\,2}=\Delta$, $\cos^2\theta=1-\sin^2\theta$ and the specific values of $A$, $B$, $c$. A second trap is in the negative-spin system: the replacement rules put sign changes inside the operators, and an identity proved for a "simplified" version of the rules would be an identity about a different system. The formalisation keeps the rules literally and derives linearity separately.

Formalization scope

Coordinates are $\mathbb R^2$ with $x\,0=r$, $x\,1=\theta$; no manifold, tetrad or spacetime object is defined. Derivatives are coordinate-slice derivatives (deriv along one coordinate), and the final unknown-field interfaces use ContDiffOn ℝ ∞ _ (U p); auxiliary statements may require only coordinate-slice differentiability, and explicit coefficient statements retain the stronger analytic order ω. Real exponents $\Delta^{5/4}$, $\Delta^{-3/4}$ are Real.rpow; $\sqrt{\ }$ is Real.sqrt. All coefficient matrices are explicit Matrix (Fin 2) (Fin 2) ℂ; the separated form $R+i\Theta$ is an independent explicit definition, not derived from $C$, so Cmat_eq_Csep is a genuine check. The spin label is a real parameter $\varsigma$ in the definitions of $B$ and $c$; the two spins are the instances $\varsigma=\pm1$, each proved separately with its own chiral variables.

Nothing here is vacuous: the systems are Props about arbitrary fields, the residuals are explicit, and the domain $U$ is nonempty and open. A reader can check that the Lean definitions reproduce the paper's formulas from the transcript of the paper's equations included with the source.

Reusable beyond this mission: the slice-derivative calculus (cpd, Dm, Dp, product and sum rules), the integrating-factor layer (X, A, invertibility, residual identities) and the prefactor calculus for $\Delta^{q}\sqrt{\sin\theta}$.

Selected references

• P. Hintz, Perturbations of Kerr–Newman black holes: separation and mode stability, arXiv:2609.33661 (2026). https://arxiv.org/abs/2609.33661
• E. Giorgi, Electromagnetic-gravitational perturbations of Kerr–Newman spacetime: the Teukolsky and Regge–Wheeler equations, arXiv:2002.07228 (2020). https://arxiv.org/abs/2002.07228
• B. F. Whiting, Mode stability of the Kerr black hole, J. Math. Phys. 30 (1989) 1301–1305. https://doi.org/10.1063/1.528308
• T. Adamo, E. T. Newman, The Kerr–Newman metric: a review, Scholarpedia 9 (2014), arXiv:1410.6626. https://arxiv.org/abs/1410.6626

Motivation

A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry; every totally bounded metric space is plastic (Freudenthal–Hurewicz 1936), and Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic. For the sequence space c₀, Leo (2022) proved plasticity of the unit ball under the extra hypothesis that the inverse map is continuous; the project's earlier results, all unpublished, covered c₀(Γ) itself without that hypothesis (the earlier c0 mission), smooth strictly convex blocks of any finite dimension and strictly convex planes, with scalars beside them, ℓ¹ₙ blocks of bounded dimension, and polygonal planes, also beside discs. This mission formalizes a proof that the closed unit ball of every c₀ sum of real spaces of dimension at most two is plastic, for arbitrary index sets and arbitrary norms on the blocks, together with the two-space statement that every nonexpansive bijection between the balls of two such sums is an isometry. The results come from an unpublished research project on the plasticity problem.

Setting

For a family $(E_i)_{i\in I}$ of real normed spaces, the $c_0$ sum $c_0(I;E_i)$ consists of the families $x=(x_i)$ with $x_i\in E_i$ and $\|x_i\|\to0$ along the cofinite filter, with the norm $\|x\|=\sup_i\|x_i\|$. Its closed unit ball is $B=\{x:\|x\|\le1\}$. The blocks here have dimension at most two: zero, the real line, or a real plane with any norm, whose unit ball may be a parallelogram, a polygon, a disc, or have flat edges and curved arcs in any combination, with no uniformity over $I$.

Target

$$\text{(CUB109)}\quad f\colon B_{c_0(I;E_i)}\to B_{c_0(K;E'_k)}\ \text{a nonexpansive bijection},\ \dim E_i,\dim E'_k\le2\ \Longrightarrow\ f\ \text{is an isometry.}$$ $$\text{(goal)}\quad \text{the closed unit ball of } c_0(I;E_i) \text{ is plastic whenever every } E_i \text{ has dimension at most two.}$$

For finite index sets the balls are finite-dimensional, and both statements are covered by Zavarzina's theorem for finite-dimensional targets (Ann. Funct. Anal. 9 (2018), Theorem 3.8); the content is the infinite case.

Significance

The result. It settles plasticity for all c₀ sums of blocks of dimension at most two. It gives the first infinite c₀ sums in which scalar coordinates sit beside polygons or other planes that are not strictly convex, and the first non-polygonal planes that are not strictly convex (a curved ball with two edges meeting at a corner, or with countably many extreme points). Its proof shows that nonexpansive bijections between such balls are block-diagonal linear isometries, with scalar blocks going to scalar blocks after each parallelogram plane is split into two scalar coordinates.

Formalizing it. The proofs exist only in the project's notes and were checked by AI referees; a machine-checked proof is the independent confirmation sought. Known inputs available in this environment through earlier missions are invariance of domain, the Freudenthal–Hurewicz theorem and Brouwer's fixed-point theorem; Baire's theorem, Krein–Milman and Mazur–Ulam are in Mathlib.

Difficulty

For infinite index sets the ball is not compact, its unit sphere has large flat faces, and no regularity of the inverse map is assumed. The planar geometry is the bulk: covers of a planar ball by three translates near corners where two edges meet, an extreme lens and a far-comparison estimate at extreme points where the norm is curved, and the linearization of an extreme-point correspondence between two different planes from a single radial inequality. The c₀ part must match blocks, exclude scalar coordinates that feed planar blocks, and exclude the collapse of a block by a two-lift argument.

Formalization scope

Real scalars, arbitrary index sets (no countability or nonemptiness assumed), arbitrary norms on the blocks. The $\ell_\infty$ sum is Mathlib's lp E ⊤; the c₀ sum is the submodule c0Sum E of it (definition Plasticity_C0Sum), with its subspace norm. "Dimension at most two" is Module.rank ℝ (E i) ≤ 2, which excludes infinite-dimensional blocks. The goal uses HasPlasticUnitBall (definitions Plasticity_Basic); the two-space theorem is stated for functions between the subtypes Metric.closedBall (0 : c0Sum E) 1, with LipschitzWith 1 and Function.Bijective.

Extremal graph counterexamples, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

Write $\operatorname{ex}(n,F)$ for the maximum number of edges in an $n$-vertex simple graph containing no subgraph copy of $F$, with value $0$ if there is no eligible graph; a copy is an injective edge-preserving map and need not be induced. For a finite family $\mathcal F$ of finite simple graphs, each encoded on $\{0,\ldots,q-1\}$ for its own $q\in\mathbb N$, let $E_{\mathcal F}(n)$ be the maximum edge count over simple graphs on $\{0,\ldots,n-1\}$ containing no copy of any member of $\mathcal F$, again taking $0$ for an empty collection. There exist a nonempty such family $\mathcal F$ and real constants $c,C>0$ such that every member is connected, bipartite, and not acyclic; for each $F\in\mathcal F$, $c n^{4/3}\le\operatorname{ex}(n,F)$ for all sufficiently large natural $n$, with a threshold that may depend on $F$; for every $n\in\mathbb N$ and every simple graph $G$ on $\{0,\ldots,n-1\}$ containing no copy of any member, $|E(G)|^{16}\le C n^{21}$; and for every $n\in\mathbb N$, $E_{\mathcal F}(n)^{16}\le C n^{21}$. These last two bounds use the same $C$ and include $n=0$. The conclusions also include $0<1/48$ and $21/16=4/3-1/48$, as equalities and inequalities of real numbers. No member $F\in\mathcal F$ and real constant $D>0$ satisfy $\operatorname{ex}(n,F)\le D E_{\mathcal F}(n)$ for all sufficiently large $n$. Moreover, the assertion that every nonempty finite family of finite simple graphs whose members each contain a cycle admits such a member and constant is false.

Additional targets:

• Asymptotic separation for a noncompact graph family.
• Failure of compactness for cyclic graph families.
• Two-degenerate graph with extremal exponent above 3/2.
• Failure of the bipartite degeneracy extremal bound.

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, J_CompactnessConjecture.json, J_TwoDegenerateGraphs.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

Multicolor triangle Ramsey numbers, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

For each $k\in\mathbb N$, let $R(k)$ be the infimum in $\mathbb N$ of the integers $n$ such that every labeling of the edges of the complete simple graph on $\{0,\ldots,n-1\}$ by $k$ colors has a monochromatic triangle; equivalently, no such labeling has every color graph free of a three-vertex clique. This is the least such $n$ when the set is nonempty, with infimum $0$ for an empty set. Both of the following hold: for every integer $k\ge 2$, $\left(\frac{1}{6e^{38}}\,\frac{k^{1/3}}{\log k}\right)^k\le R(k)$, where all quantities in the inequality are real; and $R(k)^{1/k}\to+\infty$ as $k\to\infty$, meaning that for each real $M$ there is $K\in\mathbb N$ such that $R(k)^{1/k}\ge M$ whenever $k\ge K$. The root sequence is defined also at $k=0$ using real division $1/0=0$, so that term equals $1$ and does not affect the limit.

Additional targets:

• Divergence of multicolor triangle Ramsey roots.
• Eventual logarithmic Ramsey coefficient bounds.
• Logarithmic Ramsey growth has order k log k.

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, I_MulticolorTriangleRamsey.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

Ehrhart volume inequality, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

Let $n$ be any positive natural number and $S\subseteq\mathbb R^n$ any convex compact set with nonempty interior. Write $V(S)$ for its Lebesgue measure converted from $[0,\infty]$ to a real number, and define its barycenter as $V(S)^{-1}\int_S x\,dx$. The conversion sends infinite measure to zero and real inversion is total, but these hypotheses make $V(S)$ finite and positive. If this barycenter is the zero vector and $\{z\in\mathbb Z^n:z\in\operatorname{int}S\}=\{0\}$, then $V(S)\leq(n+1)^n/n!$. The lattice condition says both that the origin lies in the interior and that no other integer vector does. The volume in this inequality is the real Lebesgue volume itself.

Additional targets:

• Existence of a centered body attaining the volume constant.
• Zero barycenter of the explicitly transformed standard simplex.
• Exact volume of the explicitly transformed standard simplex.

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, F_EhrhartVolumeInequality.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

Hardness of the closest vector problem, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

For every Boolean language $A$ of finite bit strings for which there exist a polynomial $P\in\mathbb N[X]$ and a deterministic polynomial-time Boolean verifier $V$ satisfying $A(x)=\mathrm{true}$ if and only if there is a bit-string certificate $c$ with $|c|\le P(|x|)$ and $V(x,c)=\mathrm{true}$, there exists a total deterministic polynomial-time map $f$ on bit strings sending every $x$ with $A(x)=\mathrm{true}$ into the following YES set and every $x$ with $A(x)=\mathrm{false}$ into the following NO set. An instance consists of a natural dimension $n>0$, an integer matrix $B\in\mathbb Z^{n\times n}$ with $\det B\ne0$, a target $t\in\mathbb Q^n$ all of whose coordinates are integers, and a rational radius $r>0$. It is in YES exactly when some $z\in\mathbb Z^n$ satisfies $\sum_{i=0}^{n-1}((Bz)_i-t_i)^2\le r^2$, and in NO exactly when every $z\in\mathbb Z^n$ satisfies $(n^{1/400}r)^2<\sum_{i=0}^{n-1}((Bz)_i-t_i)^2$. The sets consist of the exact encoded instance strings, formed by concatenating the encodings of $n$, $r$, the target coordinates in order, and the matrix entries in row-major order. Each scalar is encoded by taking its library natural-number code, applying the library's natural-number-to-bit-string encoding to get a word $w$, and prefixing $w$ with $|w|$ true bits followed by one false bit. Strings without such a valid encoded instance, and instances satisfying neither distance condition, are outside both sets; dimension one is included. Polynomial time is witnessed in the library's TM2 machine model, using its product encoding of Boolean lists for verifier input, its Boolean output encoding for the verifier, and identity encodings for the reduction's input and output.

Additional targets:

• NP-hardness of binary nearest codeword with gap n^(1/200).
• NP-hardness of feasible binary syndrome decoding with gap n^(1/200).
• NP-hardness of rational finite-p lattice distance with gap n^(1/(200p)).

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, H_GapCVP.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

Arithmetic formula lower bounds for the permanent, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

For every natural number $n\ge32$ and every finite arithmetic formula $f$ whose leaves are variables $x_{ij}$, $0\le i,j<n$, or arbitrary complex constants and whose binary operations are addition, subtraction, multiplication, and division, assume that every divisor subformula evaluates to a nonzero element of the fraction field of $\mathbb C[x_{ij}]$ and that the value of $f$ in this fraction field equals the polynomial $\operatorname{per}_n=\sum_{\sigma\in S_n}\prod_{i=0}^{n-1}x_{i,\sigma(i)}$ under the canonical inclusion. Then the number $V(f)$ of variable-leaf occurrences satisfies $n^4/(192\log_2 n)\le V(f)$, with both sides viewed as real numbers. Repeated occurrences are counted separately, constants contribute zero, and the leaves of both operands of each operation, including division, are counted. Nonzero divisors are required as rational functions, not at every numerical substitution.

Additional targets:

• Variable-leaf lower bound for division-free formulas computing the permanent.

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, C_PermanentFormulaLowerBound.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

Counterexamples to Connes rigidity, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

There exist a countable group $\Lambda$ and a sequence of countable groups $(\Gamma_n)_{n\in\mathbb N}$, indexed also at $n=0$, such that all of them are finitely generated and infinite, every conjugacy class $\{xgx^{-1}:x\in G\}$ of a nonidentity element in each such group $G$ is infinite, and every such group has property T. For every $n$, $L(\Gamma_n)$ is isomorphic to $L(\Lambda)$ as specified below, and for every $m,n$, including $m=n$, $L(\Gamma_m)$ is isomorphic to $L(\Gamma_n)$ in the same sense. If $m\ne n$, there is no group isomorphism $\Gamma_m\cong\Gamma_n$, and for every $n$ there is no group isomorphism $\Lambda\cong\Gamma_n$. For each group $G$ concerned, property T means that, for every complete complex inner-product space $H$ and every homomorphism $\pi:G\to U(H)$, if for every finite $K\subseteq G$ and every real $\varepsilon>0$ there is a vector $\xi\in H$ with $\|\xi\|=1$ and $\|\pi(g)\xi-\xi\|<\varepsilon$ for all $g\in K$, then there is a nonzero vector fixed by every $\pi(g)$. Here $L(G)$ is the double commutant, inside the bounded complex-linear operators on $\ell^2(G)$, of the left translations $(\lambda_g f)(h)=f(g^{-1}h)$, and $\tau_G(a)=\langle\delta_1,a\delta_1\rangle$. An asserted isomorphism of these tracial algebras is a complex $*$-algebra equivalence preserving $\tau$ such that both it and its inverse preserve every existing supremum of any set of self-adjoint idempotents, with projection order $q\le p$ defined by $qp=q$.

Additional targets:

• Two nonisomorphic finitely generated property T ICC groups with isomorphic tracial group algebras.

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, E_ConnesRigidity.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

A finitely presented non-sofic group, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

There exist a set $G$ and a group structure on $G$ such that $G$ has a finite presentation and is not sofic in the following precise sense: there are a finite subset $F\subseteq G$ and a real number $0<\varepsilon<1$ for which no positive integer $d$ and map $\sigma:G\to\operatorname{Sym}(\{0,\ldots,d-1\})$ with $\sigma(1)=\mathrm{id}$ simultaneously satisfy $d_H(\sigma(gh),\sigma(g)\sigma(h))<\varepsilon$ for every $g,h\in F$ and $1-\varepsilon<d_H(\sigma(g),\mathrm{id})$ for every $g\in F$ with $g\ne1$. Here $d_H(p,q)=|\{i:p(i)\ne q(i)\}|/d$ is normalized Hamming distance; $\sigma$ is defined on all of $G$ and is not assumed to be a homomorphism. The finite subsets in the defining sofic approximation property include the empty subset, and the permutation sets are required to be nonempty.

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, D_NonSoficGroup.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

Binary and spherical codes, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

For every real $\delta$ with $0<\delta<1/2$, the following strict inequality holds. Write $h(x)=-x\log_2x-(1-x)\log_2(1-x)$, with the total-real logarithm convention $\log_2 0=0$. Let $A(n,k)$ be the maximum cardinality of a finite subset of $\{0,1\}^n$ in which every two distinct words differ in at least $k$ coordinates, and put $R(\delta)=\limsup_{n\to\infty}\log_2 A(n,\lceil\delta n\rceil)/n$. Empty codes are permitted in the maximum; the $n=0$ sequence term is zero by total real division. Define $g(v)=h((1-\sqrt{1-v})/2)$ and $M(\delta)=\inf_{0\leq t\leq1-2\delta}\{1+g(t^2)-g(t^2+2\delta t+2\delta)\}$, a real infimum. Then $R(\delta)<M(\delta)$.

Additional targets:

• Binary-code rate is strictly below the classical entropy expression.
• Positive gap below the classical binary-code rate expression.
• Binary-code rate is bounded by the combined variational infimum.
• The combined variational rate is strictly below the defined MRRW rate.
• Positive gap below the defined MRRW binary-code rate.
• Binary-code rate bound and strict improvement of the MRRW rate.
• Finite spherical-code bounds and the closed hierarchy rate bound.
• Strict descent of spherical-code hierarchy rates and localized rates.
• Eventual kissing-number bound with exponent 0.39661.

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, B_BinaryCodes.json, B_SphericalCodes.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

High-dimensional sphere packing, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

For each natural number $d$, let $\mathcal F_d$ consist of complex-valued Schwartz functions on Euclidean $\mathbb R^d$ whose values and Fourier-transform values are real, with $\widehat f(\xi)\geq0$ for every $\xi$, $\widehat f(0)>0$, and $f(x)\leq0$ whenever $\|x\|\geq1$; radiality is not required. Put $q(f)=f(0)/\widehat f(0)$, $V_d=\pi^{d/2}/\Gamma(d/2+1)$, and $L_d=(V_d/2^d)\inf_{f\in\mathcal F_d}q(f)$, where the infimum is taken in $\mathbb R$. Put $A_d=\inf_{f\in\mathcal F_d}q(f)^{1/d}$, $B=\sqrt{e/(2\pi)}$, and $c=\tfrac12\log_2(2\pi/e)$. The assertion is the conjunction of the following ten claims: $A_d/\sqrt d\to1/\pi$; there exists a real sequence $u_d\to0$ such that $A_d=(1/\pi+u_d)\sqrt d$ for every $d>0$; $L_d^{1/d}\to B$; $(\log L_d)/d\to\tfrac12\log(e/(2\pi))$; there exists a real sequence $v_d\to0$ such that $L_d=(B+v_d)^d$ for all sufficiently large $d$; there exists a real sequence $\delta_d\to0$, nonnegative for every natural $d$, such that for all sufficiently large $d$ and every $f\in\mathcal F_d$, $(2^d/V_d)(B-\delta_d)^d\leq q(f)$; $c>0$; $0.604400544291677695341677307053<c<0.604400544291677695341677307054$; $(\log_2 L_d)/d\to-c$; and there exists a real sequence $w_d\to0$ such that $L_d=2^{-(c+w_d)d}$ for all sufficiently large $d$. Each limit is along natural dimensions tending to infinity, and the four existentially quantified error sequences need not coincide. The sequences are defined also at $d=0$ using total real operations, in particular $0^{-1}=0$ and division by zero equal to zero; the displayed $1/d$ powers denote those real powers.

Additional targets:

• Exact root limit of the full Cohn–Elkies program.
• Exact binary logarithmic rate of the full Cohn–Elkies program.
• Sphere-packing density bound with a vanishing root error.

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, A_SpherePacking.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

Motivation

The Angel problem asks whether bounded movement can overcome an adversary that destroys one square per turn on an infinite chessboard. It is a question about strategies for arbitrarily long play, rather than about finding a path through one fixed configuration. The Devil may act anywhere on the board, including far ahead of the Angel. The movement range therefore has to be compared with a changing obstacle set and with an opponent that observes earlier moves.

This mission collects the complete classification for natural-number powers in one formal development. The power-one loss is the known Berlekamp king-capture result described in Kutz's 2004 thesis, Section 1.1. The power-two win is Mathe's Theorem 4.6 (2007). Higher powers and the exact threshold are consequences of these published results and the movement rules. This is formalization of known mathematics; it does not propose a new solution to an open problem.

Setting

A square is a point of the integer lattice $\mathbb Z^2$. The Angel starts at the origin. Its power is a natural number $p$, including zero. A legal jump changes each coordinate by at most $p$ in absolute value. Intermediate squares impose no restriction, and zero-length moves are allowed. Thus power one has the movement range of a chess king, while power zero cannot change position.

The ordinary Devil moves first in every round. It chooses at most one square to burn, or passes. A burned square remains burned. Repeated choices are allowed and do not destroy additional squares. Naming the Angel's currently occupied square is permitted; the loss condition is checked at the Angel's subsequent landing. The Angel loses if its destination is burned or its displacement exceeds its power.

A strategy uses only the finite history available at the time of the move. A Devil strategy receives the visited positions. An Angel strategy receives these positions and the Devil actions, including the action just taken in the current round. Every pair of strategies defines a play by recursion. Write $\operatorname{Survives}(p,A,D)$ when all rounds of this play have legal, unburned landings, and define

$$\operatorname{AngelWins}(p)\;\Longleftrightarrow\;\exists A\;\forall D,\ \operatorname{Survives}(p,A,D).$$

Formalization targets

The mission's main theorem is the exact classification

$$\forall p\in\mathbb N,\qquad \operatorname{AngelWins}(p)\;\Longleftrightarrow\;2\le p.$$

Its two principal outcomes are

$$\exists D\;\forall A,\quad \neg\operatorname{Survives}(1,A,D),$$

and

$$\forall p\in\mathbb N,\quad 2\le p\ \Longrightarrow\ \operatorname{AngelWins}(p).$$

The first statement supplies one Devil strategy defeating every power-one Angel, rather than an opponent chosen separately after seeing a complete Angel play. Likewise, the Angel's winning strategy is chosen before the opposing Devil strategy. All these statements use the same game definition.

The source milestones retain the original Nice Devil reduction and escape theorem, add Mathe's power-two theorem explicitly, and include the king-capture result from Kutz Section 1.1. A Nice Devil protects the origin and every square within movement range of any visited position other than the most recent position. The corresponding Angel objective includes leaving every finite box. This restricted opponent is an intermediate target; the headline classification concerns the ordinary, unrestricted Devil. Monotonicity and the higher-power corollary are available in the linked theorem dependency graph without attributing invented theorem numbers to either source.

Significance

The classification identifies the exact integer threshold: one square of movement in each coordinate is insufficient, whereas two suffice. It distinguishes unlimited survival from success for a fixed number of rounds. The lower endpoint is covered as well, because the formal parameter is a natural number rather than a strictly positive integer.

The formal development makes the quantifier order, observation rules, and geometric assumptions inspectable. The classification and both principal outcomes already have machine-checked proofs. The repository audit records 228 checked local theorems and six accepted extension submissions. Its classification dependency graph contains 37 nodes, 66 edges, and zero open leaves. These are verification results, not independent peer review or a new mathematical publication. The mission now presents this completed body of work as one navigable result.

Difficulty

A finite simulation cannot establish survival against every opponent forever. Conversely, failure of several candidate Angel strategies does not establish a uniform winning Devil strategy. Finite and infinite play must be related without reversing the strategic quantifiers. The geometric statements also have to constrain the evolving play, rather than describe only a static drawing. For the king-capture result, local boundary restrictions must remain valid after every legal move; for the power-two result, the source's confinement and escape assertions must refer to the same operational game.

Formalization scope

The implementation uses integer pairs, finite histories, optional Devil actions, finite sets, and recursion on natural numbers. Lean 4.33.1 and the pinned Mathlib revision match the platform environment. The closed local entry point is Solutions.PowerClassification; Solutions.Completed retains the original Mathe assembly. The definitions do not assume a winning strategy or restrict the headline game to a finite board.

The king-capture implementation uses deliberately loose radius-100 constants for an internal confinement argument. It does not claim an optimal capture time or a formalization of the smallest board illustrated by the source. Fractional speeds and Devils burning multiple squares per turn are outside this mission. Reusable material includes finite-game determinacy, finite-survival compactness, journey reduction, connected-square boundary estimates, and strategy monotonicity. Independent reproduction and documentation improvements are welcome; there is no remaining open proof obligation for the stated classification. Platform reference mirrors containing sorry are kept separate from the closed local proof library, whose audited dependencies contain only the standard Lean axioms.

Selected references

• Martin Kutz, The Angel Problem, Positional Games, and Digraph Roots, PhD thesis, Saarland University, 2004, Chapter 1, Section 1.1, pages 2–3, Figures 1–3. Thesis.
• Andras Mathe, The Angel of power 2 wins, Combinatorics, Probability and Computing 16 (2007), 363–374, Theorems 2.7, 4.5 and 4.6. DOI.

Continuous colorings of lattice actions

A graph homomorphism sends vertices of one graph to another while preserving adjacency. Requiring this map to be continuous makes graph coloring sensitive to topology: each color must occupy an open and closed region. For integer lattice actions, the resulting questions connect finite graph structure with continuous dynamics. The results considered here give an algebraic sufficient condition on a finite target graph that works in every finite lattice dimension. They are Theorem 1.4 and Proposition 7.1 of Ruijun Wang's Continuous graph homomorphisms of higher dimensional abelian group actions, a 2026 research preprint.

Actions, graphs, and reduced walks

Fix an integer $d\ge1$. The integer lattice is $G=\mathbb Z^d$, with standard generators $e_i$. Each generator has one coordinate equal to one and all other coordinates zero. An action of $G$ on a space $X$ assigns maps $x\mapsto g\cdot x$ satisfying $0\cdot x=x$ and $(g+h)\cdot x=g\cdot(h\cdot x)$. A continuous action uses the discrete topology on $G$. It is free when $g\cdot x=x$ implies $g=0$.

A Polish space has a topology induced by a complete separable metric. It is zero-dimensional when its topology has a basis of clopen sets, meaning sets that are both open and closed. The standard Schreier graph on $X$ joins $x$ to $e_i\cdot x$ for each generator, with adjacency understood symmetrically.

Let $H$ be a finite simple graph on a vertex set $V$, equipped with the discrete topology. A continuous homomorphism is a continuous function $c:X\to V$ such that

$$H.\operatorname{Adj}(c(x),c(e_i\cdot x)) \quad\text{for every }x\in X\text{ and }i.$$

Write $\operatorname{UniversalTarget}(d,H)$ when such a map exists for every free continuous lattice action on every zero-dimensional Polish space.

A closed walk starts and ends at the same vertex, and its length counts edges. Repetitions are allowed. The reduced homotopy group $\Pi_1^*(H,b)$ identifies based closed walks under cancellation of a spur and cancellation of a closed four-walk, with these relations compatible with concatenation. Its identity is the constant walk. These conventions agree with Section 2.

Formalization targets

Theorem 1.4 assumes an odd closed walk whose reduced class has trivial square:

$$\bigl(\exists b\in V,\ \exists\gamma:b\leadsto b,\quad |\gamma|\text{ odd},\quad[\gamma]^2=1\bigr) \Longrightarrow \forall d\ge1,\ \operatorname{UniversalTarget}(d,H).$$

The source statement appears in Section 1.

The main target, Proposition 7.1, permits any finite order:

$$\bigl(\exists b\in V,\ \exists\gamma:b\leadsto b,\quad |\gamma|\text{ odd},\quad\exists N>0,\ [\gamma]^N=1\bigr) \Longrightarrow \forall d\ge1,\ \operatorname{UniversalTarget}(d,H).$$

Here $N$ is a positive integer; it need not be the least exponent. The square-trivial case follows by taking $N=2$. The stronger statement is given in Section 7.1.

Mathematical significance and completion status

These results turn one finite algebraic witness into a conclusion covering all the spaces, actions, and positive dimensions specified above. Once a graph satisfies the hypothesis, an individual action requires no additional dynamical condition beyond the stated assumptions. The conclusion concerns finite discrete targets and the standard generating set.

Both results are established in the cited paper. Complete local Lean proofs now cover their full universal statements. The local project build and kernel audit have passed, and the final declarations use only Lean's standard logical axioms. Prove2Me has accepted the complete uploaded proof dependency graph. Both original headline theorem identities now have status Proved.

The completed development supplies reusable statements and checked infrastructure for lattice actions, reduced graph walks, finite probability distributions, and continuous graph homomorphisms. These components support inspection and reuse beyond the two headline results.

Why continuity requires attention

Choosing a homomorphism separately on each orbit does not ensure continuity across nearby points of the space. Freeness identifies each orbit with a lattice once an origin has been chosen, but does not supply continuously chosen origins across all orbits. A proof must therefore establish continuity of the resulting vertex map itself. Restricting attention to one action, one dimension, or an orbitwise map would leave the stated universal conclusion unresolved.

Formalization scope

The lattice is represented by $\mathrm{Fin}\ d\to\mathbb Z$, actions use additive notation, and standard adjacency includes both orientations of each generator edge. Reduced homotopy is an inductively generated relation on genuine Mathlib graph walks; powers are repeated concatenations. The target vertex type is arbitrary and finite, with its discrete topology.

Source spaces and target vertex types have independent universe parameters. Empty source spaces are allowed. No connectivity assumption is imposed on the target, and no separate nonemptiness hypothesis is added. The odd-walk witness already forces target nonemptiness. Neither a carrier-construction assumption nor an approximation condition appears in either final theorem.

Finite order refers to the class of the walk, rather than its length. An odd walk can revisit vertices and traverse edges repeatedly, so the hypothesis does not require an embedded cycle. All four-walk relations are included, including those with repeated vertices. The conclusion asserts existence of a continuous adjacency-preserving function; it asserts neither uniqueness nor injectivity. These distinctions matter when comparing a formal declaration with the source: replacing arbitrary closed walks by simple cycles or adding connectedness would change the objects quantified over. The recorded statements retain the wider walk convention used in the paper.

Further contributions can reuse the infrastructure or establish related variants while preserving these conventions. Any changed statement should distinguish its additional hypotheses and its altered conclusion from the two results recorded here.

Selected references

Ruijun Wang, Continuous graph homomorphisms of higher dimensional abelian group actions, arXiv preprint arXiv:2609.39824v1, 2026. Version and source; Theorem 1.4; definitions; Proposition 7.1.

Motivation

A metric tensor is a coordinate-free object, but every concrete exact solution of Einstein's vacuum equations is written down in coordinates, and the same spacetime appears in the literature in many charts: Schwarzschild in standard, Eddington–Finkelstein, Painlevé–Gullstrand and isotropic coordinates, Kerr in Boyer–Lindquist and ingoing form, and so on. Checking that a chart is a vacuum solution means computing the Ricci tensor of its metric components; checking that two charts describe the same solution means exhibiting a coordinate change and verifying that the metric components pull back. Release I of the Exact Vacuum Atlas (a separate, earlier mission) certified seven such charts (Minkowski ×2, Schwarzschild ×3, Kerr ×2) together with four coordinate relations.

Release II adds the missing method: a proof that the coordinate Ricci tensor used throughout the Atlas transforms as a tensor under any smooth coordinate change, so that a vacuum certificate can be transported along a coordinate relation instead of being recomputed. It then uses this to certify new Schwarzschild charts (Painlevé–Gullstrand, both signs; isotropic, both radial branches, in spherical and Cartesian form) and to give the Painlevé–Gullstrand certificate two distinct proof routes with an audited separation of their specified dependencies; they still share definitions, data and Mathlib.

Setting

All objects are coordinate-level data on open subsets of $\mathbb R^n$ ($n = 4$ in every application): a metric is a matrix $g_{ij}(x)$ of real functions, a candidate inverse $\hat g^{ij}(x)$ is another such matrix, and the coordinate Ricci tensor $\mathrm{Ric}(g,\hat g)_{ij}$ is defined by the usual Christoffel formulas from partial derivatives of slices (definition bundle Atlas_Core_Basic of release I). A vacuum certificate for $(g,\hat g)$ on an open set $U$ records eight obligations: $U$ open and nonempty, $g$ symmetric, $\hat g\,g = I$ on $U$, $g$ and $\hat g$ of class $C^\infty$ on $U$, an explicit Lorentz frame $E$ with $E^{\mathsf T} g E = \eta$ (signature $(-,+,+,+)$), and all sixteen Ricci components zero on $U$. A coordinate relation records a smooth bijection $\Phi : U \to V$ with inverse $\Psi$, a Jacobian matrix $J$ whose entries are genuine derivatives, and the pull-back identity $J^{\mathsf T}\,(h\circ\Phi)\,J = g$ on $U$. Mathlib provides real analysis, matrices and multivariable calculus. In the pinned Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474, the project did not find the complete indefinite-metric connection and Ricci definitions required by this development. The registered B3 coordinate definitions supplement that fixed version; this is not a claim about all current or future versions of Mathlib.

Formalization targets

Goal (ExactVacuumAtlas.Release02.ricci_law)

For any dimension $n$, open sets $U, V$, a smooth map $\Phi : U \to V$ with a genuine Jacobian $J$ and a right inverse $K$ ($JK = I$ on $U$), and regular metric data $(h,\hat h)$ on $V$ (symmetric, genuinely invertible, $C^\infty$; no curvature condition), if $g = J^{\mathsf T}(h\circ\Phi)J$ and $\hat g = K(\hat h\circ\Phi)K^{\mathsf T}$ on $U$ then

$$\mathrm{Ric}(g,\hat g)_{ij}(y) \;=\; \sum_{a,b} J(y)_{a i}\,J(y)_{b j}\;\mathrm{Ric}(h,\hat h)_{ab}(\Phi(y)) \qquad (y \in U).$$

The proof goes through the Christoffel transformation with its second-derivative term $K\,\partial_i J$ (the Christoffel symbols are not a tensor), the tensoriality of the matrix curvature $F_{cd} = \partial_c\Gamma_d - \partial_d\Gamma_c + [\Gamma_c,\Gamma_d]$ (the $K\partial J$ and $\partial K$ terms cancel), and the contraction to the Ricci tensor. The final Ricci theorem does not assume the Ricci transformation law. The intermediate curvature lemma has an explicit connection-transformation premise, which the proved Christoffel transformation discharges in the metric application. The registered Ricci tensor is not redefined.

Milestones (each a theorem item; the Goal and the definitions are never milestones)

1. certificate_transport — a vacuum certificate on $V$, a coordinate relation $U \to V$, the explicit conditions that $U$ is open and nonempty, a right inverse of the genuine Jacobian on $U$, and any genuine left inverse $\hat g$ of $g$ yield a vacuum certificate on $U$ (all eight obligations, 4D).
2. pg_route_direct — Painlevé–Gullstrand metric $-dT^2 + (dr + \varepsilon\sqrt{2M/r}\,dT)^2 + r^2 d\Omega^2$, $M \ge 0$, $\varepsilon^2 = 1$, certified on $\{r > 0,\ 0 < \theta < \pi\}$ (regular-coordinate points with $r=2M$ included when $M>0$; no global event-horizon statement) by direct computation (release-II sprint 01).
3. pg_route_transport — the same statement, proved a second time by transporting the Eddington–Finkelstein certificate of release I along the PG↔EF relation. The independence of this route is a constant-level dependency-closure audit (no PG table, PG certificate or PG root is reached), not a conjunction of two proofs.
4. control_direct, control_transport, control_witness — a non-vacuum control family: the cylinder metric pulled back by $\beta \mapsto \beta + \lambda\sin\alpha$ (non-affine for $\lambda\ne0$, and the identity for $\lambda=0$); the sixteen Ricci components ($R_{22} = 1 + \lambda^2 c^2 s^2$, $R_{23} = R_{32} = \lambda c s^2$, $R_{33} = s^2$, rest $0$; $c = \cos\alpha$, $s = \sin\alpha$) are proved twice (tables, and the transformation law from the release-I cylinder values), with the nonzero witness $R_{23}(0,1,\pi/4,0) = \sqrt2/4$ at $\lambda = 1$.
5. isotropic_branches — the two radial relations $r = \rho(1 + \frac{M}{2\rho})^2$ between the isotropic chart and the standard chart: outer branch $\rho > M/2$ ($M \ge 0$) and inner branch $0 < \rho < M/2$ ($M > 0$), both onto $r > 2M$.
6. isotropic_main — isotropic Schwarzschild $-A^2dt^2 + B^4(d\rho^2 + \rho^2 d\Omega^2)$, $B = 1 + \frac{M}{2\rho}$, $A = (1 - \frac{M}{2\rho})/B$, certified for every $M \ge 0$ on $\{\rho > 0,\ \rho \ne M/2,\ 0 < \theta < \pi\}$ (both branches transported from the standard certificate and glued; $M = 0$ is Minkowski).
7. isotropic_sph_cart_relation — the spherical ↔ Cartesian isotropic chart relation on the slit chart ($-\pi < \varphi < \pi$ on the spherical side and $r_{xy}+x>0$ on the Cartesian side), with $\rho>0$ and $\rho\ne M/2$ on both sides and $0<\theta<\pi$ on the spherical side, for every real $M$. This is a relation of the specified coordinate data; the vacuum certificates below are restricted to $M\ge0$.
8. isotropic_cartesian — the Cartesian isotropic certificate $-A(\rho)^2dt^2 + B(\rho)^4(dx^2+dy^2+dz^2)$ for every $M \ge 0$ on the natural domain $\{\rho > 0,\ \rho \ne M/2\}$ (no axis or slit cut: the slit certificate is transported along the reflection $x \mapsto -x$ and the relabelling $(x,y,z)\mapsto(y,z,x)$ and the three domains are glued).
9. pg_main, pg_coverage, pg_std_restricted — the sprint-01 PG roots: both signs; $M = 0$ and the regular data at $r = 2M$ for $M>0$; the PG↔EF relation on the whole domain and the composite standard → EF → PG relation on $r \ne 2M$ only.

Significance

The transformation law is the reusable link between a full certificate in one coordinate representation and a certificate in another. Transport also discharges the required source-domain, inverse-matrix, regularity and Lorentz-signature obligations; a bare table of zero Ricci components alone is not treated as a full certificate.

Difficulty

The law is a long but elementary computation (second derivatives of the Jacobian, Cramer's rule for the smoothness of the inverse Jacobian, symmetry of mixed partials, index bookkeeping over Fin n); the isotropic charts need genuine inverse functions with square roots, arccos and a half-angle arctan, with smoothness and bijectivity on explicit open domains. Nothing is stated at the manifold level.

Formalization scope

Coordinate-level statements on open subsets of $\mathbb R^4$ (the law itself on $\mathbb R^n$). Not claimed: an identification with a Mathlib manifold Ricci tensor in the pinned development; any global, event-horizon or maximal-extension theorem; PG or isotropic vacuum certificates for negative mass; certification of $\rho=M/2$ (for $M>0$ this is the excluded degenerate isotropic sphere, while for $M=0$ it is the excluded origin); that the union of the two isotropic branches is a single bijection; that the inner branch is the interior $r < 2M$.

Selected references

Müller, T., Grave, F.: Catalogue of Spacetimes, arXiv:0904.4184v3 (§2.2.3 isotropic, PG); Martel, K., Poisson, E.: Regular coordinate systems for Schwarzschild and other spherical spacetimes, arXiv:gr-qc/0001069; Carroll, S.: Lecture Notes on General Relativity, arXiv:gr-qc/9712019 (§3, transformation of the connection and curvature); release I of the Exact Vacuum Atlas (platform mission on this site).

Source and licence

New material of release II is released under Apache-2.0; the Kerr, release-I and third-party sources keep their recorded origins and licences. A public Git repository is not yet available: every node's source field cites the local release-candidate commit 11fb317259353b71a41d6daed466c495cffd7db4 with file, line range and SHA-256 of the staged file. Environment: Lean v4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. Local audits: no sorry, no native_decide; axiom closure ⊆ {propext, Classical.choice, Quot.sound}.

中文摘要

1. 坐标 Ricci 变换律（Goal）。 对任意维 n、任意光滑坐标变换（真实 Jacobian J，显式右逆 K）与任意对称、真实可逆、 C^∞ 的旧度规（不要求真空），R'_{ij}(y) = Σ_{ab} J_{ai} J_{bj} R_{ab}(Φ y)。证明经 Christoffel 变换（含二阶导数项 K ∂J）、 矩阵曲率张量性、收缩。最终 Ricci 定理不把待证变换律作为假设；中间联络变换前提由已证明的定理提供；ricciOf 定义未改。
2. 证书传递。 旧证书 + 第一版 CoordRelation + 源域开且非空 + Jacobian 的显式右逆 + 新度规的真实左逆 ⇒ 新证书（八项逐字段），四维。
3. PG 直接路线。 M ≥ 0、ε² = 1，整个 {r > 0, 0 < θ < π}（M > 0 时包含域内 r = 2M 的正则坐标点），第一阶段表格直接计算。
4. PG 传递路线。 同一陈述的第二个证明：EF 证书沿 PG↔EF 关系传递；独立性由常量级依赖闭包审计给出（不触及 PG 表/证书/根），不是 P ∧ P。
5. 非真空对照（两路线 + 见证）。 圆柱度规经剪切（λ ≠ 0 时非仿射，λ = 0 时为恒等映射） β ↦ β + λ sin α 拉回；16 个 Ricci 分量由表与变换律各证一次： R₂₂ = 1+λ²c²s²、R₂₃ = R₃₂ = λcs²、R₃₃ = s²、其余 0；λ = 1 时 R₂₃(0,1,π/4,0) = √2/4 ≠ 0；λ = 0 为恒等映射。
6. isotropic 两支径向关系。 外支 ρ > M/2（M ≥ 0）、内支 0 < ρ < M/2（M > 0），都映到 r > 2M；互逆、真实 Jacobian、拉回均已证。
7. isotropic 球坐标完整证书。 所有 M ≥ 0，域 ρ > 0, ρ ≠ M/2, 0 < θ < π；两支分别由标准证书传递后并域；M = 0 为 Minkowski。
8. 球 ↔ Cartesian 关系（slit 图）。 两侧均要求 ρ > 0, ρ ≠ M/2；球坐标另有 0 < θ < π, −π < φ < π，Cartesian 一侧另有 r_xy + x > 0；fromCart 用 arccos 与半角 arctan；对所有实 M 成立（不推出负质量真空证书）。
9. isotropic Cartesian 自然域证书。 所有 M ≥ 0，域 ρ > 0, ρ ≠ M/2，无极轴/切口限制：slit 证书经反射与循环重标传递并并域。
10. PG 阶段根（覆盖与关系）。 M = 0 特例，以及 M > 0 时 r = 2M 正则坐标点的覆盖；PG↔EF 在整个域的双向关系；正向为 standard → EF → PG 的合成关系只在 domStd（r ≠ 2M），单独标示。

不声称：流形/全局事件视界/最大延拓；PG或isotropic的负质量真空证书；在ρ = M/2处的证书（M>0为排除的退化球面，M=0为排除的原点）；ricciOf 等于 Mathlib 流形 Ricci；两支并域是一个双射；内支是 r < 2M。