Stochastic Witness Calculus:
Exact Measure Certificates for Mathematical Existence, Learned Proof
Search, and Anytime-Valid Empirical Claims
Kenju Tomita
Rochester Institute of Technology; Ephemerent Research

September 4, 2026
Abstract
Probability can establish deterministic existence, but automated reasoning systems typically treat
randomized search, formal proof, model counting, and empirical confidence as unrelated objects. We
introduce Stochastic Witness Calculus (SWC), a machine-oriented certificate interface for proving
that a sound verifier accepts a set of witnesses with strictly positive measure. The resulting conclusion
is an ordinary deterministic theorem: probability is used to certify nonemptiness, not to weaken truth.
We give an instance-indexed semantics, a small proof calculus, family and cover rules for universal
statements, support-preserving mixtures, change-of-measure and conditioning rules, product and
sequential composition, moment-based mass certificates, a dual obstruction rule, and a compactness
extension for continuous witness spaces. We also identify a no-free-lunch boundary: for full-support
finite distributions, positive accepted mass is equivalent to satisfiability, and exact mass computation
inherits weighted model-counting hardness.
We implement an exact finite kernel and evaluate six settings. On 60 planted 16-variable SAT
instances, a learned product proposal raises median exact witness mass from 1/65,536 to 0.939; a 10%
uniform mixture preserves support while yielding a median 27,810-fold increase. A non-enumerative
dynamic-programming backend certifies weighted mass over witness spaces of size 22048 in about 1.1
seconds and agrees exactly with an independent closed form. A quantifier-audit stress test shows that
104 random checks miss a single exceptional instance among 106 with probability 0.9900, while 105
samples miss a true witness mass of 10−6 with probability 0.9048. For the Erdős–Straus case study,
exact enumeration certifies finite witnesses for all 82,887 primes p ≡ 1 (mod 24) below 107 using shifts
c ≤ 127; this is finite verification, not a proof of the open conjecture. A proof-carrying integrity stress
test accepts all 300 exact certificates and rejects all 1,800 tampered or floating-point-only variants.
Finally, optional-stopping simulations contrast a 30.8% null crossing rate for repeated nominal tests
with 4.34% for a likelihood-ratio e-process. SWC is a certificate and systems abstraction built on the
classical probabilistic method, not a new axiom or a shortcut around proof complexity.

Keywords: probabilistic method; formal verification; automated theorem proving; proof certificates;
witness distributions; weighted model counting; quantifier auditing; e-processes; anytime-valid inference;
Erdős–Straus conjecture.

1

Introduction

A probabilistic proof can establish a statement with complete mathematical certainty. The standard
mechanism is elementary: if a random construction produces a valid object with positive probability, then
at least one valid object exists. This idea underlies the probabilistic method throughout combinatorics
[1]. Its logical force is exact, not approximate.
1

Stochastic Witness Calculus

Kenju Tomita

Yet three distinct practices are often conflated:
1. probability inside a proof , where a measure calculation proves deterministic existence;
2. randomized proof search, where a generator samples candidate witnesses but supplies no proof that
success mass is positive;
3. statistical evidence about physical reality, where conclusions remain conditional on a data-generating
model and an error budget.
This paper proposes SWC as a common certificate language that keeps these modes separate. The
exact mode is designed for formal mathematics and automated theorem proving. The empirical mode is
designed for sequential physical experiments and scientific monitoring. They share a generator–verifier–
auditor architecture, but they do not share the same epistemic endpoint.
The logical core is classical. Formal probabilistic reasoning already appears in Coq, Isabelle/HOL,
EasyCrypt, probabilistic program logics, and formalizations of the probabilistic method [2, 3, 7, 8].
Recent proof-mining work also studies extraction of computable bounds from probabilistic existence
arguments [17]. The proposed contribution is therefore not the implication “positive probability implies
existence.” It is the following systems-level synthesis:
• an instance-indexed certificate schema for positive-mass existence;
• an explicit trusted-kernel boundary between learned generation and deductive verification;
• support-preserving mixtures that prevent learned policies from erasing rare witnesses;
• a dual obstruction rule for probabilistic discovery of certified counterexamples;
• quantifier-discipline checks that block invalid average-to-pointwise promotion;
• a separate anytime-valid empirical mode for claims about physical systems;
• a reproducible benchmark spanning SAT, an open-number-theory case study, and sequential testing.
Main claim. When all mathematical obligations are formally discharged, an exact SWC certificate is
as strong as an ordinary proof because it compiles into one. In physical science, no method can remove
assumptions about instruments, interventions, and data generation; the appropriate analogue is instead
a theorem about the protocol’s false-certification risk under an explicit assumption set.
Contributions.
explicit.

This paper makes six concrete contributions while keeping the classical logical core

1. We define a proof judgment for positive-mass existence certificates and prove soundness and conservativity relative to an ambient logic.
2. We extend the basic rule to universal families through pointwise, cover, and well-founded reduction
rules, making the quantifier obligations explicit.
3. We give compositional certificate rules for mixtures, products, Markov kernels, conditioning, change
of measure, deterministic pushforwards, first/second moments, and local-lemma backends.
4. We specify a trusted-kernel boundary and a proof-carrying mass architecture compatible with exact
enumeration, dynamic programming, knowledge compilation, and formally verified model counting.
5. We define an adversarial quantifier-audit discipline that rejects average-to-pointwise promotion and
zero-hit-to-zero-mass inference.
2

Stochastic Witness Calculus

Kenju Tomita

6. We evaluate the interface in six complementary experiments spanning learned discrete search,
non-enumerative exact counting, universal-quantifier stress tests, open-number-theory certificates,
proof-carrying integrity, and anytime-valid empirical monitoring.

2

Related Work and Positioning

2.1

The probabilistic method

The classical probabilistic method proves existence by defining a probability space and showing that the
set of desired objects has nonzero measure, often through expectation, concentration, deletion, alteration,
or the Lovász local lemma [1]. Edmonds and Paulson formalize reusable versions of these arguments in
Isabelle/HOL, including a formal Lovász local lemma, and document gaps that informal treatments can
hide [8]. SWC packages the same logical pattern as an instance-indexed certificate intended to interact
with search models and proof kernels.

2.2

Verification of probabilistic programs

Randomized algorithms and probabilistic programs have been formalized in Coq and Isabelle/HOL [2, 7].
Relational logics and coupling methods support reasoning about uniformity, independence, privacy, and
cryptographic games [3]. Systems such as Caesar target deductive verification of probabilistic programs,
while reparameterization methods compile randomness into deterministic functions of random seeds [21,
24]. Those systems primarily verify probabilistic computations. SWC instead takes a theorem-facing
view: the output of a probabilistic program is treated as a witness distribution, and the central certificate
is a lower bound on the mass of deterministically valid witnesses.

2.3

Formal proof assistants, witnessing distributions, and AI-guided search

Lean and Mathlib exemplify the small-kernel model in which generated proof terms are checked
independently of the generator [15, 23]. Contemporary theorem-proving agents similarly place exact
verifiers in the loop, while recent systems automate proof engineering in specialized probabilistic logics
such as EasyCrypt [13]. Paradise et al. use a sparse witnessing distribution as a proof oracle for checking
approximate consistency of exponentially many probabilistic claims [18]; their goal is complexity-theoretic
verification of a predictor, whereas SWC treats a distribution over mathematical witnesses as an object
whose accepted mass can certify deterministic existence. SWC complements these lines by asking a
generator to propose not only a witness or proof script, but a distribution plus a checkable lower bound
on its accepted mass.

2.4

Certified counting and proof-carrying mass

For a finite Boolean witness space, accepted probability is a weighted model count. Exact counting
is generally intractable—the classical counting complexity of Boolean solution sets traces to Valiant’s
#P framework [25]—but structured representations can make counting and checking tractable. Capelli
studies knowledge-compilation languages as proof systems for #SAT [5]. Bryant, Nawrocki, Avigad,
and Heule introduce certified partitioned-operation graphs and a Lean-verified toolchain for weighted
and unweighted model counting [4]. Tan et al. formally verify the PAC guarantee of an approximate
model counter and dynamically certify solver calls [22]. These systems provide natural back ends for
SWC mass obligations. Exact proof-producing counts can discharge mathematical certificates directly;
3

Stochastic Witness Calculus

Kenju Tomita

PAC counts remain bounded-error unless a separate deterministic lower-bound certificate removes the
residual failure probability.

2.5

Proof-carrying systems and trusted kernels

The architectural principle is close to proof-carrying code: an untrusted producer may perform expensive
synthesis, while a small consumer checks a portable certificate [16]. In SWC, the producer may be a
language model, optimizer, sampler, model counter, or human mathematician. The trusted consumer
checks distribution normalization, verifier soundness, the accepted-mass lower bound, positivity, and
quantifier scope. The system is therefore designed so that improvements in search do not enlarge the
trusted base.

2.6

Anytime-valid empirical inference

Confidence sequences and e-processes provide time-uniform error guarantees under adaptive monitoring
[11, 19]. Their conclusion remains statistical rather than deductive about nature, but the error statement
is itself mathematical and can be machine checked. We adopt this distinction in the empirical mode of
SWC.

3

Exact Mathematical Mode

3.1

Instance-indexed witness systems

Definition 3.1 (Witness problem). A witness problem is a tuple
P = (I, {Wi }i∈I , R),
where I is an instance space, Wi is the witness space for instance i, and R(i, w) is the target relation.
The intended theorem is
∀i ∈ I ∃w ∈ Wi R(i, w).
Definition 3.2 (Exact stochastic witness certificate). For a fixed instance i, an exact SWC certificate is
Πi = (µi , Vi , δi , πsound , πmass , π+ ),
where:
1. µi is a probability measure on Wi ;
2. Vi : Wi → {0, 1} is a deterministic verifier;
3. πsound proves Vi (w) = 1 ⇒ R(i, w);
4. πmass proves µi ({w : Vi (w) = 1}) ≥ δi ;
5. π+ proves δi > 0.
Theorem 3.3 (Stochastic witness soundness). If an exact SWC certificate exists for instance i, then
∃w ∈ Wi such that R(i, w).
Proof. Let Ai = {w : Vi (w) = 1}. If no valid witness existed, verifier soundness would imply Ai = ∅.
Every probability measure satisfies µi (∅) = 0, contradicting µi (Ai ) ≥ δi > 0. Thus Ai contains an
accepted witness, and soundness converts it into a valid witness.
4

Stochastic Witness Calculus

Kenju Tomita

The conclusion is deterministic. There is no residual probability that the theorem is false once the
certificate obligations are proved.

3.2

Family certificates and universal theorems

A universal statement requires more than many successful instances. It requires one proof object whose
obligations range over every instance.
Definition 3.4 (Uniform certificate family). A uniform SWC family for a witness problem P consists
of definable maps
i 7→ (µi , Vi , δ(i))
and proofs, uniform in i, that Vi is sound, that µi (Vi−1 (1)) ≥ δ(i), and that δ(i) > 0 for every i ∈ I.
Corollary 3.5 (Pointwise compilation). A uniform certificate family proves
∀i ∈ I ∃w ∈ Wi R(i, w).
i

The lower bound need not be uniform in magnitude. A function such as δ(i) = 2−2 is logically sufficient,
although it gives an impractical extraction algorithm. The crucial requirement is pointwise positivity,
not a positive average over i.

3.3

A proof rule

The exact mode can be exposed as the inference rule
µi ∈ Prob(Wi )

∀w [Vi (w) = 1 ⇒ R(i, w)] µi (Vi−1 (1)) ≥ δi
∃w ∈ Wi R(i, w)

δi > 0

SWC-Exists.

A universal theorem requires the premises for every instance i, not merely on average over an instance
distribution.
Proposition 3.6 (Conservativity). Assume the measure theory and verifier semantics used by SWC
are formalized in an ambient logic T . Every theorem derived by SWC-Exists is derivable in T without
adding a new axiom.
Proof. The rule is an abbreviation for the theorem that a measurable set of positive measure is nonempty,
followed by verifier soundness. Both are ordinary derivations in T .
Proposition 3.7 (Embedding ordinary constructive proofs). If a conventional proof provides a witness
wi with R(i, wi ), then it induces an SWC certificate with the point mass µi = δwi and lower bound
δi = 1.
Thus SWC does not replace ordinary proofs; it contains constructive existence as a degenerate case.

3.4

Quantifier discipline

Proposition 3.8 (Pointwise requirement). The statement
Pi∼ν [∃w R(i, w)] = 1
does not in general imply ∀i ∃w R(i, w).
5

Stochastic Witness Calculus

Kenju Tomita

Proof. A probability-one event may exclude a nonempty ν-null set. A universal conclusion requires a
certificate for each instance or a separate proof that the null exceptional set is empty.
This blocks a common invalid transition in open problems: density-zero or almost-sure solvability is not
universal solvability.
Proposition 3.9 (Finite cover rule). Suppose I = I1 ∪ · · · ∪ Im and, for each j, a uniform certificate
family proves ∀i ∈ Ij ∃w R(i, w). Then the families compose into a proof over all of I.
Proof. For any i ∈ I, choose an index j with i ∈ Ij and apply the corresponding certificate family. In a
proof assistant, membership evidence or a decidable classifier supplies the branch tag.
Proposition 3.10 (Well-founded reduction rule). Let ≺ be a well-founded relation on I. Suppose
base instances have exact certificates and every nonbase instance i has a computable reduction r(i) ≺ i
together with a sound witness transformer
Ti : Wr(i) → Wi ,

R(r(i), w) ⇒ R(i, Ti (w)).

Then certificates for reduced instances compile by well-founded induction into certificates for all instances.
This rule clarifies that SWC is compatible with ordinary induction and reduction arguments; probability
need only enter at the leaves where nonemptiness is established.

3.5

Support-preserving learned generators

A learned proposal may concentrate mass on likely witnesses but accidentally assign negligible or zero
mass to rare valid ones. The following mixture protects sound search support.
Proposition 3.11 (Support-preserving mixture). Let µ0 be a baseline distribution, µ1 any learned
distribution, and
µη = ηµ0 + (1 − η)µ1 ,
0 < η ≤ 1.
For every measurable accepted set A,
µη (A) ≥ ηµ0 (A).
Hence any positive baseline witness mass remains positive after learning.
Proof. Immediate from nonnegativity: µη (A) = ηµ0 (A) + (1 − η)µ1 (A) ≥ ηµ0 (A).
The learned policy is therefore outside the trusted logical core. It may improve search efficiency, but the
mixture and exact mass proof preserve theorem soundness.
Proposition 3.12 (Change-of-measure transfer). Let µ and ν be probability measures and let A be the
accepted set. If µ ≪ ν on A and
dµ
(w) ≤ C < ∞
dν

for ν-almost every w ∈ A,

then

µ(A)
.
C
Consequently, a certified positive mass under µ transfers to ν whenever the density-ratio bound is proved.
ν(A) ≥

6

Stochastic Witness Calculus

Kenju Tomita

Proof. By the Radon–Nikodym representation, µ(A) =

A (dµ/dν) dν ≤ Cν(A).

R

Proposition 3.13 (Conditioning and rejection). Let A ⊆ B with µ(B) > 0. Under the conditioned
generator µ(· | B),
µ(A)
µ(A | B) =
.
µ(B)
Thus rejection sampling preserves positivity whenever the retained event has positive mass and the
accepted subset already has positive mass.

3.6

Certificate combinators

The term “calculus” refers to a small algebra of certificate-preserving transformations. The following
rules are elementary consequences of measure theory, but making them explicit permits a checker to
assemble large certificates from smaller ones without trusting the search procedure.
Proposition 3.14 (Tagged disjunction). Let A1 ⊆ W1 and A2 ⊆ W2 have certified masses µ1 (A1 ) ≥ δ1
and µ2 (A2 ) ≥ δ2 . On the tagged union W1 ⊔ W2 , choose the mixture ηµ1 + (1 − η)µ2 , where 0 ≤ η ≤ 1,
and accept the corresponding tagged accepted set. Its mass is at least
ηδ1 + (1 − η)δ2 .
In particular, any positive component proves the disjunctive existence claim.
Proof. The two tagged components are disjoint, so their accepted masses add under the mixture.
Proposition 3.15 (Product conjunction). Suppose µj (Aj ) ≥ δj for j = 1, 2. Under the explicit product
measure µ1 ⊗ µ2 , the product accepted set A1 × A2 has mass at least δ1 δ2 . Thus two existence certificates
compose into a certificate for a witness pair satisfying both relations.
Proof. By the defining property of the product measure, (µ1 ⊗ µ2 )(A1 × A2 ) = µ1 (A1 )µ2 (A2 ) ≥ δ1 δ2 .
Proposition 3.16 (Sequential composition). Let µ be a distribution on W1 , let A ⊆ W1 satisfy µ(A) ≥ δ,
and let K(w1 , ·) be a probability kernel on W2 . If for every w1 ∈ A a measurable accepted set B(w1 ) ⊆ W2
satisfies
K(w1 , B(w1 )) ≥ ε,
then the joint generator w1 ∼ µ, w2 ∼ K(w1 , ·) assigns mass at least δε to
{(w1 , w2 ) : w1 ∈ A, w2 ∈ B(w1 )}.
Proof. Integrating the conditional lower bound over A gives
Z
A

K(w1 , B(w1 )) dµ(w1 ) ≥ εµ(A) ≥ δε.

Proposition 3.17 (Sound pushforward). Let f : W → W ′ be measurable. If acceptance of w implies
acceptance and soundness of f (w), then the pushforward distribution f∗ µ assigns the target accepted set
at least the source accepted mass. Deterministic witness transformations therefore preserve a certified
lower bound.
These rules separate two notions that are frequently conflated. Product and sequential composition use
explicitly defined joint measures; they do not infer independence from data. A checker should reject a
product lower bound unless the product construction or an equivalent dependence proof is part of the
certificate.
7

Stochastic Witness Calculus

Kenju Tomita

Derivation-level soundness. Let certificate derivations be generated from atomic mass certificates by
tagged disjunction, product, sequential bind, conditioning, change of measure, pushforward, finite cover,
and well-founded reduction. Soundness of the full calculus follows by structural induction: each rule
maps valid premises to a valid positive-mass conclusion, and the terminal SWC-Exists rule converts
positive accepted mass into ordinary existence. This gives a clean implementation strategy: the trusted
kernel checks a small derivation tree rather than re-running the untrusted search.

3.7

Witness extraction

Theorem 3.18 (Repeated-sampling extraction). Suppose independent samples from µi are computable
and accepted with probability at least δi > 0. Then after k trials,
P(no accepted witness) ≤ (1 − δi )k ,
and the expected number of trials to the first accepted witness is at most 1/δi .
Existence may be mathematically useful even when δi is too small for practical extraction. SWC records
both logical success and algorithmic cost.

3.8

Classical versus constructive extraction

The logical status of a mass certificate depends on the ambient foundations and on how the measure is
represented.
Proposition 3.19 (Finite atomic extraction). Let W = (w1 , . . . , wm ) be a finite list, let V be decidable,
P
and assign exact nonnegative integer weights aj with j aj > 0. If
aj > 0,

X
j:V (wj )=1

then a linear scan computes an index j with aj > 0 and V (wj ) = 1.
Proof. If every accepted entry had weight zero, the accepted-weight sum would be zero. Decidability of
V and the finite list permit exhaustive search for the first accepted positive-weight entry.
Thus the finite rational kernel used in our experiments is constructive: positivity both proves existence
and yields an explicit witness. In a general uncountable measure space, the theorem “positive measure
implies nonempty” remains an ordinary classical existence argument, but it need not provide an algorithm
for locating a point. A formal implementation should therefore record two independent fields: theorem
status and extraction status. This distinction prevents a nonconstructive H3 certificate from being
advertised as an efficient H4 witness generator.
For countably supported generators, effective extraction additionally requires a computable enumeration
and a certified procedure that eventually exposes enough accepted mass. Merely knowing an abstract
real number µ(A) > 0 need not reveal where its mass is located.

3.9

Expectation certificates

The usual first-moment method fits the same interface.

8

Stochastic Witness Calculus

Kenju Tomita

Proposition 3.20 (Expectation-to-witness rule). Let F : Wi → R be measurable and integrable. If
Eµi [F ] ≥ τ , then there exists w with F (w) ≥ τ .
Proof. If F (w) < τ for every w, then the measurable function τ − F is strictly positive everywhere.
S
Since Wi = k≥1 {w : τ − F (w) ≥ 1/k} and µi (Wi ) = 1, at least one set in the union has positive
measure. Hence E[τ − F ] > 0, contradicting E[F ] ≥ τ . In a finite space this reduces to the familiar fact
that at least one value is no smaller than the average.
A proof compiler can reduce this rule to nonemptiness of {w : F (w) ≥ τ }, sometimes with an explicit
mass lower bound when F is bounded.
Theorem 3.21 (Paley–Zygmund backend). Let X ≥ 0 be square-integrable with E[X] > 0. For
0 ≤ θ < 1,
E[X]2
P(X ≥ θE[X]) ≥ (1 − θ)2
.
E[X 2 ]
In particular,
P(X > 0) ≥

E[X]2
> 0.
E[X 2 ]

Proof. Write A = {X ≥ θE[X]}. Then
E[X] ≤ θE[X] + E[X1A ],
so (1 − θ)E[X] ≤ E[X1A ]. Cauchy–Schwarz gives E[X1A ]2 ≤ E[X 2 ]P(A), yielding the bound.
This rule turns second-moment calculations into explicit positive-mass certificates and is often stronger
than a bare expectation argument.
Proposition 3.22 (Union-bound backend). Let B1 , . . . , Bm be measurable bad events. If certified upper
bounds satisfy
m
X

µ(Bj ) ≤ 1 − ε

for some ε > 0,

j=1

then the good event G =

T

c
j Bj has µ(G) ≥ ε and therefore contains a witness.

Proof. The union bound gives µ(

S

j Bj ) ≤

j µ(Bj ) ≤ 1 − ε, so µ(G) = 1 − µ(

P

S

j Bj ) ≥ ε > 0.

Example 3.23 (Ramsey lower-bound certificate). Choose a uniformly random labeled graph on n
vertices. For each
k-vertex set S, let BS be the event that S induces either a clique or an independent
k
set. Since all 2 edges are independent,
P(BS ) = 21−(2) .
k

Consequently,

!

P

\
S

BSc

!

n 1−(k)
≥1−
2 2 .
k

Whenever the right side is positive, Theorem 3.22 compiles the mass bound into a deterministic existence
theorem for a graph with neither a k-clique nor a k-vertex independent set, hence R(k, k) > n. In SWC
terms, the graph distribution, the forbidden-subgraph verifier, the exact union-bound arithmetic, and
the positive remainder are separate checkable fields.
9

Stochastic Witness Calculus

Kenju Tomita

Local-lemma backend. The symmetric Lovász local lemma is another native mass compiler: if bad
events each have probability at most p, each depends on at most d others, and ep(d + 1) ≤ 1, then the
probability of avoiding all bad events is positive [1, 10]. A proof-carrying implementation need only
certify the event probabilities, the dependency graph, and the inequality. Existing formalizations of the
local lemma make this a realistic proof-assistant backend [8].

3.10

Dual certified refutation

Definition 3.24 (Obstruction verifier). An obstruction verifier U (i, c) is sound if
U (i, c) = 1 ⇒ ∀w ∈ Wi ¬R(i, w).
Theorem 3.25 (Stochastic obstruction rule). If a probability distribution over pairs (i, c) assigns positive
mass to certificates accepted by a sound obstruction verifier, then there exists a counterexample instance
i.
Proof. Positive accepted mass implies at least one accepted pair (i, c). Soundness of U proves that this
i has no valid witness.
Sampling many failed witnesses is not a refutation. The accepted object must certify nonexistence.

3.11

Continuous witness spaces

For continuous distributions, an isolated exact witness often has measure zero. Positive mass is sufficient
but not necessary. One remedy uses nested approximate certificates.
Theorem 3.26 (Nested approximation rule). Let K be compact, let F : K → R≥0 be continuous, and
let
Ak = {w ∈ K : F (w) ≤ 2−k }.
If each Ak is nonempty, then there exists w⋆ ∈ K with F (w⋆ ) = 0.
Proof. The sets Ak are nonempty, closed, and nested. Compactness gives a point in their intersection.
Continuity and F (w) ≤ 2−k for every k imply F (w) = 0.
An SWC proof may establish nonemptiness of each Ak through positive mass, while interval arithmetic
and compactness discharge the limiting step.

4

Exactness Levels and Complexity Boundaries

4.1

Certificate-status lattice

The word “probabilistic” can describe several epistemically different objects. SWC uses explicit status
labels:

10

Stochastic Witness Calculus

Kenju Tomita

Level

Object

Mathematical consequence

H0
H1
H2

Heuristic or Monte Carlo success estimate
PAC or confidence lower bound with failure probability β > 0
Exact mass theorem conditional on an unproved arithmetic or
physical hypothesis
Exact proof-carrying lower bound µ(A) ≥ δ > 0
Extracted witness accepted by a deterministic verifier

Evidence only
Bounded-error claim
Conditional theorem

H3
H4

Ordinary existence theorem
Constructive certificate

Only H3 and H4 have unconditional theorem status relative to the ambient axioms. A checker must
preserve these labels rather than silently promoting H0–H2.

4.2

Full-support equivalence and no free lunch

Proposition 4.1 (Finite full-support equivalence). Let W be finite and let µ(w) > 0 for every w ∈ W .
For any accepted set A ⊆ W ,
µ(A) > 0 ⇐⇒ A ̸= ∅.
Thus positive mass is a different proof interface, not an automatic reduction in logical or computational
difficulty.
Proposition 4.2 (Complexity boundary). Let W = {0, 1}n , let µ be uniform, and let Vφ verify whether
an assignment satisfies a CNF formula φ. Deciding whether µ(Vφ−1 (1)) > 0 is exactly SAT, while
computing the exact numerator is #SAT and is #P-complete in general [25].
The value of SWC therefore comes from structured mass proofs, reusable certificate rules, and independent checking—not from bypassing worst-case complexity. A short certificate may exist when a direct
witness is difficult to discover, but no theorem in this paper implies that such certificates are always
short.

5

Trusted Kernel and Mass-Certificate Back Ends

For finite witness spaces, the trusted computation can be particularly small. Assign each witness wj a
nonnegative integer weight aj , not all zero. The exact accepted mass is
P

δ=

j:V (i,wj )=1 aj

P

j aj

.

The numerator is positive if and only if at least one positive-weight witness is accepted.
Listing 1: Reference finite-mass certificate checker.
check(instance, witnesses, integer_weights, verifier):
assert len(witnesses) == len(integer_weights)
assert all(weight >= 0)
assert sum(integer_weights) > 0
accepted_weight = 0
first_witness = None
for w, weight in zip(witnesses, integer_weights):
if verifier(instance, w):

11

Stochastic Witness Calculus

Kenju Tomita

accepted_weight += weight
if weight > 0 and first_witness is None:
first_witness = w
delta = accepted_weight / sum(integer_weights) # exact rational
return delta, first_witness

This enumerator is a reference semantics, not a scalability claim. In serious applications, πmass should
be supplied by symbolic counting, concentration, local lemmas, couplings, algebraic identities, proofproducing model counters, or a proof assistant.

5.1

Proof objects and kernel judgments

A portable derivation can be represented by the grammar
π ::= atom(C) | mix(η, π1 , π2 ) | product(π1 , π2 ) | bind(π1 , K, π2 )
| condition(B, π) | change(C, π) | push(f, π) | cover(π1 , . . . , πm ) | reduce(r, T, π).
The kernel judgment

Γ ⊢ π : (i, R, δ)

means that, under assumptions Γ, the derivation certifies a sound accepted set for instance i with mass
at least δ. The terminal rule may emit an existence theorem only after checking δ > 0. This syntax
makes dependency, conditioning, and quantifier scope explicit in the proof object rather than implicit in
prose.
Theorem 5.1 (Kernel soundness by structural induction). If every atomic certificate is sound and
each derivation constructor is checked against its corresponding rule in this paper, then every accepted
derivation Γ ⊢ π : (i, R, δ) with δ > 0 proves ∃w R(i, w) in the ambient logic.
Proof. Induct on the syntax of π. The atomic case is Theorem 3.3. Each constructor preserves a
valid lower bound by the associated mixture, product, sequential, conditioning, change-of-measure,
pushforward, cover, or reduction proposition. The terminal positivity check and verifier soundness yield
ordinary existence.

5.2

Trusted computing base

The intended exact kernel contains only:
1. a parser for the instance, distribution, verifier, and derivation tree;
2. exact arithmetic or proof-term checking for normalization and mass bounds;
3. a deterministic verifier soundness theorem;
4. implementations of the small certificate rules; and
5. a quantifier-scope checker.
Language models, neural proposal policies, Monte Carlo estimators, SAT solvers, compilers, and
theorem-search agents remain untrusted unless their outputs carry independently checkable certificates.

12

Stochastic Witness Calculus

5.3

Kenju Tomita

Proof-producing counting back ends

For Boolean witnesses, an accepted mass is a weighted model count. Certified knowledge compilation
can translate a CNF into a tractable graph together with a proof of equivalence; a small verified checker
then computes the exact weighted count [4]. This is a direct large-scale backend for H3 certificates.
Approximate counting with formally verified PAC guarantees [22] is valuable for search and boundederror evidence, but by itself remains H1: a nonzero failure budget cannot be silently compiled into
theoremhood.
Proposition 5.2 (Certified interval positivity). Suppose a sound interval checker proves
0 < L ≤ µ(A) ≤ U
with exact rational endpoints L, U . Then L is an H3 mass certificate and A is nonempty. A floating-point
b(A) > 0 without a proved enclosure is not an H3 certificate.
estimate µ
This permits scalable numerical back ends provided every rounding and truncation error is enclosed
with directed arithmetic or a proof term. It also makes a sharp interface distinction: floating point may
guide search, but only an exact positive lower endpoint may cross the trusted boundary.

5.4

Threat model

The kernel rejects certificates with floating-point-only positivity, unproved normalization, hidden conditioning, unverifiable randomness, circular references, mismatched verifier versions, inferred independence,
or a universal conclusion supported only by sampled instances. Cryptographic hashes and reproducible
builds protect provenance, but they do not replace mathematical soundness.

6

AI-Assisted Stochastic Proof Search

6.1

Architecture

Let Gθ (w | i) be a learned witness generator. SWC separates four roles:
1. Generator: proposes witnesses and structured distributions.
2. Verifier: deterministically checks candidate validity.
3. Bound prover: derives a symbolic lower bound δi on accepted mass.
4. Adversarial auditor: searches for zero-mass instances, hidden independence assumptions, quantifier
swaps, and verifier mismatches.
A useful training objective is not merely empirical solve rate, but certifiable mass:
max Ei∼D log δ θ (i) ,




θ

where δ θ (i) is a formally justified lower bound rather than a Monte Carlo estimate. The support mixture
in Theorem 3.11 allows aggressive learning without deleting the baseline proof route.

13

Stochastic Witness Calculus

Instance i

Kenju Tomita

Learned generator
Gθ (· | i)

Deterministic
verifier Vi

Mass-bound prover
µi (Ai ) ≥ δi

Adversarial auditor

Formal kernel
δi > 0

Ordinary theorem
∃w R(i, w)

Figure 1: The generator is untrusted. Soundness comes from a deterministic verifier and a checked
positive-mass certificate.

6.2

Failure modes

The framework explicitly rejects:
• estimating δi from samples and treating the estimate as exact;
• assuming independence because empirical correlations are small;
• proving Ei [δi ] > 0 and concluding δi > 0 for every i;
• accepting a probabilistic verifier with nonzero false-acceptance risk as an exact theorem checker;
• defining a distribution whose normalization or measurability is not proved;
• moving from a continuous density around an approximate solution to existence of an exact point
without a limiting theorem.

7

Empirical Reality Mode

Mathematical truth is relative to axioms and formal semantics. Claims about physical systems additionally depend on assumptions about measurement, intervention, stationarity, confounding, and instrument
integrity. No statistical method converts these assumptions into assumption-free certainty.
We define an empirical certificate
Πemp = (A, P, D, Et , α, πcal ),
where A is the declared model class, P a preregistered protocol, D a signed data record, Et an evidence
process, and πcal a proof of risk calibration.
Theorem 7.1 (Anytime-valid certification). Suppose that under every distribution P in a null model
H0 , (Et ) is a nonnegative supermartingale with E0 ≤ 1. Then
sup PP

P ∈H0

1
sup Et ≥
α
t≥0

!

≤ α.

This is Ville’s inequality and is central to e-process methodology [19]. The certificate proves a statement
about the protocol’s false-certification frequency under A, even under optional stopping. It does not
prove an assumption-free proposition about nature.

14

Stochastic Witness Calculus

Physical analogue of proof strength.

Kenju Tomita
The strongest honest physical endpoint is therefore:

formal protocol validity + auditable assumptions + bounded risk + independent replication.
This is not logically identical to a mathematical theorem, but it is a rigorous, machine-checkable empirical
guarantee.

8

Experiments

All experiments use fixed seeds and are included in the accompanying source archive. Exact mathematical
experiments recompute accepted mass from integer weights or certified recurrences; sampling is used
only to train proposals or illustrate what sampling cannot prove. We organize the evaluation around six
questions:
1. Can an untrusted learned generator increase exact witness mass while a baseline mixture preserves
support?
2. Can a non-enumerative checker certify mass over exponentially large witness spaces?
3. Do explicit stress tests catch average-to-pointwise and zero-hit-to-zero-mass errors?
4. Can the interface audit a model-led investigation of an open mathematical problem without promoting
finite evidence to a theorem?
5. Does the empirical mode preserve its declared risk under optional stopping?
6. Can a small proof-carrying checker accept exact certificates while rejecting semantic tampering and
floating-point-only claims?

8.1

Experiment 1: learned witness distributions for SAT

Setup. We generated 60 planted 3-CNF instances with 16 variables and 112 clauses, plus 20 deliberately
unsatisfiable controls formed by adding contradictory unit clauses. The witness space contains all
216 = 65,536 assignments. A deterministic verifier evaluates every clause.
The baseline generator is uniform. A cross-entropy method trains an independent Bernoulli proposal
from clause-satisfaction scores. Final probabilities are quantized to multiples of 1/256, allowing exact
accepted mass to be computed as an integer numerator over the common denominator 25616 . To protect
support, we also evaluate
µmix = 0.1µuniform + 0.9µlearned .
Results. All 60 planted instances had exactly certified positive mass; all 20 controls had exactly
zero accepted mass under exhaustive enumeration. The median uniform witness mass was 1/65,536 ≈
1.526×10−5 . The learned proposal’s median exact mass was 0.9393, and the support-preserving mixture’s
median was 0.8454. Relative to uniform, the mixture produced a median mass increase of 27,809.8× and
a geometric-mean increase of 4,346.3×. Its worst-case ratio was exactly 0.1, matching Theorem 3.11.
To test literal support collapse, we also hardened each learned product proposal to a point mass at its
coordinate-wise mode. The resulting deterministic proposal landed on a satisfying assignment for 50 of
the 60 satisfiable instances and assigned exactly zero accepted mass on the remaining 10. Mixing this
hard proposal with 10% uniform mass restored certified positive mass on all 60 instances; the minimum
restored mass was 1.5259 × 10−6 . The soft learned proposal itself retained formal full support because
15

Stochastic Witness Calculus

Empirical cumulative fraction

1.0

Kenju Tomita

median = 27809.8x

0.8

0.6

0.4

0.2

0.0
10−1

101
104
100
102
103
Exact mass speedup of support-preserving learned generator

105

Figure 2: Exact accepted-mass speedup for the support-preserving learned SAT generator. Learning
often concentrates almost all mass on satisfying assignments, while the 10% uniform component enforces
a certified floor.
its rational Bernoulli parameters were clipped away from zero and one, but it performed worse than
uniform on 10 instances. The ablation therefore separates concentration from support: optimization can
improve typical extraction while a theorem-level baseline component protects rare witnesses against
model hardening or truncation.
This experiment does not show that learning makes proof easier in every case. It shows that an untrusted
optimizer can greatly improve extraction while a simple mixture theorem preserves the logical route.

8.2

Experiment 2: a non-enumerative dynamic-programming certificate

Witness problem. For the path graph Pn , a bit vector encodes an independent set. We accept
exactly those vectors with k = ⌊n/4⌋ selected vertices and no adjacent selected pair. The witness space
has size 2n , while the number of accepted witnesses is
n−k+1
.
k
!

Under a product Bernoulli generator with integer one-weight w and common denominator Q, every
accepted string has weight wk (Q − w)n−k /Qn .
Proof-carrying recurrence.

The checker recomputes exact integer numerators using

Ai,j,0 = (Ai−1,j,0 + Ai−1,j,1 )(Q − w),

16

Ai,j,1 = Ai−1,j−1,0 w,

Stochastic Witness Calculus

Kenju Tomita

0

Uniform generator
Biased product generator
5% uniform + 95% biased

log10 exact accepted mass

−25
−50
−75
−100
−125
−150
−175
−200
0

250

500
750
1000
1250
1500
Path size n (witness space size = 2^n)

1750

2000

Figure 3: Exact accepted mass for path independent-set witnesses. The checker handles witness spaces
of size 2n without enumeration; the support-preserving proposal changes extraction scale while exact
recurrence checking remains unchanged.
with A0,0,0 = 1. The final numerator is An,k,0 + An,k,1 . This dynamic program requires O(nk) exact
updates rather than enumerating 2n vectors. We independently cross-check it against the closed form
for every tested size.
Results. For n = 16, 32, . . . , 2048, every recurrence/closed-form comparison matched exactly. At
n = 2048 the witness space contains 22048 strings, the common denominator has 4,933 decimal digits, and
the checker completed in 1.04 seconds for uniform weights and 1.10 seconds for a product proposal with
P(Xi = 1) = 1/4. The uniform accepted mass was approximately 10−193.40 , while the biased proposal
achieved 10−77.05 . A trajectory-level mixture with 5% uniform mass preserved a certified baseline floor
and yielded a mass ratio of 2.12 × 10116 relative to uniform.

17

Stochastic Witness Calculus

Exact checker runtime (seconds)

100

Kenju Tomita

Uniform weights
Biased weights

10−1

10−2

10−3

10−4

10−5

102

103
Path size n

Figure 4: Runtime of the exact dynamic-programming checker. This is a structured benchmark rather
than a general #SAT solver, but it demonstrates that mass certificates need not enumerate the witness
space.

8.3

Experiment 3: adversarial quantifier auditing

This experiment targets two invalid inferences that repeatedly appear in open-problem reasoning.
Hidden exceptional instance. Consider a finite family of N instances in which every instance except
one has positive witness mass. A random benchmark drawing k instances with replacement misses the
unique zero-mass exception with exact probability
1
1−
N



k

.

For N = 106 , k = 104 random checks miss the exception with probability 0.99005; even k = 105 checks
miss it with probability 0.90484. Seeded simulations with 20,000 repetitions per cell agreed with the
exact curves to maximum absolute error 0.0085.
Zero observed hits. If a witness generator has true positive mass δ > 0, the probability of observing
no accepted witness in k independent samples is (1 − δ)k . For δ = 10−6 and k = 105 , zero hits occur with
probability 0.90484; for δ = 10−8 and k = 106 , the probability is 0.99005. Thus finite failure-to-sample
cannot establish zero mass.
A finite pointwise checker catches the planted exception exactly, but this is only a toy illustration. For
infinite families, the required object is a uniform symbolic family certificate, a cover, or a well-founded
reduction—not an arbitrarily large benchmark.

18

Stochastic Witness Calculus

Kenju Tomita

Probability of missing the unique exception

1.0

0.8

0.6

0.4
N=1,000
N=10,000
N=100,000
N=1,000,000

0.2

0.0

101

104
102
103
Randomly benchmarked instances (with replacement)

105

Probability of observing zero accepted witnesses

Figure 5: A high benchmark success rate cannot certify a universal theorem. When one exceptional
instance is hidden among N , random testing can miss it with high probability even for large test budgets.

100

10−1

10−2
delta=1e-08
delta=1e-06
delta=0.0001
delta=0.01

10−3

10−4

10−5

10−6

102

103

104
105
106
Independent samples

107

108

Figure 6: Zero sampled witnesses is compatible with strictly positive mass. Exact or symbolic lower
bounds are required to distinguish an empty accepted set from a rare one.
19

Stochastic Witness Calculus

8.4

Kenju Tomita

Experiment 4: finite Erdős–Straus certificates

The Erdős–Straus conjecture asks whether
1 1 1
4
= + +
n
x y z
has positive integer solutions for every n ≥ 2. It remains open [6, 9]. For primes p ≡ 1 (mod 4), the
anchor-shift framework sets
p+c
ac =
,
c ≡ 3 (mod 4),
4
and the exact fixed-shift divisor criterion accepts when some d | a2c satisfies
d ≡ −ac

(mod c)

or

4d ≡ −1

(mod c).

An accepted pair reconstructs explicit denominators and is checked by integer cross multiplication. A
self-contained derivation of the criterion and of the bound c ≤ 2p appears in Section A.
Distribution. For each prime p ≡ 1 (mod 24) below 107 , we use the 32 shifts
c ∈ {3, 7, 11, . . . , 127}.
The uniform generator chooses a shift uniformly and then a divisor of a2c uniformly. We also test a
support-preserving small-shift prior with integer shift weight ⌊128/c⌋.
Results. There are 82,887 tested primes. Exact enumeration found positive witness mass for every
one, and the first reconstructed identity for every prime passed exact verification. The largest least
successful shift was c = 107, attained at p = 8,803,369. The median uniform accepted mass was 0.048398
(about 20.66 expected independent draws); the small-shift prior increased the median to 0.176253 (about
5.67 expected draws). The minimum uniform mass was 1/3600 at the same hardest prime.
This experiment is an exact proof for the stated finite range and witness space. It is not evidence that
the same 32 shifts suffice universally, and it is not a proof of the conjecture. Salez verified the conjecture
through 1017 , later work reports 1018 , and Dahan proves strong depth-dependent exceptional-set bounds
while explicitly leaving the universal conjecture open [6, 14, 20].

20

Kenju Tomita

40000

30000

20000

10000

7
10

59

55

51

47

43

39

35

31

27

23

19

15

11

7

0

3

Number of primes p ≡ 1 (mod 24), p < 10^7

Stochastic Witness Calculus

Least successful shift c

Figure 7: Least successful shift for all primes p ≡ 1 (mod 24) below 107 . The isolated c = 107 case is
visible at the extreme right.

Uniform over shifts
Small-shift prior

Exact accepted mass

10−1

10−2

10−3

10−4
0.0

0.2

0.4
0.6
Quantile over tested primes

0.8

1.0

Figure 8: Exact finite accepted-mass distributions. A small-shift prior improves typical extraction but
slightly reduces mass on the rare hardest cases; full support preserves positivity.
21

Stochastic Witness Calculus

8.5

Kenju Tomita

Arbiter v23 contribution to the case study

Arbiter v23 is an internal looped 27B-parameter reasoning model used in the preceding project that
motivated this paper. According to the audited project logs, Arbiter:
• derived the bounded multiplicative-box reformulation of the anchor shift;
• tightened a provisional shift bound to c ≤ 2p using the least denominator;
• generated 122 machine-verified residue families during abductive search;
• produced proof drafts for two central structural theorems;
• proposed many false families that exact tools rejected before inclusion.
The current artifact independently reimplements the finite divisor criterion and the p < 107 survey, but
it does not reproduce all 122 family-generation runs. Arbiter is treated as a discovery system, not as an
author or trusted verifier. Its relevance to SWC is architectural: it proposes witness distributions and
structural hypotheses, while exact tools determine what survives.

8.6

Experiment 5: optional stopping in empirical mode

Setup. We simulated 50,000 Bernoulli paths of length 500 under the simple null p0 = 0.5 and 50,000
under p1 = 0.6. We compare:
1. a one-sided nominal 5% z-test repeated at every time t ≥ 20 without multiplicity correction;
2. the likelihood-ratio e-process
Et =



0.6
0.5

St 

0.4
0.5

t−St

,

stopped when Et ≥ 1/0.05 = 20.
Under the simple null, (Et ) is a nonnegative martingale of mean one, so its crossing probability is at
most 0.05.
Results. The repeated nominal test crossed on 30.826% of null paths (Wilson 95% half-width 0.405
percentage points), whereas the e-process crossed on 4.342% (half-width 0.179 points). At p = 0.6,
the corresponding detection probabilities by time 500 were 99.946% and 97.738%; median stopping
times conditional on crossing were 41 and 115 observations. Thus the anytime-valid method pays some
detection delay but maintains its risk interpretation under continuous monitoring.

22

Cumulative false-certification rate under null

Stochastic Witness Calculus

Kenju Tomita

0.30
0.25
0.20
Repeated nominal 5% z-test
E-process threshold 1/alpha
Nominal alpha = 0.05

0.15
0.10
0.05
0.00
0

100

200
300
Monitoring time

400

500

Cumulative detection probability at p=0.60

Figure 9: Optional-stopping behavior under the null. Repeated nominal testing accumulates false
certifications; the e-process remains below the 5% time-uniform bound in the simulation.

1.0

0.8

0.6

0.4

0.2
Repeated nominal z-test
E-process

0.0
0

100

200
300
Monitoring time

400

500

Figure 10: Detection probability under the alternative p = 0.6. The anytime-valid e-process is slower
than repeated nominal testing but retains a valid interpretation under optional stopping.
23

Stochastic Witness Calculus

8.7

Kenju Tomita

Experiment 6: proof-carrying certificate integrity

Setup. We implemented a portable JSON certificate for the path-graph mass problem in Experiment
2. Each certificate binds the semantic claim (n, k, w, Q) to a canonical SHA-256 digest and carries the
claimed exact accepted numerator, common denominator, reduced fraction, backend identifier, and
positivity flag. The artifact includes a machine-readable schema and a complete example certificate. An
independent checker validates the schema, recomputes the digest, reruns the exact O(nk) recurrence,
verifies normalization and fraction reduction, and refuses floating-point-only positivity.
We generated 300 valid certificates over path sizes 16 ≤ n ≤ 256. For each certificate, an untrusted
mutation harness produced six altered variants: an incremented accepted numerator, an incremented
denominator, a changed target size, a changed distribution weight, an unsupported schema version, and
a pseudo-certificate containing only a decimal mass estimate.
Results. The checker accepted all 300 valid certificates and rejected all 1,800 altered variants. Median
checking time for valid certificates was 0.433 ms, and the 99th percentile across all checked objects was
4.06 ms on the reference machine. The experiment is not a cryptographic security proof and SHA-256
does not authenticate an author; it tests a narrower systems claim: semantic fields, exact arithmetic,
and proof status are bound tightly enough that the specified corruptions cannot silently cross the kernel
boundary.
Table 1: Proof-carrying integrity stress test.
Quantity
Valid exact certificates
Tampered or float-only variants
Mutation classes per certificate
Median valid-certificate check
99th percentile over all objects
Exact arithmetic

9

Result
300 / 300 accepted
1,800 / 1,800 rejected
6
0.433 ms
4.06 ms
Python integers and rational reduction

What the Experiments Establish

The experiments test different layers of the methodology rather than one aggregate claim. The SAT
study shows that an untrusted learned proposal can increase exact witness mass by orders of magnitude
while a theorem-level mixture floor protects support; the hard-mode ablation makes the protection
concrete by turning 10 satisfiable instances from zero learned support back into positive certified
mass. The path-graph study shows that exact mass certificates can be checked over exponentially
large witness spaces using structure rather than enumeration. The quantifier audit demonstrates, with
exact probabilities, why benchmark coverage and zero observed hits cannot substitute for pointwise
mass proofs. The Erdős–Straus study shows how an open-problem investigation can produce exact
finite certificates while the framework refuses a universal promotion. The sequential study validates
the separate empirical endpoint: a theorem about time-uniform risk, not certainty about nature. The
proof-carrying integrity study shows that the proposed trust boundary can be instantiated as a small
recomputing checker that rejects altered semantics, altered mass claims, unsupported schemas, and
floating-point-only evidence.
No experiment proves that short mass certificates exist for arbitrary theorems. Exact model counting
is hard in general, learned generators can collapse, structured recurrences may be unavailable, open
24

Stochastic Witness Calculus

Kenju Tomita

problems may resist all known lower bounds, and empirical guarantees remain model-conditional. The
experiments are therefore reference implementations and falsification tests for the interface, not evidence
that SWC automatically resolves hard conjectures. The integrity experiment covers a declared mutation
suite, not arbitrary implementation bugs, side channels, collision attacks, or compiler compromise.

10

Discussion

10.1

Positioning and novelty boundary

The nearest ingredients of SWC already exist separately. The classical probabilistic method supplies the
logical implication from positive probability to existence; probabilistic program logics verify distributional
computations; model counters compute accepted weight; proof-carrying systems separate untrusted
production from trusted checking; and e-processes provide anytime-valid empirical risk control. The
paper’s claim is that these pieces can be organized into one theorem-facing certificate interface with
explicit pointwise quantifiers and proof-status boundaries.
Table 2: Relationship to adjacent paradigms. The final column states the interface layer proposed here,
not a claim that the preceding field lacks formal rigor.
Paradigm

Native strength

Layer emphasized by SWC

Probabilistic method

Proves existence from a
positive-probability construction

Probabilistic program
verification
Weighted model
counting

Proves quantitative properties of
randomized programs
Computes or certifies accepted
weight for Boolean constraints

Proof-carrying code

Untrusted producer emits a small
independently checked object
Generates candidate proofs or
witnesses checked by a formal
environment
Controls false certification under
adaptive monitoring

Instance-indexed machine certificate, explicit
mass object, and compiler to verifier-backed
existence
Treats program output as a theorem-witness
distribution with a deterministic target relation
Connects the count to verifier soundness,
universal quantifier scope, and certificate
composition
Specializes the object to distributions, mass
lower bounds, positivity, and theorem extraction
Allows the learned object to be a distribution or
structural mass argument while keeping it
outside the kernel
Places empirical guarantees in a separate
assumption-indexed mode rather than calling
them mathematical truth

AI theorem search
Anytime-valid
inference

Accordingly, the novelty claim is deliberately architectural and methodological. We do not claim a
new axiom, a new proof of the probabilistic method, or a general complexity reduction. We propose
a typed certificate calculus, a trusted-boundary specification, a status lattice, adversarial quantifier
checks, proof-carrying mass back ends, and an evaluation protocol for learned proof search. Whether
this synthesis proves useful at scale is an empirical research question, not a consequence of the soundness
theorem alone.

10.2

Why positive mass is a useful target

Proof search normally asks for one valid path through an enormous discrete space. A mass certificate
asks a different question: can a tractable region of the distribution be shown to intersect the accepted

25

Stochastic Witness Calculus

Kenju Tomita

set? This can expose tools unavailable to direct search, including expectation arguments, symmetry,
couplings, local lemmas, inclusion–exclusion, algebraic counting, and concentration.
Even a tiny lower bound proves existence. Computational usefulness, however, depends on its scale. SWC
therefore separates the Boolean field proves_existence from the quantitative field expected_trials.

10.3

Why learned mass must not be trusted directly

Monte Carlo success rates are not mass proofs. A model may overfit tested instances or assign zero
mass to an exceptional class. The trusted object must be a symbolic or exact lower bound. Learning is
most naturally used to suggest decompositions, symmetries, partitions, change-of-measure arguments,
and candidate inequalities that a proof kernel can check.

10.4

Relation to derandomization

A positive-mass proof establishes existence without necessarily constructing a witness efficiently. Conditional expectations, pseudorandomness, and algorithmic local lemmas may extract deterministic
constructions. Formal work on pseudorandomness and randomized algorithms provides a natural implementation substrate [12]. SWC records derandomization as an optional compiler stage rather than a
prerequisite for theoremhood.

10.5

Mathematical and physical reality

In mathematical mode, an accepted certificate is an ordinary proof relative to its axioms. In empirical
mode, the strongest defensible statement is conditional:
under assumptions A,

P(false certification) ≤ α.

The distinction is not a weakness of SWC; it is a boundary between deductive and empirical knowledge
that the framework is designed to expose.

10.6

When a stochastic certificate is scientifically useful

A mass certificate is most valuable when at least one of the following holds: the accepted set has
exploitable symmetry; a second-moment or local-lemma argument is easier than explicit construction;
a knowledge compiler produces a compact counting graph; a learned generator exposes a tractable
high-mass region; or a reduction decomposes a universal theorem into families with separate certificates.
It is least useful when positivity is exactly as hard as the original satisfiability problem and no concise
lower-bound proof exists.

10.7

Evaluation criteria for future systems

We recommend reporting six quantities separately: verifier soundness status, mass-certificate status level
H0–H4, minimum pointwise mass over the audited family, expected extraction cost, certificate-checking
cost, and coverage of the intended instance domain. Average mass or benchmark solve rate should never
replace the minimum/coverage fields for a universal claim.

26

Stochastic Witness Calculus

11

Kenju Tomita

Limitations and Threats to Validity

1. Classical logical core. Positive probability implying existence is not new. The contribution is
the certificate interface, compositional rules, quantifier discipline, AI integration, and reference
implementation.
2. No proof-assistant implementation yet. The trusted kernel is Python/C++ with exact
arithmetic, not a fully formal Lean, Isabelle, or Coq development. The paper proves the rules on
paper; machine-checked metatheory remains future work.
3. Worst-case hardness remains. By Theorem 4.2, deciding positive mass under a full-support
Boolean generator is SAT, and exact mass is #P-hard. SWC reorganizes proof obligations but does
not remove complexity barriers.
4. Structured scalability only. The new dynamic-programming benchmark scales because the
witness constraint has bounded local structure. It is not representative of arbitrary industrial #SAT.
5. Synthetic SAT distribution. Planted formulas and contradictory controls are suitable for testing
semantics and support collapse, not for claiming state-of-the-art SAT performance.
6. Quantifier audit is deliberately adversarial and simple. Its value is logical calibration, not
algorithmic novelty.
7. Finite number-theory evidence. The Erdős–Straus survey certifies only the stated range and
shifts. It cannot justify a universal extrapolation.
8. Simple sequential null. The e-process experiment uses a simple Bernoulli null and fixed alternative.
Composite nulls, nuisance parameters, dependence, and distribution shift need richer constructions.
9. Certificate provenance. Arbiter’s historical contributions are based on internal audited logs;
independent reproduction of the complete 122-family search requires public release of those prompts,
hashes, and certificates.
10. Scope of empirical mode. A formal risk theorem is only as relevant as its declared physical
assumptions. Instrument failure, unmodeled confounding, and adversarial data corruption remain
external threats unless explicitly modeled.

12

Research Agenda

Machine-checked metatheory. Formalize the certificate judgment, derivation rules, and finite-weight
kernel in Lean 4 or Isabelle/HOL. The first milestone is a proof-producing checker whose trusted result
is an ordinary existential theorem.
Certified knowledge-compilation backend. Integrate CPOG-style proof-producing weighted model
counting [4]. This would replace exhaustive SAT enumeration with independently checked compiled
circuits on realistic formulas.
Moment and local-lemma compilers. Build tactic support that converts first/second-moment
calculations, dependency graphs, and local-lemma inequalities into accepted-mass lower bounds. This
targets the classical probabilistic method more directly than raw counting.

27

Stochastic Witness Calculus

Kenju Tomita

Distribution synthesis. Train theorem-proving agents to maximize certified rather than empirical
witness mass. Candidate objectives should reward symbolic density-ratio bounds, decomposable support,
and short mass proofs, not just sampled success.
Adversarial quantifier auditing. Automate checks for average-to-pointwise promotion, hidden
independence, measure-zero exceptions, unproved normalization, and finite-search extrapolation. The
stress-test suite should include adversarially hidden exceptional classes.
Continuous certificates. Implement rational interval and compactness certificates for nested approximate witnesses, including exact proof objects for closure, nesting, and diameter convergence.
Empirical certificate standard. Combine protocol hashes, immutable raw data, instrument metadata, e-processes, confidence sequences, sensitivity analysis, and replication records into portable
assumption-indexed artifacts.
Open-mathematics benchmarks. Use problems with exact finite verifiers but unknown universal
theorems. Score systems on new witnesses, certified mass lower bounds, obstruction discovery, certificate
size, pointwise coverage, and honest localization of the remaining quantifier.

13

Conclusion

Stochastic reasoning does not need to weaken proof. If a sound verifier accepts a set of candidates with
formally certified positive probability, then the accepted set is nonempty and the resulting mathematical
conclusion is deterministic. SWC makes that classical principle explicit as a certificate boundary suitable
for learned generators, exact auditors, and proof assistants.
The same language cannot make physical claims assumption-free. It can, however, produce machinecheckable statements about false-certification risk under explicit models and adaptive protocols. This
yields a unified architecture with two honest endpoints: ordinary theoremhood in mathematical mode,
and calibrated, auditable evidence in empirical mode.
The experiments show both promise and restraint. Learned distributions can increase exact witness
mass by orders of magnitude; exact finite certificates can audit a model-led investigation of an open
conjecture; and e-processes can preserve risk under optional stopping. At the same time, none of these
mechanisms licenses promotion of finite evidence or probabilistic intuition into an unproved universal
claim. That separation is the central design principle of Stochastic Witness Calculus.

Reproducibility Statement
The accompanying archive contains source code, fixed random seeds, raw CSV/JSON results, figures,
tests, and the LaTeX source. The reported exact counts and probability values were regenerated in a
clean rerun and matched the manuscript. Runtime measurements are environment-dependent and are
not expected to be byte-for-byte identical. The principal commands are:
python experiments/exp_sat.py
python experiments/exp_chain_wmc.py
python experiments/exp_quantifier_audit.py

28

Stochastic Witness Calculus

Kenju Tomita

python experiments/exp_certificate_integrity.py
g++ -O3 -std=c++17 experiments/exp_erdos.cpp -o experiments/exp_erdos
./experiments/exp_erdos 10000000 127 results/erdos_results.csv results/erdos_summary.json
python experiments/exp_eprocess.py
python experiments/make_figures.py
python -m unittest discover -s tests

The exact finite results can be regenerated without network access.

Acknowledgments and Contribution Disclosure
Arbiter v23, an internal looped 27B-parameter reasoning model, contributed hypotheses, reformulations,
and proof drafts to the Erdős–Straus case study. All mathematical claims retained from those runs were
subjected to deterministic symbolic or computational checks. Arbiter is not listed as an author and is
not part of the trusted verification base. GPT-5.6 Pro assisted with literature synthesis, code and figure
generation, and manuscript drafting. The human author directed the project, selected and audited the
retained claims, and is responsible for the manuscript.

References
[1]

Noga Alon and Joel H. Spencer. The Probabilistic Method. 4th ed. Wiley, 2016.

[2] Philippe Audebaud and Christine Paulin-Mohring. “Proofs of Randomized Algorithms in Coq”. In:
Mathematics of Program Construction. Vol. 4014. Lecture Notes in Computer Science. Springer,
2006, pp. 49–68. doi: 10.1007/11783596_6.
[3] Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. “Proving Uniformity and Independence by Self-Composition and Coupling”. In: arXiv preprint
arXiv:1701.06477 (2017).
[4] Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn J. H. Heule. “Certified Knowledge Compilation with Application to Formally Verified Model Counting”. In: arXiv preprint
arXiv:2501.12906 (2025).
[5] Florent Capelli. “Knowledge Compilation Languages as Proof Systems”. In: arXiv preprint
arXiv:1903.04039 (2019).
[6] Benjamin Dahan. “Sieve Dimension and Search Depth for the Erdős–Straus Conjecture, n ≡ 1
(mod 24)”. In: arXiv preprint arXiv:2608.24035 (2026).
[7] Manuel Eberl, Johannes Hölzl, and Tobias Nipkow. “A Verified Compiler for Probability Density
Functions”. In: arXiv preprint arXiv:1707.06901 (2017).
[8] Chelsea Edmonds and Lawrence C. Paulson. “Formal Probabilistic Methods for Combinatorial
Structures using the Lovász Local Lemma”. In: arXiv preprint arXiv:2310.00513 (2023).
[9] Christian Elsholtz and Terence Tao. “Counting the Number of Solutions to the Erdős–Straus
Equation on Unit Fractions”. In: Journal of the Australian Mathematical Society 94.1 (2013),
pp. 50–105. doi: 10.1017/S1446788712000468.
[10] Paul Erdős and László Lovász. “Problems and Results on 3-Chromatic Hypergraphs and Some
Related Questions”. In: Infinite and Finite Sets 10 (1975), pp. 609–627.

29

Stochastic Witness Calculus

Kenju Tomita

[11] Steven R. Howard, Aaditya Ramdas, Jon McAuliffe, and Jasjeet Sekhon. “Time-Uniform, Nonparametric, Nonasymptotic Confidence Sequences”. In: The Annals of Statistics 49.2 (2021),
pp. 1055–1080. doi: 10.1214/20-AOS1991.
[12] Emin Karayel. “Derandomization with Pseudorandomness”. In: arXiv preprint arXiv:2404.16614
(2024).
[13] Yiping Ma, Yu-Lin Tsai, Mayank Rathee, Deevashwer Rathee, François Dupressoir, Pierre-Yves
Strub, and Raluca Ada Popa. “ShannonProver: Towards Automating Formal Cryptographic
Proofs”. In: arXiv preprint arXiv:2607.02847 (2026).
[14] Spiridon Mihnea and Dumitru C. Bogdan. “Further Verification and Empirical Evidence for the
Erdős–Straus Conjecture”. In: arXiv preprint arXiv:2509.00128 (2025).
[15] Leonardo de Moura and Sebastian Ullrich. “The Lean 4 Theorem Prover and Programming
Language”. In: Automated Deduction – CADE 28. Vol. 12699. Lecture Notes in Computer Science.
Springer, 2021, pp. 625–635. doi: 10.1007/978-3-030-79876-5_37.
[16] George C. Necula. “Proof-Carrying Code”. In: Proceedings of the 24th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages. 1997, pp. 106–119. doi: 10.1145/263699.
263712.
[17] Morenikeji Neri, Paulo Oliva, and Nicholas Pischke. “A Systematic Way of Analysing Proofs in
Probability Theory”. In: arXiv preprint arXiv:2604.08078 (2026).
[18] Orr Paradise, Oliver Richardson, Yoshua Bengio, and Shafi Goldwasser. “How to Verify Consistency
of Probabilistic Claims”. In: arXiv preprint arXiv:2608.11181 (2026).
[19] Aaditya Ramdas, Peter Grünwald, Vladimir Vovk, and Glenn Shafer. “Game-Theoretic Statistics
and Safe Anytime-Valid Inference”. In: Statistical Science 38.4 (2023), pp. 576–601. doi: 10.1214/
23-STS894.
[20] Serge E. Salez. “The Erdős–Straus Conjecture: New Modular Equations and Checking up to
N = 1017 ”. In: arXiv preprint arXiv:1406.6307 (2014).
[21] Philipp Schröer et al. “A Deductive Verifier for Probabilistic Programs – Caesar”. In: arXiv
preprint arXiv:2605.15827 (2026).
[22] Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel. “Formally
Certified Approximate Model Counting”. In: arXiv preprint arXiv:2406.11414 (2024).
[23] The mathlib Community. “The Lean Mathematical Library”. In: Proceedings of the 9th ACM
SIGPLAN International Conference on Certified Programs and Proofs. 2020, pp. 367–381. doi:
10.1145/3372885.3373824.
[24] Jean-Baptiste Tristan et al. “Verification of Machine Learning Systems via Reparameterization”.
In: arXiv preprint arXiv:2007.06776 (2020).
[25] Leslie G. Valiant. “The Complexity of Enumeration and Reliability Problems”. In: SIAM Journal
on Computing 8.3 (1979), pp. 410–421. doi: 10.1137/0208032.

A

Erdős–Straus Criterion Used in the Case Study

This appendix makes the number-theory verifier in Experiment 4 self-contained. It does not prove the
universal conjecture; it proves that every accepted finite certificate reconstructs a valid solution and
that every prime solution can be represented by some admissible shift.

30

Stochastic Witness Calculus

Kenju Tomita

Theorem A.1 (Anchor-shift and two-target divisor equivalence). Let p ≡ 1 (mod 4) be prime. Then
4/p has a representation by three positive unit fractions if and only if there is an integer
c≡3

(mod 4),

0 < c ≤ 2p,

for which, with a = (p + c)/4, some divisor d | a2 satisfies
d ≡ −a (mod c)

4d ≡ −1

or

(mod c).

Each accepted pair (c, d) yields explicit positive denominators.
Proof. Suppose first that

4
1 1 1
= + + ,
p
x y z

x ≤ y ≤ z.

Because the other two terms are positive, x > p/4. Also 4/p ≤ 3/x, so x ≤ 3p/4. Set
c = 4x − p,

a = x,

M = ap.

Then c ≡ 3 (mod 4) and 0 < c ≤ 2p, while
c
1 1
= + .
M
y z
Multiplication and completion of the rectangle give
(cy − M )(cz − M ) = M 2 .
Both factors are positive because each of 1/y and 1/z is smaller than their sum c/M . Thus, with
e = cy − M,

e′ = cz − M,

c | M + e,

c | M + e′ .

we have ee′ = M 2 and

Conversely, any positive divisor pair ee′ = M 2 satisfying these congruences defines
x = a,

y=

M +e
,
c

z=

M + e′
,
c

and direct substitution gives 1/x + 1/y + 1/z = 4/p.
It remains to collapse the divisors of M 2 = a2 p2 . Since c is odd and 4a = p + c, we have
gcd(a, c) = gcd(p, c) = 1,
so gcd(M, c) = 1. Hence one congruence e ≡ −M (mod c) automatically implies the complementary
one: from ee′ = M 2 ,
(−M )e′ ≡ M 2

(mod c)

=⇒

e′ ≡ −M

(mod c).

Every divisor e | M 2 is uniquely e = pj d with j ∈ {0, 1, 2} and d | a2 . Since p ≡ 4a (mod c):
• if j = 1, then e ≡ −M is equivalent to d ≡ −a (mod c);
• if j = 2, it is equivalent to 4d ≡ −1 (mod c);
31

Stochastic Witness Calculus

Kenju Tomita

• if j = 0, then d ≡ −4a2 (mod c); replacing d by the complementary divisor a2 /d gives the preceding
4d ≡ −1 target.
The reverse constructions choose e = pd in the first branch and e = p2 d in the second branch. The
displayed formulas for x, y, z then give positive integers and the exact identity. This proves both
directions.
The experiment enumerates the stated finite shift set and all divisors of a2 . Its C++ verifier reconstructs
e, e′ = M 2 /e, and (x, y, z), then checks the integer identity
4xyz = p(xy + xz + yz)
using 128-bit integer arithmetic.

B

Exact Finite Certificate Schema

A portable certificate may contain:
claim_id
instance_encoding
witness_space_encoding
generator_family
exact_weight_representation
deterministic_verifier
verifier_soundness_reference
accepted_mass_numerator
accepted_mass_denominator
positivity_proof
assumptions
software_and_formalization_hashes

For non-enumerative certificates, the accepted-mass fields may be replaced by a theorem reference and
proof term establishing the lower bound.

32

Stochastic Witness Calculus

C

Kenju Tomita

Additional Experimental Results

Table 3: SAT exact-mass results. “Speedup” denotes accepted-mass ratio, not wall-clock runtime.
Quantity

Value

Satisfiable instances
Unsatisfiable controls
Variables / clauses
Median uniform mass
Median learned mass
Median 10% support-mixture mass
Median support-mixture mass ratio
Geometric-mean mass ratio
Worst support-mixture ratio
Hardened modes satisfying
Hardened modes with zero witness mass
Hard-mode mixtures with positive mass
Minimum hard-mode mixture mass

60
20
16 / 112
1.5259 × 10−5
0.9393
0.8454
27,809.8×
4,346.3×
0.1×
50/60
10/60
60/60
1.5259 × 10−6

Table 4: Erdős–Straus finite certificate results.
Quantity
Value
Prime range
Number of primes
Shifts
Certified positive
Exact first-witness checks passed
Maximum least shift
Median uniform accepted mass
Median small-shift-prior mass
Minimum uniform accepted mass

p < 107 , p ≡ 1 (mod 24)
82,887
3, 7, . . . , 127 (32 total)
82,887
82,887
107 at p = 8,803,369
0.048398
0.176253
1/3600

Table 5: Sequential monitoring simulation, 50,000 paths per condition.
Method

Null crossing

Power at p = 0.6

30.826%
4.342%

99.946%
97.738%

Repeated nominal 5% z-test
Likelihood-ratio e-process

33

Stochastic Witness Calculus

Kenju Tomita

Table 6: Non-enumerative path-graph mass certificate.
Quantity

Value

Largest path
Witness-space size
DP / closed-form cross-checks
Uniform exact mass
Biased proposal exact mass
5% support-mixture mass ratio
Uniform / biased checker runtime

n = 2048, k = 512
22048
all passed
10−193.396
10−77.047
2.12 × 10116
1.04 s / 1.10 s

Table 7: Quantifier-audit examples.
Scenario

Test budget

Probability of misleading observation

One exception among 106 instances
One exception among 106 instances
True mass 10−6
True mass 10−8

104 draws
105 draws
105 samples
106 samples

0.99005 miss
0.90484 miss
0.90484 zero hits
0.99005 zero hits

Table 8: Proof-carrying certificate integrity results.
Quantity

Value

Valid certificates accepted
Altered certificates rejected
Mass-field mutations
Semantic claim mutations
Schema and float-only mutations
Median valid-certificate check
99th percentile over all objects

34

300 / 300
1,800 / 1,800
600 / 600 rejected
600 / 600 rejected
600 / 600 rejected
0.433 ms
4.06 ms

