Necessary outward-normal conditions for genuine full ray endpoints and strict forbidden points. These are geometric implications, not assumptions encoded in a certificate. The finite index set may include redundant halfspaces.

structure ConwaySoifer.HalfspaceSystem (ι : Type u_1) : Type u_1

A finite intersection of closed linear halfspaces.

• normal : ι → Point →ₗ[ℝ] ℝ

  The linear functional defining each closed halfspace.

• offset : ι → ℝ

  The upper bound for each defining functional.

def ConwaySoifer.HalfspaceSystem.carrier {ι : Type u_1} (H : HalfspaceSystem ι) : Set Point

The closed intersection of the system's linear halfspaces.

Equations

• H.carrier = {p : ConwaySoifer.Point | ∀ (i : ι), (H.normal i) p ≤ H.offset i}

@[simp]

theorem ConwaySoifer.HalfspaceSystem.normal_linePoint {ι : Type u_1} (H : HalfspaceSystem ι) (i : ι) (p d : Point) (t : ℝ) : (H.normal i) (linePoint p d t) = (H.normal i) p + t * (H.normal i) d

theorem ConwaySoifer.HalfspaceSystem.active_of_exit {ι : Type u_1} [Finite ι] (H : HalfspaceSystem ι) {p d : Point} (hp : p ∈ H.carrier) (hexit : ∀ (ε : ℝ), 0 < ε → linePoint p d ε ∉ H.carrier) : ∃ (i : ι), 0 < (H.normal i) d ∧ (H.normal i) p = H.offset i

If every positive displacement leaves the intersection, some active facet has strictly positive derivative in that direction. Finiteness is essential.

theorem ConwaySoifer.HalfspaceSystem.violated_of_forbidden {ι : Type u_1} (H : HalfspaceSystem ι) {v d : Point} (hv : v ∈ H.carrier) {t : ℝ} (ht : 0 < t) (hout : linePoint v d t ∉ H.carrier) : ∃ (i : ι), 0 < (H.normal i) d ∧ H.offset i < (H.normal i) (linePoint v d t)

A violated halfspace at a positive point on a ray from an included anchor necessarily has a strictly positive outward derivative on that ray.

theorem ConwaySoifer.rayLen_has_supporting_normal {ι : Type u_1} [Finite ι] (T : EquilateralTriangle) (H : HalfspaceSystem ι) (hrep : T.carrier = H.carrier) {v d : Point} (hv : v ∈ T.carrier) (hd : sqDist d (0, 0) = 1) : ∃ (i : ι), 0 < (H.normal i) d ∧ (H.normal i) (linePoint v d (rayLen T v d)) = H.offset i ∧ ∀ q ∈ T.carrier, (H.normal i) q ≤ (H.normal i) (linePoint v d (rayLen T v d))

Exact ray endpoints supply a supporting normal for every mandatory point.

theorem ConwaySoifer.forbidden_ray_has_strict_support {ι : Type u_1} (T : EquilateralTriangle) (H : HalfspaceSystem ι) (hrep : T.carrier = H.carrier) {v d : Point} (hv : v ∈ T.carrier) {t : ℝ} (ht : 0 < t) (hout : linePoint v d t ∉ T.carrier) : ∃ (i : ι), 0 < (H.normal i) d ∧ ∀ q ∈ T.carrier, (H.normal i) q < (H.normal i) (linePoint v d t)

A forbidden positive ray point supplies the strict support inequality used by the contact-sensitive finite certificates.