OddExtensions.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Ryser counterexamples in all sufficiently large odd extension degrees

For every sufficiently large prime congruent to two modulo three, every sufficiently large odd extension degree yields an intersecting partite uniform hypergraph whose covering number equals its rank. The degree threshold may depend on the prime. Infinitely many ranks occur; part sizes need not be equal.

def OAI.RyserOdd.Specification.EventualOddRanks line 25
Source documentation
The base-prime threshold is uniform; the odd-degree threshold may depend on the base prime. Every sufficiently large odd degree is included.
```
def EventualOddRanks : Prop :=
…
```
def OAI.RyserOdd.Specification.InfiniteRanks line 31
Source documentation
Infinitude refers to ranks of actual finite hypergraphs.
```
def InfiniteRanks : Prop :=
…
```
def OAI.RyserOdd.Specification.ExplicitFailureAt line 36
Source documentation
An actual finite partite uniform hypergraph witnessing strict failure of Ryser's inequality.
Distinct definitions of this name: ComparatorChallenges/RyserOddExtensions.lean:50 (different declaration text). Qualify references as OAI.RyserOdd.Specification.ExplicitFailureAt@path.
```
def ExplicitFailureAt (r : ℕ) : Prop :=
…
```
theorem OAI.RyserOdd.Specification.explicitFailureAt_of_counterexampleRank line 48
Source documentation
A counterexample rank yields a uniform hypergraph that strictly violates Ryser's inequality.
```
theorem explicitFailureAt_of_counterexampleRank {r : ℕ}
    (hr : CounterexampleRank r) : ExplicitFailureAt r := by
…
```
def OAI.RyserOdd.Specification.WholeUnbalancedPaper line 60
Source documentation
Eventual odd-degree counterexamples and infinitely many counterexample ranks, without any requirement that the parts have equal size.
```
def WholeUnbalancedPaper : Prop := EventualOddRanks ∧ InfiniteRanks
…
```
Mentions: OAI.RyserOdd.Specification.EventualOddRanks, OAI.RyserOdd.Specification.InfiniteRanks
theorem OAI.RyserOdd.eventualOddRanks line 68
theorem OAI.RyserOdd.infiniteRanks line 105
theorem OAI.RyserOdd.eventualExplicitFailures line 118
theorem OAI.RyserOdd.full_main line 129
theorem OAI.RyserOdd.eventualOddFailures_and_infinite line 132
Distinct definitions of this name: ComparatorChallenges/RyserOddExtensions.lean:61 (same statement text; different proof or body). Qualify references as OAI.RyserOdd.eventualOddFailures_and_infinite@path.
theorem OAI.RyserOddReference.challenge line 146