Shortening.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Shortening a Hamiltonian cycle when there is no independent triple

This is Lemma size:shortening of the manuscript. A step-two chord bypasses one vertex. If all such chords are absent, every step-four edge is forced, and an explicit reordered cycle omits just vertex zero.

theorem OAI.CycleClique.Construction.cycleNext_eq_add_one line 15
Distinct definitions of this name: OAI/Combinatorics/Ramsey/CycleClique/Construction/ClosedIndexed.lean:9 (different declaration text). Qualify references as OAI.CycleClique.Construction.cycleNext_eq_add_one@path.
def OAI.CycleClique.Construction.skipOne line 21
theorem OAI.CycleClique.Construction.skipOne_injective line 24
theorem OAI.CycleClique.Construction.adjacent_of_successive_values line 32
theorem OAI.CycleClique.Construction.shorten_at_zero line 41
def OAI.CycleClique.Construction.stepFourLabel line 72
theorem OAI.CycleClique.Construction.stepFourLabel_injective line 78
theorem OAI.CycleClique.Construction.adjacent_of_step_four_values line 86
theorem OAI.CycleClique.Construction.step_four_cycle line 96
theorem OAI.CycleClique.Construction.labelled_cycle_shortening line 148
Source documentation
Labelled form of the manuscript's cycle-shortening lemma.
```
theorem labelled_cycle_shortening {r : ℕ} (hr : 7 ≤ r)
    {G : SimpleGraph (Fin r)} (hc : ∀ i, G.Adj i (cycleNext i))
    (hi : ¬ HasIndependent G 3) : HasCycle G (r - 1) := by
…
```
Mentions: OAI.CycleClique.Construction.cycleNext, OAI.CycleClique.Construction.HasIndependent, OAI.CycleClique.Construction.HasCycle
theorem OAI.CycleClique.Construction.cycle_shortening line 204
Source documentation
A Hamiltonian cycle on at least seven vertices can be shortened by one when the graph has no independent triple (manuscript Lemma size:shortening).
```
theorem cycle_shortening {V : Type*} {r : ℕ} (hr : 7 ≤ r) {G : SimpleGraph V}
    (hc : HasCycle G r) (hi : ¬ HasIndependent G 3) : HasCycle G (r - 1) := by
…
```
Mentions: OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.HasIndependent
theorem OAI.CycleClique.Construction.cycle_shorten_to line 213
Source documentation
Repeated shortening reaches every prescribed order at least six.
```
theorem cycle_shorten_to {V : Type*} {G : SimpleGraph V} {q r : ℕ}
    (hq : 6 ≤ q) (hqr : q ≤ r) (hc : HasCycle G r)
    (hi : ¬ HasIndependent G 3) : HasCycle G q := by
…
```
Mentions: OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.HasIndependent