# Verification scope and trusted components

The active no-hit proof uses one grid: eight signed atoms, 140 angular cells and 400 time steps. Independence comes from a separate implementation of the checker, not agreement between producer grids.

## Independent continuous-domain checks

`scripts/check_barrier_independent.py` imports neither `experiments.ieee` nor the producer's derivative or aggregation functions. It uses mpmath interval arithmetic at 40 decimal digits. It consumes all endpoint and tube boxes in `certificates/*.npz`, verifies the exact radical initial conditions, positive atom weights and complete angular partition, and independently integrates the Haar polynomial on each angular cell.

For every full angular cell and time slab it verifies the Picard inclusion and second-order Taylor endpoint remainder, checks that a excludes zero, differentiates the scalar observables with an independent second-order implementation, aggregates all eight atoms, and verifies the full early and late windows. Intersections with nonnegative h and b use their analytically invariant signs. The step is the exact binary64 value of 0.001; 400 steps cover the exact rational interval [0, 2/5]. No success flag or reported lower bound from the producer is used. A smoke run cannot write a successful certificate. Running Python with -O is rejected.

The checked lower bounds imply H1'' > 16.485 near zero, H1 > 0.000648 on the far early window, H1 > 4.12036 on the late window, and g > 0.343 through T0. The report contains input and checker hashes. Twenty-eight tests include deliberate corruption of initial boxes, time tubes, endpoints, angular coverage and nonfinite entries.

`scripts/check_freeze_independent.py` separately verifies the explicit polynomial comparison, its slopes and endpoint positivity, the atom-weight inequality, a lower bound on common existence, and J8 > 25 with 512 rational panels and 50-digit interval arithmetic. The independent J8 enclosure is [25.02066538271988959…, 25.42710316984979688…]. The lower integrated-capacity threshold 8141/10000 > 4/5 is exact.

`scripts/check_exact_identities.py` evaluates actual compact-law moments symbolically and checks the base invariants, pairing polynomial, capacity convexity identity, general-dimensional Wick formula, Wronskian, coupling split, initialization germs and GS expansion. These are exact symbolic checks rather than simulation fits.

## What remains trusted

The analytical derivation linking particle flow, angular averaging, response kernel and scalar barrier is shared mathematical input, now written in the paper. It has been checked by derivation and symbolic identities, not formalized in a proof assistant. We trust Python, SymPy's exact simplification, mpmath's interval operations, NumPy's numeric file decoder, and the hardware. The producer uses NumPy binary64 and outward nextafter; its proposed boxes are independently checked. The checker does not certify arbitrary uses of that producer beyond the published evidence.

The claim is independent verification of the computational obligations used by this proof, not formal verification of the whole paper or a guarantee that software is infallible. The novelty comparison is scoped, not exhaustive peer review. Finite-epsilon infinite-time no-overshoot remains open. Arbitrary initialization, dimensions outside the stated results, finite-width and finite-sample generalization are outside scope.

## Ordinary numerical evidence

The perturbation suite uses RK4 without clipping and angular quadrature for both closing probe pairs. Five mixing values, halved time step and larger quadrature orders are recorded. A real 50-digit arithmetic comparison is included because longdouble has only 53 mantissa bits on this platform. It uses identical float64 quadrature nodes to isolate arithmetic effects; it is not a high-precision quadrature certificate. Freeze-distance estimates use two independently refined ordinary integrations. Distances below their roughly 3e-8 refinement difference are unresolved. None of these empirical results supplies an interval proof.