Seven.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem160.properColoring_seven_of_normalized_cover line 16
Source documentation
The elementary covering-radius statement is the only geometric input needed to turn the index-seven lattice coloring into a plane coloring.
```
theorem properColoring_seven_of_normalized_cover
    (hcover : ∀ x y : ℝ, ∃ a b : ℤ,
      (x - ((a : ℝ) + (b : ℝ) / 2)) ^ 2 +
        (y - Real.sqrt 3 * b / 2) ^ 2 ≤ (1 / 3 : ℝ)) :
    ProperColoring 7 := by
…
```
Mentions: OAI.Problem160.ProperColoring
theorem OAI.Problem160.properColoring_seven line 36
Source documentation
The classical seven-color upper bound, with all boundary points assigned using the closed triangular-lattice cover.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OAI.Problem160.ProperColoring, OfNat.ofNat, Nat
Proof uses: OAI.Problem160.properColoring_seven_of_normalized_cover, OAI.Problem160.triangular_lattice_cover
1 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: ComparatorChallenges/PlaneColoring.lean:15 (same statement text; different proof or body). Qualify references as OAI.Problem160.properColoring_seven@path.
```
theorem properColoring_seven : ProperColoring 7 :=
…
```
Mentions: OAI.Problem160.ProperColoring
theorem OAI.Problem160.exists_measurable_proper_seven line 41
Source documentation
The seven-color construction admits a measurable choice on its boundary points: select the first covering center in a countable enumeration.
```
theorem exists_measurable_proper_seven :
    ∃ c : Plane → Fin 7, Measurable c ∧
      ∀ x y : Plane, dist x y = 1 → c x ≠ c y := by
…
```
Mentions: OAI.Problem160.Plane
theorem OAI.Problem160.weakMeasurableColoring_seven line 60
Source documentation
The classical measurable seven-color construction satisfies the exact weak pair-measure condition.
```
theorem weakMeasurableColoring_seven : WeakMeasurableColoring 7 := by
…
```
Mentions: OAI.Problem160.WeakMeasurableColoring