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.
The five-point configuration used to exclude an owner bridging local sections.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ConwaySoifer.Simplified.bridgeLocal_obstruction
{Q : EquilateralTriangle}
{s : ℝ}
(hs0 : 0 < s)
(hs : s ≤ 1 / 3)
(hq : 0 < Q.side)
(hpts : ∀ (i : Fin 5), bridgeLocalPoint s i ∈ Q.carrier)
: