Finite Window and Global Boundary

Abstract

Finite-window sampling floors are positive, while gap approximants force the global floor to vanish.

Theorem 1.1 (Finite windows are interior and the global limit is boundary).

$$\forall H\in Type,K\in Type,sampling\in \mathrm{ContinuousLinearMap}\left(\mathrm{Real}\left(\right),H,K\right),windowAdmissible\in \mathrm{Real}\left(\right)\to \left(H\to Prop\right),probe\in \mathrm{Nat}\left(\right)\to H,probeWindow\in \mathrm{Nat}\left(\right)\to \mathrm{Real}\left(\right),\left(\mathrm{NormedAddCommGroup}\left(H\right)\wedge \left(\mathrm{NormedSpace}\left(\mathrm{Real}\left(\right),H\right)\wedge \left(\mathrm{NormedAddCommGroup}\left(K\right)\wedge \left(\mathrm{NormedSpace}\left(\mathrm{Real}\left(\right),K\right)\wedge \left(\left(\forall L1\in \mathrm{Real}\left(\right),L2\in \mathrm{Real}\left(\right),L1\le L2\Rightarrow \left(\forall f\in H,\mathrm{applyTwo}\left(windowAdmissible,L1,f\right)\Rightarrow \mathrm{applyTwo}\left(windowAdmissible,L2,f\right)\right)\right)\wedge \left(\left(\forall L\in \mathrm{Real}\left(\right),L>0\Rightarrow \left(\exists f\in H,\mathrm{applyTwo}\left(windowAdmissible,L,f\right)\wedge \Vert f\Vert =1\right)\right)\wedge \left(\left(\forall L\in \mathrm{Real}\left(\right),L>0\Rightarrow \left(\exists c\in \mathrm{Real}\left(\right),c>0\wedge \left(\forall f\in H,\mathrm{applyTwo}\left(windowAdmissible,L,f\right)\Rightarrow \mathrm{mul}\left(c,{\Vert f\Vert }^2\right)\le {\Vert \mathrm{apply}\left(sampling,f\right)\Vert }^2\right)\right)\right)\wedge \left(\left(\forall n\in \mathrm{Nat}\left(\right),\Vert \mathrm{apply}\left(probe,n\right)\Vert =1\right)\wedge \left(\left(\forall n\in \mathrm{Nat}\left(\right),\mathrm{applyTwo}\left(windowAdmissible,\mathrm{apply}\left(probeWindow,n\right),\mathrm{apply}\left(probe,n\right)\right)\right)\wedge \mathrm{Tendsto}\left((n:\mathrm{Nat}\left(\right)\mapsto {\Vert \mathrm{apply}\left(sampling,\mathrm{apply}\left(probe,n\right)\right)\Vert }^2),atTop,\mathrm{nhds}\left(0\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \mathrm{let}floor=L:\mathrm{Real}\left(\right)\mapsto \mathrm{sInf}\left(\left\{\exists f\in H,\mathrm{applyTwo}\left(windowAdmissible,L,f\right)\wedge \left(\Vert f\Vert =1\wedge r={\Vert \mathrm{apply}\left(sampling,f\right)\Vert }^2\right)\mid r\in \mathrm{Real}\left(\right)\right\}\right),\left(\forall L\in \mathrm{Real}\left(\right),L>0\Rightarrow \mathrm{apply}\left(floor,L\right)>0\right)\wedge \mathrm{Tendsto}\left(floor,atTop,\mathrm{nhds}\left(0\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaAnalytic/FiniteWindowGlobalBoundary.finite_window_positive_global_boundary (✓ std3). ∎

Source. Repository-derived.

Commentary.

Conditional completeness turns each positive frame witness into a strictly positive unit-sphere infimum. Nested admissibility carries each vanishing-energy gap probe into all larger windows, which gives the upper half of the order-topology limit.

References

• Truth anchor: D5/S3/Weil/ZetaAnalytic/FiniteWindowGlobalBoundary.finite_window_positive_global_boundary
• Dependency: D5/S3/Weil/ZetaAnalytic/WhiteFloorSamplingDuality