show/hide visualization coordinates
a : (-0.02329247488749997, 0.63445982295, -0.5815018576375)
b : (0.6083484222125, -0.007168442549999987, -1.0166371703375)
c : (-0.3443381756875, 0.03807760734999999, -1.3172048491375)
d : (-0.8085882671875, 0.03378151844999999, -0.43151072253749995)
e : (-0.6819615960875, 0.8436533632500001, 0.1412636100625)
f : (0.2799809309125, 1.09230847235, 0.25420489446250005)
g : (0.9481440920124999, 0.6509760368499999, -0.3447835511374999)
h : (0.6771219405125, -0.26639364615, -0.053272268837499914)
i : (-0.0727079959875, -0.61842009175, -0.6134804825375)
j : (-0.7839915362875, -0.84040505515, 0.05345393506250007)
k : (-1.0290044481875, -0.003661984249999972, 0.5431786666625)
l : (-0.05845780138750001, 0.22504321745, 0.6194328524625001)
m : (0.9217460815125, 0.42303052264999996, 0.6285329318625001)
n : (0.5901268848125001, -0.47382551615, 0.9211004709625001)
o : (0.16942489551249995, -1.07565245005, 0.2422707756625)
p : (-0.3925509517875, -0.65580337525, 0.9549527649625)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['n', 'h', 'o'], ['c', 'b', 'i'], ['d', 'e', 'k'], ['f', 'e', 'l'], ['e', 'l', 'k'], ['l', 'p', 'k'], ['g', 'b', 'a'], ['d', 'e', 'a'], ['d', 'j', 'k'], ['f', 'g', 'm'], ['n', 'l', 'p'], ['n', 'm', 'l'], ['n', 'p', 'o'], ['f', 'g', 'a'], ['g', 'h', 'm'], ['f', 'e', 'a'], ['d', 'c', 'a'], ['j', 'i', 'o'], ['f', 'm', 'l'], ['c', 'b', 'a'], ['d', 'j', 'i'], ['d', 'c', 'i'], ['g', 'h', 'b'], ['j', 'p', 'k'], ['h', 'b', 'i'], ['n', 'h', 'm'], ['h', 'i', 'o'], ['j', 'p', 'o']]
Coordinate Data:
i : [3204797929 / 5000000000, -2496626893 / 10000000000, -298840683 / 5000000000]
k : [-394171083 / 1250000000, 1825477091 / 5000000000, 5484455063 / 5000000000]
j : [-140647909 / 2000000000, -4716476527 / 10000000000, 607166281 / 1000000000]
m : [16354136633 / 10000000000, 7917879251 / 10000000000, 5911226389 / 5000000000]
c : [3693294061 / 10000000000, 2034175049 / 5000000000, -954365629 / 1250000000]
l : [1638024451 / 2500000000, 5938006199 / 10000000000, 733215749 / 625000000]
h : [13907895223 / 10000000000, 1023637563 / 10000000000, 5004400771 / 10000000000]
f : [9936485127 / 10000000000, 3652664687 / 2500000000, 2019793101 / 2500000000]
o : [8830924773 / 10000000000, -1767237619 / 2500000000, 497489451 / 625000000]
d : [-474603427 / 5000000000, 4025389209 / 10000000000, 611008117 / 5000000000]
b : [330504001 / 250000000, 3615889599 / 10000000000, -1157312061 / 2500000000]
p : [32111663 / 100000000, -179403733 / 625000000, 15086651109 / 10000000000]
e : [317059857 / 10000000000, 12124107657 / 10000000000, 173743989 / 250000000]
a : [6903751069 / 10000000000, 5016086127 / 5000000000, -277895117 / 10000000000]
n : [6518972333 / 5000000000, -1050681137 / 10000000000, 14748128169 / 10000000000]
g : [8309058369 / 5000000000, 10197334393 / 10000000000, 522321987 / 2500000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 16
|E| = 42
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 2128875040044898059079011468724515474984239566198961448369 / 3852682156113536771240002767913852160600000000000000000000
Collision distance in [2973401 / 4000000, 37167513 / 50000000] ~ [0.74335, 0.74335]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [113 / 625, 181 / 1000] ~ [0.1808, 0.181]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 807742452468848402660226039485007 / 10000000000000000000000000000000000000000
rho in [1421 / 5000000, 28421 / 100000000] ~ [0.00028, 0.00028]
sigma_min ^ 2 / (16 * E ^ .5) in [102152 / 324037035, 819025 / 2592296276] ~ [0.00032, 0.00032]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [12342599 / 100000000, 497077 / 4000000] ~ [0.12343, 0.12427]
LHS DEN := 8 * |E| ^ .5 in [648074069 / 12500000, 64807407 / 1250000] ~ [51.84593, 51.84593]
LHS := (LHS NUM) / (LHS DEN) in [12342599 / 5184592560, 12426925 / 5184592552] ~ [0.00238, 0.0024]
CD / |V| ^ .5 in [74335025 / 400000001, 37167513 / 200000000] ~ [0.18584, 0.18584]
Success: LHS < CD / |V| ^ .5
Success: existence proven