# Claims and limits

## Exact mathematical claims in the paper

- A sound deterministic verifier plus a formally certified positive lower bound on accepted witness mass proves ordinary deterministic existence.
- The rule is conservative over the ambient logic in which the measure and verifier obligations are formalized.
- Pointwise certificate families, finite covers, and well-founded reductions can prove universal statements when their obligations are discharged for every instance.
- Mixture, product, sequential, conditioning, change-of-measure, pushforward, moment, local-lemma, and obstruction rules preserve the stated certificate semantics under their explicit hypotheses.
- In a finite full-support witness space, deciding whether accepted mass is positive is equivalent to deciding whether a witness exists; exact counting remains hard in general.

## Exact experimental outputs

- SAT accepted masses are recomputed from integer product weights over every assignment.
- In the SAT support-collapse ablation, hardening the learned proposal to a point mass yields zero accepted mass on 10 of 60 satisfiable instances; a 10% uniform mixture restores exact positive mass on all 60.
- The path-graph benchmark recomputes exact weighted counts by dynamic programming and cross-checks them against a closed form.
- The Erdős–Straus survey reconstructs and integer-checks a finite certificate for every reported prime in the stated range.
- The proof-carrying integrity suite accepts 300 valid path certificates and rejects 1,800 specified mutations.

## Statistical outputs

- Quantifier-audit and optional-stopping simulations use fixed seeds and are reported with their finite simulation scope.
- The e-process theorem is exact under its null-model assumptions; the displayed crossing rates are Monte Carlo estimates.

## Claims not made

- SWC does not claim that positive probability implying existence is a new mathematical principle; this is the classical probabilistic method.
- SWC does not bypass SAT, #P, or general proof-search complexity.
- The current software is a reference kernel, not a formally verified proof assistant implementation.
- The certificate mutation test is not a cryptographic security proof.
- The Erdős–Straus conjecture is not proved by this paper.
- Arbiter v23 is a discovery system, not a trusted verifier or an author.
