Finite Toroidal Frame Reconstruction

Abstract

A compact pointwise-nonvanishing twist cover yields finite weighted frames that reconstruct the completed-zeta amplitude.

Theorem 1.1 (Finite weighted period frames reconstruct xi).

$$\forall Index\in \mathrm{Type}\left(\right),K\in \mathrm{Set}\left(\mathrm{Complex}\left(\right)\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),\left(\left(\forall i\in Index,\mathrm{Continuous}\left(T\left(i\right)\right)\right)\wedge \left(\left(\forall i\in Index,s\in \mathrm{Complex}\left(\right),P\left(i\right)\left(s\right)=xiReading\left(s\right)\times T\left(i\right)\left(s\right)\right)\wedge \left(\mathrm{IsCompact}\left(K\right)\wedge \left(\forall s\in \mathrm{Complex}\left(\right),\mathrm{mem}\left(s,K\right)\Rightarrow \left(\exists i\in Index,T\left(i\right)\left(s\right)\ne 0\right)\right)\right)\right)\right)\Rightarrow \left(\exists I\in \mathrm{Finset}\left(Index\right),\left(\forall s\in \mathrm{Complex}\left(\right),\mathrm{mem}\left(s,K\right)\Rightarrow \left(\exists i\in Index,\mathrm{mem}\left(i,I\right)\wedge T\left(i\right)\left(s\right)\ne 0\right)\right)\wedge \left(\forall w\in Index\to \mathrm{Real}\left(\right),\left(\forall i\in Index,\mathrm{mem}\left(i,I\right)\Rightarrow 0<w\left(i\right)\right)\Rightarrow \left(\forall s\in \mathrm{Complex}\left(\right),\mathrm{mem}\left(s,K\right)\Rightarrow \left(\mathrm{weightedFrame}\left(I,w,T,s\right)\ne 0\wedge xiReading\left(s\right)=\frac{\mathrm{inner}\left(\mathrm{Complex}\left(\right),\mathrm{weightedFrame}\left(I,w,T,s\right),\mathrm{weightedFrame}\left(I,w,P,s\right)\right)}{{\Vert \mathrm{weightedFrame}\left(I,w,T,s\right)\Vert }^2}\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Adelic/FiniteToroidalFrameReconstruction.finite_toroidal_frame_reconstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

Continuity makes each twist-nonvanishing locus open. Compactness then extracts a finite subcover from the pointwise nonvanishing family.

Positive square-root weights construct a nonzero complex Euclidean carrier frame at every point of the window. The period factorization constructs the observed frame as its canonical xi multiple.

The displayed inner product is ordered carrier first because Lean is conjugate linear in its first argument. It therefore represents the source convention that is linear in the period-frame argument.

References

• Truth anchor: D5/S3/Analytic/Adelic/FiniteToroidalFrameReconstruction.finite_toroidal_frame_reconstruction
• Dependency: D5/S3/Analytic/Adelic/ToroidalCechCompletion