# SWC reachability certificates with failed paths

2026-09-05. Scope: a probabilistic verification rule allowing cycles and
explicit rejection. This is not a universal Erdős–Straus proof. The
probability argument uses standard submartingale and drift reasoning;
no novelty claim is made.

## What improves

The earlier drift argument required reaching a successful terminal state with
probability one. For SWC, positive probability is enough. This rule separates
two questions: whether the run finishes, and how much of its finished mass
reaches verified witnesses rather than failure. It can certify success even
when failure has positive probability.

## Certificate

Fix an integer n>=2. Let a stochastic process have success terminals G,
failure terminals B, and nonterminal states. Every success terminal carries
positive integers x,y,z checked against 4xyz=n(xy+xz+yz).
Terminal states are absorbing.

Provide two functions:

* L(s) in [0,1], equal to 1 at success and 0 at failure.
* V(s)>=0, equal to 0 at both kinds of terminal.

For every nonterminal state, prove the local inequalities

    L(s) <= E[L(next)|s],
    V(s) >= epsilon + E[V(next)|s], epsilon>0.

Transition probabilities must be nonnegative and sum to one. For the finite
checker all expectations are exact rational sums. Larger/infinite process
versions would also need the appropriate measurability and integrability
hypotheses; the prototype does not certify those automatically.

For any positive integer horizon H,

    Pr(success by H) >= L(start) - V(start)/(epsilon H).

When the right-hand side is positive, it supplies a valid SWC mass certificate.

## Proof

Absorbing terminal states preserve L. The first local inequality therefore
implies E[L(S_H)]>=L(start). Since L=1 at success, L=0 at failure and
L<=1 elsewhere,

    E[L(S_H)] <= Pr(success by H) + Pr(not yet terminal at H).

The drift inequality, with V=0 after termination, telescopes to

    epsilon * sum_{t=0}^{H-1} Pr(T>t) <= V(start).

Every summand is at least Pr(T>H), so

    Pr(T>H) <= V(start)/(epsilon H).

Combining the two inequalities proves the displayed success bound without
assuming in advance that the expected hitting time is finite. Every successful
terminal emits a checked witness for the original n, completing the SWC
soundness argument.

Nested calls can be encoded as states including a stack; cycles do not require
every step to decrease V, only the proved conditional expectation inequality.
The finite prototype uses an explicit graph rather than an unbounded stack.

## Small exact example

The example concerns n=73 and has positions i=0,...,32. Position 0 is a
success terminal carrying (22,110,4015). Position 32 is a failure terminal.
Interior positions move left or right with probability 1/2. Start at i=3.

Set

    L(i)=(32-i)/32, V(i)=i(32-i).

At each interior position the expected L is unchanged and the expected V
decreases by exactly 1. The start values are L=29/32 and V=87.
Taking H=192 gives

    Pr(success by 192) >= 29/32 - 87/192 = 29/64 > 0.

Exact finite path counting gives approximately 82.86554%, above the certified
45.3125% lower bound. The eventual failure probability is nonzero; it does not
invalidate the existence certificate for this particular n.

The example illustrates a cyclic proof-search schedule with a verified
terminal witness already available. It is not a new solution for 73 or
evidence of universal parameter construction.

## Verification

The standalone checker imports no producer modules. It checks the target
equation, terminal behavior, probability normalization, both local
inequalities, and the claimed positive finite-horizon bound.
Seven mutations are rejected: an invalid witness, inflated initial success
potential, negative weight, unnormalized weight, a nonterminating self-loop,
positive success value at a failed terminal, and a forged final bound.

The implementation handles at most 128 explicit states. The demonstration
uses 33 states and 192 transitions in the finite path calculation. No large
prime sweep, additional installation or deployment was performed.

## Universal proof obligation

To cover every prime p, we still need a uniform construction of a transition
system and functions L_p,V_p satisfying the certified inequalities with

    L_p(start) - V_p(start)/(epsilon_p H_p) > 0.

This theorem permits failed paths and therefore removes an unnecessary
almost-sure-success requirement from the earlier plan. It does not supply
the number-theoretic construction needed for all primes. That construction
remains open.

Reproduce:

    python3 -B research/swc_reachability_example.py --out research/evidence/swc-reachability-certificate.json
    python3 -B research/verify_swc_reachability.py research/evidence/swc-reachability-certificate.json
