Ramsey.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GrahamSpherical.not_euclideanRamsey_of_fifty_colorings line 9
Source documentation
Fixed fifty-color avoidance in every positive dimension contradicts the ordinary Ramsey quantifier, without assuming any copy exists.
```
theorem not_euclideanRamsey_of_fifty_colorings
    (havoid : ∀ n : ℕ, 0 < n →
      ∃ color : Point n → Fin 50, AvoidsCopy witness color) :
    ¬ EuclideanRamsey witness := by
…
```
Mentions: OAI.GrahamSpherical.Point, OAI.GrahamSpherical.AvoidsCopy, OAI.GrahamSpherical.witness, OAI.GrahamSpherical.EuclideanRamsey
theorem OAI.GrahamSpherical.assemble_full_result line 20
Source documentation
The geometric and coloring properties jointly imply the spherical non-Ramsey conclusion.
```
theorem assemble_full_result
    (hcard : witness.ncard = 12)
    (hsphere : witness ⊆ Metric.sphere (0 : Point 2) 1)
    (havoid : ∀ n : ℕ, 0 < n →
      ∃ color : Point n → Fin 50, AvoidsCopy witness color) :
    Specification.FullAuthoredResult :=
…
```
Mentions: OAI.GrahamSpherical.witness, OAI.GrahamSpherical.Point, OAI.GrahamSpherical.AvoidsCopy, OAI.GrahamSpherical.Specification.FullAuthoredResult