FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024)
FC11 — Peters & Sterk, Symmetric and Quadratic Forms.
This chapter contains 4 definitions, 5 theorems, 2 propositions, 2 lemmas, 2 corollaries, 1 example, 3 remarks and 1 convention.
Of the 20 statements checked against Lean, 5 are formalized somewhere and 15 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 15 | 75% | A documented search found no Lean statement of it anywhere. |
| in lean-categories | 2 | 10% | This repository states and proves it. |
| in another Lean project | 2 | 10% | Some other Lean development has it; using it means porting that code. |
| in Mathlib | 1 | 5% | Mathlib states and proves it. |
| checked in total | 20 |
- Canonical source block: FC11 Peters–Sterk Chapter 3, “Quadratic Forms over ℚ and ℚ_p”,
FC11-C03-U001–FC11-C03-U020, 20 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 20 units received successful unit-level LeanSearch searches before rate limiting began on later chapters. Project and pinned/current Mathlib were searched locally; Mathlib history/open-PR families, Reservoir/package index, Loogle, broad GitHub Lean, the source atlas, formal-conjectures, TauCeti, jonhanke/quadratic_forms_in_lean, and current mariainesdff/HassePrinciple were checked. HassePrinciple was fetched at 47df8f51939b364e678893d54e8a3faf6ec52302 and audited for explicit sorry dependencies.
- Unit-level LeanSearch captures: 20/20 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. - HassePrinciple candidates, when used, are pinned at
47df8f51939b364e678893d54e8a3faf6ec52302(Apache-2.0, Lean 4.34.0-rc2, Mathlib2fbace17aa59d5dd7d99fc4af3849722f69272df) and likewise route asreference-port; declarations whose proof or required dependency remainssorryare not accepted as positive evidence. - Route totals:
mathlib1,project-existing2,package-import0,reference-port2,unmatched15. - 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.
Definition / construction
The Hasse invariant of a diagonal quadratic form is the product of the Hilbert symbols of its diagonal coefficients.
Formalized. LeanCategories/Lattices/Valued/Hasse.lean::hasseMinkowskiInvariantOfDiagonal, hasseMinkowskiInvariantOfDiagonal_eq_prod_Iio — For a diagonal tuple of nonzero coefficients this is exactly the product over i<j of the Hilbert symbols, matching the source Hasse invariant definition.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction
Over a field of characteristic different from \(2\), a quadratic form \(q\) has associated symmetric bilinear form \(x\cdot y=\frac12(q(x+y)-q(x)-q(y))\), so that \(x\cdot x=q(x)\).
Formalized. Mathlib/LinearAlgebra/QuadraticForm/Basic.lean::QuadraticMap.associatedHom, QuadraticMap.associated_apply, QuadraticMap.associated_eq_self_apply — When 2 is invertible, associatedHom is one half of the polar form q(x+y)-q(x)-q(y), and associated_eq_self_apply gives b(x,x)=q(x), exactly the source convention.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Convention / notation
The split non-degenerate binary quadratic space is called the hyperbolic plane.
Formalized. HassePrinciple/QuadraticForm/Basic.lean::QuadraticMap.XY, QuadraticMap.IsHyperbolic, QuadraticMap.XY_isHyperbolic — The reference source defines the binary split form XY and calls a quadratic form hyperbolic exactly when it is equivalent to that two-dimensional model. The declarations are complete, but the source targets Lean 4.34.0-rc2 and therefore require a port.
Searched: reference source pinned in targets; Apache-2.0; source port required to Lean 4.33.0
Definition / construction / notation
The concept of a contiguous chain of orthogonal bases will be used to show that the Hasse invariant does not depend on the particular diagonalization. By definition, such a chain starts from a given orthogonal basis and at each step one forms a new orthogonal basis by replacing a finite number of vectors of the basis, making sure that at least one vector stays the same.
Not formalized. The reference source has the intended vocabulary, but its Chain structure currently states contiguity of a basis with itself rather than consecutive bases, so it is not interface-equivalent to the source definition.
Example / comparison
Example 3.1.1. Take \(\mathbb { R } ^ { 3 }\) with the standard euclidean metric. Let \(\{ e _ { 1 } , e _ { 2 } , e _ { 3 } \}\) be orthonormal. Take a rotation in the plane spanned by \(\{ e _ { 2 } , e _ { 3 } \}\) giving \(\{ e _ { 1 } , e _ { 2 } ^ { \prime } , e _ { 3 } ^ { \prime } \}\) followed by a rotation in the plane \(\{ e _ { 1 } , e _ { 2 } ^ { \prime } \}\) giving \(\{ e _ { 1 } ^ { \prime } , e _ { 2 } ^ { \prime \prime } , e _ { 3 } ^ { \prime } \}\) . This gives the contiguous chain \[ \{ e _ { 1 } , e _ { 2 } , e _ { 3 } \} \{ e _ { 1 } , e _ { 2 } ^ { \prime } , e _ { 3 } ^ { \prime } \} \{ e _ { 1 } ^ { \prime } , e _ { 2 } ^ { \prime \prime } , e _ { 3 } ^ { \prime } \} . \]
Not formalized. No exact formalization of the displayed Euclidean rotation example was identified; the reference chain file contains only the general setup.
Proposition 3.1.2
Proposition 3.1.2. Suppose that \(\dim V \geq 3\) . Then any two orthogonal bases are connected by a contiguous chain of orthogonal bases.
Not formalized. The exact reference theorem exists only with a sorry proof in current upstream, so it is not accepted as a completed owner.
Proposition 3.1.3
Proposition 3.1.3. The Hasse invariant is well defined, i.e., independent of the choice of orthogonal basis.
Formalized. LeanCategories/Lattices/Valued/HasseInvariance.lean::hasseMinkowskiInvariantOfDiagonal_eq_of_equivalent, DiagonalPresentation.hasseMinkowskiValue_eq, hasseMinkowskiInvariant — The project proves directly that the diagonal Hasse value is invariant under quadratic equivalence and that any two diagonal presentations compute the same canonical value. This supplies the source well-definedness result without the incomplete chain proof.
Searched: A=12618f8abc2b4852b3da9ab65c3bc547ac4c1f19; Apache-2.0; Lean 4.33.0
Definition / construction / notation
A quadratic form \(q\) represents \(a\in k\) if \(q(x)=a\) for some non-zero vector \(x\); in particular, it represents \(0\) exactly when it has a non-zero isotropic vector.
Formalized. HassePrinciple/QuadraticForm/Basic.lean::QuadraticMap.Isotropic, QuadraticMap.represents, QuadraticMap.represents_zero_iff_isotropic — The reference source defines representation by a nonzero vector and proves representation of zero equivalent to isotropy exactly as in the source. These declarations are complete but require a toolchain port.
Searched: reference source pinned in targets; Apache-2.0; source port required to Lean 4.33.0
Lemma 3.2.1
Lemma 3.2.1. If \(x \in V\) is isotropic, then \(q\) represents all elements in \(k\) .
Not formalized. The reference source has the exact theorem under nondegeneracy, but its current proof is sorry; no independent completed owner was found.
Remark 3.2.2
Remark 3.2.2. The preceding result is subsumed by the more general Lemma 6.3.8.
Not formalized. This is a cross-reference to a later general lemma; no independent completed declaration matching the remark was found.
Lemma 3.2.3
Lemma 3.2.3 (Representability criterion (characteristic \(\neq 2\) )). Let \(a \in k ^ { \times }\) . Then the following conditions are equivalent: 1. ?? represents \(a\) ; 2. \(q \simeq q ^ { \prime } \oplus [ a ]\) where \(q ^ { \prime }\) has rank \(n - 1\) ; 3. \(q \oplus [ - a ]\) represents 0.
Not formalized. The reference source contains the crucial representation-versus-isotropy criterion, but it is still sorry in current upstream; the full three-way equivalence therefore has no completed owner.
Theorem 3.2.4
Theorem 3.2.4. Any quadratic form \(q\) of rank \(\geq 5\) over \(\mathbb { Q } _ { p }\) represents zero.
Not formalized. The searched reference project proves only the rational Hasse-Minkowski high-rank step, and its key high-rank isotropy theorem remains sorry; no completed theorem that every rank-at-least-five form over Q_p is isotropic was found.
Theorem 3.2.5
Theorem 3.2.5 (Representability criterion (over \(\mathbb { Q } _ { p }\) )). Let \(q\) be a non-degenerate quadratic form over \(\mathbb { Q } _ { p }\) of rank \(n\) and \(a \in \mathbb { Q } _ { p } ^ { \times }\) . In order that ?? be represented by \(q\) , depending on its rank \(n\) , the necessary and sufficient condition is for \(n = 1\) : \(a = \operatorname { d i s c } ( q )\) ; for \(n = 2\) : \(( a , - \operatorname { d i s c } ( q ) ) _ { p } = \varepsilon _ { p } ( q )\) ; for \(n = 3\) : either \(a \neq - \operatorname { d i s c } ( q )\) , or \(a = - \operatorname { d i s c } ( q )\) and \(( - 1 , - \operatorname { d i s c } ( q ) ) _ { p } = \varepsilon _ { p } ( q )\) ; for \(n \geq 4\) : no condition ( \(\mathit { \Pi } _ { a }\) is always represented by \(q\) ).
Not formalized. Rank-two/three Hilbert-symbol ingredients and p-adic symbol formulae exist, but the source row is the complete rank-by-rank Q_p representability classification. No single completed owner supplies all four cases.
Remark 3.2.6
Remark 3.2.6. If \(q\) is the localization of a non-degenerate ternary form over \(\mathbb { Q }\) , this implies that \(q\) assumes all values of \(\mathbb { Q } _ { p } ^ { \times }\) with one possible exception, \(e _ { p } : = - \operatorname { d i s c } ( q )\) , but this happens at most for the finite set of primes \(p\) for which \({ \varepsilon } _ { p } ( q ) \cdot ( - 1 , e _ { p } ) _ { p } =\) \(^ { - 1 }\) .
Not formalized. The local Hilbert-symbol computations do not provide the finite-exceptional-prime theorem for a localized rational ternary form as an existing declaration.
Theorem 3.3.1
Theorem 3.3.1. Two non-degenerate quadratic forms over \(\mathbb { Q } _ { p }\) are isometric if and only if they have the same rank, discriminant and Hasse invariant.
Not formalized. Rank, discriminant and Hasse invariants are represented, but no completed theorem classifies all nondegenerate Q_p quadratic forms up to isometry by those invariants.
Theorem 3.3.2
Theorem 3.3.2 (Hasse–Minkowski). A non-degenerate form \(q\) over \(\mathbb { Q }\) represents 0 if and only if \(q _ { v }\) represents zero for all places \(v \in \mathcal { P }\) .
Not formalized. The reference source has the exact Hasse-Minkowski statement, but every rank branch of the current proof is sorry; it is therefore not accepted as a completed reference port.
Corollary 3.3.3
Corollary 3.3.3. A rational non-zero number ?? is represented by a non-degenerate form \(q\) over \(\mathbb { Q }\) precisely if for all \(v \in \mathcal { P }\) the number ?? is represented over \(\mathbb { Q } _ { v }\) by the non-degenerate form \(q _ { v }\) .
Not formalized. The representability corollary would require the incomplete Hasse-Minkowski theorem together with the incomplete representation/isotropy criterion; no independent completed theorem was found.
Corollary 3.3.4
Corollary 3.3.4 (Meyer’s theorem). A non-degenerate rational quadratic form of rank \(\geq 5\) represents 0 if and only if it is indefinite.
Not formalized. Meyer’s theorem is not present as a completed declaration; deriving it would require the incomplete global theorem plus local high-rank isotropy.
Theorem 3.3.5
Theorem 3.3.5 (Hasse Principle). Two non-degenerate quadratic forms over \(\mathbb { Q }\) are isometric if and only if this is so locally, that is over each \(\mathbb { Q } _ { v }\) , \(v \in \mathcal { P }\) . In other words: if \(L _ { 1 }\) and \(L _ { \mathrm { 2 } }\) are two quadratic spaces over \(\mathbb { Q }\) , then an isometry \(L _ { 1 } \stackrel { \sim } { } L _ { 2 }\) exists if and only if isometries \(L _ { 1 , v } \stackrel { \simeq } { \to } L _ { 2 , v }\) exist for all places \(v \in \mathcal { P }\) .
Not formalized. The searched sources formalize isotropy local-global infrastructure, not the source isometry Hasse principle for two rational quadratic spaces. No completed exact owner was found.
Remark 3.3.6
Remark 3.3.6. 1. If for all \(v \in { \mathcal { P } }\) we have isometries \(\phi _ { v } : q _ { 1 , v } \to q _ { 2 , v }\) , the above theorem states that a global isometry exists. However its localization at \(v \in \mathcal { P }\) need not be equal to \(\phi _ { v }\) . 2. A non-degenerate real form \(q\) is classified by its signature, \(( s , t )\) . Since \(\mathrm { d i s c } ( q _ { \infty } )\) \(\mathbf { \Phi } = \mathbf { \Phi } ( - 1 ) ^ { t }\) and \(\varepsilon _ { \infty } ( q ) = ( - 1 ) ^ { t ( t - 1 ) / 2 }\) , the Hasse invariants and the discriminant don’t suffice for the classification at \(\infty\) . 3. The Hilbert product formula (Theorem A.4.6) implies that \[ \prod _ { v } \varepsilon _ { v } ( q ) = 1 , \]
Not formalized. Parts of the bundled remark are formalized (real Hasse invariant/signature behavior and Hilbert-product infrastructure), but the row also asserts the behavior of prescribed local isometries and the full global product statement. Strict whole-row semantics therefore leave it unmatched.