Internal audit: closed normal sectors

8 September 2026. Same-agent audit, not independent review.

Mathematical gates checked

Integer image versus saturation. The surjectivity proof uses -2X in E+T for every integral closed X. Its image lambda is actually in Lambda intersect 2L. No integral peripheral row or half-edge lift is assumed.
All homology sectors. The native unit includes every closed mod-two normal-homology sector. Replacing its value by only I^0(0) would be an unjustified restriction. Formula (6) keeps the finite sum over all allowed sectors.
Native phase. The evenness of p follows from integral Euler characteristic of the closed class Y. Both the exponent and Gaussian phase in (5) were computed, not inferred from equal valuations.
Geometric hypotheses. Corollary 10.19 was checked in the printed GHHR paper, pp. 326–327. Its irreducibility hypothesis is applied to monoid summands; their coordinatewise bound by a reduced X excludes tetrahedral summands. Its two manifold exceptions are retained.
Convergence on odd root inputs. The published scalar convergence theorem is not substituted for all-input descent. The prior affine-input signed theorem supplies that step after H=N_Z identifies its cone. The primitive native edge relation is also tested on odd inputs in the controls.
Exceptional examples are actual data. The incidence matrices come from GHHR Examples 11.1 and 11.3. The original characters of every row are verified, including the zero row of the product-torus example. Their degree-one edges force angle 2 and preclude a nonnegative certificate; these are genuinely outside the preceding angle-positive examples.
Euler evaluation pitfall. For the solid-torus positive difference m, substituting into the uncancelled generating quotient gives 0/0, and the raw double family has nonpositive k-slope. The proof cancels the common factors first and uses a summable expansion with seed parameter -m. Direct native averages agree with the resulting rational formula.
Nonzero module versus nonzero trace. The conclusion concerns Q^6/im(tau) and compatible quotients. It does not prove a nonzero filled map. A nonzero functional on the all-plus projection is pulled back, never used to lift a vanishing identity backwards.
No triangulation invariance overclaim. Only the two specific exceptional data are proved. Scalar invariance cannot transport their nonperipheral detecting inputs, and no connectedness of the 1-efficient move graph is assumed.

Exact verification

verify-normal-sector.py uses Gaussian integer coefficients in x=A^(1/2), q=x^8. It reduces the tetrahedron seed by triality to a nonnegative quadratic expansion. Each averaged input has an explicit piecewise quadratic degree; beyond all its minimum breakpoints, the checked quadratic tail is increasing and above the requested cutoff. This certifies the finite coefficient windows, not a universal topology claim.

Checks cover original row characters, primitive edge relations, correct-sided tetrahedron multiples, the finite phase bridge and the solid-torus closed formula. The two detecting series have constant coefficients -1 and 1. A second implementation by the same agent is not an independent route to the general theorem.

Remaining vulnerability and next obligation

The general proof remains dependent on the published normal-surface theorems and the prior Lab native comparison, entire-image grading and all-input convergence proofs. An independent checker should reconstruct this dependency chain, especially the root/quad convention match. No full Lean, Rocq or Isabelle proof exists. The present synthesis is not assigned higher maturity because it cites a published theorem.

The remaining general nonvanishing question lies in arbitrary 1-efficient triangulations of the solid torus and T^2 x I. The fixed data do not settle that universal quantifier.