# Stochastic Witness Calculus artifact

This reproducibility artifact accompanies the paper **“Stochastic Witness Calculus: Exact Measure Certificates for Mathematical Existence, Learned Proof Search, and Anytime-Valid Empirical Claims.”**

## Contents

- `paper/`: LaTeX source, bibliography, compiled PDF, and bibliography cache.
- `src/swc_core.py`: exact finite-mass reference kernel and calculus combinators.
- `src/path_certificate.py`: portable proof-carrying path-mass certificate producer/checker.
- `tests/`: unit tests for exact arithmetic, composition rules, quantifier guards, and certificate tamper rejection.
- `experiments/exp_sat.py`: exact finite SAT witness-mass experiment.
- `experiments/exp_chain_wmc.py`: non-enumerative dynamic-programming certificate over witness spaces up to `2^2048`.
- `experiments/exp_quantifier_audit.py`: exact and simulated stress tests for hidden exceptions and rare positive mass.
- `experiments/exp_erdos.cpp`: exact finite Erdős–Straus anchor-divisor survey.
- `experiments/exp_eprocess.py`: optional-stopping simulation.
- `experiments/exp_certificate_integrity.py`: valid/tampered proof-object stress test.
- `experiments/make_figures.py`: regenerates all plots from result files.
- `results/`: raw CSV/JSON outputs.
- `figures/`: PDF and PNG figures used in the paper.
- `schemas/`: machine-readable schema for the proof-carrying path-mass certificate.
- `examples/`: a complete exact certificate example.
- `CLAIMS_AND_LIMITS.md`: compact theorem-status and scope ledger.
- `CITATION.cff`: citation metadata for a public repository.
- `REVIEWER_GUIDE.md`: audit map for theorems, nonclaims, trusted-base obligations, and experiment checks.
- `CHANGELOG.md` and `VERSION`: release history and artifact version.

## Environment used

- Python 3.13.5
- NumPy 2.3.5
- pandas 2.2.3
- Matplotlib 3.10.8
- g++ 14.2.0
- pdfTeX 1.40.26 (TeX Live 2025/dev)
- biber 2.20

## Reproduce

Run from the project root:

```bash
python -m pip install -r requirements.txt
./run_all.sh
```

The complete run regenerates all six experiment families, figures, unit tests, and the manuscript. The Erdős–Straus survey is the longest single experiment. TeX compilation time depends on the local installation.

To compile only the manuscript:

```bash
cd paper
pdflatex main.tex
biber main
pdflatex main.tex
pdflatex main.tex
```

## Scope and trust boundary

The exact trusted core is limited to deterministic verifiers, exact integer/rational arithmetic, checked recurrence or counting back ends, certificate-rule validation, and pointwise quantifier discipline. Learned policies, heuristic model outputs, Monte Carlo estimates, floating-point plots, compilers, and generators remain outside that core unless they emit independently checkable certificates.

The proof-carrying integrity experiment checks a declared mutation suite; it is not a cryptographic security proof. SHA-256 binds semantic fields inside the artifact but does not authenticate an author or eliminate compiler/system compromise.

The Erdős–Straus experiment is finite verification only. It does not prove the open conjecture.

## Authorship and model disclosure

Kenju Tomita directed the project and is responsible for all claims. Arbiter v23, an internal looped 27B-parameter model, contributed hypotheses, reformulations, and proof drafts to the Erdős–Straus case study; retained claims were checked independently. GPT-5.6 Pro assisted with literature synthesis, implementation, figure generation, experiments, and manuscript drafting.
