Mod-Five Character Word Scalar Quotient

Abstract

The scalar product identifies two distinct directed mod-five character words.

Theorem 1.1 (The scalar quotient forgets character-word direction).

$$\begin{array}{r}\mathrm{let}characterWord:\mathrm{ZMod}\left(5\right)\to \mathbb{Z}\times \mathbb{Z}=(n:\mathrm{ZMod}\left(5\right)\mapsto (\mathrm{legendreSym}\left(5,\mathrm{val}\left(n\right)\right),\mathrm{legendreSym}\left(5,\mathrm{val}\left(n+2\right)\right))),\\ \mathrm{let}scalarProduct:\mathbb{Z}\times \mathbb{Z}\to \mathbb{Z}=(w:\mathbb{Z}\times \mathbb{Z}\mapsto \mathrm{fst}\left(w\right)\times \mathrm{snd}\left(w\right)),\\ \mathrm{let}validWords:\mathrm{Finset}\left(\mathbb{Z}\times \mathbb{Z}\right)=\mathrm{image}\left(characterWord,\mathrm{univ}\left(\mathrm{ZMod}\left(5\right)\right)\right),\\ (\mathrm{characterWord}\left(1\right)=(1,-1)\wedge \left(\mathrm{characterWord}\left(2\right)=(-1,1)\wedge \left(\mathrm{characterWord}\left(1\right)\ne \mathrm{characterWord}\left(2\right)\wedge \left(\mathrm{scalarProduct}\left(\mathrm{characterWord}\left(1\right)\right)=-1\wedge \left(\mathrm{scalarProduct}\left(\mathrm{characterWord}\left(2\right)\right)=-1\wedge \left(\mathrm{scalarProduct}\left(\mathrm{characterWord}\left(1\right)\right)=\mathrm{scalarProduct}\left(\mathrm{characterWord}\left(2\right)\right)\wedge \left(validWords=\left\{(0,-1),(1,-1),(-1,1),(-1,0),(1,1)\right\}\wedge \left(\neg \mathrm{InjOn}\left(scalarProduct,\mathrm{coe}\left(validWords\right)\right)\right)\right)\right)\right)\right)\right)\right))\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenCoding/ModFiveCharacterWordQuotient.mod_five_character_word_scalar_quotient (✓ std3). ∎

Source. Repository-derived.

Commentary.

For offsets zero and two, the quadratic character modulo five sends residues one and two to the directed words (1,-1) and (-1,1).

The complete residue image is the displayed five-word finite set. The two mixed-sign words are distinct but both have scalar product -1, so pair multiplication is not injective on this character-word image.

References

• Truth anchor: D5/S3/Observer/GoldenCoding/ModFiveCharacterWordQuotient.mod_five_character_word_scalar_quotient