Explicit real support fans for the handwritten geometric point set. The polynomial decompositions are proved by ring; their signs by positivity. Each cone carries one fixed triple on both endpoints. No Boolean checker is used.

noncomputable def ConwaySoifer.Simplified.middleThirdPoint : Fin 3 → Point

The three-point configuration used by the middle-third obstruction.

Equations

• ConwaySoifer.Simplified.middleThirdPoint = ![(0, 0), (2 / 3, 1 / 3), (1 / 3, 2 / 3)]

theorem ConwaySoifer.Simplified.middleThird_obstruction {Q : EquilateralTriangle} (hq : 0 < Q.side) (hpts : ∀ (i : Fin 3), middleThirdPoint i ∈ Q.carrier) : 1 ≤ Q.side