OAI/Combinatorics/SphericalRamsey/Model.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The explicit twelve-point witness and the ordinary Euclidean Ramsey property. These definitions contain no proof-specific field derivation or affine-placement assumption.

  1. abbrev OAI.GrahamSpherical.Point line 14

    Also declared: ComparatorChallenges/GrahamSpherical.lean:10 (same declaration text).

  2. abbrev OAI.GrahamSpherical.Label line 15

    Also declared: ComparatorChallenges/GrahamSpherical.lean:11 (same declaration text).

  3. def OAI.GrahamSpherical.parameter line 18

    Source documentation

    The factorial series starts at 1!.

    Also declared: ComparatorChallenges/GrahamSpherical.lean:13 (same declaration text).

    def parameter : ℝ := ∑' m : ℕ, 1 / (10 : ℝ) ^ ((m + 1).factorial)
  4. def OAI.GrahamSpherical.u line 20

    Also declared: ComparatorChallenges/GrahamSpherical.lean:15 (same declaration text).

  5. def OAI.GrahamSpherical.v line 21

    Also declared: ComparatorChallenges/GrahamSpherical.lean:16 (same declaration text).

  6. def OAI.GrahamSpherical.squareCoordinate line 23

    Also declared: ComparatorChallenges/GrahamSpherical.lean:18 (same declaration text).

  7. def OAI.GrahamSpherical.coordinates line 30

    Source documentation

    First the positively rotated square, then the negatively rotated square, and finally the original coordinate square.

    Also declared: ComparatorChallenges/GrahamSpherical.lean:23 (same declaration text).

    def coordinates (i : Label) : Fin 2 → ℝ :=
…

    Mentions: OAI.GrahamSpherical.Label

  8. def OAI.GrahamSpherical.vertex line 35

    Also declared: ComparatorChallenges/GrahamSpherical.lean:28 (same declaration text).

  9. def OAI.GrahamSpherical.witness line 37

    Also declared: ComparatorChallenges/GrahamSpherical.lean:30 (same declaration text).

  10. def OAI.GrahamSpherical.weight line 39
  11. def OAI.GrahamSpherical.AvoidsCopy line 43

    Source documentation

    Arbitrary colorings and exact distance-preserving copies; no measurability, computability, continuity of the coloring, or extension of the copy is assumed.

    Also declared: ComparatorChallenges/GrahamSpherical.lean:32 (same declaration text).

    def AvoidsCopy {d n r : ℕ} (X : Set (Point d)) (color : Point n → Fin r) : Prop :=
…

    Mentions: OAI.GrahamSpherical.Point

  12. def OAI.GrahamSpherical.EuclideanRamsey line 46

    Also declared: ComparatorChallenges/GrahamSpherical.lean:35 (same declaration text).

  13. def OAI.GrahamSpherical.Specification.FullAuthoredResult line 58

    Also declared: ComparatorChallenges/GrahamSpherical.lean:46 (same declaration text).