NineStatement.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The literal rational parametrization of the nine-point circle configuration.

def OAI.EuclideanRamsey.NineStatement.literalCircleConfig line 11
Source documentation
The rational parametrization of nine points in the Euclidean plane.
Also declared: ComparatorChallenges/EuclideanRamseyNine.lean:20 (same declaration text).
```
def literalCircleConfig (t : Fin 9 → ℝ) (i : Fin 9) : Space 2 :=
…
```
Mentions: OAI.EuclideanRamsey.Space
theorem OAI.EuclideanRamsey.NineStatement.literalCircleConfig_eq line 15
theorem OAI.EuclideanRamsey.NineStatement.nine_circle_configuration line 24
Source documentation
Nine points on the unit circle form a non-Ramsey configuration when their parameters are algebraically independent over the rationals.
Distinct definitions of this name: ComparatorChallenges/EuclideanRamseyNine.lean:26 (same statement text; different proof or body). Qualify references as OAI.EuclideanRamsey.NineStatement.nine_circle_configuration@path.
```
theorem nine_circle_configuration (t : Fin 9 → ℝ)
    (ht : AlgebraicIndependent ℚ t) :
    Function.Injective (literalCircleConfig t) ∧
      (∀ i, dist (literalCircleConfig t i) 0 = 1) ∧
      ¬ Ramsey (literalCircleConfig t) := by
…
```
Mentions: OAI.EuclideanRamsey.NineStatement.literalCircleConfig, OAI.EuclideanRamsey.Ramsey