The surface and threefold charges are one kernel

CentralCharge/Exponential/Kernel.lean states the exponential charge once, indexed by truncation degree. This file proves that the two charges already in the tree are that kernel at m = 2 and m = 3, so neither is a root any more.

The separation is the point. The kernel imports CentralCharge/Family.lean and Mathlib and nothing else, so it imports no leaf; this file may import both leaves because it is the comparison and not the root. Putting the comparisons in the kernel would have made the root depend on the things it parents.

What is proved

• stCharge_eq_exp — the surface charge (CentralCharge/Numerical/SurfaceFamily.lean) is the kernel at m = 2, w = s + tI.
• threefold_charge_eq_exp — the Bayer--Macrì--Toda charge (CentralCharge/Numerical/Threefold.lean) is the same kernel at m = 3, w = β + αI.
• the two family-level statements, which is the form a consumer needs: each existing ChargeFamily is a reindex of Exp.chargeFamily along its chart, pulled back along the coordinate identification.

The coordinate identifications are equivalences, not projections

surfaceVec and threefoldVec are ≃+, not one-way maps. The compressed degree vectors and the tuple carriers hold the same data in the same order, so nothing is lost passing between them, and stating them as equivalences is what lets a later slice push wall theory in either direction. This is in contrast to the divisorial lane, where the H-compression genuinely loses information once the Picard rank exceeds one.

What this does not claim

That the two families have the same walls, or that either is a stability condition. A charge is one datum of a stability condition; the heart, the slicing and the support property are elsewhere and are untouched.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.surfaceVec : NumClass ≃+ Exp.HDeg 2

The surface lane's tuple carrier and the kernel's compressed degrees hold the same three reals, in the same order.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.stCharge_eq_exp (s t : ℝ) (v : NumClass) : (stCharge s t) v = (Exp.charge 2 (Exp.stChart (s, t))) ![v.rk, v.deg, v.ch2]

The surface charge is the kernel at m = 2, w = s + tI.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.threefold_charge_eq_exp (a b : ℝ) (v : Threefold.NumClass) : (Threefold.charge a b) v = (Exp.charge 3 (Exp.alphaBetaChart (a, b))) ![v.deg0, v.deg1, v.deg2, v.deg3]

The Bayer--Macrì--Toda threefold charge is the same kernel at m = 3, w = β + αI. Note the chart transposition against the surface case.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.stChargeFamily_eq : stChargeFamily = ((Exp.chargeFamily 2).reindex Exp.stChart).pullback surfaceVec.toAddMonoidHom

The surface charge family is the kernel's family, reindexed by its chart and pulled back along the coordinate identification.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.threefold_chargeFamily_eq : Threefold.chargeFamily = ((Exp.chargeFamily 3).reindex Exp.alphaBetaChart).pullback threefoldVec.toAddMonoidHom

The threefold charge family, likewise.