A previous post described a Lean 4 proof of the identity $F\_{\mathrm{hm}} = \hat{G}(1)$ in a two-variable Hahn series ring — the core of a tenth-order mock theta function theorem from Chapter 10 of H.-C. Chen’s An Invitation to q-Series. That proof was complete and axiom-clean, but it left one question open: how do you get from the two-variable algebraic identity back to the one-variable statement that the classical literature actually cares about?

This post describes how that gap was closed, completing the full formal proof chain with zero sorry.

The gap

The proved identity lives in $S = \mathrm{HahnSeries}\;\mathrm{Exp}\_{QXY}\;\mathbb{Q}$, a ring of formal power series indexed by triples $(q\text{-degree}, x\text{-degree}, y\text{-degree})$. Each element of $S$ is a two-variable generating function. The one-variable cone identity, on the other hand, lives in $\mathrm{QLaurent} = \mathrm{HahnSeries}\;\mathbb{Z}\;\mathbb{Q}$ — ordinary Laurent series in a single variable $q$.

The bridge between the two is specialization: given an element $F \in S$ and integers $X, Y$, define

where $w(g) = q\text{-deg}(g) + X \cdot x\text{-deg}(g) + Y \cdot y\text{-deg}(g)$ is the weight, and the sum runs over all monomials $g$ in the support of $F$, grouped by their weight. This collapses two variables into one by “specializing” $x \mapsto q^X$, $y \mapsto q^Y$.

The cone identity we want is $\mathrm{spec}(\hat{G}(1), 18, 18) = h\_{2,3,2}(q)$, where $h\_{2,3,2}$ is the one-variable Hickerson–Mortenson function. If we can prove this, then the already-proved $F\_{\mathrm{hm}} = \hat{G}(1)$ immediately gives $\mathrm{spec}(F\_{\mathrm{hm}}, 18, 18) = h\_{2,3,2}(q)$, which is precisely the classical identity.

The circular dependency trap

The most natural approach is to specialize $\hat{G}(1)$ directly. Since $\hat{G}$ is built from products of theta functions, Appell–Lerch numerators, and localized inverses, one might hope that $\mathrm{spec}$ distributes over these operations and reduces each factor to its one-variable counterpart.

But there is a problem. $\hat{G}$ contains localized inverses $\mathrm{locInv}(B)$ — formal inverses of boundary theta functions. These localized inverses do not specialize cleanly. The specialization $\mathrm{spec}(\mathrm{locInv}(B) \cdot N)$ is not $\mathrm{spec}(N) / \mathrm{spec}(B)$, because $\mathrm{QLaurent}$ is not a field (and even if it were, the quotient would require convergence arguments absent from the purely algebraic setup).

The codebase already had a one-variable cone identity (cone_eq_thetaAppell_00) as a sorry stub. Using it to prove the specialization theorem would be circular — it was the very thing we were trying to prove.

The idea: boundary clearing

The key insight is that before specializing, we can multiply by the boundary theta functions to clear the localized inverses.

Recall that $\hat{G}(1)$ is a sum of four row terms, each of the form

where $q^{\ell\_i}$ is a monomial lead, $j(\alpha\_i; q^{18})$ is a theta function, $B\_i$ is a boundary theta, $N\_i$ is an Appell numerator, and $\mathrm{locInv}(B\_i)$ is its formal inverse. There are two boundary functions, $B\_0$ and $B\_1$, shared across pairs of rows: $R\_0, R\_2$ use $\mathrm{locInv}(B\_0)$ and $R\_1, R\_3$ use $\mathrm{locInv}(B\_1)$.

The “cleared” product $\hat{G}(1) \cdot B\_0 \cdot B\_1$ eliminates all localized inverses (since $\mathrm{locInv}(B\_i) \cdot B\_i = 1$). What remains is a sum of products of theta functions and Appell numerators — no inverses, no denominators.

Now compute $\mathrm{spec}(\hat{G}(1) \cdot B\_0 \cdot B\_1, 18, 18)$ two ways:

Route 1 (multiplicative): Since $\mathrm{spec}$ distributes over multiplication (provided each factor has a finite weight fiber — the SpecGood condition), we get

Route 2 (via the cleared identity): The already-proved $F\_{\mathrm{hm}} = \hat{G}(1)$ implies $F\_{\mathrm{hm}} \cdot B\_0 \cdot B\_1 = P\_Y \cdot B\_1 + P\_X \cdot B\_0$ (the “cleared identity”), where $P\_Y, P\_X$ are the boundary-cleared numerator sums. Specializing the right-hand side reduces each factor to its one-variable counterpart:

where $j\_0 = \mathrm{spec}(B\_0) = j(q^{18}; q^{90})$ and $j\_1 = \mathrm{spec}(B\_1) = j(q^{-18}; q^{90})$ are nonzero Laurent series.

Setting the two routes equal and cancelling $j\_0 \cdot j\_1 \neq 0$ gives the desired

Why (18, 18)?

A subtlety: the specialization theory requires SpecGood — a condition that each weight fiber $\{g : w(g) = E \text{ and } F[g] \neq 0\}$ is finite. For theta functions, this holds at any $(X, Y)$ because the weight is a quadratic function of the summation index, and each level set of a quadratic is finite. But for Appell–Lerch numerators, the situation is different.

The Appell denominator exponent at row $R\_i$ and index $r$ is $d\_i(r) = 90(r-1) + a\_i + z\_i$, where $a\_i, z\_i$ are evaluated at $(X, Y)$. If $d\_i(r) = 0$ for some $r$, the Appell strip term at $r$ has infinitely many nonzero coefficients at the same weight, and SpecGood fails.

At the specific values $(X, Y) = (18, 18)$, the denominator evaluates to $d\_i(r) = 90r - D\_i$ where $D\_i \in \{36, 72, 81, 117\}$. None of these is divisible by 90, so $d\_i(r) \neq 0$ for all integers $r$, and SpecGood holds. This is verified by a cases row <;> omega in Lean.

At, say, $(X, Y) = (0, 72)$, the row R0 denominator becomes $90r - 72$, which vanishes at $r = 4/5$ — not an integer, still fine. But at other specialization points, the denominator can vanish, and the generic SpecGood statement is actually false (the file contains a documented counterexample at $Y = 72$).

The proof-irrelevance barrier

A recurring technical obstacle: spec carries a proof term witnessing SpecGood as an explicit argument. This means spec(F \cdot G, h) and spec(F, h\_F) \cdot \mathrm{spec}(G, h\_G) have different types even when $h$ is the product witness constructed from $h\_F$ and $h\_G$. The spec_mul theorem proves they are equal, but applying it requires matching the Lean proof terms exactly.

When the SpecGood witnesses are built from nested chains of SpecGood.mul and SpecGood.add, the proof terms become large and fragile. Lean’s definitional equality does not automatically identify all witnesses. The solution was to introduce proof-irrelevant wrappers spec_mul' and spec_add' that accept any SpecGood witnesses for the parts and use proof_irrel internally:

theorem spec_mul' (F G : S) (hF : SpecGood X Y F) (hG : SpecGood X Y G) :
    spec X Y (F * G) (SpecGood.mul hF hG) =
      spec X Y F hF * spec X Y G hG

Without this, every spec_mul application required a show tactic to unfold the precise SpecGood term, and the proofs were unreadably long.

Scale

The full Chapter 10 proof chain spans 382 commits and approximately 50 Lean files. The final axiom audit on all eight exported theorems — cleared_identity_final, Fhm_eq_Ghat_final, spec_theta, SpecGood_appellNumerator_18_18, spec_appellNumerator_18_18, spec_Ghat_eq_hmF232Laurent_18_18, Ghat_specializes_to_hmF232_18_18, and cone_eq_thetaAppell_00_faithful — shows each depending only on propext, Classical.choice, and Quot.sound. No sorry, no custom axioms.

The specialization layer itself (SpecTheory + SpecConcrete + FaithfulBridge) is roughly 1400 lines of Lean 4.

Reflection

The proof took an indirect route that no one planned. The original approach — prove the one-variable cone identity directly by a coefficient reindex — ran into a combinatorial wall (the “BUV reindex” in ConeToFiber.lean, still sorry). The eventual proof lifts to a richer algebraic structure, proves the identity there, and then projects back down. The boundary-clearing trick — multiply by denominators, specialize, cancel — is a standard move in algebraic number theory and algebraic geometry, but it was not part of the original proof plan for this $q$-series identity.

The formalization exposed the circular dependency (specialization needs the identity, but the identity was what we were proving) and forced the discovery of the bypass. It is hard to imagine finding the boundary-clearing route without the machine repeatedly rejecting the circular one.

「众里寻他千百度，蓦然回首，那人却在灯火阑珊处。」—— 辛弃疾《青玉案·元夕》

“A thousand times I searched for her in the crowd; then, turning back by chance, there she stood — where the lantern-light was dim.” — Xin Qiji, “Green Jade Cup: The Lantern Festival”