PublishedInputs.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The published Hamiltonicity input

Chvátal and Erdős, A note on Hamiltonian circuits, Discrete Mathematics 2 (1972), 111–113, Theorem 1: https://users.renyi.hu/~p_erdos/1972-02.pdf.

Only its s = 2 specialization at order at least six is needed here. The proposition below is an explicit parameter of the conditional development, not an axiom or an assumed instance.

def OAI.CycleClique.Construction.CEAlphaTwo line 22
Source documentation
The precise Chvátal–Erdős specialization used in the size test. Connectivity after every one-vertex deletion is the required two-connectivity condition at this order.
```
def CEAlphaTwo : Prop :=
…
```