Quartic Character Completion Modulo Sixty

Abstract

A quartic modulo-five character completes the mod-sixty splitting profile.

Definition 1.1 (The Gaussian quadratic character).

$$ch{i}_{-4}:(\mathbb{Z}/60\mathbb{Z}{)}^{\times }\to m{u}_2.$$

Formalization. D5/S3/PrimeForms/Splitting/QuarticCharacterCompletion.chiMinusFour (✓ std3).

Source. Repository-derived.

Commentary.

The Gaussian split-inert reading is composed with the standard binary root character to obtain a homomorphism into mu two.

Definition 1.2 (The Eisenstein quadratic character).

$$ch{i}_{-3}:(\mathbb{Z}/60\mathbb{Z}{)}^{\times }\to m{u}_2.$$

Formalization. D5/S3/PrimeForms/Splitting/QuarticCharacterCompletion.chiMinusThree (✓ std3).

Source. Repository-derived.

Commentary.

The Eisenstein split-inert reading is composed with the same standard binary root character.

Definition 1.3 (The quartic modulo-five character).

$$ps{i}_5:(\mathbb{Z}/60\mathbb{Z}{)}^{\times }\to m{u}_4.$$

Formalization. D5/S3/PrimeForms/Splitting/QuarticCharacterCompletion.psiFive (✓ std3).

Source. Repository-derived.

Commentary.

Reduction from units modulo sixty to units modulo five is followed by the discrete logarithm base two and the standard character into the fourth roots of unity.

The discrete logarithm table is total on the four unit residues. Its identity and multiplication laws are checked on that finite group, so the definition is representative-independent.

Definition 1.4 (The quadratic-quadratic-quartic completion).

$$Ps{i}_{60}=(ch{i}_{-4},ch{i}_{-3},ps{i}_5):(\mathbb{Z}/60\mathbb{Z}{)}^{\times }\to m{u}_2\times m{u}_2\times m{u}_4.$$

Formalization. D5/S3/PrimeForms/Splitting/QuarticCharacterCompletion.psiSixty (✓ std3).

Source. Repository-derived.

Commentary.

The completed map records the Gaussian and Eisenstein quadratic characters together with the quartic modulo-five character.

Theorem 1.5 (The modulo-five generator maps to i).

$$ps{i}_5(7)=i.$$

Proof. Machine-checked in Lean as D5/S3/PrimeForms/Splitting/QuarticCharacterCompletion.psi_five_maps_mod_five_generator_two_to_i (✓ std3). ∎

Source. Repository-derived.

Commentary.

The unit class seven reduces to the generator two modulo five. Its discrete logarithm is one, so the standard quartic character takes the value i.

Theorem 1.6 (The quartic completion separates every unit class).

$$\forall u,v:(\mathbb{Z}/60\mathbb{Z}{)}^{\times },Ps{i}_{60}(u)=Ps{i}_{60}(v)\Rightarrow u=v.$$

Proof. Machine-checked in Lean as D5/S3/PrimeForms/Splitting/QuarticCharacterCompletion.psi_sixty_injective (✓ std3). ∎

Source. Repository-derived.

Commentary.

Equality of completed values recovers the Gaussian and Eisenstein readings and the full modulo-five residue.

These data give equal three-ring profiles and equal orientation bits. The preceding orientation theorem then forces the two unit classes to be equal.

Theorem 1.7 (The quartic coordinate strictly improves the binary profile).

$$\begin{gathered} \exists u,v:(\mathbb{Z}/60\mathbb{Z}{)}^{\times },u\ne v\wedge \\ triRingImage(u)=triRingImage(v)\wedge \\ Ps{i}_{60}(u)\ne Ps{i}_{60}(v). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/PrimeForms/Splitting/QuarticCharacterCompletion.quadratic_profile_collision_but_quartic_completion_separates (✓ std3). ∎

Source. Repository-derived.

Commentary.

The distinct classes one and forty-nine have the same three-ring binary profile, while the completed character values differ. This is the concrete mu-two-cubed versus mu-two-squared times mu-four contrast.

References

• Truth anchor: D5/S3/PrimeForms/Splitting/QuarticCharacterCompletion.chiMinusFour
• Truth anchor: D5/S3/PrimeForms/Splitting/QuarticCharacterCompletion.chiMinusThree
• Truth anchor: D5/S3/PrimeForms/Splitting/QuarticCharacterCompletion.psiFive
• Truth anchor: D5/S3/PrimeForms/Splitting/QuarticCharacterCompletion.psiSixty
• Truth anchor: D5/S3/PrimeForms/Splitting/QuarticCharacterCompletion.psi_five_maps_mod_five_generator_two_to_i
• Truth anchor: D5/S3/PrimeForms/Splitting/QuarticCharacterCompletion.psi_sixty_injective
• Truth anchor: D5/S3/PrimeForms/Splitting/QuarticCharacterCompletion.quadratic_profile_collision_but_quartic_completion_separates
• Dependency: D5/S3/Factorization/Galois/GeneralPowerCharacterLayer
• Dependency: D5/S3/PrimeForms/Splitting/ModFiveOrientationBit
• Dependency: D5/S3/PrimeForms/Splitting/QuadraticCharacterProfileRedundancy