The exponential charge, indexed by truncation degree #
One polynomial. CentralCharge/Numerical/ carries the surface charge on three
real coordinates and the Bayer--Macrì--Toda charge on four, and
the threefold file's own docstring records that they are the same expansion of
-∫exp(-(β + iα)H)ch at two codimensions. They are nevertheless two unrelated
roots, and no fourfold charge exists. This file is the shared parent, and
CentralCharge/Exponential/Comparison.lean proves both existing families are instances of it.
The index is the truncation degree, never the dimension #
m counts how many codimensions survive, not how many the variety has. The two
are equal for the untilted charge of an n-fold, and that coincidence is what
made the wrong index look right: a family indexed by dimension covers the
surface at m = n = 2 and the threefold at m = n = 3, and then fails at the
first example where they differ. The cubic-threefold Kuznetsov charge is one,
at (n, m) = (3, 2), and Walls/Threefold/Tilt.lean's Tilt.tiltFamily is the
truncation that produces it.
That sentence used to promise an Exp.tiltChargeFamily in a later slice. The
slice never happened and the declaration does not exist; what landed instead was
Tilt.tiltFamily, built from the surface family. It is the same object, and
Walls/Threefold/TiltComparison.lean proves it -- tiltFamily_eq_exp is this
kernel at m = 2, reindexed and pulled back. The adjudication that settled
which spelling survives is #1228.
This is also why numerical-k-theory-e5 is parked. That track assumed one type
indexed by dimension would cover the surface, threefold and fourfold numerical
formulas, recorded the assumption FALSIFIED on 2026-08-27, and parked the epic.
The falsification stands; the index was the defect.
What the moments are for #
ofMoments takes an arbitrary moment sequence rather than a vector of degrees,
so that the two genuinely different sources of moments share it:
- scalar moments
μ j = w^j · d_{m-j}on compressedH-degrees, below, which is the polarised case of Picard rank one; - intersection-form moments
μ₀ = ch₂,μ₁ = ⟨w, ch₁⟩,μ₂ = ⟨w, w⟩·rk, which is the divisorial case of arbitrary Picard rank, in a later slice.
The second does not factor through the first: the H-compression is not
injective once the Picard rank exceeds one. So the two are siblings under
ofMoments rather than one being a specialization of the other, and a kernel
indexed by compressed degrees alone would have excluded the divisorial charge —
which two of the three independent designs of this tree wrongly concluded.
What is not here #
The exponential action and charge translation identity are in Twist.lean.
This primitive kernel imports CentralCharge/Family.lean and Mathlib, so it
imports no leaf; comparisons with the existing families live downstream in
Comparison.lean and Divisorial.lean.
The exponential coefficient (-1)^j / j!, written once.
Every charge in the tree spells these out per dimension: 1, -1, 1/2 for
the surface and additionally -(1/6) for the threefold.
Equations
Instances For
The charge. Z = -∑_{j ≤ m} (-1)^j/j! · μ j.
The moment sequence is arbitrary; moments below supplies the scalar one and
the divisorial lane supplies the intersection-form one. The leading sign is the
convention of -∫exp(-(B + iω))ch, which is what both existing families use.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The scalar moments: compressed H-degrees #
Compressed H-degrees at truncation degree m: d k = ∫H^(n-k)·ch_k, so
the slot index is codimension and slot 0 carries the weight ∫Hⁿ rather than
the bare rank. Both existing transports already obey that convention.
An abbrev, so no new carrier is introduced and
scripts/check_single_instantiation.py, which counts structure heads, has
nothing to see.
Equations
Instances For
The scalar moments μ j = w^j · d_{m-j} of a compressed degree vector.
w is the single complex parameter B + iω of the polarised lane; the two
lanes disagree about which of its parts comes first, and stChart and
alphaBetaChart below are where that disagreement is written down.
Equations
Instances For
The scalar charge family, an inhabitant of the dimension-independent wall
root with parameter space ℂ.
The parameter space is ℂ and not ℝ × ℝ on purpose: w is one complex
number, and the real charts that present it as a pair are reindexes of this
family rather than its definition.
Equations
Instances For
The two real charts #
The surface lane parameterizes by (s, t) and the threefold lane by (α, β),
and the two orders are transposed. Writing both here means the transposition is
recorded once instead of at every consumer that moves between the lanes.
The surface lane's chart: (s, t) ↦ s + tI.
Equations
Instances For
The threefold lane's chart: (α, β) ↦ β + αI.
Note the transposition against stChart. The threefold family's parameter pair
is (α, β) with α the ample coefficient, where the surface family's is
(s, t) with t the ample coefficient.