Solution to https://puzzling.stackexchange.com/questions/111833/ernie-and-the-equi-area-tetrahedra

tet.zpl

# https://puzzling.stackexchange.com/questions/111833/ernie-and-the-equi-area-tetrahedra

# coordinates of vertices
var x[{1..4}] >= -1 <= 1;
var y[{1..4}] >= -1 <= 1;
var z[{1..4}] >= -1 <= 1;

# squared area of each face
var a_sq[{1..4}];
# cross product for face areas
var c_x[{1..4}] >= -infinity <= infinity;
var c_y[{1..4}] >= -infinity <= infinity;
var c_z[{1..4}] >= -infinity <= infinity;

# squared volume
var v_sq;
# triple product for volume
var t_x[{1..2}] >= -infinity <= infinity;
var t_y[{1..2}] >= -infinity <= infinity;
var t_z[{1..2}] >= -infinity <= infinity;

defnumb mod4(i) := ((i-1) mod 4)+1;

# maximize area1: a_sq[1];
maximize volume: v_sq;

subto in_sphere: forall <i> in {1..4}: x[i]^2 + y[i]^2 + z[i]^2 <= 1;
subto area_ratio: forall <i> in {2..4}: a_sq[i] == i^2 * a_sq[1];

subto cross_prod: forall <i> in {1..4}:
    c_x[i] == (y[mod4(i+1)]-y[i])*(z[mod4(i+2)]-z[i]) - (z[mod4(i+1)]-z[i])*(y[mod4(i+2)]-y[i]) and
    c_y[i] == (z[mod4(i+1)]-z[i])*(x[mod4(i+2)]-x[i]) - (x[mod4(i+1)]-x[i])*(z[mod4(i+2)]-z[i]) and
    c_z[i] == (x[mod4(i+1)]-x[i])*(y[mod4(i+2)]-y[i]) - (y[mod4(i+1)]-y[i])*(x[mod4(i+2)]-x[i]);
subto area: forall <i> in {1..4}: a_sq[i] == (c_x[i]^2 + c_y[i]^2 + c_z[i]^2)/2^2;

subto triple_prod:
    t_x[1] == (y[2]-y[1])*(z[3]-z[1]) - (z[2]-z[1])*(y[3]-y[1]) and
    t_y[1] == (z[2]-z[1])*(x[3]-x[1]) - (x[2]-x[1])*(z[3]-z[1]) and
    t_z[1] == (x[2]-x[1])*(y[3]-y[1]) - (y[2]-y[1])*(x[3]-x[1]) and
    t_x[2] == t_x[1] * (x[4]-x[1]) and
    t_y[2] == t_y[1] * (y[4]-y[1]) and
    t_z[2] == t_z[1] * (z[4]-z[1]);
subto volume: v_sq == (t_x[2]^2 + t_y[2]^2 + t_z[2]^2)/6^2;

# remove degrees of freedom by constraining the orientation of the tetrahedron:
# the first vertex is on the positive x-axis
# the second vertex is on the upper half of the x-y plane
subto fix_vertex: x[1] >= 0 and y[1] == 0 and z[1] == 0 and y[2] >= 0 and z[2] == 0;