Stopping-Cylinder Trial Energy
Abstract
Every function constant on an actual biased stopping partition has a finite unit-edge extension and a strict free-root Rayleigh bound.
Theorem 1.1 (The Original Single-Edge Trial Extension).
Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Geometry/BiasedBoundaryTrialEnergy.actual_stopping_trial_energy (✓ std3). ∎
Source. Repository-derived.
Commentary.
Fix any real threshold t strictly between zero and one. A(t) is the first actual biased mass crossing, with equality included as a stopping event. Vt(t) is the span of its cylinder indicators in the original G=L2(M). The coefficients x(p)=atomMean(p)(F) are the actual normalized cylinder integrals of F.
The orthogonal cylinder projection fixes each F in Vt(t), so F is the sum of x(p) times its actual cylinder indicators. Put the coefficient x(p) on the single original edge p for every p in A(t), with every other edge coefficient zero and root value zero. Applying J to this finite increment sum gives F. The squared increment norm is the sum of x(p) squared.
The actual partition norm identity and its constant conditional pullbacks give the boundary squared norm as the sum of mass(p) times x(p) squared. Each actual stopping mass is strictly greater than bt. If F is nonzero, at least one coefficient is nonzero, so the weighted sum is strictly greater than bt times the squared increment norm.
This extension places F in the original free-root domain D. The attained original minimum energy is at most the squared norm of this extension, hence strictly less than the boundary squared norm divided by b*t for every nonzero F. Equality of the chosen extension energy with the minimum is not asserted. The statement includes zero F, with the strict conclusions restricted exactly to nonzero F.
Here J, M, D and energy are the original biased trace, measure, free-root domain and infimum over all original extensions. The same inequality therefore applies to the centered trial subspace. The polar range identifications, spectral cutoff dimensions and resulting global eigenvalue counts require their further operator and variational arguments.