Arithmetic of fields generated by square roots
Abstract
Galoisness, arithmetic Frobenius and unramifiedness for finite square-root families.
Theorem 1.1 (Finite square-root families generate Galois extensions).
Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/SquareRootArithmetic.squareRootAdjoin_isGalois (✓ std3). ∎
Citation. The Tau Ceti contributors, Chris Birkbeck (2026). Square-root Galois extensions and arithmetic Frobenius in TauCeti. URL: https://github.com/TauCetiProject/TauCeti/blob/14f2a0fe0892587f041a6ca7b6f6a05e31b1f65d/TauCeti/NumberTheory/Multiquadratic/Galois/Basic.lean.
Commentary.
Let K and L be fields, with a K-algebra structure on L. Let I be any finite indexing type, let d : I → K and r : I → L satisfy r(i)^2 = d(i) under the algebra map, and put M = K(r(i) : i ∈ I), the intermediate field generated by the range of r. No independence of the square classes of the radicands is assumed. The indexing type may be empty, radicands may repeat, and a radicand may be zero. Assume also that 2 is nonzero in K.
If 2 is nonzero in K, then M/K is Galois. To prove normality, form f(X) = ∏(X² − d(i)). Each factor splits in M as (X − r(i))(X + r(i)). The elements r(i), regarded as elements of M, belong to the root set of f and generate M; therefore M is a splitting field of f. To prove separability, consider each generator. When d(i) is nonzero, X² − d(i) is separable because 2 is nonzero. When d(i) is zero, the field equation forces r(i) = 0, whose minimal polynomial divides the separable polynomial X. Thus all generators are separable, and M/K is normal and separable. For an empty indexing type the product is 1 and the adjoining field is the base field, so the same statement includes the trivial extension.
The conclusion is Galoisness. A degree equal to 2 to the size of I requires additional square-class independence and is not asserted here.
This is an adaptation of TauCeti.Multiquadratic.isGalois at the immutable revision recorded in the accompanying Library note. It asserts no square-class independence or degree formula.
The finite indexing type and unrestricted radicands include the trivial extension and all zero-radicand cases.
Theorem 1.2 (Arithmetic Frobenius acts by the quadratic sign).
Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/SquareRootArithmetic.arithmeticFrobenius_sqrt (✓ std3). ∎
Citation. The Tau Ceti contributors, Chris Birkbeck (2026). Square-root Galois extensions and arithmetic Frobenius in TauCeti. URL: https://github.com/TauCetiProject/TauCeti/blob/14f2a0fe0892587f041a6ca7b6f6a05e31b1f65d/TauCeti/NumberTheory/Multiquadratic/Galois/Basic.lean.
Commentary.
For a characteristic-zero field K, write O_K for the integral closure of the integers in K. Let p be an odd rational prime, let d be an integer not divisible by p, and suppose x ∈ K satisfies x² = d. Let Q be an ideal of O_K lying over (p) in the integers. Let s be a rational algebra automorphism of K which is an arithmetic Frobenius at Q with base O_Q.
Arithmetic Frobenius uses the positive residue-cardinality exponent: for an integral element a, its image is congruent to a raised to the cardinality of the residue ring of the base. The isomorphism O_Q ≅ Z identifies that base residue cardinality with p. The conclusion is
s(x) = Jacobi(d,p) · x.
At a prime denominator the Jacobi symbol equals the Legendre symbol. Thus the automorphism fixes x when d is a quadratic residue modulo p, and negates x when it is a nonresidue. The assertion is conditional on the given arithmetic Frobenius automorphism; it does not assert that such an automorphism exists.
Here K need not be a number field, and Q is not required to be prime. The hypotheses that p is prime and Q lies over (p) are retained.
The equation x² = d makes x integral, so regard it first as an element of O_K. Since p is odd, x^p = d^(p/2)x. Euler’s criterion says that d^(p/2) and the Legendre symbol are congruent modulo p. The Frobenius congruence consequently gives s(x) − Legendre(p,d)x ∈ Q. Both s(x) and the claimed value are either x or −x, since they square to d and the Legendre symbol is a sign. Opposite signs would put 2x in Q. Multiplying by x would put 2d in Q, forcing p to divide 2d by the lies-over hypothesis. This contradicts oddness and p not dividing d. The two signs therefore agree. Transporting the equality from O_K to K and replacing the Legendre symbol by the Jacobi symbol yields the displayed formula.
The local sign calculation adapts AlgHom.IsArithFrobAt.apply_sqrt. The rational-base residue-cardinality and Jacobi-symbol transports retain the precise receiving statement; the external integer-base Legendre statement has a different full telescope.
The rational-base residue cardinality and integrality of the chosen root connect the residue congruence with the field equality.
Theorem 1.3 (Odd primes avoiding the radicands are unramified).
Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/SquareRootArithmetic.squareRoot_unramified (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. The Tau Ceti contributors, Chris Birkbeck (2026). Square-root Galois extensions and arithmetic Frobenius in TauCeti. URL: https://github.com/TauCetiProject/TauCeti/blob/14f2a0fe0892587f041a6ca7b6f6a05e31b1f65d/TauCeti/NumberTheory/Multiquadratic/Galois/Basic.lean.
Commentary.
Now let K be a number field generated over the rationals by a finite family r : I → K of square roots of integers d : I → Z. Assume r(i)^2 = d(i) for every i and Q(r(i) : i ∈ I) = K. Let p be an odd rational prime which divides none of the d(i). For every prime ideal Q of O_K lying over (p), the extension of rings of integers O_K over O_rational is unramified at Q; O_rational denotes the ring of integers of the rational field.
Galoisness is a consequence of the first result and the generation hypothesis. It is not a premise. To prove unramifiedness, let tau belong to the actual inertia subgroup at Q. Each tau(r(i)) is r(i) or −r(i). If it were the negative, inertia’s trivial action on the residue ring would put 2r(i) in Q. Primality would then put either 2 or r(i) in Q. The first possibility forces p = 2; the second forces p to divide d(i). Both are excluded. Every inertia element fixes every generator, and an automorphism fixing a generating set is the identity. The inertia subgroup is consequently trivial. Its order is the ramification index, so that index is one, which gives unramifiedness at Q.
The conclusion concerns every prime Q over p. It assumes neither an extension degree nor an unramifiedness certificate. Empty and redundant generating families are allowed. No complete-splitting criterion, count of primes, discriminant formula, dyadic law, or GPC5/GPC6 conclusion follows solely from this theorem.
This unrestricted pointwise theorem is a local inertia deduction from the attributed square-root primitives. No exact external theorem with its unrestricted telescope was authenticated. The related external RamifiedPrimes theorem requires squarefree radicands and does not replace it.
An automorphism fixing the complete generating family fixes the whole number field.
These results distinguish Galoisness, a prescribed arithmetic Frobenius action and pointwise unramifiedness; each assertion retains its own complete hypotheses.
Source attribution, immutable declaration locators and the Apache 2.0 license are recorded in D5/L/Factorization/tauceti2026squarerootarithmetic.