FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024)
FC11 — Peters & Sterk, Symmetric and Quadratic Forms.
This chapter contains 5 definitions, 8 theorems, 1 proposition, 3 lemmas, 4 corollaries, 5 examples, 5 constructions, 2 remarks and 1 other statements.
Of the 34 statements checked against Lean, 1 are formalized somewhere and 33 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 33 | 97% | A documented search found no Lean statement of it anywhere. |
| in lean-categories | 1 | 3% | This repository states and proves it. |
| checked in total | 34 |
- Canonical source block: FC11 Peters–Sterk Chapter 2, “Indefinite Unimodular Integral Lattices”,
FC11-C02-U001–FC11-C02-U034, 34 units, exact canonical order from FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024). - Project baseline
A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19(Apache-2.0, Lean 4.33.0); pinned MathlibP=db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean 4.33.0); current upstream MathlibH=71a80585ee495fc24472fd0eaffc89d94e4fd8d6. - All 34 units received successful unit-level LeanSearch searches. Project/pinned/current Mathlib, local Mathlib history and open PRs, the source atlas/formal-conjectures, TauCeti, Reservoir package index, Loogle families, and broad GitHub Lean searches were checked; topology-specific searches covered intersection forms, Freedman, Donaldson, Rokhlin/Rohlin, Stiefel-Whitney, K3 and the 11/8 conjecture.
- Unit-level LeanSearch captures: 34/34 successful.
- Strict whole-row semantics: a positive route requires an already existing complete compatible owner; partial definitions, constructors, generic ingredients, comments, axioms, or theorem fragments remain
unmatchedwhen substantive reconstruction would be required. - TauCeti candidates, when used, are pinned at
98a6bfc9f3cb4ab3a159d83858ce546d1e543c1b(Apache-2.0, Lean 4.34.0-rc2, Mathlibe21ec05048292b3de86d4cf1987e2208171a5642) and therefore route asreference-port, not direct package import, unless an independently compatible package owner is recorded. - Route totals:
mathlib0,project-existing1,package-import0,reference-port0,unmatched33. - Negative results are scoped to the inspected revisions and dated search surfaces on 2026-09-07; they are not claims about future repository/package state.
Theorem: Theorem
Theorem. An indefinite unimodular lattice is uniquely determined by its parity, rank and index.
Not formalized. The project defines parity, signature and unimodularity and supplies standard models, but no theorem classifies every indefinite unimodular integral lattice by parity, rank and index.
Definition 2.1.1
Definition 2.1.1. Let \(( L , b )\) be an integral lattice and \(p\) a prime number. Its reduction modulo \(p\) consists of the \(\mathbb { F } _ { p }\) -vector space \(L / p L\) equipped with the symmetric \(\mathbb { F } _ { p }\) -bilinear form induced by \(^ { b }\) .
Formalized. LeanCategories/Lattices/Valued/Residue.lean::reduceIntegralToResidueField, reduceIntegralToResidueField_pairing_tmul — For R=Z and the prime ideal (p), the residue-field base change is the canonical reduction of the lattice modulo p and its pairing is the reduction of the integral pairing.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Construction / comparison
Reduction of an integral lattice modulo \(p\) can become degenerate; if the original discriminant is prime to \(p\), the reduced bilinear form is non-degenerate and hence gives an inner-product space over \(\mathbf F_p\).
Not formalized. The reduction functor and the generic criterion that a finite bilinear form is nondegenerate iff its determinant is nonzero are available, but no existing declaration connects primality of the integral discriminant to nondegeneracy of this lattice reduction as one theorem.
Lemma 2.1.2
Lemma 2.1.2. Let \(( L , b ) \underline { { \ d } }\) be an even integral lattice with \(\operatorname { d i s c } ( b )\) odd. The inner product space \(V = ( L / 2 L , b )\) has even dimension and the rank of \(L\) is also even.
Not formalized. The ingredients for an alternating reduction in characteristic two are present, but the claimed even-dimensionality/rank theorem for an even odd-discriminant lattice is not an existing declaration.
Remark 2.1.3
Remark 2.1.3. An inner product space in characteristic 2 such as \(V\) is a symplectic space. These are treated from a general point of view in Appendix A.5.
Not formalized. Mathlib has alternating bilinear forms and symplectic matrices, but no bundled general symplectic-space owner matching the source remark was identified.
Definition 2.1.4
Definition 2.1.4. Let \(L\) be an integral lattice with odd discriminant. We say that \(u \in L\) is a characteristic element if \(u \cdot x \equiv x \cdot x\) mod 2 for every \(x \in L\) .
Not formalized. TauCeti defines characteristic covectors only for plumbing lattices. The source definition quantifies characteristic elements of an arbitrary odd-discriminant integral lattice.
Example / comparison
Example 2.1.5. For an even integral lattice with odd discriminant \(x \cdot x\) is even by definition, and so \(u = 0\) is a characteristic element.
Not formalized. Evenness is implemented and TauCeti has plumbing characteristic covectors, but no arbitrary-lattice theorem states that zero is characteristic under the source hypotheses.
Lemma 2.1.6
Lemma 2.1.6. Every lattice \(L\) with odd discriminant has a characteristic element \(u \in L\) . Moreover, its so-called \(\sigma\) -invariant \[ \sigma ( L ) : = u \cdot u { \bmod { 8 } } \] does not depend on the choice of the characteristic element. It is an additive invariant, that is, for all lattices \(L\) and ?? with odd discriminant we have \(\sigma ( L { \textcircled { \pm } } M ) =\) \(\sigma ( L ) + \sigma ( M )\) .
Not formalized. No searched source provides existence of characteristic elements for all odd-discriminant lattices together with well-definedness and orthogonal additivity of the square modulo eight.
Remark 2.1.7
Remark 2.1.7. The above concerns only lattices with odd discriminant, the only cases we need later on.
Not formalized. This is a scope remark about the preceding sigma-invariant construction; because that construction is unmatched, there is no independent Lean owner for the remark.
Example / comparison
Example 2.1.8. • Let \(L\) be the symmetric lattice \(L = \oplus ^ { p } \langle 1 \rangle \oplus \oplus ^ { q } \langle - 1 \rangle\) . Since \(\pm e\) is characteristic for the unimodular lattice \(\mathbb { Z } \cdot e\) with \(e \cdot e = \pm 1\) and because of additivity, \(\sigma ( L ) \equiv p - q = \tau ( L )\) mod 8, where, we recall, \(\tau ( L )\) is the index of \(L\) . • For an even lattice the zero vector is a characteristic element and so for even lattices we have \(\sigma ( L ) \equiv 0\) mod 8.
Not formalized. Standard rank-one lattices and evenness exist, but the sigma-invariant calculations modulo eight are not formalized.
Theorem 2.2.1
Theorem 2.2.1 (Classification in rank \(\leq 4\) ). Let \(L\) be a unimodular lattice of rank at most 4. Then either \(L\) is odd and diagonalizable, or, if \(L\) is even, \(L \simeq U\) , or \(L \simeq U \oplus U\) .
Not formalized. The standard hyperbolic lattice and unimodularity/signature predicates exist; the complete rank-at-most-four classification of all unimodular lattices does not.
Corollary 2.2.2
Corollary 2.2.2. Let \(L\) be an indefinite unimodular lattice, then • \(L\) contains an isotropic vector, that is, a non-zero vector \(x\) with \(x \cdot x = 0\) ; • \(L\) is isometric to either \(U \odot L ^ { \prime }\) or to \(W \left( \downarrow \right) L ^ { \prime \prime }\) where \(L ^ { \prime }\) as well as \(L ^ { \prime \prime }\) are unimodular, \(U\) is the hyperbolic plane and \(W = \left. 1 \right. \textcircled { \bullet } \left. - 1 \right.\) .
Not formalized. Generic isotropic-vector and orthogonal-complement tools do not prove that every indefinite unimodular integral lattice contains an integral isotropic vector and splits off U or the odd plane W.
Theorem 2.3.1
Theorem 2.3.1. Every odd indefinite unimodular lattice is diagonalizable, that is, isometric to an orthogonal direct sum of copies of ⟨1⟩ and \(\langle - 1 \rangle\) . In particular, such lattices are classified by their rank and index.
Not formalized. Diagonalization of symmetric forms over fields does not imply integral diagonalization of every odd indefinite unimodular Z-lattice. No integral classification theorem was identified.
Theorem 2.4.1
Theorem 2.4.1. Two even indefinite unimodular lattices with the same rank and index are isometric.
Not formalized. No theorem identifies arbitrary even indefinite unimodular lattices having the same rank and index.
Theorem 2.4.2
Theorem 2.4.2. For every unimodular lattice \(L\) , indefinite or not, we have \(\sigma ( L ) =\) \(\tau ( L )\) mod 8, that is, the index modulo 8 is the \(\sigma\) -invariant. If, moreover, \(L\) is even, the index is divisible by 8.
Not formalized. Signature/index and evenness are represented, but the van der Blij congruence sigma(L)=tau(L) mod 8 and its divisibility consequence are not formalized.
Corollary 2.4.3
Corollary 2.4.3 (Existence and uniqueness for indefinite even unimodular lattices). Let \(L\) be an even unimodular and indefinite lattice of (necessarily even) rank \(r\) and index \(\tau = 8 a \varepsilon\) , where ?? is a non-negative integer and \(\varepsilon = \pm 1\) . Then \(L\) is isometric to \[ \underbrace { ( E _ { 8 } \oplus \cdot \cdot \cdot \oplus E _ { 8 } ) } _ { a \ s u m m a n d s } ( \varepsilon ) \ \textcircled { > } \ \underbrace { U \oplus \cdot \cdot \cdot \oplus U } _ { b \ s u m m a n d s } , \quad b = \frac { 1 } { 2 } ( r - | \tau | ) . \]
Not formalized. E8, the hyperbolic plane and orthogonal-sum constructions exist, but the source row is an existence-and-uniqueness classification for all even indefinite unimodular lattices, which those constructors do not establish.
Example / comparison
Example 2.4.4. Applying this to the lattice \(E _ { 8 } \oplus E _ { 8 } ( - 1 )\) a lattice of rank 16 and index \(0\) , we obtain \(E _ { 8 } \oplus E _ { 8 } ( - 1 ) \simeq \oplus ^ { \mathrm { s } } U\) .
Not formalized. The E8 and U models are implemented, but no isometry E8 plus its opposite to eight hyperbolic planes was identified.
Definition / construction / notation
For an oriented compact \(4\)-manifold \(X\), the cup/intersection pairing on \(H^2(X,\mathbf Z)/\mathrm{tors}\) is its unimodular symmetric intersection form. A form occurring this way is called topologically, respectively differentiably, realizable.
Not formalized. Mathlib mentions intersection forms only as motivation in manifold bordism, while TauCeti constructs the form of a plumbing graph. Neither constructs the unimodular cup/intersection form on H^2 of an arbitrary oriented compact four-manifold or the realizability notions.
Lemma 2.5.1
Lemma 2.5.1. If \(X , X ^ { \prime }\) are two four-manifolds, then we have \(S _ { X \# X ^ { \prime } } = S _ { X } \oplus S _ { X ^ { \prime } }\)
Not formalized. TauCeti proves orthogonal splitting for plumbing blow-ups, not the connected-sum formula for arbitrary four-manifolds.
Construction / comparison
For a simply connected four-manifold, the intersection form is torsion-free; when it is indefinite its isometry class is determined by parity and index.
Not formalized. Simply-connected-space and unimodular-lattice APIs do not establish torsion-freeness of H^2 or the indefinite intersection-form classification for four-manifolds.
Theorem 2.5.2
Theorem 2.5.2. The oriented homeomorphism type of a simply connected fourmanifold \(X\) is completely determined by \(S _ { X }\) and, moreover, any unimodular form can occur in this way as the intersection form of some simply connected fourmanifold.
Not formalized. No formalization of Freedman classification/existence for simply connected topological four-manifolds was found in project, Mathlib, package, GitHub, or reference searches.
Theorem 2.5.3
Theorem 2.5.3 (Donaldson [54]). If a simply connected differentiable four-manifold \(X\) has a definite intersection form it is diagonalizable over \(\mathbb { Z }\) and so \[ S _ { X } = \langle 1 \rangle \oplus \cdots \oplus \langle 1 \rangle { \mathit { o r } } S _ { X } = \langle - 1 \rangle \oplus \cdots \oplus \langle - 1 \rangle . \] In particular, it cannot be an even form.
Not formalized. Algebraic diagonalization over fields is not Donaldson diagonalization over Z. No compatible formalization of Donaldson theorem was found.
Construction / comparison
Donaldson diagonalization together with the indefinite unimodular classification leaves only diagonal forms or orthogonal sums of hyperbolic planes and copies of \(E_8(\pm1)\) as possible intersection forms of smooth simply connected four-manifolds.
Not formalized. The standard U and E8 lattices exist, but the asserted restriction on smooth simply connected four-manifold intersection forms depends on Donaldson and the global integral classification, both unmatched.
Proposition 2.5.4
Proposition 2.5.4 (Criterion for even forms). Let \(X\) be a compact differentiable four-manifold such that \(H ^ { * } ( X , \mathbb { Z } )\) has no 2-torsion. Then \(S _ { X }\) is even if and only if the second Stiefel–Whitney class \(w _ { 2 } ( X )\) vanishes.
Not formalized. No second Stiefel-Whitney class API and no theorem equating its vanishing with parity of the integral intersection form under the no-2-torsion hypothesis was identified.
Example / comparison
Example 2.5.5. Let \(X\) be a simply connected four-manifold. For these \(H _ { 1 } ( X , \mathbb { Z } ) =\) 0 and then \(0 = \operatorname { T o r s } ( H _ { 1 } ( X , \mathbb { Z } ) ) = \operatorname { T o r s } ( H ^ { 2 } ( X , \mathbb { Z } ) )\) , by the universal coefficient theorem and Poincar´e duality (cf. for example [86, Ch. 28]). Hence there is no torsion at all in the cohomology. So, if \(w _ { 2 } ( X ) = 0\) , the intersection form is even.
Not formalized. The searched topology APIs do not supply this universal-coefficient/Poincare-duality torsion calculation for closed simply connected four-manifolds.
Theorem 2.5.6
Theorem 2.5.6 (Rohlin [196]). For a compact differentiable four-manifold \(X\) with \(w _ { 2 } ( X ) = 0\) , the index is divisible by 16.
Not formalized. No compatible formalization of the Rokhlin/Rohlin signature divisibility theorem was found. A broad GitHub hit merely records it as an external missing hypothesis, not a proof.
Corollary 2.5.7
Corollary 2.5.7. Let ?? be a simply connected compact differentiable four-manifold with even intersection form. Then the index of \(S _ { X }\) is divisible by 16.
Not formalized. This corollary depends on the unmatched parity criterion and Rokhlin theorem; no independent exact owner was found.
Corollary 2.5.8
Corollary 2.5.8. Let \(X\) be a simply connected complex manifold of dimension 2 such that \(c _ { 1 } ( X )\) is 2-divisible in \(H ^ { 2 } ( X , \mathbb { Z } )\) . Then \(S _ { X }\) is an even form. Examples include \(K \mathcal { 3 }\) surfaces (see below) and smooth hypersurfaces in \(\mathbb { P } ^ { 3 }\) of even degree. See Table B.3.1.
Not formalized. No formalization connects divisibility of c1 for simply connected complex surfaces to parity of the integral intersection form, and the K3/hypersurface examples are likewise absent.
Definition / construction
For a complex surface, the canonical line bundle is \(K_X=\Lambda^2T_X^*\) and represents \(-c_1(X)\); its holomorphic sections are holomorphic \(2\)-forms, so a nowhere-vanishing holomorphic \(2\)-form trivializes \(K_X\) and forces \(c_1(X)=0\).
Not formalized. Complex manifold and vector-bundle infrastructure exists, but no source-complete canonical-bundle/c1/holomorphic-two-form theorem for compact complex surfaces was identified.
Construction / comparison
For a compact complex surface, \(c_2(X)\) equals the Euler number and the signature satisfies \(\tau(X)=\frac13(c_1(X)^2-2c_2(X))=\frac13(K_X^2-2e(X))\). In particular, when \(K_X\) is trivial the signature is determined by \(e(X)\).
Not formalized. The Chern-number, Euler-number and Hirzebruch signature formula bundle for compact complex surfaces is not present in the searched APIs.
Definition / construction
Write \(E_{a,\pm b}=U^{\oplus a}\oplus E_8(\pm1)^{\oplus 2b}\) for the even indefinite unimodular form of index \(\pm16b\).
Not formalized. U and E8 plus orthogonal constructions exist, but no declared E_{a,±b} family with the stated even/unimodular/index package was identified; assembling it would be new source work.
Example / comparison
A K3 surface realizes \(E_{3,-1}\) and the oppositely oriented K3 realizes \(E_{3,1}\). Connected sums with K3 surfaces and \(Q=\mathbf P^1\times\mathbf P^1\) realize \(E_{3m+n,\pm m}\) by the manifolds \(X(\pm m,n)\).
Not formalized. The abstract K3 lattice is implemented with the right signature/parity/unimodularity, but the source row asserts geometric realization by K3 surfaces and connected-sum realization of a whole family, which are not formalized.
Conjecture (The 11/8 Conjecture)
Conjecture (The 11/8 Conjecture). For every simply connected oriented differentiable four-manifold \(X\) with even intersection form we have the inequality \[ b _ { 2 } ( X ) \geq { \frac { 1 1 } { 8 } } | \tau ( X ) | . \]
Not formalized. No Lean statement/proof of the 11/8 conjecture was found in project, pinned/current Mathlib, formal-conjectures, Reservoir, TauCeti, LeanSearch, Loogle or broad GitHub search.
Construction / comparison
The \(11/8\) conjecture would force every simply connected smooth four-manifold with even intersection form to be homeomorphic to some \(X(\pm m,n)\), with \(m=|\tau(X)|/16\) and \(n=(8b_2(X)-11|\tau(X)|)/16\ge0\). The conjecture holds for complex surfaces.
Not formalized. The consequence uses the 11/8 conjecture, Freedman classification, K3/quadric realizations and the theorem for complex surfaces; these are not jointly formalized.