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==(4/5)theta^2, epsilon^2=||(A-rho)v||^2=(4/25)theta^4. 4. TEMPLE ENCLOSURE AND ITS UNIFORM DOMAIN For 0=7/160>0, rho(beta-rho)-epsilon^2=theta^2(1/8-(8/5)theta^2)>0. Rayleigh gives lambda1<=rho= 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.