show/hide visualization coordinates
a : (0.2778287047799999, 0.13331959691333334, 0.8871769188266667)
b : (-0.1858040580200001, -0.7131793909866666, 0.6254822026266667)
c : (0.8041865163799998, -0.6295816772866667, 0.5117716713266667)
d : (1.18499364448, 0.2949803557133333, 0.49869581082666675)
e : (0.4067413109799999, 0.8461312672133332, 0.19777060712666666)
f : (-0.2867534434200001, 0.9583963939133333, 0.9094317393266667)
g : (-0.57374096222, 0.17071750131333335, 0.36427109672666674)
h : (-0.7081775520200001, -0.6274901781866666, -0.22291822847333326)
i : (0.23865687197999996, -0.9481571650866667, -0.2489423879733333)
j : (0.6116059640799999, -0.020344607786666635, -0.2574766136733333)
k : (0.0816621555799999, 0.6814989628133332, -0.7334757334733333)
l : (-0.5330989742200001, 1.0789466402133332, -0.05222387347333329)
m : (-0.8292336366200002, 0.2928656316133334, -0.5947926797733333)
n : (-0.08371811742000007, -0.28589285818666665, -0.9253153278733333)
o : (-0.4051484243200001, -1.2322104721866667, -0.9594552020733333)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['a', 'd', 'e'], ['o', 'i', 'n'], ['k', 'n', 'm'], ['l', 'e', 'k'], ['o', 'h', 'i'], ['j', 'd', 'e'], ['b', 'h', 'i'], ['j', 'c', 'i'], ['h', 'n', 'm'], ['b', 'h', 'g'], ['a', 'b', 'g'], ['j', 'e', 'k'], ['m', 'l', 'g'], ['a', 'b', 'c'], ['a', 'f', 'e'], ['a', 'c', 'd'], ['f', 'e', 'l'], ['o', 'h', 'n'], ['b', 'c', 'i'], ['j', 'k', 'n'], ['j', 'c', 'd'], ['j', 'i', 'n'], ['l', 'k', 'm'], ['a', 'f', 'g'], ['f', 'l', 'g'], ['m', 'h', 'g']]
Coordinate Data:
e : [9250084901 / 10000000000, 13099001807 / 10000000000, 3393727007 / 5000000000]
o : [282796887 / 2500000000, -7684415587 / 10000000000, -2392402039 / 5000000000]
m : [-124386583 / 400000000, 7566345451 / 10000000000, -227635771 / 2000000000]
h : [-1899103729 / 10000000000, -1637212647 / 10000000000, 1290282829 / 5000000000]
g : [-554737831 / 10000000000, 1586216037 / 2500000000, 845245891 / 1000000000]
a : [7960958839 / 10000000000, 373180319 / 625000000, 13681517131 / 10000000000]
l : [-148317951 / 10000000000, 15427155537 / 10000000000, 535938651 / 1250000000]
d : [4258152059 / 2500000000, 1896873173 / 2500000000, 9796706051 / 10000000000]
c : [2644907391 / 2000000000, -829063819 / 5000000000, 620466541 / 625000000]
n : [4345490617 / 10000000000, 1778760553 / 10000000000, -555425667 / 1250000000]
j : [1412341429 / 1250000000, 4434243057 / 10000000000, 1117490903 / 5000000000]
b : [3324631211 / 10000000000, -99764191 / 400000000, 11064569969 / 10000000000]
k : [5999293347 / 10000000000, 11452678763 / 10000000000, -157813087 / 625000000]
i : [7569240511 / 10000000000, -1210970629 / 2500000000, 2320324063 / 10000000000]
f : [2315137357 / 10000000000, 7110826537 / 5000000000, 1738008167 / 1250000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 15
|E| = 39
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 124999999916694398127975404037951338812873712902742171414841 / 249999999901872749286682757631906016223750000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [78 / 125, 3121 / 5000] ~ [0.624, 0.6242]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 2877927205815511407577 / 2500000000000000000000000000000000000000
rho in [107292631 / 100000000000000000, 1107292631 / 100000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [4056 / 1040833, 9740641 / 2497999196] ~ [0.0039, 0.0039]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-2499 / 12500000, 20089 / 100000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [624499799 / 12500000, 3122499 / 62500] ~ [49.95998, 49.95998]
LHS := (LHS NUM) / (LHS DEN) in [-357 / 89214257, 20089 / 4995998392] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [23570226 / 129099445, 70710679 / 387298334] ~ [0.18257, 0.18257]
Success: LHS < CD / |V| ^ .5
Success: existence proven