Finite Toroidal Quotient Connection

Abstract

A finite positive toroidal Gram frame recovers its common two-point factor by a local kernel quotient.

Theorem 1.1 (Finite toroidal Gram quotients recover the common factor).

$$\forall Index\in \mathrm{Type}\left(\right),K\in \mathrm{Set}\left(\mathrm{Complex}\left(\right)\right),I\in \mathrm{Finset}\left(Index\right),w\in Index\to \mathrm{Real}\left(\right),P\in Index\to \left(\mathrm{Complex}\left(\right)\to \mathrm{Complex}\left(\right)\right),T\in Index\to \left(\mathrm{Complex}\left(\right)\to \mathrm{Complex}\left(\right)\right),xi\in \mathrm{Complex}\left(\right)\to \mathrm{Complex}\left(\right),\left(\left(\forall j\in Index,\mathrm{mem}\left(j,I\right)\Rightarrow 0<w\left(j\right)\right)\wedge \left(\left(\forall j\in Index,u\in \mathrm{Complex}\left(\right),\mathrm{mem}\left(j,I\right)\Rightarrow P\left(j\right)\left(u\right)=xi\left(u\right)\times T\left(j\right)\left(u\right)\right)\wedge \left(\forall u\in \mathrm{Complex}\left(\right),\mathrm{mem}\left(u,K\right)\Rightarrow \left(\exists j\in Index,\mathrm{mem}\left(j,I\right)\wedge T\left(j\right)\left(u\right)\ne 0\right)\right)\right)\right)\Rightarrow \left(\left(\forall u\in \mathrm{Complex}\left(\right),\mathrm{mem}\left(u,K\right)\Rightarrow \mathrm{weightedGramKernel}\left(I,w,T,u,u\right)\ne 0\right)\wedge \left(\forall s\in \mathrm{Complex}\left(\right),t\in \mathrm{Complex}\left(\right),\mathrm{weightedGramKernel}\left(I,w,T,s,t\right)\ne 0\Rightarrow \mathrm{localQuotientKernel}\left(I,w,P,T,s,t\right)=xi\left(s\right)\times \mathrm{conj}\left(xi\left(t\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/Tomography/FiniteToroidalQuotientConnection.finite_toroidal_frame_quotient_connection (✓ std3). ∎

Source. Repository-derived.

Commentary.

The toric periods, twists, common factor, finite selection, and spectral window are explicit parameters. This isolates the algebraic content from external analytic constructions.

Strictly positive real weights and a nonzero selected twist at each window point make the carrier Gram kernel nonzero on the diagonal.

Pointwise period factorization pulls the common factor through the finite sum. At every pair where the carrier kernel is nonzero, division then gives the displayed quotient connection.

References

• Truth anchor: D5/S3/Observer/Tomography/FiniteToroidalQuotientConnection.finite_toroidal_frame_quotient_connection