Mod-Five Local Euler Factor

Abstract

The mod-five local observer determinant splits into its even and odd channel factors.

Theorem 1.1 (The two canonical observer channels give the two local factors).

$$\forall p\in Nat.Primes,x\in \mathrm{Complex}\left(\right),s\in \mathrm{Complex}\left(\right),\mathrm{let}chi:\mathrm{Complex}\left(\right)=\mathrm{cast}\left(\mathrm{Complex}\left(\right),\mathrm{legendreSym}\left(5,p\right)\right),\mathrm{let}localObserverOperator:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathrm{Complex}\left(\right)\right)=\mathrm{goldenLocalBranchOperator}\left(p\right),\mathrm{let}primeScale:\mathrm{Complex}\left(\right)=\mathrm{cast}{\left(\mathrm{Complex}\left(\right),p\right)}^{-s},\mathrm{inverse}\left(\det \left(\mathrm{identityMatrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Complex}\left(\right)\right)-\mathrm{smul}\left(x,localObserverOperator\right)\right)\right)=\frac{1}{\left(1-x\right)\cdot \left(1-chi\cdot x\right)}\wedge \left(\mathrm{inverse}\left(\det \left(\mathrm{identityMatrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Complex}\left(\right)\right)-\mathrm{smul}\left(primeScale,localObserverOperator\right)\right)\right)=\mathrm{inverse}\left(1-primeScale\right)\cdot \mathrm{inverse}\left(1-chi\cdot primeScale\right)\wedge \left(\mathrm{IsCompl}\left(evenChannel,oddChannel\right)\wedge \left(\left(\forall value\in \mathrm{BranchSpace}\left(\right),\mathrm{mem}\left(value,evenChannel\right)\Rightarrow \mathrm{mulVec}\left(localObserverOperator,value\right)=value\right)\wedge \left(\forall value\in \mathrm{BranchSpace}\left(\right),\mathrm{mem}\left(value,oddChannel\right)\Rightarrow \mathrm{mulVec}\left(localObserverOperator,value\right)=\mathrm{smul}\left(chi,value\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/PrimeForms/GoldenEuler/ModFiveLocalEulerFactor.mod_five_local_observer_determinant (✓ std3). ∎

Source. Repository-derived.

Commentary.

The imported golden local branch operator is the canonical sum of the even projection and the quadratic-character-weighted odd projection. No second operator definition is introduced here.

Its generic inverse determinant is the product denominator. Substituting the prime scale gives the Riemann and quadratic Dirichlet local factors.

The imported even and odd channels are complementary. The same operator acts by one on every even-channel vector and by the mod-five character on every odd-channel vector, so their one-dimensional inverse determinants are the displayed factors.

References

• Truth anchor: D5/S3/PrimeForms/GoldenEuler/ModFiveLocalEulerFactor.mod_five_local_observer_determinant
• Dependency: D5/S3/Observer/GoldenCoding/GoldenBranchObserverDecomposition