show/hide visualization coordinates
a : (-0.10743061934035569, -0.8564525698080382, 0.06702959042743384)
b : (-0.7909605918161117, -0.8276183615151786, 0.7963822932807354)
c : (-0.9985985258493172, -0.43436802315108447, -0.0992965887562075)
d : (-0.2575288276886423, -0.31465029990044235, -0.7599654689130746)
e : (0.5718048221573927, -0.8655878877162635, -0.6668339942939192)
f : (0.8338346817363834, -0.5748735783164853, 0.25339725001330626)
g : (0.15836825178506797, -0.580656847228444, 0.9907653099464151)
h : (-0.5086761707873033, 0.13139196215601945, 0.7715890535470056)
i : (-1.4783954212508028, -0.10602264661171418, 0.7143275584200639)
j : (-1.7672508485007539, 0.19834267059192134, -0.19337519900208833)
k : (-0.866562003726536, 0.44959634695255934, -0.5478201101160003)
l : (0.07008977805543026, 0.6258093607794096, -0.8505285729027652)
m : (0.5411643310389272, -0.11592235586318234, -1.327941209997587)
n : (1.1592515770964344, -0.0657890119779912, -0.5434319340218752)
o : (1.4194718749379538, 0.22623609167262682, 0.37689775442086804)
p : (1.095688761587347, -0.28402901453523954, 1.1736373711688133)
q : (0.46945741481744896, 0.3160520363593571, 0.6759054828192754)
r : (-0.18936948206734122, 0.7994630800257273, 0.0994847312822158)
s : (-1.155865916192139, 0.7694364537590211, 0.3544024523984415)
t : (0.7764745816181055, 0.7739845101014468, -0.15838362101832598)
u : (1.0250323323888084, 0.735658084225976, -1.1262421487027294)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['j', 'c', 'k'], ['a', 'g', 'f'], ['t', 'l', 'u'], ['h', 'q', 'g'], ['m', 'e', 'n'], ['t', 'n', 'u'], ['o', 'q', 'p'], ['j', 'k', 's'], ['q', 't', 'r'], ['q', 'g', 'p'], ['j', 'i', 's'], ['q', 'h', 'r'], ['l', 'k', 'r'], ['t', 'l', 'r'], ['m', 'e', 'd'], ['o', 't', 'n'], ['o', 'n', 'f'], ['h', 'i', 's'], ['c', 'i', 'b'], ['a', 'c', 'b'], ['j', 'c', 'i'], ['e', 'n', 'f'], ['g', 'p', 'f'], ['m', 'n', 'u'], ['m', 'l', 'u'], ['m', 'l', 'd'], ['l', 'k', 'd'], ['h', 'i', 'b'], ['o', 't', 'q'], ['a', 'e', 'f'], ['c', 'k', 'd'], ['o', 'p', 'f'], ['a', 'c', 'd'], ['k', 's', 'r'], ['a', 'g', 'b'], ['h', 'g', 'b'], ['h', 's', 'r'], ['a', 'e', 'd']]
Coordinate Data:
a : [21345374046581910573 / 50000000000000000000, -42166636193075499673 / 100000000000000000000, 18034409194091748757 / 25000000000000000000]
l : [1208855756654848243 / 2000000000000000000, 106059556865669287483 / 100000000000000000000, -19618179556652904499 / 100000000000000000000]
o : [195380997520994780603 / 100000000000000000000, 66102229954991002767 / 100000000000000000000, 20624890635142082747 / 20000000000000000000]
h : [2566192948469057753 / 100000000000000000000, 56617817003330266041 / 100000000000000000000, 17824197886040520503 / 12500000000000000000]
k : [-33222390345454207539 / 100000000000000000000, 88438255482984248899 / 100000000000000000000, 83223958765809237 / 781250000000000000]
c : [-23213021278866164349 / 50000000000000000000, 41818472619869547 / 100000000000000000000, 27752509429001434417 / 50000000000000000000]
n : [42339741934210707023 / 25000000000000000000, 18449859794964597541 / 50000000000000000000, 11091484331436100737 / 100000000000000000000]
u : [155937043266080243533 / 100000000000000000000, 3657638412822684757 / 3125000000000000000, -47189537136649326167 / 100000000000000000000]
f : [4275539943776179223 / 3125000000000000000, -14008737043920218247 / 100000000000000000000, 354587510683415013 / 390625000000000000]
b : [-12831124577205887409 / 50000000000000000000, -19641607681894775503 / 50000000000000000000, 2266764172839017869 / 1562500000000000000]
j : [-61645637411437987931 / 50000000000000000000, 31656443923460223229 / 50000000000000000000, 23048578916707390459 / 50000000000000000000]
p : [163002686185934064837 / 100000000000000000000, 3015143866840872941 / 20000000000000000000, 45699603712626235317 / 25000000000000000000]
q : [501897757544721457 / 500000000000000000, 75083824423664020693 / 100000000000000000000, 66512613007775583379 / 50000000000000000000]
r : [17248430910232635281 / 50000000000000000000, 123424928790301037579 / 100000000000000000000, 15076630172369038461 / 20000000000000000000]
g : [69270635205706190291 / 100000000000000000000, -7293531967558041093 / 50000000000000000000, 164511208728265116679 / 100000000000000000000]
t : [131081268189009941181 / 100000000000000000000, 15109633974734123571 / 12500000000000000000, 24798157815895508543 / 50000000000000000000]
d : [27680927258335159271 / 100000000000000000000, 6006795398842041241 / 50000000000000000000, -10561869157683846099 / 100000000000000000000]
s : [-121392151546903353 / 195312500000000000, 60211133081815214651 / 50000000000000000000, 4034996918938710333 / 4000000000000000000]
e : [110614292242938665879 / 100000000000000000000, -43080167983898038427 / 100000000000000000000, -1248721695768301611 / 100000000000000000000]
m : [26887560782773027183 / 25000000000000000000, 15943192600705042613 / 50000000000000000000, -33679721633067545713 / 50000000000000000000]
i : [-94405732097880889179 / 100000000000000000000, 16438178063278449833 / 50000000000000000000, 17108429196953751663 / 12500000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 21
|E| = 57
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 120179099787711802992916513966661729238695508940803321804332263639472803894408826806254428014062954228906931867305169 / 228935272289912039585429098920930194019415450374664861187063486079012462415595000000000000000000000000000000000000000
Collision distance in [724532912226126215581994569531 / 1000000000000000000000000000000, 181133228056531553895498642383 / 250000000000000000000000000000] ~ [0.72453, 0.72453]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [1111 / 2500, 2223 / 5000] ~ [0.4444, 0.4446]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 757256596625224171836835368032441873617089 / 25000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [870204916456591948067298186231 / 5000000000000000000000000000000000000000000000000, 870204916461591948067298186231 / 5000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [12343210000000000000000000000 / 7549834435270749697236684806947, 12183750000000000000000000 / 7445596090010601279326119139] ~ [0.00163, 0.00164]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999976356624223101 / 1000000000000000000000000000000, 100000000000011827008180097 / 500000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [3774917217635374848618342403473 / 62500000000000000000000000000, 7549834435270749697236684806947 / 125000000000000000000000000000] ~ [60.39868, 60.39868]
LHS := (LHS NUM) / (LHS DEN) in [-199999999999976356624223101 / 60398675482165997577893478455568, 100000000000011827008180097 / 30199337741082998788946739227784] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [724532912226126215581994569531 / 4582575694955840006588047193729, 181133228056531553895498642383 / 1145643923738960001647011798432] ~ [0.15811, 0.15811]
Success: LHS < CD / |V| ^ .5
Success: existence proven