ISOLATION OF THE LIGHT NEUTRAL MODE IN A DECLARED GHU BLOCK
28 October 2026. Written proof and exact replay. No mathematical novelty claimed.

QUESTION AND HYPOTHESES
Does the light vector mode remain positive and isolated as the imposed Wilson
angle changes, for fixed walls? Work on the unit square (x,y) in (0,1)^2,
with five complex components, the L2 mass metric and positive wall coefficients
muOmega=muPhi=1. No localized kinetic term (eta=0). The matrices K, b, C and
the vector n are supplied explicitly in certificate.json. Let O=b* b, G=C* C,
N0=span(e0,e3,e4), Ntheta=exp(theta K)N0, and use zero-based indices.
The form domain Vtheta consists of H1 fields with traces in N0 at x=0 and
Ntheta at x=1. The form is
 a[v]=integral |grad v|^2 + integral_(x=0) |bv|^2 + integral_(y=1) |Cv|^2.
All lengths and coefficients here are dimensionless declared inputs.
The associated nonnegative selfadjoint operator A has compact resolvent:
Vtheta is closed in H1; trace boundedness makes a+mass equivalent to H1;
the H1-to-L2 embedding on the square is compact. Order its eigenvalues with
multiplicity as lambda1<=lambda2<=... . This order is within the active block.
Three decoupled constant zero directions of the larger neutral block are
retained separately, not discarded by numerical tolerances. Their first
nonconstant Neumann eigenvalue is pi^2. No assertion about other GHU sectors.

1. A LOWER BOUND AT theta=0
Zero form energy implies a constant in N0 annihilated by b and C. The kernel
is exactly span(n), n=(2,0,0,-1,0). Let u be L2-orthogonal to this kernel and
c=integral u. Then c3=2c0, and
 |c|^2=|c1|^2+|c2|^2+|c4|^2+(4/5)|bc+c4/2|^2
      <=|c1|^2+|c2|^2+(7/5)|c4|^2+(8/5)|bc|^2.
Differences between the volume mean and the left/top edge means are integrals
of (1-x)u_x and -y u_y. Cauchy gives squared constant 1/3. Thus
 |c1|^2+|c2|^2 <= (1/3)||u_x||^2, since these components vanish on the left;
 |c4|^2 <= 2||u4|top||^2+(2/3)||u_y||^2;
 |bc|^2 <= 2||bu|left||^2+||u_x||^2, since ||b||^2=3/2.
It follows that
 |c|^2 <= (29/15)||u_x||^2+(14/15)||u_y||^2
          +(16/5)||bu|left||^2+(14/5)||u4|top||^2.
For an H1 function on the unit interval,
 ||f-mean f||^2=(1/2) integral integral |f(s)-f(t)|^2 <= (1/2)||f'||^2.
The fundamental theorem and Cauchy prove this, using |s-t|<=1. Apply it
successively to x and y averages, with Jensen on the derivative of an average:
 ||u-c||^2 <= (1/2)(||u_x||^2+||u_y||^2).
The mean and fluctuation are orthogonal in L2. Since 73/30 and 43/30 are
both below 16/5 and ||u4|top||<=||Cu|top||, we obtain
 ||u||^2 <= (16/5) a0[u].  Hence lambda2(0)>=5/16 by min-max.
These trace statements use edge averages, not corner point evaluation.

2. TRANSPORT TO NONZERO ANGLE
Utheta u=exp(theta x K)u maps V0 onto Vtheta unitarily in L2.
K*=-K, ||K||=1, [G,K]=0, and Utheta=I on the left wall. The transported
form on the fixed domain V0 is
 atilde_theta[u]=||u_x+theta K u||^2+||u_y||^2+the same wall terms.
Using ||p+q||^2 >= (1/2)||p||^2-||q||^2 yields
 atilde_theta >= (1/2)a0-theta^2 mass.
Min-max implies lambda2(theta)>=beta(theta)=5/32-theta^2.

3. AN OPERATOR-DOMAIN TRIAL, INCLUDING NATURAL BOUNDARIES
v=exp(theta x K)n/sqrt(5)=(2cos(theta x),0,2sin(theta x),-1,0)/sqrt(5).
Its L2 norm is one. Essential traces are in N0/Ntheta. It also lies in Dom(A):
on the left, bv=0 and Pi0(-v_x+Ov)=0; on the right PiTheta v_x=0;
on top v_y+Gv=0; on the bottom v_y=0. Here Pi denotes orthogonal projection.
The exact replay checks these identities, including the rotation and wall
commutation. The field is smooth, so Green's identity with every H1 test in
Vtheta proves Av=-Delta v. No H2 regularity of arbitrary eigenfunctions is
assumed. One must NOT apply this step to arbitrary conforming FEM trials.
Direct integration, or the constant pointwise scalar products, gives
 rho=<v,Av>=(4/5)theta^2, epsilon^2=||(A-rho)v||^2=(4/25)theta^4.

4. TEMPLE ENCLOSURE AND ITS UNIFORM DOMAIN
For 0<theta<=1/4,
 beta-rho=5/32-(9/5)theta^2 >=7/160>0,
 rho(beta-rho)-epsilon^2=theta^2(1/8-(8/5)theta^2)>0.
Rayleigh gives lambda1<=rho<beta<=lambda2, so the first mode is simple.
Temple's existing inequality gives
 0<rho-epsilon^2/(beta-rho) <= lambda1 <= rho,
 lambda2-lambda1 >= beta-rho.
To see the bound directly, each spectral value satisfies
(lambda_j-lambda1)(lambda_j-beta)>=0. Integrating against the spectral
weights of v yields epsilon^2+(rho-lambda1)(rho-beta)>=0. Rearrangement
gives the inequality. Only v in Dom(A) is required: the second spectral
moment is ||Av||^2, not a claim that v is in Dom(A^2).
The verifier checks the matrix identities and exact rational endpoints;
this written argument connects those finite checks to the continuous operator.
At theta=1/5, the sharper beta=93/800 gives
 lambda1 in [244/8425,4/125], gap >=337/4000.
This improves the valid but looser choice beta=11/100 and [28/975,4/125].
The UI exposes only the three exact queries 1/10,1/5,1/4. The external engine
accepts rational queries in the proved interval and rejects theta=0 or values
outside it. There is no numerical extrapolation or mesh-error estimate.

REFERENCES AND REUSE
Kuroda, Estimates of Kato-Temple Type for n-dimensional Spectral Measures,
Publ. RIMS 43 (2007), 505-520, section1.1 Theorem A (p506), section2.1.
https://ems.press/content/serial-article-files/40994
Vejchodsky and Sebestova, New guaranteed lower bounds on eigenvalues by
conforming finite elements, arXiv:1705.10180v1, section2, especially2.2-2.5.
https://arxiv.org/pdf/1705.10180v1
These are existing methods. Their weak-residual variants require their own
residual and separation hypotheses; a small finite-matrix residual is not
a continuous certificate. The elementary specialization above is an
application to this stated block, not a claim of new mathematics.

USE AND LIMITS
Compare the admitted angles to test positivity and isolation of this mode.
The results are lambdaZ=mZ^2 L5^2, not masses in GeV. Scalar zero modes,
other blocks, arbitrary wall coefficients and boundary kinetic terms are
outside this certificate. The finite neutral quotient elsewhere in the lab
is a different calculation and does not supply these spectral inequalities.
No certified value of S_Z=theta lambdaZ'/(2lambdaZ) or RZW=S_Z/S_W follows.
Differentiating interval endpoints is not a bound on the derivative.
Vacuum selection, currents and physical Higgs direction remain necessary
before interpreting a Wilson response as an experimental observable.
Replay: python verify.py certificate.json --self-test (requires SymPy).
No Lean formalization, experimental exclusion or global GHU certification.
