Public research preprintVersion 6 · not peer-reviewed40 pages · September 5, 2026

Original research · formal verification · automated reasoning

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

Exact certificates for returned answers. Complete coverage for a declared domain. Measured reliability for a specified population.

Kenju TomitaRochester Institute of Technology · Ephemerent Research

Read v6 PDF Download LaTeX source Read the intuitive explainer

Version 6 record. The manuscript and LaTeX source are compiled and available below. Peer review, journal acceptance, and arXiv submission are pending. Six older artifact checksum entries still require reconciliation.

Scope of the claims. The finite-domain results are exact mathematical claims. The availability bound assumes the recorded IID sampling model and frozen solver. No physical deployment was evaluated, and neither the universal Erdős–Straus nor Lonely Runner conjecture is solved here.

Certified computation and reliability

A claim with a defined scope.

An exact answer, a complete domain, and a reliable service require different evidence. Version 6 gives each claim an executable contract and a record that another checker can inspect.

01 · Returned answers
Check the witness.
Every returned mathematical answer must satisfy its exact relation. If the solver cannot supply a checked witness, the outcome is unresolved.
02 · Declared domain
Account for every input.
All 12,673 primitive open seven-speed sets in 1–20 have checked witnesses. The verifier reconstructs this finite domain and rejects missing cases.
03 · Sampled population
Measure availability.
4,603 fresh generated inputs, zero failures. The fixed test supports at least 99.9% verified-answer availability at 99% confidence for uniform seven-speed subsets of 1–60, under the stated IID assumptions and frozen solver.

These are generated mathematical inputs. The availability percentage describes how often a verified answer is returned; it is not a probability that an exact witness is true. No physical deployment has been validated.

Why the complete fallback matters

The proposed canonical pair-position rule fails on the primitive open set (44, 60, 104, 205). A complete search still finds the valid time 9/148, with minimum distance 12/37 > 1/5. The new interface treats a canonical miss as unresolved and retains complete candidate support within its work budget.

Read the 40-page v6 paper LaTeX source Code and complete evidence

PDF and source manifest · Evaluation summary · Read the intuitive account. The recorded trial ledger, finite certificate, and independent verifier are included in the supplement.

September 5 research checkpoint

What the final proof attempt established.

The final literature pass did not close universal existence. Version 5 records the corrected constructions, the useful SWC improvements, and the exact boundary of the combined proof.

ArithmeticCorrected hypotheses

Positive shifts and coprimality repair the monomial and prime-anchor claims. A derived complete range is c ≤ p−6 for primes p ≡ 1 (mod 4), p > 5; the PDF includes the proof.

Sampling1.5×–2.5× conditional gain

Jacobi-character conditioning preserves valid Type-II witnesses through the specified recursion. The comparison assumes the same uniform-exponent baseline; it does not establish starting positivity.

Verification24 checks · 12 families

The exact-arithmetic kernel checks polynomial identities, mixtures, witness transport, and case unions. A family proof retains its own domain rather than claiming all-prime coverage.

Reproducible correctionInfinite families do not automatically exhaust the primes.

The combined certificate verifies twelve infinite families and two individual instances. Induction proves existence throughout their union. A separate arithmetic theorem must show that every remaining prime enters that union or has another sound positive-mass certificate.

What the final literature pass found

Exact parametrizations and exceptional-set bounds remain useful, but they do not provide pointwise positivity. Dahan explicitly leaves the conjecture open. Pomerance and Weingartner address the generalized numerator problem. Local-to-global and drift results require additional hypotheses; the inspected claimed closures did not discharge the coverage step.

Read the integrated 40-page PDF Download arXiv source Download notes and checkers

PDF and source manifest · Supplement manifest. The corrected results are now integrated into the original LaTeX manuscript, with a portable source archive and rebuilt bibliography. The separate supplement contains exact checkers and the research record; it is not the accepted-journal deposit.

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.

Version 6 adds an operating-contract evaluation: all 12,673 inputs in a declared finite Lonely Runner domain have verified witnesses. A separately planned test returned verified answers for all 4,603 fresh generated inputs, supporting a 99% confidence bound of at least 99.9% availability under its specified IID input model and frozen solver. This is a mathematical-input laboratory result, with no physical deployment evaluated.

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. Codex assisted the follow-up research and presentation; no exact serving variant or independent peer review is implied. The human author directed 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 compiled v6 PDF for the integrated corrected proofs, final literature audit, and complete manuscript. Exact checkers remain in the research supplement, and earlier editions remain linked in the version record.

Open v6 PDF