Golden Character Quotient

Abstract

The quadratic character modulo five gives a binary quotient of unramified prime words.

Theorem 1.1 (Golden character quotient specification).

$$\left(\left(\left(\left(\left(\left(\forall w\in \mathrm{List}\left(UnramifiedPrime\right),\mathrm{coe}\left(\mathrm{holFiveQuotient}\left(\mathrm{ofList}\left(w\right)\right)\right)=\mathrm{holFive}\left(w\right)\right)\wedge \left(\forall u\in \mathrm{List}\left(UnramifiedPrime\right),\forall v\in \mathrm{List}\left(UnramifiedPrime\right),\mathrm{holFive}\left(\mathrm{append}\left(u,v\right)\right)=\mathrm{holFive}\left(u\right)\cdot \mathrm{holFive}\left(v\right)\right)\right)\wedge \left(\forall u\in \mathrm{List}\left(UnramifiedPrime\right),\forall v\in \mathrm{List}\left(UnramifiedPrime\right),\mathrm{Perm}\left(u,v\right)\Rightarrow \mathrm{holFive}\left(u\right)=\mathrm{holFive}\left(v\right)\right)\right)\wedge \left(\forall w\in \mathrm{List}\left(UnramifiedPrime\right),\mathrm{holFive}\left(w\right)={\left(-1\right)}^{\mathrm{inertCount}\left(w\right)}\right)\right)\wedge \left(\forall w\in \mathrm{List}\left(UnramifiedPrime\right),\mathrm{holFive}\left(w\right)=1\vee \mathrm{holFive}\left(w\right)=-1\right)\right)\wedge \left(\left(\left(\mathrm{goldenCharacter}\left(eleven\right)=1\wedge \mathrm{goldenCharacter}\left(nineteen\right)=1\right)\wedge \mathrm{goldenCharacter}\left(two\right)=-1\right)\wedge \mathrm{goldenCharacter}\left(three\right)=-1\right)\right)\wedge \left(\mathrm{holFive}\left(\mathrm{word}\left(two,three\right)\right)=1\wedge \mathrm{holFive}\left(\mathrm{word}\left(two,eleven\right)\right)=-1\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencyHolonomy/GoldenCharacterQuotient.golden_character_quotient_spec (✓ std3). ∎

Source. Repository-derived.

Commentary.

Restrict every letter to a rational prime different from five. The Legendre symbol modulo five then takes values in the two integer units, and its product defines a homomorphism from the free monoid of prime words to this binary group.

Concatenation becomes multiplication, permutations do not change the value, and the value is negative one raised to the number of inert letters. The words [2, 3] and [2, 11] witness both quotient values.

The source passage does not define the full holonomy, observer rapidity, or commutator holonomy. No formal claim about forgetting those data is made here.

References

• Truth anchor: D5/S3/Observer/AgencyHolonomy/GoldenCharacterQuotient.golden_character_quotient_spec
• Dependency: D5/S3/Arith/Lattices/RamifiedFiveBoundarySelection