# SWC for certified computation and empirical reliability

Research extension and executable demonstration, 2026-09-05.

## Product contract

Every returned mathematical answer carries a checked witness. Complete coverage
is certified for a named finite input domain. Outside that domain, the rate of
returning verified answers is evaluated under a stated sampling protocol.

These are three separate guarantees, each with its own evidence and scope.
They make SWC useful without requiring a solution to an infinite existence
conjecture. They build on the exact and empirical modes already present in
SWC; no new probability axiom or novelty for classical confidence bounds is
claimed.

## 1. Correctness of returned answers

Let R(x,w) be a specified mathematical relation, and let V be an exact checker
whose acceptance implies R. An untrusted solver A may produce a candidate or
report that it has no result. The certified wrapper is

    T(x) = (w, receipt) if A produces w and V(x,w)=1;
           unresolved otherwise.

If the checker is sound, every answer emitted by T satisfies R. This follows
directly from the acceptance guard. There is no statistical confidence level
on the truth of a correctly verified mathematical witness. The claim does not
include termination or successful search on every input.

The current receipt checker supports:

* Lonely Runner: integer speeds and a rational time m/q, checked by exact
  integer distances against 1/(n+1).
* Erdos-Straus: integer n and positive denominators x,y,z, checked by
  4xyz=n(xy+xz+yz).

The receipt binds the relation, input, witness, and single-instance scope.
Floating-point replacements, altered hashes, unsupported relations, and
broader caller-supplied scopes are rejected. The SHA-256 fingerprint identifies
bytes; exact arithmetic checks establish the mathematical relation. The Python
checker remains part of the trusted implementation, and this is not a
proof-assistant formalization.

## 2. Complete coverage of a declared finite domain

For a domain D specified independently of the solver's successes, provide a
witness w_x for every x in D. The verifier reconstructs D from its manifest,
checks every witness, and rejects omissions, duplicates, extra rows, incorrect
domain membership, or a changed manifest. Passing establishes the ordinary
finite theorem

    for every x in D, there exists w such that R(x,w).

This is stronger than a large list of successful experiments because the
domain is explicit and its coverage is complete. The theorem's quantifier is
over D, not over an unspecified population.

### Completed finite certificate

The recorded domain is exactly the seven-element subsets V of {1,...,20}
such that gcd(V)=1 and every integer r=2,...,8 divides some speed. There are
12,673 such sets. The certificate contains one valid rational time per set.

Both the main checker and an independent implementation reconstructed the
domain and verified every witness. Therefore the displayed finite existence
statement is certified over all 12,673 inputs. This certifies witnesses, not a
new universal Lonely Runner theorem or a previously unknown small-runner result.

Domain SHA-256:

    f9311aecced06886398ef8d502c0cf7fc84d3b8d9418242131abf43660160268

## 3. How often the system returns a verified answer

Let P be a named input distribution and freeze the solver configuration before
evaluation. Let X_1,...,X_N be fresh IID draws from P. Set F_i=1 whenever the
system fails to return a verified receipt, including unresolved searches,
invalid candidates, errors, and timeouts. All draws remain in the denominator.
Let p=Pr_P(F=1) and f=sum_i F_i.

For fixed N, a one-sided exact binomial confidence bound supplies an upper
bound U on p. The confidence guarantee is a statement about the repeated
sampling procedure:

    Pr_p[p <= U(F_1,...,F_N)] >= 1-alpha.

It is not a posterior probability for a fixed unknown p, and it says nothing
about a different deployment distribution. The implementation evaluates
binomial tails using rational arithmetic and rounds numerical bounds upward
on a rational grid, so approximation cannot make the reported bound too strong.

For zero failures, the conventional exact endpoint is

    U = 1 - alpha^(1/N).

For a target failure rate epsilon, it is enough to check the equivalent exact
inequality

    (1-epsilon)^N <= alpha.

Under p>=epsilon, the probability of observing zero failures is at most that
quantity. Therefore reporting the target only after the prescribed zero-failure
test has false-certification probability at most alpha. A fixed epsilon and
alpha permit selecting N before seeing any outcomes.

For epsilon=1/1000 and alpha=1/100, the minimum zero-failure sample size is
4,603: N=4,602 fails the inequality and N=4,603 satisfies it. No floating-point
approximation is required for this decision.

### Completed fresh evaluation

The fixed plan was written before sampling. It specified:

* Inputs: uniform seven-element subsets of integers 1 through 60.
* Draws: 4,603 independent draws, with replacement between trials; individual
  tuples contain distinct speeds. Inputs are not filtered for openness,
  primitiveness, difficulty, success, or novelty relative to prior examples.
* Random source: Python SystemRandom using operating-system randomness.
* Failures: anything without a verified receipt.
* Solver: the frozen implementation identified by the plan's configuration hash.

Observed result: 4,603 verified receipts, zero unresolved/invalid/error/timeout
outcomes. A separate verifier checked every receipt and the binomial threshold.

Under the plan's IID and provenance assumptions, the evaluation supports the
one-sided 99% confidence statement

    p <= 0.001,

equivalently at least 99.9% verified-answer availability for the frozen solver
under this particular generated-input distribution. The exact-output checker
and the availability confidence statement establish different things.

This is a mathematical-input laboratory evaluation. It includes no physical
measurements and does not validate a physical deployment. The original 75
curated residuals were not used as an IID reliability sample.

Plan SHA-256:

    450d10c6880c217b80f68a919a94ddfabea3dd94b8da7e56f899d3fe7d1084e4

Frozen configuration SHA-256:

    6100639ea3593084201f6487a8ee37debc718716738773a34943787b49329707

## 4. Meaning of grounding in reality

For integer and rational inputs, ground truth is the exact relation being
checked. We can inspect a witness and establish that relation without guessing
from a model's confidence score.

For a physical application, add a separate measurement contract: what is
observed, how it is measured, calibration and uncertainty, data provenance,
the relevant population, and the definition of success. An exact calculation
over recorded measurements proves a fact about those recorded values. A claim
about the underlying physical system additionally needs the measurement and
sampling assumptions.

The empirical branch can then supply a statistically valid, auditable claim
under those assumptions. No physical sensor or deployment stream was supplied
for this demonstration, so no such validation is asserted. The implemented
contract is ready to separate those claims when real measurements are added.

## 5. Execution semantics

The solver first normalizes speeds and checks a small denominator certificate.
It then tries canonical proposals, including non-unit multipliers, and uses the
complete pair-sum grid if needed and within the work budget. Every successful
output is checked again at the original input. Exceeding a budget is unresolved,
not a conclusion that no witness exists.

An outcome ledger records each trial's input, status, plan fingerprint,
configuration fingerprint, receipt, and previous-event fingerprint. The fixed
horizon check rejects missing, reordered, duplicated, or extra trials. Model
changes and mismatched receipts invalidate the report. Hashes detect changes
relative to the recorded plan; they do not independently attest that the
sampling history is honest or IID.

The pilot refuses to overwrite an existing evidence directory. Raw trials
are flushed to disk as they occur. A failed or interrupted run must be retained
and reported, not replaced by an unnoticed rerun until success. No repeated
physical experiment or human-subject interaction was performed.

The statistics module deliberately supports a fixed horizon only. Curated
residual sets, filtered-success samples, and optional-stopping designs do not
satisfy that contract. An anytime-valid e-process or confidence sequence would
be a different supported protocol, building on the empirical mode already in
SWC; its justification must accompany its implementation.

## 6. Tests and sources

Twelve new test methods cover exact receipts, finite completeness, altered
scope, missing and duplicate domain rows, integer binomial tails, minimum
sample size, conservative confidence coverage over complete small binomial
distributions, failure inclusion, all-failure cases, mixed configurations,
wrong-input receipts, selected samples, and work budgets.

They pass alongside the 45 existing certificate and canonical-search tests.
The independent verifier imports no producer or assurance-module functions.
It reconstructs all 12,673 domain inputs, checks all 4,603 trial receipts with
Fraction arithmetic, and evaluates the statistical threshold by a direct
binomial sum. Passing tests supports the implementation; it is not independent
peer review or evidence of a novel probability theorem.

The exact binomial method follows the established confidence-bound framework
documented by NIST:
https://itl.nist.gov/div898/software/dataplot/refman2/auxillar/exacbino.htm

For a future anytime-valid protocol, see Howard, Ramdas, McAuliffe, and Sekhon,
*Time-uniform, nonparametric, nonasymptotic confidence sequences*, Annals of
Statistics 49(2), 2021:
https://arxiv.org/abs/1810.08240

## 7. Artifacts and use

Implementation:

* `swc_assurance.py`: exact-output receipts, finite-domain verification, and
  exact fixed-horizon reliability calculations.
* `run_swc_assurance_pilot.py`: producer, frozen plan, fresh sampling, and ledger.
* `verify_swc_assurance_pilot.py`: independent verification of the stored pilot.
* `test_swc_assurance.py`: regression and coverage tests.

Recorded evidence is under `evidence/swc-assurance-v1/`: `domain.json`,
`finite-coverage.json`, `plan.json`, `trials.jsonl`, `reliability.json`,
`summary.json`, and `SHA256.json`.

To verify the existing experiment without sampling again:

```sh
python3 -B verify_swc_assurance_pilot.py evidence/swc-assurance-v1
python3 -B -m unittest test_swc_assurance test_swc_canonical_pair test_swc_lonely_runner test_swc_certificate_kernel
```

A new run needs a new, explicitly named evidence directory and constitutes a
new evaluation. Do not pool it with the earlier run without a valid sampling
and multiple-testing plan.

## Research statement

SWC provides exact certificates for returned mathematical answers, complete
coverage certificates for declared finite domains, and confidence-qualified
reliability statements for fixed systems under stated input distributions.
This demonstration certifies a 12,673-instance operating domain and evaluates
4,603 fresh generated inputs. It does not claim to settle an infinite
existence conjecture or establish assumption-free facts about physical reality.

Original new code: Apache-2.0. Explanatory text and numerical records: CC BY 4.0.
