Threefold wall equations and BMT numerical quantities

The threefold class, twist, and charge are owned upstream by CentralCharge/Numerical/Threefold.lean. This file adds only the determinant wall equation and the numerical quantities used by downstream tilt-wall work.

No nonnegativity of Q is asserted here; geometric hypotheses belong downstream.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.chargeFamily_alignmentValue (p : ℝ × ℝ) (v w : NumClass) : chargeFamily.alignmentValue p v w = reZ p.1 p.2 v * imZ p.1 p.2 w - imZ p.1 p.2 v * reZ p.1 p.2 w

The universal determinant of the threefold family, written out in the two polynomials.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.alignmentValue_div_alpha (α β : ℝ) (v w : NumClass) : reZ α β v * imZ α β w - imZ α β v * reZ α β w = α * (reZ α β v * (imZ α β w / α) - imZ α β v / α * reZ α β w) ∨ α = 0

Dropping the outer α from the imaginary part rescales every wall expression by α, so it moves no wall off α = 0. This is why the two normalisations of the threefold charge found in the literature agree about walls.

The Bayer--Macrì--Toda quantities, as definitions

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.discr (v : NumClass) : ℝ

The H-discriminant of a compressed threefold class, Δ_H = (∫H²ch₁)² − 2(∫H³ch₀)(∫H·ch₂).

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.discr v = v.deg1 ^ 2 - 2 * v.deg0 * v.deg2

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.discr_eq_selfPairing (v : NumClass) : discr v = Mukai.selfPairing (LinearMap.mul ℝ ℝ) (v.deg0, v.deg1, v.deg2)

The threefold discriminant is the Mukai self-pairing of the first three slots, at coefficient ring ℝ with the multiplication of ℝ as the form.

The fourth slot ∫ch₃ is not in the triple and is not meant to be: the arity of the root is fixed at three. Generalising the root over the DIMENSION instead would make this leaf unreachable — a dimension-indexed self-pairing vanishes identically in odd degree — which is recorded as a negative result in docs/architecture/abstraction-tree.md.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.nu (α β : ℝ) (v : NumClass) : ℝ

The tilt slope ν_{α,β}, junk where the denominator vanishes — the same convention the surface slope uses at rank zero.

Equations

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

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.Q (α β : ℝ) (v : NumClass) : ℝ

The Bayer--Macrì--Toda quantity Q_{α,β} = α²Δ_H + 4(∫H·ch₂^β)² − 6(∫H²ch₁^β)(∫ch₃^β).

Defining it is all this does. Its nonnegativity on tilt-semistable objects is the BMT conjecture, which is false in general; see the module docstring and AlgebraicGeometry/Numerical/Stability/BMT.lean.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.Q_zero_alpha (β : ℝ) (v : NumClass) : Q 0 β v = 4 * (betaTwist β v).deg2 ^ 2 - 6 * (betaTwist β v).deg1 * (betaTwist β v).deg3

At α = 0 the quantity loses its discriminant term.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.Q_zero_beta (α : ℝ) (v : NumClass) : Q α 0 v = α ^ 2 * discr v + 4 * v.deg2 ^ 2 - 6 * v.deg1 * v.deg3

At β = 0 the twist disappears.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.nu_zero_alpha (β : ℝ) (v : NumClass) : nu 0 β v = (betaTwist β v).deg2 / (betaTwist β v).deg1

At α = 0 the tilt slope is the plain ratio of the two twisted degrees.