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.aownCentralPoint (s : ℝ) : Fin 5 → Point

The five-point configuration used by the Aown central obstruction.

Equations

• ConwaySoifer.Simplified.aownCentralPoint s = ![(-1 * s, 1 / 2 * s), (-1 / 2 * s, -1 / 2 * s), (1 / 2 * s, -1 * s), (1 + -4 / 3 * s, 0), (-1 / 2 * s, s)]

theorem ConwaySoifer.Simplified.aownCentral_obstruction {Q : EquilateralTriangle} {s : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 10) (hq : 0 < Q.side) (hpts : ∀ (i : Fin 5), aownCentralPoint s i ∈ Q.carrier) : 1 ≤ Q.side