OAI/Combinatorics/EuclideanRamsey/Nine.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Nine algebraically independent circle parameters give a non-Ramsey configuration.

  1. def OAI.EuclideanRamsey.NineMain.gridToFin9 line 23
  2. def OAI.EuclideanRamsey.NineMain.gridToColumn line 25
  3. def OAI.EuclideanRamsey.NineMain.rowEquiv line 28
  4. def OAI.EuclideanRamsey.NineMain.polynomialEmbedding line 32

    Source documentation

    Renaming the polynomial variables into the independent-variable field.

    def polynomialEmbedding : NineGrid.Poly →+* NineField.TargetField :=
…

    Mentions: OAI.EuclideanRamsey.NineGrid.Poly, OAI.EuclideanRamsey.NineField.TargetField

  5. theorem OAI.EuclideanRamsey.NineMain.polynomialEmbedding_injective line 36
  6. theorem OAI.EuclideanRamsey.NineMain.polynomialEmbedding_T line 40
  7. theorem OAI.EuclideanRamsey.NineMain.polynomialEmbedding_U line 44
  8. theorem OAI.EuclideanRamsey.NineMain.paramVector_eq_r line 48
  9. theorem OAI.EuclideanRamsey.NineMain.evaluationMatrix_eq line 56

    Source documentation

    The tensor evaluation matrix is the rational-coordinate matrix after reindexing.

    theorem evaluationMatrix_eq (t : Fin 9 → ℝ) (ht : AlgebraicIndependent ℚ t) :
    NineLinearObstruction.evaluationMatrix (circleConfig t)
      (NineField.coordinateTensorEmbedding t ht) rowEquiv =
    Matrix.reindex gridToColumn gridToColumn
      (NineRational.genericMatrix polynomialEmbedding) := by
…

    Mentions: OAI.EuclideanRamsey.NineLinearObstruction.evaluationMatrix, OAI.EuclideanRamsey.NineField.coordinateTensorEmbedding, OAI.EuclideanRamsey.NineMain.rowEquiv, OAI.EuclideanRamsey.NineMain.gridToColumn, OAI.EuclideanRamsey.NineRational.genericMatrix, OAI.EuclideanRamsey.NineMain.polynomialEmbedding

  10. theorem OAI.EuclideanRamsey.NineMain.evaluationMatrix_det_ne_zero line 70
  11. theorem OAI.EuclideanRamsey.NineMain.nine_circle_not_ramsey line 79

    Source documentation

    Nine algebraically independent real parameters give a non-Ramsey configuration.

    theorem nine_circle_not_ramsey (t : Fin 9 → ℝ)
    (ht : AlgebraicIndependent ℚ t) : ¬ Ramsey (circleConfig t) := by
…

    Mentions: OAI.EuclideanRamsey.Ramsey

  12. theorem OAI.EuclideanRamsey.NineMain.nine_circle_configuration line 88

    Source documentation

    Nine distinct points on the unit circle form a non-Ramsey configuration.

    theorem nine_circle_configuration (t : Fin 9 → ℝ)
    (ht : AlgebraicIndependent ℚ t) :
    Function.Injective (circleConfig t) ∧
      (∀ i, dist (circleConfig t i) 0 = 1) ∧ ¬ Ramsey (circleConfig t) :=
…

    Mentions: OAI.EuclideanRamsey.Ramsey