show/hide visualization coordinates
a : (0.6815578579500001, 0.6672437704624999, 0.52405819526875)
b : (1.09262627855, -0.23060551063749996, 0.68182223796875)
c : (0.7058004442500001, -0.008067683537499981, -0.21307587203125006)
d : (0.005848742249999983, 0.7061218078625001, -0.21208431503125003)
e : (-0.28318758285, 0.8198963558625, 0.73844890276875)
f : (0.12324443255, -0.08304880163749995, 0.87810223536875)
g : (0.50833054855, -1.0047140758375, 0.92544989566875)
h : (0.92190879815, -0.9571292887375, 0.016225660268749942)
i : (0.35207187614999996, -0.7523281589374999, -0.77960248293125)
j : (0.20066045144999994, 0.19812026386250003, -1.05112122453125)
k : (-0.69670535775, 0.6189624922625, -0.91835696153125)
l : (-0.94487373025, 0.9346029947625, -0.0025057337312500705)
m : (-0.68571284825, 0.016971917762500066, 0.29880614066875)
n : (-0.045250655750000035, -0.7339708996375, 0.13789292016875)
o : (-0.53963566645, -0.3253876140375, -0.62933792423125)
p : (-1.39668358855, 0.13333243016250007, -0.39472167413125003)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['c', 'j', 'i'], ['p', 'o', 'm'], ['k', 'p', 'l'], ['o', 'n', 'i'], ['c', 'h', 'i'], ['d', 'a', 'e'], ['a', 'c', 'b'], ['a', 'f', 'b'], ['o', 'j', 'i'], ['f', 'm', 'n'], ['h', 'g', 'n'], ['o', 'm', 'n'], ['f', 'e', 'm'], ['k', 'o', 'p'], ['p', 'm', 'l'], ['d', 'j', 'k'], ['h', 'n', 'i'], ['b', 'f', 'g'], ['d', 'a', 'c'], ['b', 'g', 'h'], ['f', 'g', 'n'], ['d', 'e', 'l'], ['a', 'e', 'f'], ['e', 'm', 'l'], ['d', 'c', 'j'], ['b', 'h', 'c'], ['d', 'k', 'l'], ['k', 'j', 'o']]
Coordinate Data:
n : [4198187441 / 10000000000, -15926499 / 156250000, 1284235427 / 2000000000]
j : [6657298513 / 10000000000, 8301615699 / 10000000000, -683620539 / 1250000000]
o : [-372831333 / 5000000000, 76663423 / 250000000, -1251131309 / 10000000000]
p : [-9316141887 / 10000000000, 3826868681 / 5000000000, 136878899 / 1250000000]
k : [-2316359579 / 10000000000, 12510037983 / 10000000000, -2070660841 / 5000000000]
e : [181881817 / 1000000000, 14519376619 / 10000000000, 12426736961 / 10000000000]
g : [2433499871 / 2500000000, -1863363849 / 5000000000, 1429674689 / 1000000000]
b : [973559799 / 625000000, 2007178977 / 5000000000, 11860470313 / 10000000000]
m : [-551608621 / 2500000000, 3245066119 / 5000000000, 401515467 / 500000000]
l : [-599755413 / 1250000000, 61197043 / 39062500, 1254297649 / 2500000000]
d : [4709181421 / 10000000000, 13381631139 / 10000000000, 2921404783 / 10000000000]
c : [11708698441 / 10000000000, 249589449 / 400000000, 2911489213 / 10000000000]
a : [5733136289 / 5000000000, 2598570153 / 2000000000, 5141414943 / 5000000000]
i : [204285319 / 250000000, -1202868529 / 10000000000, -10756941 / 39062500]
h : [693489099 / 500000000, -3250879827 / 10000000000, 650563067 / 1250000000]
f : [1470784581 / 2500000000, 1372481261 / 2500000000, 13823270287 / 10000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 16
|E| = 42
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 132343377631178054605730701429684838408031924082699181001 / 241340418400162768219738229514386841551708984375000000000
Collision distance in [74051877 / 100000000, 37025939 / 50000000] ~ [0.74052, 0.74052]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [561 / 1250, 449 / 1000] ~ [0.4488, 0.449]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 460775466322105989386951909 / 5000000000000000000000000000000000000000
rho in [303570573 / 1000000000000000, 313570573 / 1000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [69938 / 36004115, 5040025 / 2592296276] ~ [0.00194, 0.00194]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-3299 / 20000000, 23623 / 100000000] ~ [-0.00016, 0.00024]
LHS DEN := 8 * |E| ^ .5 in [648074069 / 12500000, 64807407 / 1250000] ~ [51.84593, 51.84593]
LHS := (LHS NUM) / (LHS DEN) in [-16495 / 5184592552, 23623 / 5184592552] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [74051877 / 400000001, 37025939 / 200000000] ~ [0.18513, 0.18513]
Success: LHS < CD / |V| ^ .5
Success: existence proven