show/hide visualization coordinates
a : (0.3158236116384616, -0.32371408093076925, 0.38535287891538456)
b : (-0.3814548764615384, -1.0371458753307692, 0.3159426200153846)
c : (0.5145558837384615, -1.1708359491307694, -0.10748586388461545)
d : (0.7696217462384617, -0.28944476623076926, -0.5050924398846155)
e : (0.8204556876384616, 0.4953811985692307, 0.11253537401538455)
f : (-0.038379559561538434, 0.5822143488692308, 0.6173739850153845)
g : (-0.6264821096615384, -0.08113786643076926, 0.1546654094153846)
h : (-0.17576036036153841, -0.6099483514307692, -0.5645072904846155)
i : (-0.2957378648615384, -1.6009693670307692, -0.5054925035846154)
j : (0.015917756638461622, 0.36667905416923074, -0.46725292768461546)
k : (0.20817688323846162, 1.2644395717692307, -0.07094183168461543)
l : (-0.40627801326153845, 1.510048859869231, 0.6788056324153846)
m : (-0.7204587849615385, 0.8944332232692307, -0.04390304258461547)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['b', 'a', 'c'], ['m', 'l', 'f'], ['j', 'g', 'h'], ['m', 'g', 'f'], ['i', 'h', 'c'], ['k', 'l', 'f'], ['m', 'j', 'g'], ['b', 'g', 'a'], ['g', 'a', 'f'], ['d', 'a', 'e'], ['b', 'h', 'g'], ['h', 'd', 'j'], ['m', 'k', 'l'], ['e', 'a', 'f'], ['j', 'e', 'k'], ['h', 'd', 'c'], ['k', 'e', 'f'], ['b', 'i', 'h'], ['b', 'i', 'c'], ['d', 'a', 'c'], ['j', 'd', 'e'], ['m', 'j', 'k']]
Coordinate Data:
k : [7307126777 / 10000000000, 18391098301 / 10000000000, 4142448549 / 10000000000]
m : [-395845981 / 2000000000, 229547419 / 156250000, 110320911 / 250000000]
b : [70540459 / 500000000, -462475617 / 1000000000, 4005646533 / 5000000000]
f : [4841562349 / 10000000000, 1446105759 / 1250000000, 2756401679 / 2500000000]
e : [13429914821 / 10000000000, 10700514569 / 10000000000, 2988610303 / 5000000000]
c : [5185458391 / 5000000000, -1490414227 / 2500000000, 3777008227 / 10000000000]
a : [8383594061 / 10000000000, 1254780887 / 5000000000, 1741079131 / 2000000000]
h : [3467754341 / 10000000000, -352780931 / 10000000000, -793206039 / 10000000000]
g : [-64966447 / 625000000, 4935323919 / 10000000000, 9997689 / 15625000]
l : [290644453 / 2500000000, 10423595591 / 5000000000, 1163992319 / 1000000000]
j : [5384535511 / 10000000000, 15061589 / 16000000, 179337589 / 10000000000]
d : [12921575407 / 10000000000, 2852254921 / 10000000000, -199057533 / 10000000000]
i : [70874353 / 312500000, -10262991087 / 10000000000, -20305817 / 1000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 13
|E| = 33
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 31249999973469819953698095546377557571405570526451111263841 / 62500000290222090603607840534881897961950000000000000000000
Collision distance in [70710677 / 100000000, 35355339 / 50000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [468 / 625, 749 / 1000] ~ [0.7488, 0.749]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 1093162781763216750172899 / 10000000000000000000000000000000000000000
rho in [4182177 / 400000000000000, 8182177 / 400000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [3504384 / 574456265, 14025025 / 2297825056] ~ [0.0061, 0.0061]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-623 / 3125000, 10063 / 50000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [71807033 / 1562500, 114891253 / 2500000] ~ [45.9565, 45.9565]
LHS := (LHS NUM) / (LHS DEN) in [-623 / 143614066, 10063 / 2297825056] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [70710677 / 360555128, 70710678 / 360555127] ~ [0.19612, 0.19612]
Success: LHS < CD / |V| ^ .5
Success: existence proven