The forbidden corner section, proved directly on two closed orientation sectors. No Boolean geometry checks or external polynomial results are used.

theorem ConwaySoifer.Simplified.two_supports_sq {U V a b : ℝ} (hU0 : 0 ≤ U) (hV0 : 0 ≤ V) (hUV : 2 ≤ U + V + U * V) (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 + a * b + b ^ 2 ≤ max (a + V * b) (U * a + b) ^ 2

The two linear supports dominate the triangular norm.

theorem ConwaySoifer.Simplified.forbidden_corner_section {Q : EquilateralTriangle} {s c : ℝ} (hs : 0 ≤ s) (hsc : s ≤ c) (hc : c ≤ 1) (hbound : c * (2 - s) + s ^ 2 ≤ 1) (hside : 0 < Q.side) (h0 : (0, 0) ∈ Q.carrier) (he : (1 - c, 0) ∈ Q.carrier) (hf : (0, s) ∈ Q.carrier) (hp : (1 - s, s) ∈ Q.carrier) : 1 ≤ Q.side

The handwritten corner-section obstruction in the standard 60-degree basis.