The polarised wall transport, for every dimension and correction class

CentralCharge/Exponential/ states the exponential charge once. This is the geometric side: the map that turns a numerical class on a polarised variety into the compressed H-degrees that the charge consumes, written once for every dimension n, truncation degree m and correction class κ.

Before this the transport existed twice: Surface.toNumClass (WallTransport.lean) at n = 2 and Threefold.toNumClass (ThreefoldWallTransport.lean) at n = 3, the second a hand-copy of the first at one more codimension. Both are proved below to be this map.

The rank slot carries ∫Hⁿ

Slot k is ∫ H^(n-k) · (ch(E)·κ)_k, so the index is codimension and slot 0 is ∫Hⁿ · rk(E), not the bare rank. Both existing transports already did this and said so in their docstrings, but nothing tied the convention to a root; hDegrees_zero now does, in every dimension at once.

The weight is as easy to get wrong in the other direction. The slope μ_H is not the ratio of slots d₁/d₀: that ratio is the slope divided by ∫Hⁿ. slopeH_eq_degree_mul_ratio states the true relation, and slopeH_ne_ratio_of_degree_ne_one records the false one as a negative result, because the naive reading was written down during this lane's own design review and is wrong on every polarization of degree other than one.

κ is a pullback, never a coefficient

The correction class enters through corrComp, a convolution in the right-hand slot, and nothing else here knows which class it is. Two values matter today: unitCorr, giving the plain Chern character, and sqrtToddComp, giving the Mukai vector. corrComp_sqrtToddComp is rfl, because NumericalVarietyData.mukaiComp was already this convolution written out, so the Mukai vector is not a second construction. The two are pullbacks of one transport with genuinely different walls and must not be fused into one family.

What is proved about the existing families

surface_toNumClass_eq and threefold_toNumClass_eq are the class-level comparisons. surface_wallChargeFamily_eq is the family-level one, which is the form a consumer actually needs: the existing surface wall family is this root's family, reindexed by the surface chart.

The threefold family-level twin is deliberately absent. It needs a truncation map that does not exist yet, which belongs to the tilt slice; inventing a second route to it here is exactly what the tilt adjudication exists to stop.

def AlgebraicGeometry.Numerical.Polarised.unitCorr (A : Type u) [CommRing A] : ℕ → A

The trivial correction class κ = 1, giving the plain Chern character.

Equations

• AlgebraicGeometry.Numerical.Polarised.unitCorr A j = if j = 0 then 1 else 0

def AlgebraicGeometry.Numerical.Polarised.corrComp {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (κ : ℕ → A) (E : N) (k : ℕ) : A

(ch(E)·κ)_k, the codimension-k component of the corrected character.

The convolution is in the right-hand slot, which keeps κ a parameter rather than a coefficient baked into the transport.

Equations

• AlgebraicGeometry.Numerical.Polarised.corrComp V κ E k = ∑ j ∈ Finset.range (k + 1), V.chComp E j * κ (k - j)

theorem AlgebraicGeometry.Numerical.Polarised.corrComp_unitCorr {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (E : N) (k : ℕ) : corrComp V (unitCorr A) E k = V.chComp E k

With κ = 1 the convolution is the identity. This is the one fact both dimension comparisons need, proved once instead of per dimension.

theorem AlgebraicGeometry.Numerical.Polarised.corrComp_sqrtToddComp {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (E : N) (k : ℕ) : corrComp V V.sqrtToddComp E k = V.mukaiComp E k

At κ = √td the convolution IS the Mukai component, by rfl.

theorem AlgebraicGeometry.Numerical.Polarised.corrComp_add {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (κ : ℕ → A) (E F : N) (k : ℕ) : corrComp V κ (E + F) k = corrComp V κ E k + corrComp V κ F k

The corrected character is additive, because the Chern character is.

def AlgebraicGeometry.Numerical.Polarised.hDegrees {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (P : Polarization V.ring) (κ : ℕ → A) (m : ℕ) (E : N) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Exp.HDeg m

The compressed H-degree vector, d k = ∫ H^(n-k) · (ch(E)·κ)_k for k ≤ m. One map for every (n, m, κ).

Equations

• AlgebraicGeometry.Numerical.Polarised.hDegrees V P κ m E k = ↑(V.ring.degree (AlgebraicGeometry.Numerical.Polarised.corrComp V κ E ↑k * P.cls ^ (n - ↑k)))

theorem AlgebraicGeometry.Numerical.Polarised.hDegrees_add {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (P : Polarization V.ring) (κ : ℕ → A) (m : ℕ) (E F : N) : hDegrees V P κ m (E + F) = hDegrees V P κ m E + hDegrees V P κ m F

The transport is additive.

def AlgebraicGeometry.Numerical.Polarised.hDegreesHom {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (P : Polarization V.ring) (κ : ℕ → A) (m : ℕ) : N →+ CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Exp.HDeg m

The transport bundled as an additive map, which is what pullback needs.

Equations

• AlgebraicGeometry.Numerical.Polarised.hDegreesHom V P κ m = AddMonoidHom.mk' (AlgebraicGeometry.Numerical.Polarised.hDegrees V P κ m) ⋯

noncomputable def AlgebraicGeometry.Numerical.Polarised.wallChargeFamily {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (P : Polarization V.ring) (κ : ℕ → A) (m : ℕ) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily ℂ N

The wall family of a polarised variety: the kernel's family pulled back along the transport. Every dimension and every correction class gets its walls from here rather than from a charge of its own.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Polarised.wallChargeFamily_charge {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (P : Polarization V.ring) (κ : ℕ → A) (m : ℕ) (w : ℂ) (E : N) : ((wallChargeFamily V P κ m).charge w) E = (CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Exp.charge m w) (hDegrees V P κ m E)

The root family evaluates as the kernel on the transported degrees. The accessor the surface leaf has had since WallTransport.lean:161; a consumer that unfolds pullback by hand is reaching past this definition.

theorem AlgebraicGeometry.Numerical.Polarised.hDegrees_zero {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (P : Polarization V.ring) (E : N) : V.ring.degree (corrComp V (unitCorr A) E 0 * P.cls ^ (n - 0)) = ↑(V.rank E) * V.ring.degree (P.cls ^ n)

PROVED. Slot 0 is ∫Hⁿ · rank E.

########################################################################### (3) N4 — the honest relation between slopeH and the root's slots. slopeH (Slope.lean:133) is degH / rank, while slot 0 is rank · ∫Hⁿ. So the ratio d₁ / d₀ is NOT the slope: it is the slope divided by ∫Hⁿ. ###########################################################################

theorem AlgebraicGeometry.Numerical.Polarised.hDegrees_one {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (P : Polarization V.ring) (hn : 1 ≤ n) (E : N) : hDegrees V P (unitCorr A) n E ⟨1, ⋯⟩ = ↑(degH V P E)

Slot 1 of the root is degH, in every dimension n ≥ 1.

theorem AlgebraicGeometry.Numerical.Polarised.slopeH_eq_degree_mul_ratio {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (P : Polarization V.ring) (hn : 1 ≤ n) (E : N) : ↑(slopeH V P E) = ↑(V.ring.degree (P.cls ^ n)) * (hDegrees V P (unitCorr A) n E ⟨1, ⋯⟩ / hDegrees V P (unitCorr A) n E ⟨0, ⋯⟩)

N4, corrected and proved. μ_H(E) = ∫Hⁿ · (d₁ / d₀).

The report's §2.6 reading slopeH = d₁ / d₀ is FALSE whenever ∫Hⁿ ≠ 1: the rank slot carries the ∫Hⁿ weight, so the ratio of the root's slots is the slope scaled down by ∫Hⁿ. Note there is no rank hypothesis — at rank E = 0 both sides are Lean's junk 0, which is the same junk slopeH already has.

theorem AlgebraicGeometry.Numerical.Polarised.slopeH_ne_ratio_of_degree_ne_one {n : ℕ} {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData n A N) (P : Polarization V.ring) (hn : 1 ≤ n) (E : N) (hdeg : V.ring.degree (P.cls ^ n) ≠ 1) (hne : slopeH V P E ≠ 0) : ↑(slopeH V P E) ≠ hDegrees V P (unitCorr A) n E ⟨1, ⋯⟩ / hDegrees V P (unitCorr A) n E ⟨0, ⋯⟩

The falsified reading, recorded as a negative result. slopeH = d₁/d₀ holds exactly when ∫Hⁿ = 1 (or the slope is zero); it is not an identity.