Local Euler Transition Non-Reconstruction

Abstract

Local Euler determinants do not determine cross-prime frame transitions.

Theorem 1.1 (Local determinants forget frame transitions).

$$\forall chi\in Nat.Primes\to \mathrm{Complex}\left(\right),\mathrm{let}{p}_2:Nat.Primes=\mathrm{prime}\left(2\right),\mathrm{let}{p}_3:Nat.Primes=\mathrm{prime}\left(3\right),\mathrm{let}localOperator:Nat.Primes\to \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathrm{Complex}\left(\right)\right)=(p:Nat.Primes\mapsto \mathrm{diagonal}\left((branch:\mathrm{Fin}\left(2\right)\mapsto \mathrm{ite}\left(branch=0,1,chi\left(p\right)\right))\right)),\exists firstFrame\in Nat.Primes\to \mathrm{GL}\left(\mathrm{Fin}\left(2\right),\mathrm{Complex}\left(\right)\right),secondFrame\in Nat.Primes\to \mathrm{GL}\left(\mathrm{Fin}\left(2\right),\mathrm{Complex}\left(\right)\right),\left(\forall p\in Nat.Primes,x\in \mathrm{Complex}\left(\right),\det \left(\mathrm{identityMatrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Complex}\left(\right)\right)-\mathrm{smul}\left(x,firstFrame\left(p\right)\cdot localOperator\left(p\right)\cdot \mathrm{inverse}\left(firstFrame\left(p\right)\right)\right)\right)=\left(1-x\right)\cdot \left(1-x\cdot chi\left(p\right)\right)\right)\wedge \left(\left(\forall p\in Nat.Primes,x\in \mathrm{Complex}\left(\right),\det \left(\mathrm{identityMatrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Complex}\left(\right)\right)-\mathrm{smul}\left(x,secondFrame\left(p\right)\cdot localOperator\left(p\right)\cdot \mathrm{inverse}\left(secondFrame\left(p\right)\right)\right)\right)=\left(1-x\right)\cdot \left(1-x\cdot chi\left(p\right)\right)\right)\wedge \mathrm{inverse}\left(firstFrame\left(p_3\right)\right)\cdot firstFrame\left(p_2\right)\ne \mathrm{inverse}\left(secondFrame\left(p_3\right)\right)\cdot secondFrame\left(p_2\right)\right)$$

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

Source. Repository-derived.

Commentary.

The local operator at every prime is the diagonal two-branch operator with eigenvalues one and chi at that prime.

Two general-linear frame families produce the same local Euler determinant for every prime and scalar parameter, while their inverse-frame transition products from the smallest prime two to the next prime three are unequal.

References

• Truth anchor: D5/S3/Observer/AgencyHolonomy/LocalEulerTransitionNonreconstruction.local_euler_determinants_do_not_determine_transition