How to solve this geometric problem with Mathematica?

Question

I try to solve the following problem, making use of 14.0 on Windows 10

Let a triangle $\Delta$ (a contour with its interior) be chosen in the unit square $S$. To prove that the closure of the difference of the sets $\overline{S\setminus \Delta}$ includes a triangle of the area at least $1/6$

Here are my unsuccessful attempts. First, I try to apply quantifiers to this end. Let us denote the coordinates of the vertices of the chosen triangle by {x1,x2}, {y1,y2}, {z1,z2} and the coordinates of the vertices of the the desired triangle by {a1,a2}, {b1,b2}, {c1,c2}. The quantifiers do not directly work withRegions, so RegionMemberis needed to be used to rewrite regions as systems of algebraic equations and inequalities.

The command

ForAll[{x1, x2, y1, y2, z1, z2},  x1 >= 0 && x1 <= 1 && y1 >= 0 && y1 <= 1 && y2 >= 0 && 
y2 <= 1 &&  z1 >= 0 && z2 <= 1,  Exists[{a1, a2, b1, b2, c1, c2}, 
RegionMember[RegionDifference[Rectangle[],
Triangle[{{x1, x2}, {y1, y2}, {z1, z2}}]], {a1, a2}] && 
RegionMember[RegionDifference[Rectangle[], 
Triangle[{{x1, x2}, {y1, y2}, {z1, z2}}]], {b1, b2}] && 
 RegionMember[RegionDifference[Rectangle[], 
 Triangle[{{x1, x2}, {y1, y2}, {z1, z2}}]], {c1, c2}], 
 Area[Triangle[{{a1, a2}, {b1, b2}, {c1, c2}}]] >= 1/6 && 
 ForAll[{x, y},Implies[RegionMember[Triangle[{{a1, a2}, {b1, b2}, {c1, c2}}], {x, y}], 
 RegionMember[RegionConvert[RegionDifference[Rectangle[], 
 Triangle[{{x1, x2}, {y1, y2}, {z1, z2}}]], "Implicit"], {x,y}]]]]]

seems syntactically correct. Unfortunately,

Resolve[%, Reals]

The kernel Local has quit (exited) during the course of an evaluation

on my comp (which is not powerful) in several hours.

Second, I try to apply NMaximize to find a desired triangle by

f[x1_?NumericQ, x2_?NumericQ, y1_?NumericQ, y2_?NumericQ, z1_?NumericQ, z2_?NumericQ] := 
 NMaximize[{Area[ Triangle[{{a1, a2}, {b1, b2}, {c1, c2}}]], 
(RegionConvert[ RegionDifference[Rectangle[], 
     Triangle[{{x1, x2}, {y1, y2}, {z1, z2}}]], 
    "Implicit"] /. {\[FormalX] -> a1, \[FormalY] -> a2})[[1]]
&& (RegionConvert[ RegionDifference[Rectangle[], 
     Triangle[{{x1, x2}, {y1, y2}, {z1, z2}}]], 
    "Implicit"] /. {\[FormalX] -> b1, \[FormalY] -> b2})[[
 1]] && (RegionConvert[RegionDifference[Rectangle[], 
     Triangle[{{x1, x2}, {y1, y2}, {z1, z2}}]], 
    "Implicit"] /. {\[FormalX] -> c1, \[FormalY] -> c2})[[1]] && 
RegionIntersection[RegionDifference[Rectangle[], 
   Triangle[{{x1, x2}, {y1, y2}, {z1, z2}}]], 
  Triangle[{{a1, a2}, {b1, b2}, {c1, c2}}]] == 
 Triangle[{{a1, a2}, {b1, b2}, {c1, c2}}]}, {a1, a2, b1, b2, c1, c2}]

and then to NMinimize the function f, but

f[1/4, 0.3, 1/4, 0.7, 0.8, 0.8]

NMaximize::bcons: The following constraints are not valid: {Triangle[{{a1,a2},{b1,b2},{c1,c2}}] ==BooleanRegion[{#1,#2}&,{Polygon[{{<<2>>},{<<2>>},{<<2>>},{<<2>>}}->{{<<3>>}}], Triangle[{{a1,a2},{b1,b2},{c1,c2}}]}],0. +1. a1<=1.,<<6>>,-0.8 c1-0.2 c2<=-0.8,-0.2 c1+0.2 c2<=0.}. Constraints should be equalities, inequalities, or domain specifications involving the variables.

I don't think GeometricTest is able to solve it at the present and, as far as my knowledge goes, AlphaGeometry is not implemented in Mathematica yet.

Edit. In order to make the formulation more accurate, the difference of the sets $S\setminus \Delta$ is replaced by the closure of the difference of the sets $\overline{S\setminus \Delta}$.

Answer 1

Based on the interesting answer of @three777 we can define quite general triangle depending on three paramters 0<\[Alpha], \[Beta], \[Gamma] <1 as shown in the picture

Graphics[{Arrow[{{0, 0}, {\[Alpha], 0}}], 
   Arrow[{{1, 0}, { 1, \[Beta]}}], Arrow[{{1, 1}, {1 - \[Gamma], 1}}],
    Text["\[Alpha]", {\[Alpha], 0}/2, {0, -1}], 
   Text["\[Beta]", { 1, \[Beta]/2}, { 1, 0}], 
   Text["\[Gamma]", {1 - \[Gamma]/2, 1}, {0, 1}], FaceForm[None], 
   EdgeForm[Black], Rectangle[], FaceForm[Red], 
   Triangle[{{\[Alpha], 0}, { 1, \[Beta]}, {1 - \[Gamma], 1}}]
   } /. {\[Alpha] -> .2, \[Beta] -> .3, \[Gamma] -> .9}]

Minimization of the four neighboring triangles gives

sol = Minimize[{
Max[{ Cross[{\[Alpha], 0}] . {1 - \[Gamma], 1}/2,Cross[{1 - \[Gamma], 1}] . {0, 1}/2 , (1 - \[Alpha]) \[Beta]/2, (1 - \[Beta]) \[Gamma]/2}] }
, {\[Alpha], \[Beta], \[Gamma]}]

(*{1/6, {\[Alpha] -> 1/3, \[Beta] -> 1/2, \[Gamma] -> 2/3}}*)

Graphics[{Arrow[{{0, 0}, {\[Alpha], 0}}], 
   Arrow[{{1, 0}, { 1, \[Beta]}}], Arrow[{{1, 1}, {1 - \[Gamma], 1}}],
    FaceForm[None], EdgeForm[Black], Rectangle[], FaceForm[Red], 
   Triangle[{{\[Alpha], 0}, { 1, \[Beta]}, {1 - \[Gamma], 1}}]
   } /. sol[[2]]]

Answer 2

Manipulate[
 Graphics[{{Transparent, EdgeForm[Black], Rectangle[{0, 0}, {1, 1}]}, 
   Black, Triangle[{{0, a}, {1/2, 1}, {1, a}}], 
   Arrow[{{1.05, 0}, {1.05, a}}], Arrow[{{1.05, a}, {1.05, 0}}], 
   Inset["a", {1.08, a/2}], Red, Triangle[{{1/2, 1}, {1, a}, {1, 1}}],
    Green, Triangle[{{0, 0}, {1, 0}, {1, a}}]}], {{a, 1/3}, 0, 1}]

Minimizing max of red and green triangle areas.

Minimize[Max@{Area@Triangle[{{1/2, 1}, {1, a}, {1, 1}}], 
   Area@Triangle[{{0, 0}, {1, 0}, {1, a}}]}, a]

$$\left\{\frac{1}{6},\left\{a\to \frac{1}{3}\right\}\right\}$$