# Formalization guide

## The statement

`Erdos870Target` in `Erdos870/Defs.lean` is the exact public target:

```lean
def Erdos870Target : Prop :=
  ∀ k : ℕ, 3 ≤ k → ∀ C : ℝ, 0 < C →
    ∃ E : Set ℕ,
      BasisAtMost E k ∧
      LogRepLowerBound E k C ∧
      ContainsNoMinimalSubbasis E k
```

Representations are finite multisets of positive naturals in `E`, with cardinality between `1` and `k`. The multiset convention makes representations nondecreasing and identifies permutations.

## Recommended reading order

1. `Erdos870/Main.lean`: the public theorem alias.
2. `Erdos870/MainTheorem.lean`: the split into `k = 3` and `k >= 4`.
3. `Erdos870/Filler.lean`: the deterministic reductions.
4. `Erdos870/Order2Input.lean`: the order-2 source used for `k >= 4`.
5. `Erdos870/ClusteredInput.lean`: the shifted construction used for `k = 3`.
6. The probability support files when checking a specific estimate.

## Main dependency chain

```text
ProbabilityTools / ClaudeProbCore
        |                |
        +---- LLProp5AntiClustering
        +---- LarsenLarsenL7BC
                     |
            Order2Input     ClusteredInput
                     \       /
                       Filler
                         |
                   MainTheorem
                         |
                       Main
```

## Key theorem names

- `larsen_larsen_order2_input`: order-2 witness.
- `finite_shift_clustered_input_uniform`: uniform clustered witness.
- `kge4_from_order2`: deterministic reduction for `k >= 4`.
- `k3_from_clustered`: deterministic reduction for `k = 3`.
- `main_theorem`: final theorem in the original source layout.
- `erdos_870`: public repository entry point.