Prime Radical Fields: Rational Square Kernel and Degree

Abstract

The actual complex field generated by a finite set of prime square roots has the expected rational square kernel and degree, without an independence assumption.

Definition 1.1 (The actual intermediate field).

$$\forall S\in \mathrm{Finset}(\mathbb{N}),E(S)={\mathrm{adjoin}}_{\mathbb{Q}}(\{\sqrt{p}\mid p\in S\})\subseteq \mathbb{C}$$

Formalization. D5/S3/Factorization/Galois/QuadraticPrimeRadicalKernel.primeRadicalField (✓ std3).

Citation. J. S. Milne (2022). Fields and Galois Theory, version 5.10. URL: https://www.jmilne.org/math/CourseNotes/FT.pdf.

Commentary.

For every finite set S of natural numbers, E(S) is IntermediateField.adjoin over the rationals inside the complex numbers, generated by the complex images of the nonnegative real square roots of the members of S. The theorems below require every member of S to be prime.

Lemma 1.2 (The prime-product obstruction used by the induction).

$$\forall S\in \mathrm{Finset}(\mathbb{N}),(\forall p\in S,\mathrm{Prime}(p))⟹\forall p\in \mathbb{N},(\mathrm{Prime}(p)\wedge \neg (p\in S))⟹\forall T\in \mathrm{Finset}(\mathbb{N}),T\subseteq S⟹\neg \mathrm{IsSquare}(p\cdot \prod _{q\in T}q)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/QuadraticPrimeRadicalKernel.prime_mul_subset_not_square (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. J. S. Milne (2022). Fields and Galois Theory, version 5.10. URL: https://www.jmilne.org/math/CourseNotes/FT.pdf.

Commentary.

If S consists of primes, p is a prime outside S and T is a subset of S, then p times the product of T is not a rational square. Rational nonsquareness is reduced to natural-number nonsquareness and prime divisibility. This obstruction is used by the simultaneous induction and the full original application.

Theorem 1.3 (Exactly which rational numbers become squares).

$$\forall S\in \mathrm{Finset}(\mathbb{N}),(\forall p\in S,\mathrm{Prime}(p))⟹\forall a\in \mathbb{Q},\mathrm{IsSquare}(\mathrm{algebraMap}(\mathbb{Q},E(S),a))⟺\exists T\in \mathrm{Finset}(\mathbb{N}),T\subseteq S\wedge \mathrm{IsSquare}(a\cdot \prod _{p\in T}p)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/QuadraticPrimeRadicalKernel.prime_radical_square_kernel (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. J. S. Milne (2022). Fields and Galois Theory, version 5.10. URL: https://www.jmilne.org/math/CourseNotes/FT.pdf.

Commentary.

The scalar a ranges over all rational numbers, including zero and negative values. The empty support and the prime two are included. IsSquare means existence of an element whose product with itself is the specified scalar. The statement neither assumes square-class independence nor replaces E(S) by an abstract quadratic algebra.

The simultaneous induction uses quadratic coordinate descent: for nonzero d in characteristic different from two, a base scalar is a square in the quadratic model precisely when a or a*d is a base square. Prime divisibility shows that a new prime times any product of distinct earlier primes is not a rational square. A lift into the complex numbers then proves that the model’s field range is exactly the enlarged actual adjoin.

Theorem 1.4 (Finite dimensionality and exact degree).

$$\forall S\in \mathrm{Finset}(\mathbb{N}),(\forall p\in S,\mathrm{Prime}(p))⟹\mathrm{FiniteDimensional}(\mathbb{Q},E(S))\wedge [E(S):\mathbb{Q}]=2^{|S|}$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/QuadraticPrimeRadicalKernel.prime_radical_degree (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. J. S. Milne (2022). Fields and Galois Theory, version 5.10. URL: https://www.jmilne.org/math/CourseNotes/FT.pdf.

Commentary.

For every finite prime support, the actual field is finite dimensional over the rationals and has degree two to the cardinality of the support. The empty support gives degree one. Each insertion uses the square-kernel induction to establish nonsquareness in the entire earlier field; the proved field-range equivalence transports the quadratic rank and the tower formula multiplies the degrees.

Original GPC5 application

The original application takes B(i) from GoldenCubicBlockKummerTower.block, forms A(j) as the product of rad(B(i)) over every 1 <= i < j, and takes S to be the prime factors of A(j). This includes the earlier primes from even depths. The square kernel gives fresh-prime nonsquareness in this field, which supplies the p=2 instance of X_pow_sub_C_irreducible_of_prime.

Arithmetic application: the actual field and its signs

The displayed Lean declarations retain their square-kernel and degree statements. The application below composes those results with the existing normality, ring-of-integers, inertia, residue-Frobenius and ideal-factorization interfaces; it describes their mathematical consequences, rather than an additional public theorem exported by this module. No square-class independence assumption is added.

Let S be any finite set of genuine rational primes, including the empty set and sets containing 2. Use the same actual intermediate field E(S) inside C. For p in S let beta_p be its positive real square root, viewed in E(S), and let b_p be the integral representative in O(E(S)) with underlying element beta_p. Both square to p and are nonzero. The beta_p generate E(S) over Q, and prime_radical_degree gives [E(S):Q] = 2^|S|. Each singleton adjoin is quadratic and normal; their compositum is normal, characteristic zero supplies separability, and finite degree supplies the number-field structure. Thus E(S)/Q is Galois.

Every embedding phi:E(S)->C sends each beta_p to beta_p or -beta_p, since it preserves its square p. These images are real, and generation makes every phi(x) real; hence E(S) is totally real. For G = Gal(E(S)/Q), define sign_p(sigma) in the integer units {1,-1} by sigma(beta_p) = sign_p(sigma)*beta_p. The resulting homomorphism G -> (S -> Z-units) is faithful by generation. The Galois automorphism count and the degree theorem give both groups cardinality 2^|S|, so the sign homomorphism is also surjective. Consequently G is commutative and every sigma satisfies sigma^2 = 1. When S is empty these statements give Q, degree one and the trivial sign group.

Odd primes: actual residues, inertia and arithmetic Frobenius

For every odd rational prime q outside S, write R = O(Q), A = O(E(S)) and e:R->Z for the actual ring equivalence Rat.ringOfIntegersEquiv. Define q_0 = comap(e,(q)) in R, with (q) in Z the principal ideal generated by q. This is a nonzero prime ideal, and the quotient equivalence R/q_0 = ZMod(q) gives cardinality q. For every actual prime ideal P of A lying over q_0, the induced quotient map R/q_0 -> A/P is injective. The upper residue field A/P is finite and has characteristic q; these are the actual quotients of the actual rings of integers.

An inertia element acts on beta_p by one of its two signs. If it acted negatively, its residue identity on b_p would give 2*b_p in P. Primality puts either 2 or b_p in P; squaring b_p and contracting to Z would then give q dividing 2 or p. The assumptions q odd and q outside S exclude both cases. Thus inertia fixes every radical and, by generation, is trivial. The existing inertia-cardinality and ramification-index identities give ramification index one at every P, hence Algebra.IsUnramifiedAt R P and unramifiedness over q_0.

Let F_P(q) be the actual arithmetic Frobenius at P, with residue action x -> x^q. Its residue equation on b_p, together with beta_p^2 = p and Euler’s criterion, gives the residue of (p/q)*b_p, where (p/q) is the Legendre symbol. Since q does not divide p, this symbol is 1 or -1. Comparing it with the two possible signs of F_P(q)(beta_p), a mismatched sign would give 2 times the residue of b_p equal to zero. Odd characteristic and q outside S exclude this. Therefore F_P(q)(beta_p) = (p/q)*beta_p for every p in S. These values determine the automorphism on its generators, so F_P(q) is independent of the upper prime P. Write this common actual automorphism as F(q); its sign_p coordinate is the integer Legendre symbol (p/q).

Complete splitting as an exhaustive product of actual ideals

For every such q, F(q) = 1 is equivalent to the following literal splitting statement. There exists a finite set U of ideals of A with |U| = 2^|S|, whose membership is exactly P in U iff P is prime and lies over q_0. Thus U lists all upper primes, without repetition. Every P in U has |A/P| = q. All three ideal equalities hold: map(R->A,q_0) = product(P in U,P); map(Z->A,(q)) = product(P in U,P); and the principal ideal (q) in A = product(P in U,P). Here map denotes ideal extension along the indicated algebra map, and the product is the ideal product.

To derive the forward direction, use the existing Frobenius-order/residue-degree identity underlying Chebotarev.frobenius_order_stabilizer: trivial Frobenius gives residue degree one. Unramifiedness gives ramification index one, and the Galois efg formula with prime_radical_degree gives exactly 2^|S| primes above q_0. The existing primesOverFinset supplies the exhaustive finite set and its membership characterization. The ideal-factorization formula has exponent one at each member, while the residue norm formula gives each quotient cardinality q. Transport through e and preservation of principal ideals identify the extensions of q_0 and of the integer ideal (q) with the principal ideal (q) in A, proving all three equalities.

Conversely, the stipulated quotient cardinality q at any upper prime, together with the injective map from the base residue field of cardinality q, makes that map bijective. Its linear equivalence gives residue degree one; the same Frobenius-order identity then gives F(q) = 1. Upper-prime independence transfers this conclusion to every upper prime. Faithfulness of signs also identifies F(q) = 1 with (p/q) = 1 for every p in S.

Actual blocks, initial depths and odd-depth kernels

For every j >= 1 put r_j = 3^(j+1), B_j = L_(3^j)^2 + 3 and T_j = {q prime : q divides B_j}, with L = goldenLucas. The integer B_j is positive, so its natural absolute value is the same block. For every q in T_j use the original signed-index Fibonacci depth h_q = v_q(F_(q-(5/q))), where (5/q) is the Legendre symbol, equivalently jacobiSym 5 q. The existing block prime data identify h_q = v_q(B_j) = v_q(F_(rho(q))) > 0. They also give q > 5, (5/q) = 1, rho(q) = pi(q) = 2r_j and q = 1 modulo 2r_j. Thus q is WSS precisely when q^2 divides F_(q-(5/q)), equivalently h_q >= 2. No index-multiplier depth is substituted.

Define s_j = product(q in T_j with h_q odd, q) and a_j = product(q in T_j, q^floor(h_q/2)). The actual factorization gives B_j = s_j*a_j^2. The product defining s_j has distinct prime factors, so s_j is squarefree. It is greater than one: B_j = 19 modulo 80 gives B_j = 3 modulo 8, whereas s_j = 1 would make B_j a square. Pairwise coprimality of the blocks, supplied by GoldenCubicBlockNativePowerPeriods.cubic_block_native_power_periods, implies pairwise coprimality of the s_j.

Every prime factor of a_j is odd, so a_j^2 = 1 modulo 8. Each actual block prime has square 1 modulo 5, by its golden splitting condition. Consequently a_j^2 = 1 modulo 5, s_j = 3 modulo 8 and s_j = 4 modulo 5. Every factor of s_j is 1 modulo 2r_j, hence s_j = 1 modulo 2r_j and in particular modulo 3. These three congruences yield s_j = 19 modulo 120. For 1 <= i < j, removing the square factors in either slot of the coprime Jacobi symbols gives (s_j/s_i) = (B_j/B_i) = -1 and (s_i/s_j) = (B_i/B_j) = 1. Removing only the later square factor also gives (s_j/B_i) = -1.

Unconditional weighted Frobenius on the full earlier support

Fix j >= 2. Form A_j = product(1 <= i < j, rad(B_i)), where rad uses every distinct prime factor, and put S_j = {p prime : p divides A_j} = union(1 <= i < j,T_i), t_j = |S_j| and E_j = E(S_j). This support includes earlier primes whose initial depths are even; it is not the union of the odd-depth kernels alone. The generic arithmetic application above gives the same actual totally real Galois field E_j inside C, degree 2^t_j and faithful surjective independent signs. Every actual q in T_j is odd and outside S_j, by disjoint block supports. Its arithmetic Frobenius F(q) is therefore unramified, independent of the upper prime, and acts on sqrt(p) by (p/q) for every p in S_j.

The primewise condition D is unconditional for these actual objects: for every p in S_j, product(q in T_j,(p/q)^h_q) = 1. To see the parameter correspondence, choose an earlier block B_i containing p. The existing cubic block congruence gives B_j = 3 modulo p, so (B_j/p) = (3/p). Since p = 1 modulo 3, quadratic reciprocity gives (3/p) = (-1)^((p-1)/2). Expanding the actual later factorization and reversing each symbol introduces the sign (-1)^(((p-1)/2)sum(q in T_j,h_q(q-1)/2)). The inner sum is odd because B_j = 3 modulo 4, so this reciprocity sign cancels (3/p). This proves D for every earlier p, including even-depth ones, with no squarefree, depth-one or extra D hypothesis.

Apply the existing weighted Frobenius consumer to these identical S_j, T_j, F and h. Its rank-depth exponent agrees with the original signed-index h_q by the exact block valuation equality. The sign homomorphism takes product(q in T_j,F(q)^h_q) to product(q in T_j,(p/q)^h_q) = 1 in each p-coordinate. Faithfulness gives the unconditional identity product(q in T_j,F(q)^h_q) = 1 in Gal(E_j/Q). This is the original GPC9 application; the field construction and arithmetic Frobenius proof are the existing ones.

Exactly one odd depth: literal splitting and directed tests

Assume Q belongs to the actual later support T_j, h_Q is odd and every other q in T_j has even h_q. The Galois group has exponent two, so all other factors of the weighted identity are one and its remaining factor is F(Q). Thus F(Q) = 1. The complete-splitting equivalence above applies to Q in this same E_j. It yields an exhaustive finite set of 2^t_j distinct prime ideals of O(E_j), with membership exactly prime ideals lying over Q, every residue quotient of cardinality Q, and all three displayed ideal-extension and principal-ideal products. The conclusion retains the exactly-one-odd-depth hypothesis.

On every earlier coordinate this also gives (p/Q) = 1 for every p in S_j. Since s_j = Q under the hypothesis, the reduced directed law gives (Q/B_i) = -1 for every 1 <= i < j. The kernel congruences give Q = 19 modulo 40 and Q = 1 modulo 2r_j. In particular, if j >= 3, the exact first blocks B_1 = 19 and B_2 = 5779 give (Q/19) = (Q/5779) = -1. These are tests on the same actual Q; they do not select a comparison prime from another set.

All-WSS multiplicity five: the full two-prime specialization

For every j >= 1, suppose every actual q in T_j is WSS and the actual total multiplicity sum(q in T_j,h_q) is five. Then there are distinct actual primes P and Q with T_j = {P,Q}, h_P = 2, h_Q = 3 and B_j = P^2*Q^3. Indeed each depth is at least two, so there are at most two factors. A single factor would make B_j a fifth power, excluded by GoldenCubicBlockNonFifthPower.golden_cubic_block_not_fifth_power. There are therefore two factors, and their depths must be two and three. This is the multiplicity-five case of the DCE4 pattern; it does not assume the factorization as an extra premise.

The same Q satisfies Q = 19 modulo 40 and Q = 1 modulo 2r_j. Both P and Q split in the golden quadratic field and have exact Fibonacci rank and Pisano period 2r_j. Write P = 1 + 2r_ju and Q = 1 + 2r_jv. Expanding P^2Q^3 gives (B_j-1)/r_j = 4u + 6v + r_jc for an integer c. The existing normalized ternary block unit gives (B_j-1)/r_j = (-1)^j modulo 3, so u = (-1)^j modulo 3 and 3 does not divide u. Hence P = 1 + 2(-1)^j*r_j modulo 6r_j and v_3(P-1) = j+1. Finally, B_j = 3 modulo 16: if Q = 19 modulo 80 then Q^3 = 11 modulo 16 and P^2 = 9 modulo 16; if Q = 59 modulo 80 then Q^3 = 3 modulo 16 and P^2 = 1 modulo 16. These are the full DCE5 congruence and valuation conditions.

For j >= 2 this actual Q is the unique odd-depth prime in T_j. It therefore has F(Q) = 1, the literal complete splitting in E_j, (p/Q) = 1 for every p dividing A_j and (Q/B_i) = -1 for every earlier block. For j >= 3 it also satisfies both tests at 19 and 5779. All hypotheses concern the actual initial Fibonacci depths and the actual factor support.

Scope and applicability limits

These consequences complete the original GPC5 and GPC6 application of the existing block, multiquadratic, residue and ideal interfaces. They assert neither existence nor impossibility of an all-WSS block or of the two-prime pattern, and do not decide whether an odd depth is one or at least three. The later GPC7 density theorem, its comparison primes and the remaining parent problem are separate work. No full parent-problem completion or new general field-arithmetic result is claimed. The four displayed formulas remain author-written descriptions of their linked Lean declarations; the linked library note records their classical source.

References

• Truth anchor: D5/S3/Factorization/Galois/QuadraticPrimeRadicalKernel.primeRadicalField
• Truth anchor: D5/S3/Factorization/Galois/QuadraticPrimeRadicalKernel.prime_mul_subset_not_square
• Truth anchor: D5/S3/Factorization/Galois/QuadraticPrimeRadicalKernel.prime_radical_degree
• Truth anchor: D5/S3/Factorization/Galois/QuadraticPrimeRadicalKernel.prime_radical_square_kernel
• Dependency: D5/S3/Factorization/Galois/QuadraticCompositeRank