# Paper to Lean correspondence

| Paper location | Mathematical role | Lean source |
|---|---|---|
| Sections 1-2 | Definitions, target, two input propositions | `Defs.lean`, interfaces in `Order2Input.lean` and `ClusteredInput.lean` |
| Section 3 | Finite filler gadget and the reduction for `k >= 4` | `Filler.lean`, especially `kge4_from_order2` |
| Section 4 | Parity reduction for `k = 3` | `Filler.lean`, especially `k3_from_clustered` |
| Section 5 | Repaired Larsen-Larsen input, density zero, canary exactness, deletion | `Order2Input.lean` plus the probability support files |
| Section 6 | Clustered construction and finite-shift deletion property | `ClusteredInput.lean` |
| Section 7 | Clean representation supply and loss estimates | `ClusteredInput.lean`, `ProbabilityTools.lean`, `ClaudeProbCore.lean`, `LLProp5AntiClustering.lean`, `LarsenLarsenL7BC.lean` |
| Appendix A | Final source map and theorem | `MainTheorem.lean`, exposed publicly by `Main.lean` |

## Interface boundary

The deterministic reductions consume two packaged witnesses:

- `Order2Witness`, corresponding to Proposition 2.1;
- `ClusteredWitness`, corresponding to Proposition 2.2.