What the checker proves

For a square real system A x = b, the certificate stores the coefficients, proposed answer x and approximate inverse R as canonical binary64 hexadecimal values. Their exact represented values define the mathematical problem. The checker uses integer arithmetic to recompute every claim.

The proof

Let C = I − R A and q be its maximum absolute row sum. If q < 1, the Neumann series makes I − C = R A invertible. Both square matrices R and A are therefore invertible. For the unique exact solution x*, (I − C)(x* − x) = R(b − Ax). Its maximum component error is at most η / (1 − q), where η is the largest absolute component of R(b − Ax). Each component lies between the candidate minus this radius and the candidate plus it.

The checker derives q and η from the stored data. It accepts no asserted residual, condition estimate or error radius. When q ≥ 1 it refuses this proof, which does not imply the equations have no solution. A wide certified interval does not imply an accurate answer. The threshold claim is separate: the entire interval must be above the threshold, or entirely at or below it. Otherwise the decision is undecidable from this certificate.

The boundary

This certifies declared equations, not measured hardware, a physical model, calibration, intended exact decimal inputs, source authenticity, a GPU execution trace or a proof assistant. Python and JavaScript implementations use independently developed exact arithmetic. Source and input hashes identify bytes, not a trusted author.

The original ladder fixture has 64 unknown voltages, 1-ohm neighboring links, grounded ends and a 1 A injection at node 32. NumPy supplies a candidate and inverse. The independently derived exact Green-function solution checks all enclosures. This is an ideal mathematical circuit, not an electrical measurement.

Inputs are bounded to 2 MiB and dimensions 1–128. Finite canonical binary64 values are required. Browser work runs in a disposable Web Worker, with a 20-second deadline and Cancel; input changes revoke old claims. The standalone Python checker applies the same parser/arithmetic limits, but its command-line run has no browser worker deadline. Dense multiplication has cubic worst-case cost.

Established foundations

This is established numerical verification theory. See Rump, Validated Solution of Large Linear Systems, INTLAB and IntervalLinearAlgebra.jl. These environments provide broader methods. Certloom focuses on a small, source-bearing result artifact that a recipient can check without the producing solver.

Original source and reproducible evidence. Developed and reviewed with Codex assistance.