# A reusable SWC certificate checker

2026-09-05. This prototype turns several previously separate experiments into
one compositional proof interface. It does not prove the Erdős–Straus
conjecture universally or claim novelty for the underlying mathematics.

## Supported judgments

The checker computes the scope of its conclusion:

* A single integer n with an exact accepted witness mass.
* Every member n(t) of an explicitly checked polynomial family, for integer t>=0.

It never accepts a caller-supplied “all primes proved” flag. A family result
identifies its actual target polynomial rather than claiming broader coverage.
Finite mass may be zero; in that case no existence conclusion is issued.

## Five proof rules

### Exact finite mass

Supply a normalized list of exact rational weights and candidate integer
triples. The checker verifies each triple against 4xyz=n(xy+xz+yz).
It counts invalid triples as rejection. Accepted mass is recomputed from the
weights; a positive number supplied by the caller is not evidence.

### Mixture

Combine checked instance distributions with nonnegative rational weights
summing to one. All components must concern the same n. The checker preserves
rejection mass and adds probabilities when components return the same witness.
Its accepted mass is the corresponding weighted sum.

### Witness transport

Given a checked distribution for q whose accepted triples have first
denominator a, and integer L>=2, put n=q+4(L-1)a.
For each accepted triple (a,y,z), form

    (La, Lny/q, Lnz/q).

The checker requires exact integral divisions, independently verifies the
new identity and checks q<n/2. Rejection remains rejection. A parent with
an incompatible accepted first denominator is rejected rather than silently
conditioned away.

### Polynomial family

Supply coefficient arrays for n(t),x(t),y(t),z(t), in increasing powers of t.
The checker requires nonnegative integer coefficients, positive constant
denominator coefficients, n(0)>=2, and nonconstant n.
These are sufficient to prove integrality and positivity for every integer
t>=0. They intentionally exclude some positive polynomials with negative
coefficients; those would need a stronger positivity proof rule.

It then expands and compares the coefficients of

    4x(t)y(t)z(t) and n(t)[x(t)y(t)+x(t)z(t)+y(t)z(t)].

Exact coefficient equality proves the identity for every t, without sampling
particular parameter values. Point mass on the resulting triple has accepted
mass one for every family member.

The included example checks n(t)=97+120t, the family already derived in
swc-family-induction-and-coverage.md. This is a stronger verification method
for that result, not new mathematical coverage.

### Instantiation

Evaluate a checked family at a specified nonnegative integer t, recheck its
integer witness, and return an instance result that can enter mixtures or
transports.

## Why the composition is sound

Certificate dependencies are required to form an acyclic graph. Induction
over this graph establishes that every node's emitted judgment follows from
the earlier checked judgments:

* The finite rule explicitly checks its witnesses and normalization.
* Convex mixtures preserve normalization and add exact accepted mass.
* Transport preserves every accepted output by its checked arithmetic map.
* The family rule establishes an identity in the polynomial ring together
  with sufficient positivity conditions.
* Instantiation specializes that identity at a permitted integer.

The output includes a SHA-256 fingerprint binding the supplied certificate.
The fingerprint protects identification of the checked input; it is not a
mathematical proof or an author authentication mechanism by itself.

## Verified examples

The composition example begins with mass 1/2 on a valid witness for 33,
transports it to 73, then mixes it with a mass-one witness for 73.
Weights 1/4 and 3/4 produce accepted mass

    (1/4)(1/2)+(3/4)(1)=7/8.

The family example proves existence for every n=97+120t, t>=0, with accepted
point mass one. Neither example asserts that every prime is covered.

Fifteen small tests cover valid proofs and rejection of wrong targets,
incompatible anchors, nonintegral transformations, negative or floating-point
probabilities, failed normalization, cycles, duplicate nodes, altered
polynomial identities, missing positivity conditions and forged universal scope.

## Limits and resources

### Combined constructions

The case_union rule checks existence over the union of its verified case
domains, without mixing evidence for different target numbers. The saved
bundle evidence/swc-combined-cases.json contains twelve polynomial families
and two instance certificates. Its derivation is in
swc-combined-case-induction.md. The extended suite has 24 passing tests.

### Two-parameter extension

The kernel additionally supports polynomial_family_2d and instantiate_2d.
These check a two-variable coefficient identity and specialize both variables.
The documented double-induction example is in swc-double-induction.md;
its certificate is evidence/swc-kernel-double-family.json.
The extended suite has 20 passing tests. The conclusion is restricted to
the displayed n(u,v), not promoted to all integers or primes.

This is a Python exact-arithmetic prototype, not a Lean/mathlib formalization
or an independently reviewed proof kernel. Its implementation remains part of
the trusted base. The tests help detect errors; they do not establish that no
implementation errors remain.

The checker performs no search or network calls. It limits certificate size,
dependency depth, polynomial degree and integer size. The included checks are
small and completed without large sieves or parallel numerical runs.

Examples from the repository root:

    python3 -B research/swc_certificate_kernel.py research/evidence/swc-kernel-family.json
    python3 -B research/swc_certificate_kernel.py research/evidence/swc-kernel-composition.json

Tests from the research directory:

    python3 -B -m unittest test_swc_certificate_kernel

This strengthens reproducibility and claim checking. Universal positivity still
requires a new arithmetic theorem establishing coverage beyond the particular
instances and families certified here.
