show/hide visualization coordinates
a : (0.9324827479804589, -0.5741887368487046, -1.9873957712123196)
b : (1.1868904790325312, -0.05663882661702935, -1.1704387363566784)
c : (1.8844985881877545, -0.5585417228529757, -1.681747262386553)
d : (1.673422057725945, -0.6339303812256205, -2.656305238331021)
e : (1.4894533408067365, -1.402794574021963, -2.0439300557584996)
f : (1.1975343935906881, -1.0564196412568083, -1.152410154573894)
g : (0.32677315888136443, -0.5662897469620525, -1.1917491790420416)
h : (0.39489643592252904, 0.27754943239838337, -0.6594948615382015)
i : (0.8749826063559302, -0.5453767397085556, -0.35566960876942316)
j : (-0.12245567825931536, -0.49943920956445387, -0.3008370298764325)
k : (-0.40123826760396675, 0.43396937873937647, -0.07494175511633028)
l : (0.43817575046473145, 0.054778735712301796, 0.3144148455860037)
m : (-0.4519085661882295, -0.28467682914023373, 0.6185855686003621)
n : (-1.1097347800766364, 0.46840745275740464, 0.6299317873520993)
o : (-0.15419171062566117, 0.6354867331054169, 0.8728761359231227)
p : (-0.7426517703230513, 0.11217552574234874, 1.4892040830333864)
q : (-1.6712728393043548, 0.4818285660346502, 1.4572738458485635)
r : (-0.8858102744953364, 1.0953899702103471, 1.3760891022720436)
s : (-1.090088476005192, 0.6578552552341594, 2.251779566750563)
t : (-2.0809612398533863, 0.5829816896869187, 2.3638737907145253)
u : (-1.6887959562135377, 1.3778736685770892, 1.900890926880727)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['l', 'j', 'i'], ['s', 'u', 't'], ['p', 'n', 'q'], ['c', 'f', 'e'], ['c', 'b', 'a'], ['b', 'g', 'h'], ['c', 'e', 'd'], ['o', 'n', 'k'], ['p', 's', 'q'], ['q', 'n', 'r'], ['u', 'q', 'r'], ['h', 'l', 'i'], ['h', 'g', 'j'], ['p', 'm', 'o'], ['o', 'n', 'r'], ['h', 'j', 'k'], ['p', 'm', 'n'], ['c', 'a', 'd'], ['e', 'a', 'd'], ['p', 's', 'r'], ['f', 'e', 'a'], ['b', 'g', 'a'], ['o', 'l', 'm'], ['m', 'n', 'k'], ['m', 'j', 'k'], ['g', 'f', 'a'], ['p', 'o', 'r'], ['u', 't', 'q'], ['i', 'b', 'h'], ['c', 'b', 'f'], ['m', 'l', 'j'], ['o', 'l', 'k'], ['g', 'i', 'j'], ['b', 'f', 'i'], ['s', 't', 'q'], ['s', 'u', 'r'], ['h', 'l', 'k'], ['g', 'f', 'i']]
Coordinate Data:
b : [-39901835395921691583 / 50000000000000000000, 1582445941448873851 / 3125000000000000000, 78202355756579310971 / 50000000000000000000]
m : [420381168651163443 / 500000000000000000, 36721035189342198069 / 50000000000000000000, -22497718982545424803 / 100000000000000000000]
g : [6208061223273293569 / 100000000000000000000, 10160336216086627861 / 10000000000000000000, 79267877890847476631 / 50000000000000000000]
a : [-3397681105414760117 / 6250000000000000000, 25598315287382870353 / 25000000000000000000, 238100414998722748203 / 100000000000000000000]
c : [-74782240853682854701 / 50000000000000000000, 20165711949991718517 / 20000000000000000000, 51883891029036522501 / 25000000000000000000]
k : [39504601935903206613 / 50000000000000000000, 394362397680843989 / 25000000000000000000, 46855013389123807061 / 100000000000000000000]
t : [123490750548374199009 / 50000000000000000000, -6661890752015418829 / 50000000000000000000, -39405308238792350227 / 20000000000000000000]
s : [147894224711928934877 / 100000000000000000000, -20811138058754917441 / 100000000000000000000, -185817118797565516611 / 100000000000000000000]
u : [103882486366381747381 / 50000000000000000000, -46406489696523945277 / 50000000000000000000, -37682063702645479501 / 25000000000000000000]
i : [-48612883524183283663 / 100000000000000000000, 49756030717758293957 / 50000000000000000000, 74927798754433098437 / 100000000000000000000]
l : [-4932197935063411873 / 100000000000000000000, 39496513893430846323 / 100000000000000000000, 3959676659445205359 / 50000000000000000000]
q : [41202532208369046141 / 20000000000000000000, -3208469138803992917 / 100000000000000000000, -106366546707365565711 / 100000000000000000000]
o : [54304548173975850281 / 100000000000000000000, -371485716917613257 / 2000000000000000000, -2995423482176343617 / 6250000000000000000]
p : [11315055414371486599 / 10000000000000000000, 16878417445213076397 / 50000000000000000000, -10955957042584785849 / 10000000000000000000]
n : [29971771023814675989 / 20000000000000000000, -933178905539720081 / 50000000000000000000, -11816170428859577233 / 50000000000000000000]
d : [-64228414330592390011 / 50000000000000000000, 54183712793611536101 / 50000000000000000000, 304991361710592852961 / 100000000000000000000]
r : [25493280912188675109 / 20000000000000000000, -32282304778186848141 / 50000000000000000000, -19649614469942716483 / 20000000000000000000]
h : [-604266480843170131 / 100000000000000000000, 8609722112411345511 / 50000000000000000000, 52655162015655460503 / 50000000000000000000]
f : [-80868062247659078709 / 100000000000000000000, 37654087897585465537 / 25000000000000000000, 38650463333720048689 / 25000000000000000000]
e : [-110059956969263916823 / 100000000000000000000, 185253844866857327529 / 100000000000000000000, 243753843453340733367 / 100000000000000000000]
j : [51130944937341276349 / 100000000000000000000, 47459154210553204231 / 50000000000000000000, 2777781634605361061 / 4000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 21
|E| = 57
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 124999999999999999991934890990158057428217026602228579453715738962917919830147301737131473996613275739693669172034486209 / 250000000000000000005940491636035316420036106010723671977072815023256307956408675000000000000000000000000000000000000000
Collision distance in [353553390593273762184815832589 / 500000000000000000000000000000, 707106781186547524369631665179 / 1000000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [2479 / 10000, 2481 / 10000] ~ [0.2479, 0.2481]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 630087585093855383050588495557268396581747 / 25000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1587561129649948796642500984279 / 10000000000000000000000000000000000000000000000000, 1587561129659948796642500984279 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [3840900625000000000000000000 / 7549834435270749697236684806947, 641183437500000000000000000 / 1258305739211791616206114134491] ~ [0.00051, 0.00051]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999961351636647389 / 1000000000000000000000000000000, 200000000000038679543960643 / 1000000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [3774917217635374848618342403473 / 62500000000000000000000000000, 7549834435270749697236684806947 / 125000000000000000000000000000] ~ [60.39868, 60.39868]
LHS := (LHS NUM) / (LHS DEN) in [-66666666666653783878882463 / 20132891827388665859297826151856, 66666666666679559847986881 / 20132891827388665859297826151856] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524369631665178 / 4582575694955840006588047193729, 707106781186547524369631665179 / 4582575694955840006588047193728] ~ [0.1543, 0.1543]
Success: LHS < CD / |V| ^ .5
Success: existence proven