# Minimal SWC formal core

`SwcCore.lean` proves the logical kernel of Stochastic Witness Calculus without
trusting a learned generator or a floating-point probability calculation.  An
external exact mass backend must establish:

1. event extensionality;
2. zero mass for the empty event; and
3. nonzero accepted mass for every quantified instance.

The final theorem is an ordinary deterministic existence theorem.

The file intentionally uses only Lean's core language.  Run:

```bash
lean SwcCore.lean
```

The release script records whether this command was available and successful in
`results_v3/lean_compile_status.json`.
