The threefold wall transport, on ℙ³

Stability/ThreefoldWallTransport.lean carries a polarised threefold class into the four-coordinate (α, β) charge plane, and Models/Threefold/ProjectiveSpace.lean builds the ℙ³ model. Nothing connected them: the model was referenced only inside its own file, and no polarization was defined for it at all. So the threefold charge arithmetic had no worked example, exactly as the surface arithmetic had none before Examples/Surface/RankOneRealization.lean.

This file supplies the polarization and evaluates the transport.

The coordinates

With ∫H³ = 1 and linear-section coordinates (a, b, c, e), the four degrees come out as

∫H³ch₀ = a,   ∫H²ch₁ = b,   ∫H·ch₂ = -b/2 + c,   ∫ch₃ = b/6 - c + e,

which is threefoldChCoeff read against ∫H³ = 1. The four p3_toNumClass_deg* lemmas are that computation, and everything else in the file is a consequence of it together with the general theorems of the transport.

The Bayer--Macrì--Toda datum, and what a witness can honestly be

BMTData has no witness anywhere in the tree, so every consequence of it is vacuous. It cannot be given an honest one by proving the inequality: the conjecture is false for some threefolds — the blow-up of ℙ³ at a point, Schmidt — and true for ℙ³ itself only by a real theorem this repository does not contain.

p3BMTSanity is therefore a sanity witness in the exact style of k3BogomolovSanity: its TiltSemistable predicate is defined to be the conclusion, so nonneg holds tautologously. It asserts nothing whatsoever about sheaves or about tilt stability, and must not be read as the Bayer--Macrì--Toda inequality for ℙ³. What it buys is that the transported statements below are about an inhabited structure.

The polarization

theorem AlgebraicGeometry.Numerical.Examples.p3_degree_H_pow_three : p3NumericalVariety.ring.degree (rankOneH 3 ^ 3) = 1

∫_{ℙ³} H³ = 1.

noncomputable def AlgebraicGeometry.Numerical.Examples.p3Polarization : Polarization p3NumericalVariety.ring

The hyperplane class as a polarization of ℙ³. The first polarization of a threefold model in the repository.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p3Polarization_cls : p3Polarization.cls = rankOneH 3

The transported class

The four degrees of a class on ℙ³

The transport of (a, b, c, e) is (a, b, -b/2 + c, b/6 - c + e). These four lemmas are the computation the rest of the file rests on.

theorem AlgebraicGeometry.Numerical.Examples.p3_toNumClass_deg0 (E : ThreefoldNum) : (Threefold.toNumClass p3NumericalVariety p3Polarization E).deg0 = ↑(E 0)

Not a simp lemma: the generic Threefold.toNumClass_deg* projections are already simp and rewrite the left-hand side first, so the normal-form linter rejects the attribute. p3_reZ and p3_imZ name these explicitly.

theorem AlgebraicGeometry.Numerical.Examples.p3_toNumClass_deg1 (E : ThreefoldNum) : (Threefold.toNumClass p3NumericalVariety p3Polarization E).deg1 = ↑(E 1)

Not a simp lemma: the generic Threefold.toNumClass_deg* projections are already simp and rewrite the left-hand side first, so the normal-form linter rejects the attribute. p3_reZ and p3_imZ name these explicitly.

theorem AlgebraicGeometry.Numerical.Examples.p3_toNumClass_deg2 (E : ThreefoldNum) : (Threefold.toNumClass p3NumericalVariety p3Polarization E).deg2 = ↑(-↑(E 1) / 2 + ↑(E 2))

Not a simp lemma: the generic Threefold.toNumClass_deg* projections are already simp and rewrite the left-hand side first, so the normal-form linter rejects the attribute. p3_reZ and p3_imZ name these explicitly.

theorem AlgebraicGeometry.Numerical.Examples.p3_toNumClass_deg3 (E : ThreefoldNum) : (Threefold.toNumClass p3NumericalVariety p3Polarization E).deg3 = ↑(↑(E 1) / 6 - ↑(E 2) + ↑(E 3))

Not a simp lemma: the generic Threefold.toNumClass_deg* projections are already simp and rewrite the left-hand side first, so the normal-form linter rejects the attribute. p3_reZ and p3_imZ name these explicitly.

The charge family on the model

noncomputable def AlgebraicGeometry.Numerical.Examples.p3WallChargeFamily : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily (ℝ × ℝ) ThreefoldNum

The threefold charge family of ℙ³, indexed by (α, β).

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.p3WallChargeFamily_charge (p : ℝ × ℝ) (E : ThreefoldNum) : (p3WallChargeFamily.charge p) E = (CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.charge p.1 p.2) (Threefold.toNumClass p3NumericalVariety p3Polarization E)

theorem AlgebraicGeometry.Numerical.Examples.p3_reZ (α β : ℝ) (E : ThreefoldNum) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.reZ α β (Threefold.toNumClass p3NumericalVariety p3Polarization E) = -↑(↑(E 1) / 6 - ↑(E 2) + ↑(E 3)) + β * ↑(-↑(E 1) / 2 + ↑(E 2)) - (β ^ 2 - α ^ 2) / 2 * ↑(E 1) + (β ^ 3 - 3 * β * α ^ 2) / 6 * ↑(E 0)

The real part of the ℙ³ charge, in linear-section coordinates.

theorem AlgebraicGeometry.Numerical.Examples.p3_imZ (α β : ℝ) (E : ThreefoldNum) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.imZ α β (Threefold.toNumClass p3NumericalVariety p3Polarization E) = α * (↑(-↑(E 1) / 2 + ↑(E 2)) - β * ↑(E 1) + (3 * β ^ 2 - α ^ 2) / 6 * ↑(E 0))

The imaginary part of the ℙ³ charge, in linear-section coordinates.

A sanity witness for the Bayer--Macrì--Toda datum

def AlgebraicGeometry.Numerical.Examples.p3BMTSanity : Threefold.BMTData p3NumericalVariety p3Polarization

A sanity witness, not geometry.

TiltSemistable is taken to be the conclusion itself, so nonneg holds tautologously. This asserts nothing whatsoever about sheaves or about tilt stability: it exists only to show BMTData is inhabitable and that the transported theorems fire on a concrete model. Do not read it as the Bayer--Macrì--Toda inequality for ℙ³, which is a real theorem this repository does not contain, nor as evidence for the conjecture, which is false for some threefolds.

Equations

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

theorem AlgebraicGeometry.Numerical.Examples.p3_Q_toNumClass_nonneg {α β : ℚ} {E : ThreefoldNum} (hα : 0 < α) (hE : p3BMTSanity.TiltSemistable α β E) : 0 ≤ CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.Q (↑α) (↑β) (Threefold.toNumClass p3NumericalVariety p3Polarization E)

The transported inequality, on the model. Its content is exactly the content of p3BMTSanity, which is none.