Hill.lean`

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Harary–Hill arithmetic, residue-page definitions, and the even-order deletion inequality.

def OAI.Paper170.hill line 33
Source documentation
The integer in the Harary–Hill formula.
Distinct definitions of this name: ComparatorChallenges/CompleteCrossing.lean:78 (different declaration text). Qualify references as OAI.Paper170.hill@path.
```
def hill (n : ℕ) : ℕ :=
…
```
def OAI.Paper170.residueColor line 37
Source documentation
The two contiguous residue blocks used by the explicit drawing.
```
def residueColor (n r : ℕ) : Bool := decide (r % n < n / 2)
```
def OAI.Paper170.crossingTuples line 40
Source documentation
Increasing four-tuples whose alternating edges occupy the same page.
```
def crossingTuples (n : ℕ) : Finset (Fin 4 → Fin n) := by
…
```
def OAI.Paper170.sameColorResidues line 47
Source documentation
Residues with the same color after a cyclic shift by k.
```
def sameColorResidues (n k : ℕ) : Finset ℕ :=
…
```
def OAI.Paper170.sameColorGapTuples line 51
Source documentation
Cyclic starting points and the first two positive gaps in the source count.
```
def sameColorGapTuples (n k : ℕ) : Finset (ℕ × ℕ × ℕ) :=
…
```
def OAI.Paper170.residueFiber line 57
Source documentation
Starting labels producing a prescribed diagonal-sum residue.
```
def residueFiber (n b r : ℕ) : Finset ℕ :=
…
```
def OAI.Paper170.sameColorResiduesParity line 61
Source documentation
One parity class of the same-color residues.
```
def sameColorResiduesParity (n k p : ℕ) : Finset ℕ :=
…
```
def OAI.Paper170.firstGapParity line 65
Source documentation
One parity class of the first-gap choices after a fixed offset.
```
def firstGapParity (k b p : ℕ) : Finset ℕ :=
…
```
def OAI.Paper170.crossingAntiderivative line 69
Source documentation
The polynomial whose finite difference evaluates the crossing sum.
```
def crossingAntiderivative (n k : ℤ) : ℤ :=
…
```
theorem OAI.Paper170.crossingAntiderivative_sub line 83
theorem OAI.Paper170.hill_numerator_dvd line 89
theorem OAI.Paper170.hill_even line 98
theorem OAI.Paper170.hill_odd line 106
theorem OAI.Paper170.hill_eq_floor_product line 118
theorem OAI.Paper170.crossing_sum_partial line 140
theorem OAI.Paper170.crossing_sum_telescope line 156
theorem OAI.Paper170.cyclic_count_pairing line 172
lemma OAI.Paper170.four_mul_hill line 237
lemma OAI.Paper170.four_mul_hill_even line 241
lemma OAI.Paper170.four_mul_hill_preceding line 251
lemma OAI.Paper170.hill_deletion_relation line 261
lemma OAI.Paper170.even_lower_bound_of_deletion line 272