# Quorum sandwich proof artifact

This artifact machine-checks two finite theorems about exactly five voters:

1. Any two groups containing at least three of the five voters overlap.
2. If no voter signs two values in the same term, two conflicting values cannot both hold a 3-of-5 certificate in that term.

The artifact does not prove Raft, implementation correctness, liveness, network recovery, or preference aggregation.

## Requirements

- Lean 4.30.0, selected by the included `lean-toolchain` file.
- Elan is the recommended Lean version manager.

## Run

```powershell
python verify_artifact.py --run-lean
```

A successful run exits with status 0 and prints that all four named declarations depend on no axioms. The Python verifier also checks the source hash, saved Lean output, forbidden proof escapes, and manifest claims; those static checks record provenance and do not replace the Lean kernel check.

## Proof boundary

The model contains ten Boolean decisions: five possible signatures for order A and five for order B. `isMajority` means at least three signatures, while `isDisjoint` represents the rule that no voter signed both orders. Lean checks all assignments to those ten Booleans when elaborating the proofs produced by `by decide`.

The theorem is universal inside that finite model. The connection between the model and a real consensus implementation remains a separate verification problem.