The tilt family on a polarised threefold, and the slope it induces

ThreefoldWallTransport.lean transports a polarised threefold class to the four-coordinate (α, β) model and proves nu_toNumClass: the model's Wall.Threefold.nu is the BMT.nu this directory already had. Walls/Threefold/ Tilt.lean proves nu_eq_tilt_slope: that same model slope is α times the charge slope of the tilt family.

This file composes the two, which is what #1228 asked for and what neither half could state alone. The result is the geometric reading of the tilt charge:

the Bayer--Macrì--Toda slope of a class on a polarised numerical threefold is α times the charge slope of Tilt.tiltFamily at its transported class.

No new carrier

There is deliberately no tiltWallChargeFamily here. The sketch had one, and Walls/Threefold/TiltComparison.lean records why it is not reinstated: the implemented transport pulls back the untilted Threefold.chargeFamily, the two families genuinely differ, and Tilt.exists_tilt_alignmentValue_ne_threefold proves it with a computed witness. A family here would need the two independent consumers the abstraction tree requires before a root is minted, and it has none: the statements below need Tilt.tiltFamily applied at a transported class, which is not the same thing as a new family.

No third slope

nu (this directory) and Wall.Threefold.nu (the model) are the two the adjudication kept, and both appear below in the same equation rather than a third being defined.

The tilt charge, in the degrees this directory reads

theorem AlgebraicGeometry.Numerical.Threefold.tiltFamily_im_toNumClass {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (α β : ℚ) (E : N) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.tiltFamily.im (↑α, ↑β) (toNumClass V P E) = ↑(α * degH1Beta V P β E)

The tilt family's imaginary part at a transported class is α·∫H²·ch₁^β.

This is what makes the positivity hypothesis of the slope theorems below checkable on a threefold: it is a statement about degH1Beta, not about a coordinate of an abstract quadruple.

theorem AlgebraicGeometry.Numerical.Threefold.tiltFamily_re_toNumClass {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (α β : ℚ) (E : N) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.tiltFamily.re (↑α, ↑β) (toNumClass V P E) = -↑(degH2Beta V P β E - α ^ 2 / 2 * (V.ring.degree (P.cls ^ 3) * ↑(V.rank E)))

The tilt family's real part at a transported class is the negated Bayer--Macrì--Toda numerator, −(∫H·ch₂^β − (α²/2)·∫H³·ch₀).

ch₀ carries no β, which is why the subtrahend reads the untwisted rank slot of the transported class.

The slope, composed

theorem AlgebraicGeometry.Numerical.Threefold.nu_eq_tiltFamily_slope {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (α β : ℚ) (E : N) (h : 0 < α * degH1Beta V P β E) : ↑(nu V P α β E) = ↑α * (-CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.tiltFamily.re (↑α, ↑β) (toNumClass V P E) / CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.tiltFamily.im (↑α, ↑β) (toNumClass V P E))

The Bayer--Macrì--Toda slope is the tilt family's charge slope, rescaled.

Tilt.nu_eq_tilt_slope says this of the four-coordinate model and nu_toNumClass says the model's slope is this directory's nu; neither alone connects Tilt.tiltFamily to a threefold. This is the composition, and it is the sense in which the library has one tilt charge rather than three.

The hypothesis is the one the slope convention needs, stated in the degrees a threefold supplies.

theorem AlgebraicGeometry.Numerical.Threefold.chargeSlope_tiltFamily_toNumClass {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (α β : ℚ) (E : N) (h : 0 < α * degH1Beta V P β E) : CategoryTheory.Triangulated.chargeSlope ((CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.tiltFamily.charge (↑α, ↑β)) (toNumClass V P E)) = ↑(↑(nu V P α β E) / ↑α)

The same statement as a chargeSlope, which is the form the semistability vocabulary of Abelian/Stability/ uses.