Golden Positivity Induction

Abstract

A two-step positive recurrence propagates through a chosen cofinal support schedule.

Theorem 1.1 (Recurrent-layer positivity reaches every compact Weil test).

$$\begin{array}{r}\forall L:\mathrm{Nat}\left(\right)\to \mathrm{Real}\left(\right),\\ Q:\mathrm{WeilTestFunction}\left(\right)\to \mathrm{Real}\left(\right),\\ \mathrm{let}Layer(n):=\left\{\forall x\in \mathrm{Real}\left(\right),f\left(x\right)\ne 0\Rightarrow \left|x\right|\le L\left(n\right)\mid f\in \mathrm{WeilTestFunction}\left(\right)\right\},\\ \forall A:\forall n\in \mathrm{Nat}\left(\right),\mathrm{Layer}\left(n+2\right)\to \mathrm{Layer}\left(n+1\right),\\ B:\forall n\in \mathrm{Nat}\left(\right),\mathrm{Layer}\left(n+2\right)\to \mathrm{Layer}\left(n\right),R:\forall n\in \mathrm{Nat}\left(\right),\mathrm{Layer}\left(n+2\right)\to \mathrm{Real}\left(\right),\\ \left(\forall n\in \mathrm{Nat}\left(\right),0<L\left(n\right)\right)\wedge \left(\left(\forall n\in \mathrm{Nat}\left(\right),L\left(n+2\right)=L\left(n+1\right)+L\left(n\right)\right)\wedge \left(\left(\forall f\in \mathrm{Layer}\left(0\right),0\le Q\left(\mathrm{val}\left(f\right)\right)\right)\wedge \left(\left(\forall f\in \mathrm{Layer}\left(1\right),0\le Q\left(\mathrm{val}\left(f\right)\right)\right)\wedge \left(\left(\forall n\in \mathrm{Nat}\left(\right),f\in \mathrm{Layer}\left(n+2\right),Q\left(\mathrm{val}\left(f\right)\right)=Q\left(\mathrm{val}\left(A\left(n,f\right)\right)\right)+Q\left(\mathrm{val}\left(B\left(n,f\right)\right)\right)+R\left(n,f\right)\right)\wedge \left(\forall n\in \mathrm{Nat}\left(\right),f\in \mathrm{Layer}\left(n+2\right),0\le R\left(n,f\right)\right)\right)\right)\right)\right)\Rightarrow \\ \left(\forall n\in \mathrm{Nat}\left(\right),f\in \mathrm{Layer}\left(n\right),0\le Q\left(\mathrm{val}\left(f\right)\right)\right)\wedge \left(\forall f\in \mathrm{WeilTestFunction}\left(\right),0\le Q\left(f\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/GoldenPositivityInduction.golden_positivity_induction (✓ std3). ∎

Source. Repository-derived.

Commentary.

The carrier is the canonical compactly supported Weil-test space. The chosen positive support schedule satisfies L(n+2)=L(n+1)+L(n), the source relation (1219.1). Layer n consists of tests supported within radius L(n). Two-step induction proves positivity on every layer, and cofinality derived from positivity and the recurrence places every Weil test in one of those layers.

References

• Truth anchor: D5/S3/Weil/TestFunctions/GoldenPositivityInduction.golden_positivity_induction