The wall layer of ℙ⁴, at zero polynomial cost #
Models/Fourfold/ProjectiveSpace.lean builds the ℙ⁴ numerical model with
proved Riemann--Roch, and until this file nothing connected it to a charge: no
fourfold charge or wall family existed anywhere in the tree, because every
charge in the tree was written per dimension and nobody had written the
dimension-four one.
This file writes no charge polynomial. Its entire content is one
Polarization, after which Polarised.wallChargeFamily at (n, m, κ) = (4, 4, 1)
supplies the family and Wall.Exp.ofMoments supplies the polynomial. That is
the point of the slice: a new dimension costs a polarisation, not a charge.
What the slots come out as #
The transport's slot k is ∫ H^(4-k) · ch_k(E), and on a Picard-rank-one
model ∫ H^(4-k) · Hᵏ = ∫H⁴. With ∫_{ℙ⁴} H⁴ = 1 the five slots are therefore
the linear-section Chern coefficients themselves, which is what
p4_hDegrees_eq_chCoeff says in one statement for all five. Slot 0 is
E 0 = rank E, which is the ∫H⁴ = 1 case of the root's hDegrees_zero; on
the sextic (CalabiYauWalls.lean) the same slot carries the factor 6 and the
weighting is visible.
p4_charge evaluates the family, and it is the only place the coefficients
1, -1, 1/2, -1/6, 1/24 appear — read off Wall.Exp.coeff, not written down
here.
The gap this slice records rather than fills #
The n = 4 graded pairing has no counterpart in this repository. There is
no fourfold discriminant, no fourfold self-pairing, and hence no comparison to
prove and no consumer to serve. The charge needs none of that — ofMoments
takes moments, and the scalar moments of a compressed degree vector are all the
family uses — so the slot is left genuinely empty. Inventing a pairing to fill
it would add a definition with no leaf reaching it, which is the failure the
abstraction tree's root-review clause exists to prevent.
Main definitions #
p4Polarization— the hyperplane class ofℙ⁴, the first polarisation of a fourfold model in the repository.p4WallChargeFamily— the wall family, inherited rather than defined.
Main results #
p4_degree_H_pow_four—∫_{ℙ⁴} H⁴ = 1.p4_hDegrees_eq_chCoeff— the five slots, in linear-section coordinates.p4_charge— the charge evaluated on those coordinates.
The polarization #
∫_{ℙ⁴} H⁴ = 1.
The hyperplane class as a polarization of ℙ⁴. The first polarization
of a fourfold model in the repository, and the entire cost of the wall layer
below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The transported H-degrees #
The five slots of ℙ⁴, all at once. Slot k is
∫ H^(4-k) · ch_k(E) = ch_k(E) because ∫_{ℙ⁴} H⁴ = 1, so the compressed
degree vector is the linear-section coefficient sequence on the nose.
Stated for every k : Fin 5 rather than five times: the k-dependence is
entirely inside fourfoldChCoeff, and the only fact about k the proof uses is
k ≤ 4, which is Fin.isLt.
The charge family on the model #
The wall family of ℙ⁴, inherited from Polarised.wallChargeFamily at
(n, m, κ) = (4, 4, 1). No charge polynomial is written here or anywhere else
for dimension four; the polynomial is Wall.Exp.ofMoments.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ℙ⁴ charge in linear-section coordinates.
Z(w) = -(ch₄ - w·ch₃ + w²/2·ch₂ - w³/6·ch₁ + w⁴/24·ch₀), which is
-∫exp(-wH)·ch(E) truncated at codimension four. The five coefficients are
Wall.Exp.coeff 0..4; they are read off the kernel, not written down for this
model.