Public reconstructed preprintVersion 4.1 · not peer-reviewed39 pages · September 4, 2026

Original research · formal verification · automated reasoning

Stochastic Witness CalculusExact Measure Certificates for Mathematical Existence, Learned Proof Search, and Anytime-Valid Empirical Claims

Probability is used to certify that a valid witness set is nonempty—not to weaken mathematical truth.

Kenju TomitaRochester Institute of Technology · Ephemerent Research

Read v4.1 PDF Read the intuitive explainer

Publication boundary. This page is a public reconstructed preprint and accessible HTML reading edition. Version 4.1 was built before the original source arrived; the v3 LaTeX source and reproducibility artifact have now been received and are under audit. Six files were regenerated without matching updates to the included manifest, so a source-complete v4.1 rebuild and reconciled checksums remain required. This is not the accepted Ephemerent Research journal version.

Proof-status clarification · September 4, 2026. SWC’s exact mathematical mode is a genuine proof system, not statistical confidence. The Erdős–Straus computation is likewise a genuine theorem over its declared finite domain. What remains open is the additional universal-lifting premise needed to cover every integer.

Abstract

The claim in one page.

Probability can establish deterministic existence, but automated reasoning systems often treat randomized search, formal proof, model counting, and empirical confidence as unrelated objects. Stochastic Witness Calculus (SWC) proposes 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 certifies nonemptiness rather than weakening truth. The framework supplies instance-indexed semantics, compositional certificate rules, support-preserving mixtures, exact finite backends, a dual obstruction rule, a compactness extension for continuous spaces, and a separate empirical mode for anytime-valid claims.

Six evaluation settings

Learned SAT proposals, non-enumerative path counting, adversarial quantifier auditing, finite Erdős–Straus certificates, proof-carrying integrity tests, and optional-stopping simulations.

SWC exact modeGenuine deterministic proof

Certified positive witness mass plus verifier soundness proves existence with mathematical certainty.

Erdős–Straus surveyGenuine finite-domain theorem

All 82,887 declared primes are exactly verified—not estimated or merely sampled.

Universal conjectureExact lifting premise still required

The current finite family does not yet quantify over every integer n≥2.

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

Introduction

Three uses of probability that must not be conflated.

Exact mathematical modeProbability inside a proof
A checked positive-mass argument establishes a deterministic existential statement.
Search modeRandomized witness discovery
A generator samples candidates. Success is useful, but sampled success alone is not a theorem.
Empirical modeEvidence about physical reality
Claims remain conditional on a data-generating model, protocol, and declared error budget.

SWC is a common interface that keeps these statuses separate. In exact mode, an accepted certificate compiles into an ordinary verifier-backed existence proof. In empirical mode, it yields a theorem about protocol risk under declared assumptions—not assumption-free certainty about nature.

Exact mathematical mode

The witness set must have certified positive mass.

For an instance i, let Ω_i be a witness space, μ_i a probability measure, and V_i a deterministic verifier. The accepted set is A_i = {w ∈ Ω_i : V_i(w) = 1}.

Pr_{w∼μ_i}[V_i(w)=1] ≥ δ_i > 0⟹∃w R(i,w)

Theorem 3.1 · Exact existence rulePositive accepted mass implies existence.

If the verifier is sound and the kernel checks μ_i(A_i) ≥ δ_i > 0, then A_i is nonempty and a valid witness exists.

Proof sketch

If A_i were empty, every probability measure would assign it mass zero, contradicting the certified positive lower bound. Verifier soundness converts accepted membership into the target relation.

Clarifying corollary · Full-support universal liftingAn exact probability-one certificate can prove every instance in a countable family.

Let I be countable and let ν be a distribution with full support, so ν(i)>0 for every i∈I. For each i, let μ_i be a witness distribution and V_i a sound verifier. If an exact certificate proves

Pr_{i∼ν,w∼μᵢ}[V_i(w)=1] = 1,

then every instance i has at least one valid witness.

Why this is a universal proof

If some instance i₀ had no valid witness, soundness would force V_i₀ to reject every candidate. Because ν(i₀)>0, that single failure class would contribute positive global failure mass, contradicting the exact probability-one certificate. The premise must be proved symbolically or exactly; an observed 100% sample rate cannot substitute for it.

Theorem V4.5 · Well-founded inductive witness liftingAn infinite instance family can close through exact descent.

Let (I,≺) be well-founded. Give every base instance an exact SWC certificate. For each nonbase instance i, require a checked reduction to finitely many dependencies j≺i and a witness-lifting map that converts their valid witnesses into one for i.

[∀j≺i, ∃w_j R(j,w_j)] ⟹ ∃w_i R(i,w_i)

Proof by well-founded induction

Assume all strictly smaller dependencies are certified. A base instance is settled directly. Otherwise the induction hypothesis supplies witnesses for every dependency and the checked lifting map constructs a witness for i. Therefore every instance in I has a valid witness.

Corollary V4.6 · Erdős–Straus divisor liftCertified factors prove their multiples.

If d divides n, write n=kd. From 4/d=1/x+1/y+1/z, multiplying each denominator by k gives 4/n=1/(kx)+1/(ky)+1/(kz). Strong induction therefore settles composites from certified prime factors.

Remaining induction obligation

The unresolved domain is the remaining prime class p≡1 (mod 24). To close it inductively, one must prove a strict descent from each such prime to lower-rank certified instances—or supply another well-founded rank and an exact witness-lifting map. Version 4.1 states this obligation; it does not assume it.

Verifier soundness

V_i(w)=1 must imply the claimed relation R(i,w).

Generator normalization

μ_i must be a genuine probability measure, not an unproved score.

Exact lower bound

The mass certificate is recomputed with exact integer, rational, symbolic, or formally checked arithmetic.

Pointwise scope

A universal theorem requires the certificate for every declared instance, not merely on average.

Composition

A small calculus for building certificates.

RuleWhat it preservesWhy it matters

Family and cover

Pointwise lower bounds across indexed cases or a verified cover.

Blocks benchmark averages from becoming universal claims.

Support-preserving mixture

μ = ε μ_base + (1−ε) μ_learned.

Lets learning concentrate search while a theorem-level baseline protects rare witnesses.

Change of measure

A certified density-ratio relation transfers mass lower bounds.

Separates optimization of search from the exact proof object.

Tagged disjunction

Certificate mass from verified alternative witness families.

Combines heterogeneous proof routes without conflating them.

Product and sequential rules

Independent or conditional certificate composition.

Supports modular witnesses assembled from checked stages.

Moment-based certificate

Exact moment inequalities establish nonzero success mass.

Connects classical probabilistic-method tools to the interface.

Dual obstruction

Certified zero mass under full support refutes existence.

Provides a symmetric machine-readable failure status.

Compactness extension

Nested approximate witnesses with closure and shrinking diameter.

Handles continuous spaces without pretending density at a point proves existence.

Trusted boundary

The generator remains outside the proof base.

Paper architecture diagram: an instance flows through a learned generator and deterministic verifier; a mass-bound prover and adversarial auditor feed the formal kernel, which yields an ordinary theorem. — **Figure 1 · Original manuscript figure.**The learned generator may propose. Soundness comes from the deterministic verifier and checked positive-mass certificate.

The framework rejects sampled estimates presented as exact mass, average-to-pointwise promotion, unproved independence, unproved normalization, probabilistic verifiers with nonzero false-acceptance risk in exact mode, and continuous-density arguments without a valid limiting theorem.

Untrustedlearned proposal→Checkedverifier + mass proof→Trusted outputproof status

Empirical reality mode

Anytime-valid evidence is still evidence.

Claims about physical systems depend on measurement, intervention, stationarity, confounding, and instrument integrity. No statistical method converts these assumptions into assumption-free certainty.

sup_P∈H₀ P(sup_t≥0 E_t ≥ 1/α)≤α

Theorem 7.1 · Anytime-valid certificationOptional stopping need not silently spend the risk budget.

Under a declared null model, a nonnegative e-process with initial expectation at most one controls the probability of ever crossing 1/α. The theorem concerns the protocol’s false-certification frequency under its assumptions.

Evaluation

Six settings, six different questions.

The evaluation is organized as reference implementations and falsification tests for the interface—not as one aggregate benchmark or a claim that SWC automatically solves hard conjectures.

Experiment 1

Can an untrusted learned generator increase exact witness mass?

Uniform median1 / 65,536

Learned median0.9393

10% support mixture0.8454

Median improvement27,809.8×

All 60 planted satisfiable instances received certified positive mass; all 20 contradictory controls received exactly zero. Hardening the proposal collapsed support on 10 satisfiable cases, while the uniform mixture restored positive mass on all 60.

Cumulative distribution of exact mass speedup for the support-preserving learned SAT generator, with median 27,809.8 times. — **Figure 2 · Exact accepted-mass speedup.**Learning concentrates mass; the uniform component enforces a certified floor.

Experiment 2

Can exact mass be certified without enumerating an exponential space?

A dynamic-programming backend checks independent-set witness mass on path graphs as large as n=2048, a witness space of size 2²⁰⁴⁸. It agrees exactly with an independent closed form and runs in 1.04 seconds for uniform weights and 1.10 seconds for a biased proposal on the declared machine.

Exact accepted mass across path sizes up to 2048 for uniform, biased, and support-preserving mixture proposals. — **Figure 3 · Structured exact mass.**Scalability comes from local graph structure; this is not evidence for arbitrary industrial model counting.

Experiment 3

Can explicit audits expose invalid quantifier moves?

Ten thousand random checks miss one exceptional instance among one million with probability 0.99005. One hundred thousand samples miss a true witness mass of 10⁻⁶ with probability 0.90484. A large finite benchmark and a zero-hit sample can both look reassuring while failing to establish the required universal or exact claim.

Two manuscript plots showing the probability of missing one exceptional instance and the probability of observing zero accepted witnesses at small true masses. — **Figures 5–6 · Adversarial quantifier audit.**Sampling failure cannot establish zero mass; benchmark coverage cannot certify every instance.

Experiment 4

Can an open-problem investigation produce a fully proved finite-domain theorem without overstating its quantifiers?

Declared prime family82,887

Exactly proved82,887 / 82,887

Shift rangec ≤ 127

Largest least shift107at p=8,803,369

The verifier proves the equation for every prime p ≡ 1 (mod 24) below 10⁷ in the declared finite family and reconstructs each witness with exact 128-bit integer checks. This is a genuine finite-domain theorem—not an estimate, confidence statement, or heuristic. Closing the universal Erdős–Straus conjecture additionally requires an exact certificate covering every integer n≥2.

Two manuscript plots showing least successful shifts for the finite prime survey and exact accepted mass under two shift distributions. — **Figures 7–8 · Exact finite-domain theorem.**A small-shift prior improves typical extraction while full support preserves positive mass on the rare hardest cases.

Experiment 5

Does an anytime-valid process retain its interpretation under repeated monitoring?

Naive null crossing30.826%

E-process null crossing4.342%

Naive power99.946%

E-process power97.738%

Across 50,000 null paths and 50,000 alternative paths with horizon 500, repeatedly checking a nominal 5% test spends far more than 5% false-certification probability. The likelihood-ratio e-process remains consistent with its anytime-valid guarantee, at a cost in stopping speed.

Two manuscript plots comparing false-certification under repeated nominal testing with an e-process, and detection probability under the alternative. — **Figures 9–10 · Optional stopping.**The e-process is slower under the alternative but retains a valid interpretation under adaptive monitoring.

Experiment 6

Will a small checker reject altered proof-carrying objects?

Valid certificates300 / 300 accepted

Altered variants1,800 / 1,800 rejected

Median valid check0.433 ms

99th percentile4.06 ms

The declared suite mutates mass fields, semantic claims, schemas, and floating-point-only evidence. Passing this suite demonstrates the intended trust boundary; it does not rule out arbitrary implementation, compiler, side-channel, or collision failures.

Limitations

What the paper does not establish.

The logical core is classical.Positive probability implying existence is not new; the contribution is the machine-facing certificate interface and status discipline.
No proof-assistant implementation yet.The current trusted kernel uses exact Python/C++ arithmetic rather than machine-checked Lean, Isabelle, or Coq metatheory.
Worst-case hardness remains.SAT and #P-hardness do not disappear because the proof obligations are reorganized.
Structured scalability only.The path benchmark benefits from bounded local structure and is not representative of arbitrary #SAT.
Synthetic SAT distribution.The experiment tests semantics and support collapse, not state-of-the-art solver performance.
Finite-domain theorem only.The Erdős–Straus computation is an exact proof for the declared range and shift family. A separate exact universal-lifting premise is needed for every n≥2.
Simple sequential model.Composite nulls, dependence, nuisance parameters, and distribution shift require richer empirical constructions.
Certificate provenance remains incomplete.Independent reproduction of Arbiter’s full historical search requires public prompts, hashes, and certificates.

Research agenda

From exact reference kernel to formal system.

Machine-checked metatheory

Formalize the judgment, derivation rules, and finite-weight kernel in Lean 4 or Isabelle/HOL.

Proof-producing model counting

Integrate certified knowledge-compilation backends for realistic weighted formulas.

Moment and local-lemma compilers

Translate classical probabilistic-method arguments into explicit accepted-mass certificates.

Certified distribution synthesis

Train agents to optimize symbolic mass bounds and decomposable support rather than sampled success alone.

Adversarial quantifier auditing

Automate checks for average-to-pointwise promotion, hidden independence, and finite-search extrapolation.

Continuous certificates

Build rational interval and compactness proof objects for nested approximate witnesses.

Reproducibility

The artifact is received. Reconciliation is in progress.

The supplied archive contains fixed seeds, raw CSV/JSON results, figures, tests, LaTeX source, a C++ finite verifier, and reproduction commands. The exact Erdős–Straus certificate columns reproduce across all 82,887 rows. Six included files do not match the older SHA-256 manifest, including the final PDF and regenerated result summaries; those entries must be reconciled before the artifact can become the immutable accepted-journal deposit.

Declared principal commands

python experiments/exp_sat.py
python experiments/exp_chain_wmc.py
python experiments/exp_quantifier_audit.py
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

Funding: No external funding.
Editorial relationship: Kenju Tomita operates Ephemerent Research and is the author and accountable publisher of this preprint.
AI contribution: Arbiter v23 contributed hypotheses, reformulations, and proof drafts to the Erdős–Straus case study but is not an author or part of the trusted verification base. GPT-5.6 Pro assisted literature synthesis, code and figure generation, and manuscript drafting. The human author directed and audited the work.
Licensing: Article, figures, and numerical data: CC BY 4.0. Original code: Apache-2.0 when deposited.

Appendices

The finite criterion and portable certificate.

Appendix A · Anchor-shift and two-target divisor equivalenceThe finite Erdős–Straus verifier reconstructs explicit denominators from an accepted divisor certificate.

For prime p ≡ 1 (mod 4), the manuscript proves an equivalence between a three-unit-fraction representation of 4/p and an admissible shift c ≡ 3 (mod 4), 0 < c ≤ 2p, with a divisor d of a² satisfying one of two modular targets, where a=(p+c)/4. Each accepted pair (c,d) yields positive integers x, y, and z, and the implementation verifies 4xyz = p(xy+xz+yz) with exact 128-bit arithmetic.

Scope of the appendix result

The theorem proves the correctness and completeness of the certificate representation, and the computation proves every instance in its declared finite family. Universal closure additionally requires proving that an admissible certificate exists for every remaining instance.

Appendix B · Portable exact finite certificate schema

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. Appendix C in the canonical PDF contains the complete numerical tables for all six experiments.

References

The intellectual neighborhood.

This reading edition retains the complete 25-item bibliography. Use the canonical PDF for final journal formatting, page ranges, and the paper’s numbered citation context.

Alon & Spencer. The Probabilistic Method. 4th ed., Wiley, 2016.
Audebaud & Paulin-Mohring. “Proofs of Randomized Algorithms in Coq,” 2006.
Barthe et al. “Proving Uniformity and Independence by Self-Composition and Coupling,” 2017.
Bryant, Nawrocki, Avigad & Heule. “Certified Knowledge Compilation with Application to Formally Verified Model Counting,” 2025.
Capelli. “Knowledge Compilation Languages as Proof Systems,” 2019.
Dahan. “Sieve Dimension and Search Depth for the Erdős–Straus Conjecture, n ≡ 1 (mod 24),” 2026.
Eberl, Hölzl & Nipkow. “A Verified Compiler for Probability Density Functions,” 2017.
Edmonds & Paulson. “Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma,” 2023.
Elsholtz & Tao. “Counting the Number of Solutions to the Erdős–Straus Equation on Unit Fractions,” 2013.
Erdős & Lovász. “Problems and Results on 3-Chromatic Hypergraphs and Some Related Questions,” 1975.
Howard, Ramdas, McAuliffe & Sekhon. “Time-Uniform, Nonparametric, Nonasymptotic Confidence Sequences,” 2021.
Karayel. “Derandomization with Pseudorandomness,” 2024.
Ma et al. “ShannonProver: Towards Automating Formal Cryptographic Proofs,” 2026.
Mihnea & Bogdan. “Further Verification and Empirical Evidence for the Erdős–Straus Conjecture,” 2025.
de Moura & Ullrich. “The Lean 4 Theorem Prover and Programming Language,” 2021.
Necula. “Proof-Carrying Code,” 1997.
Neri, Oliva & Pischke. “A Systematic Way of Analysing Proofs in Probability Theory,” 2026.
Paradise, Richardson, Bengio & Goldwasser. “How to Verify Consistency of Probabilistic Claims,” 2026.
Ramdas, Grünwald, Vovk & Shafer. “Game-Theoretic Statistics and Safe Anytime-Valid Inference,” 2023.
Salez. “The Erdős–Straus Conjecture: New Modular Equations and Checking up to N = 10¹⁷,” 2014.
Schröer et al. “A Deductive Verifier for Probabilistic Programs – Caesar,” 2026.
Tan et al. “Formally Certified Approximate Model Counting,” 2024.
The mathlib Community. “The Lean Mathematical Library,” 2020.
Tristan et al. “Verification of Machine Learning Systems via Reparameterization,” 2020.
Valiant. “The Complexity of Enumeration and Reliability Problems,” 1979.

End of web edition

Use the v4.1 PDF for the formal induction and lifting chapter, original theorem numbering, retained proofs, appendices, certificate schema, tables, and complete integrated record.

Open v4.1 PDF