Full ray sections of the actual closed filled triangles. The transfer theorem uses the cover of an open segment, not merely a finite witness assignment.

theorem ConwaySoifer.sqDist_eq_zero_iff (p q : Point) : sqDist p q = 0 ↔ p = q

theorem ConwaySoifer.EquilateralTriangle.convex_carrier (T : EquilateralTriangle) : Convex ℝ T.carrier

theorem ConwaySoifer.EquilateralTriangle.isCompact_carrier (T : EquilateralTriangle) : IsCompact T.carrier

theorem ConwaySoifer.EquilateralTriangle.isClosed_carrier (T : EquilateralTriangle) : IsClosed T.carrier

theorem ConwaySoifer.EquilateralTriangle.vertex_mem_carrier (T : EquilateralTriangle) (i : Fin 3) : T.vertices i ∈ T.carrier

def ConwaySoifer.linePoint (v d : Point) (t : ℝ) : Point

The point at a real parameter along a ray from a specified base point.

Equations

• ConwaySoifer.linePoint v d t = v + t • d

theorem ConwaySoifer.continuous_linePoint (v d : Point) : Continuous (linePoint v d)

@[simp]

theorem ConwaySoifer.linePoint_zero (v d : Point) : linePoint v d 0 = v

theorem ConwaySoifer.sqDist_linePoint (v d : Point) (t : ℝ) : sqDist (linePoint v d t) v = t ^ 2 * sqDist d (0, 0)

theorem ConwaySoifer.linePoint_between {S : Set Point} (hS : Convex ℝ S) {v d : Point} (hv : v ∈ S) {u t : ℝ} (hu : linePoint v d u ∈ S) (ht : 0 ≤ t) (htu : t ≤ u) : linePoint v d t ∈ S

def ConwaySoifer.rayParams (T : EquilateralTriangle) (v d : Point) : Set ℝ

All nonnegative parameters, without truncation or a guessed endpoint.

Equations

• ConwaySoifer.rayParams T v d = {t : ℝ | 0 ≤ t ∧ ConwaySoifer.linePoint v d t ∈ T.carrier}

noncomputable def ConwaySoifer.rayLen (T : EquilateralTriangle) (v d : Point) : ℝ

The supremum of the nonnegative parameters whose ray point belongs to the triangle.

Equations

• ConwaySoifer.rayLen T v d = sSup (ConwaySoifer.rayParams T v d)

theorem ConwaySoifer.rayParams_nonempty (T : EquilateralTriangle) {v d : Point} (hv : v ∈ T.carrier) : (rayParams T v d).Nonempty

theorem ConwaySoifer.rayParams_le_side (T : EquilateralTriangle) {v d : Point} (hv : v ∈ T.carrier) (hd : sqDist d (0, 0) = 1) {t : ℝ} (ht : t ∈ rayParams T v d) : t ≤ T.side

theorem ConwaySoifer.rayParams_bddAbove (T : EquilateralTriangle) {v d : Point} (hv : v ∈ T.carrier) (hd : sqDist d (0, 0) = 1) : BddAbove (rayParams T v d)

theorem ConwaySoifer.isClosed_rayParams (T : EquilateralTriangle) (v d : Point) : IsClosed (rayParams T v d)

theorem ConwaySoifer.rayLen_mem (T : EquilateralTriangle) {v d : Point} (hv : v ∈ T.carrier) (hd : sqDist d (0, 0) = 1) : rayLen T v d ∈ rayParams T v d

theorem ConwaySoifer.rayLen_nonneg (T : EquilateralTriangle) {v d : Point} (hv : v ∈ T.carrier) (hd : sqDist d (0, 0) = 1) : 0 ≤ rayLen T v d

theorem ConwaySoifer.rayLen_le_side (T : EquilateralTriangle) {v d : Point} (hv : v ∈ T.carrier) (hd : sqDist d (0, 0) = 1) : rayLen T v d ≤ T.side

theorem ConwaySoifer.rayLen_endpoint_mem (T : EquilateralTriangle) {v d : Point} (hv : v ∈ T.carrier) (hd : sqDist d (0, 0) = 1) : linePoint v d (rayLen T v d) ∈ T.carrier

theorem ConwaySoifer.linePoint_mem_iff_le_rayLen (T : EquilateralTriangle) {v d : Point} (hv : v ∈ T.carrier) (hd : sqDist d (0, 0) = 1) {t : ℝ} (ht : 0 ≤ t) : linePoint v d t ∈ T.carrier ↔ t ≤ rayLen T v d

theorem ConwaySoifer.not_mem_after_rayLen (T : EquilateralTriangle) {v d : Point} (hv : v ∈ T.carrier) (hd : sqDist d (0, 0) = 1) {t : ℝ} (ht : rayLen T v d < t) : linePoint v d t ∉ T.carrier

def ConwaySoifer.otherCarriers (T : Configuration) (i : Fin 10) : Set Point

The union of all triangles except a specified owner is still closed.

Equations

• ConwaySoifer.otherCarriers T i = ⋃ (j : { j : Fin 10 // j ≠ i }), (T ↑j).carrier

theorem ConwaySoifer.isClosed_otherCarriers (T : Configuration) (i : Fin 10) : IsClosed (otherCarriers T i)

theorem ConwaySoifer.mem_otherCarriers (T : Configuration) (i : Fin 10) (p : Point) : p ∈ otherCarriers T i ↔ ∃ (j : Fin 10), j ≠ i ∧ p ∈ (T j).carrier

theorem ConwaySoifer.closed_cover_endpoint {S : Set Point} (hS : IsClosed S) {f : ℝ → Point} (hf : Continuous f) {a b : ℝ} (hab : a < b) (hcover : ∀ t ∈ Set.Ioo a b, f t ∈ S) : f a ∈ S

A real open segment covered by a finite closed union transfers to its endpoint.

theorem ConwaySoifer.rayLen_transfers (T : Configuration) (hc : Covers T) (i : Fin 10) {v d : Point} (hv : v ∈ (T i).carrier) (hd : sqDist d (0, 0) = 1) {b : ℝ} (hb : rayLen (T i) v d < b) (hseg : ∀ t ∈ Set.Icc 0 b, linePoint v d t ∈ target) : ∃ (j : Fin 10), j ≠ i ∧ linePoint v d (rayLen (T i) v d) ∈ (T j).carrier

Uses coverage immediately after the full endpoint.

theorem ConwaySoifer.rayLen_pos_of_unique_owner (T : Configuration) (hc : Covers T) (i : Fin 10) {v d : Point} (hv : v ∈ (T i).carrier) (hd : sqDist d (0, 0) = 1) (hunique : ∀ (j : Fin 10), j ≠ i → v ∉ (T j).carrier) {b : ℝ} (hb : 0 < b) (hseg : ∀ t ∈ Set.Icc 0 b, linePoint v d t ∈ target) : 0 < rayLen (T i) v d

Unique ownership forces a strictly positive section.