Golden Cubic Prime Transfer
Abstract
The actual rational-prime Frobenius event matches the compositum Chebotarev event away from ramification.
Theorem 1.1 (Rational primes and the prime ideals of the integers of Q).
Lean statement: D5/S3/Factorization/Galois/GoldenCubicCompatibilityPrimeTransfer.rationalPrimeIdeal_data
Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/GoldenCubicCompatibilityPrimeTransfer.rationalPrimeIdeal_data (✓ std3). ∎
Source. Repository-derived.
Commentary.
The map p to the principal ideal generated by p is injective, maps to nonzero prime ideals, preserves absolute norm and reaches every nonzero prime ideal of the integers of Q. The original prime-transfer proof continues to use this factored correspondence.
Theorem 1.2 (Forward and reverse arithmetic Frobenius transfer).
Lean statement: D5/S3/Factorization/Galois/GoldenCubicCompatibilityPrimeTransfer.actual_prime_transfer_data
Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/GoldenCubicCompatibilityPrimeTransfer.actual_prime_transfer_data (✓ std3). ∎
Source. Repository-derived.
Commentary.
A rational prime in the specified unit residue class admits a prime of the cubic cyclotomic base and a prime of the actual radical field above it with the character-defined arithmetic Frobenius exactly when its prime ideal has the selected rational Frobenius class, away from ramification. The proof constructs lifts and transports arithmetic Frobenius in both directions through the rational, cubic-base, radical and compositum towers.
The rational-prime set and the Chebotarev prime-ideal set therefore agree after excluding ramified primes. The statement retains the same actual earlier support, roots, residue and automorphisms as the compositum.