Quadratic algebras
Quadratic-algebra presentations and total fraction rings, squarefree integral-closure criteria, diagonal quadratics, real-closed negative-discriminant witnesses and chosen quadratic coordinates, and the class number of the number field generated by a square root of minus five. For any real-closed field R, QuadraticAlgebra R (-1) 0 is algebraically closed and irreducible polynomials over R have degree at most two. Its irreducible nonlinear polynomial quotients admit noncanonical algebra equivalences with this quadratic field. For real coefficients, that field identifies with the complex numbers, and evaluation at a chosen complex root gives an algebra equivalence for irreducible nonlinear quotients.
Quoted from the project description in formalization.yaml of FormalFrontier/quadratic-algebras at commit 16a5b4c5, Apache-2.0.
No articles: its formalization.yaml lists no highlights, and none of its 7 headline results links a declaration that the scan finds in the linked file at this commit, so they are quoted below.
Facts
From the repository and its formalization.yaml; the review and automation statements are quoted as written.
- Repository: FormalFrontier/quadratic-algebras, read at commit 16a5b4c5 (2026-11-04).
- Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
- License: Apache-2.0.
- Authors: Formal Frontier Agents.
- Review status: “agent-reviewed mathematical development”.
- Review notes: “The stated scope does not assert complete source correspondence.”
- Automation: agent; tool setup “Formal Frontier AI agents used Lean and pinned Mathlib to develop proofs, documentation and downstream examples.”
- Automation notes: “AI agents contributed mathematical proofs, module and client migration, and documentation.”
Literature
The sources its formalization.yaml names, with their relationship to it.
- Quadratic algebras, integral closure, diagonal forms and arithmetic of minus five (original-proof; formalizes).
Builds on
No other Formal Frontier library.
Headline results
Quoted from the headline results in README.md of FormalFrontier/quadratic-algebras at commit 16a5b4c5, Apache-2.0.
The results below extend mathlib's quadratic-algebra, polynomial, localization and number-field infrastructure. They provide changes of presentation, integral-closure tests and explicit arithmetic examples; the imported infrastructure is not a new contribution of this library. The API reference gives the historical native signatures and a guide to the newer real-closed declarations; the binding guide also describes the later complex quotient interface and module imports.
Presentations, scalar extension and integral closure
The library connects mathlib's coordinate model QuadraticAlgebra R a b with
the polynomial quotient AdjoinRoot (X ^ 2 - C b * X - C a). It also proves
that scalar extension commutes with quadratic algebras and canonically
identifies their total fraction rings with base change to FractionRing R.
These results allow zero divisors and the zero ring: a total fraction ring is
not being asserted to be a field. The library also proves
the squarefree denominator lemma for arbitrary fraction fields of unique
factorization domains: if f is squarefree and x² f lies in the base ring,
then x is already in the base ring. It also shows
that the trace and norm of an integral quadratic element over the fraction
field of an integrally closed ring belong to the base ring, without assuming
that the quadratic algebra is a domain. Combining these ingredients, it proves
that a quadratic algebra with squarefree radicand over a unique factorization
domain is integrally closed in its total quotient ring when 2 is invertible,
even if the quadratic algebra has zero divisors. Conversely, for a domain
quadratic algebra, a nonzero nonunit square divisor of the radicand gives an
explicit integral fraction outside the quadratic algebra; in particular, a
domain quadratic algebra over a unique factorization domain is not integrally
closed when its
radicand is not squarefree. Together, these results give the exact criterion:
a domain quadratic algebra over a unique factorization domain, with 2
invertible, is integrally closed if and only if its radicand is squarefree.
Here IsIntegrallyClosed uses Mathlib's total quotient ring, not necessarily a
fraction field. The forward theorem applies, for example, to A = ℚ, f = 1,
where the quadratic algebra is isomorphic to ℚ × ℚ. The reverse obstruction
and the if-and-only-if criterion retain their quadratic-domain hypothesis.
For A = ℚ, f = 0, the dual numbers have only units as regular elements,
so they are integrally closed in this total-quotient sense although 0 is not
squarefree. Thus the converse cannot simply drop the domain hypothesis.
Over the integers, where 2 is not invertible, the library separately proves
that a quadratic algebra with squarefree radicand is integrally closed when
the radicand is congruent to 2 or 3 modulo 4; this congruence also yields
the required domain property. This integer result does not assume that two is
invertible in the integers.
Key interfaces are the polynomial-quotient equivalence, scalar-extension and total-fraction-ring maps, UFD squarefree criterion and separate integer criterion.
Chosen coordinates for quadratic algebras
Over a field R with [IsRealClosed R], irreducibility of
QuadraticAlgebra.definingPolynomial a b supplies a nonzero d with
d² = -QuadraticAlgebra.discr a b; see the
real-closed witness. Separately, over
any field with [NeZero (2 : R)], a supplied d ≠ 0 satisfying this
square identity gives a chosen equivalence
from QuadraticAlgebra R a b to QuadraticAlgebra R (-1) 0. Its generator
maps to (d / 2) • omega + algebraMap R _ (b / 2); replacing d with -d
conjugates that image, without selecting a preferred sign or requiring
irreducibility of the supplied-witness equivalence. The
quotient version additionally assumes p
is monic with p.natDegree = 2, and evaluates every polynomial class
AdjoinRoot.mk p g at the image of the chosen root. These conditional chosen
coordinates are distinct from the earlier canonical quotient bridge over
arbitrary commutative rings; they do not choose a sign or provide an
arbitrary-degree quotient equivalence.
Algebraic closure over a real-closed field
For any field R with [IsRealClosed R], the canonical quadratic field
QuadraticAlgebra R (-1) 0 is algebraically closed. No order or nonsquare
witness is supplied by the caller: semireality proves the field witness
Fact (¬ IsSquare (-1 : R)). Every element of this quadratic field has a
square root, and a finite normal closure with the Galois correspondence and
Sylow's theorem rules out any further finite extension. Consequently every
irreducible p : R[X] satisfies p.natDegree ≤ 2.
The independent real model proves
IsRealClosed ℝ without importing the closure result. It exhibits irreducible
X² + 1 at the bound and reducible X² - 1 and X⁴ - 1 as boundaries.
The dependent clients exercise
the square-root and cubic-root results and compare the general degree bound
with Mathlib's real-only bound. See the
closure API.
Irreducible polynomial quotients
For an arbitrary real-closed field R, each irreducible p : R[X] with
1 < p.natDegree has an R-algebra equivalence from AdjoinRoot p to
QuadraticAlgebra R (-1) 0; no monicity or discriminant witness is required.
Over any base field, the chosen-root constructor for an irreducible quadratic
specifies the image of the adjoined root and evaluates every polynomial class
at it. The witness-free constructor chooses
such a root without identifying the maps arising from different choices.
The independent real model supplies
irreducible quadratic and reducible boundaries; the
quotient clients also exercise
a nonmonic scalar multiple and both signs of the quadratic generator.
Complex coordinates and real polynomial quotients
The complex coordinate equivalence
identifies QuadraticAlgebra ℝ (-1) 0 with ℂ as real algebras, sending
omega to Complex.I and exposing both coordinate formulas. For an
irreducible p : ℝ[X] of degree two and any specified complex root z, the
same module identifies AdjoinRoot p with ℂ by evaluation at z: the
image of AdjoinRoot.mk p g is g.eval₂ (algebraMap ℝ ℂ) z for every g.
For any irreducible nonlinear real polynomial it also provides a witness-free
equivalence using a selected complex root, without choosing a sign or
requiring monicity, a discriminant witness, or a root from the caller. The
Gaussian clients exercise
both ±Complex.I, a nonmonic scalar multiple, arbitrary quotient classes and
the variable class in the ideal quotient. This is an algebraic presentation;
it does not supply maximality, scheme residue fields or topology.
Diagonal quadratics
The library also defines the finitely supported
diagonal multivariate quadratic MvPolynomial.sumSMulXSq c. Over any field
of characteristic different from two, this polynomial is squarefree when at
least two coefficients are nonzero and irreducible when at least three are
nonzero. A binary diagonal quadratic aXᵢ² + bXⱼ² is also irreducible when
i ≠ j, a ≠ 0, and -b/a is not a square. The declarations work over
arbitrary variable types and do not assume an algebraic closure or classify
quadratic forms. Coefficient, derivative and homogeneity lemmas need only a
commutative coefficient ring; the field and NeZero (2 : k) assumptions belong
to the irreducibility and squarefreeness results.
See the diagonal construction, squarefreeness theorem, three-coefficient irreducibility theorem and binary nonsquare criterion.
The order and number field generated by a square root of minus five
A domain quadratic algebra
over a Dedekind domain is also shown to be Dedekind whenever it is integrally
closed, using its finite-module and integral structures. Finally, the library
proves that the integer quadratic algebra QuadraticAlgebra ℤ (-5) 0 is not
a unique factorization monoid: the embedded integer 2 is irreducible by the
norm form x² + 5y², but is not prime because
(1 + ω) * (1 - ω) = 6.
The fraction field of this order is also exposed as a number field, with a
canonical identification of the order with its ring of integers. Its standard
integral basis has discriminant -20; the field has degree two and one complex
place. The resulting explicit Minkowski estimate shows that every ideal class
has a representative of absolute norm at most two. This does not yet classify
those ideals by itself. Reduction to ZMod 2 defines the unique ideal of
absolute norm two; this ideal is nonprincipal, while an ideal of absolute norm
one is the unit ideal. Consequently every ideal class is either trivial or the
class of this distinguished ideal, and the class number is two.
These results are independent of the organization of any motivating source.
Entry points include failure of unique factorization, the ring-of-integers identification and the class-number-two theorem.
Main results
Its formalization.yaml lists 19 main results, and the scan finds 18 of them declared in the file the yaml gives; they are on their own page, not made articles. The scan does not find QuadraticAlgebra.instIsAlgClosedNegOfNat_quadraticAlgebras (QuadraticAlgebras/RealClosedClosure.lean).
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.