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.acrossLargeCentrePoint : Fin 5 → Point

The five mandatory central points in the large-parameter Across obstruction.

Equations

• ConwaySoifer.Simplified.acrossLargeCentrePoint = ![(-2 / 29, 1 / 29), (-1 / 29, -1 / 29), (1 / 29, -2 / 29), (2 / 29, -1 / 29), (0, 9 / 10)]

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