LayerArithmetic.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Parity growth in the breadth-first layers

These are the two numerical contradictions in the proof of manuscript Proposition clq:layer-interface. The function p records alternating layer independence sums, whose growth contradicts their global bound.

theorem OAI.CycleClique.Construction.even_layer_growth_contradiction line 15

Source documentation

The even-parameter layer inequalities force too much parity growth.

theorem even_layer_growth_contradiction {s : ℕ} (_hs : 1 ≤ s) (p : ℕ → ℕ)
    (hzero : p 0 = 1) (hbound : p s ≤ 2 * s)
    (hstep : ∀ i < s,
      2 * s * p i < s * (p (i + 1) + p i - 1)) : False := by
…

theorem OAI.CycleClique.Construction.odd_layer_growth_contradiction line 36

Source documentation

In the odd case the final increment is at least three, rather than the usual two.

theorem odd_layer_growth_contradiction {s : ℕ} (hs : 2 ≤ s) (p : ℕ → ℕ)
    (hzero : p 0 = 1) (hbound : p s ≤ 2 * s + 1)
    (hstep : ∀ i < s,
      (2 * s + 1) * p i ≤ s * (p (i + 1) + p i - 1)) : False := by
…