show/hide visualization coordinates
a : (0.000669572370317173, 0.4458031703270655, 0.06863253690922777)
b : (0.8666948347928061, 0.36845281952208, 0.5626134758900805)
c : (0.8653239723068007, 0.45475097884063986, -0.43365493595196564)
d : (-0.0007012901156882023, 0.5321013296456253, -0.9276358749328184)
e : (-0.8653556900521717, 0.523153521132051, -0.42534840207162494)
f : (-0.8641816687210421, 0.3057979664001834, 0.5507433889506723)
g : (0.0018435937014468218, 0.22844761559519788, 1.044724327931525)
h : (0.8665952812062407, 0.0027048057729442965, 1.4933273849553987)
i : (1.4763635580054972, -0.3868463276981507, 0.8030864393279675)
j : (1.711312033486255, 0.2240905451217513, 0.047073640958583685)
k : (0.9992982201921932, -0.46789878984753164, -0.07203593030761746)
l : (0.4992987098843118, -0.3339240741388133, -0.9276358749328184)
m : (-0.5007012901156882, -0.3339240741388133, -0.9276358749328184)
n : (-0.8659089162488849, 0.4542789163089177, -1.4229735735419686)
o : (-1.4771293958337304, -0.12305065568683418, -0.8815863824898775)
p : (-1.710625668528899, 0.2328931769601107, 0.023280170454846538)
q : (-1.0006993313491321, -0.4649649653400902, -0.07158082787340514)
r : (-0.5006954138236939, -0.5960053431843368, 0.7844708655620156)
s : (0.49930017895874923, -0.5989396810488086, 0.7840191167517958)
t : (-0.0007012901156882023, -0.4669209345431885, -0.07188367065720036)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['d', 'm', 'n'], ['c', 'k', 'j'], ['o', 'm', 'n'], ['t', 'm', 'l'], ['c', 'd', 'a'], ['d', 'e', 'a'], ['t', 's', 'k'], ['b', 'a', 'g'], ['f', 'e', 'p'], ['s', 'i', 'k'], ['f', 'e', 'a'], ['t', 'r', 'q'], ['c', 'd', 'l'], ['d', 'e', 'n'], ['t', 'q', 'm'], ['j', 'b', 'i'], ['h', 'b', 'g'], ['t', 'k', 'l'], ['p', 'o', 'q'], ['f', 'a', 'g'], ['t', 's', 'r'], ['c', 'b', 'a'], ['f', 'p', 'q'], ['c', 'b', 'j'], ['f', 'r', 'q'], ['d', 'm', 'l'], ['b', 'i', 'h'], ['e', 'o', 'n'], ['f', 'r', 'g'], ['s', 'h', 'g'], ['e', 'p', 'o'], ['s', 'r', 'g'], ['s', 'i', 'h'], ['o', 'q', 'm'], ['c', 'k', 'l'], ['k', 'i', 'j']]
Coordinate Data:
m : [1240204573212442176853925998607 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000, 14352829594534117806751019823 / 2000000000000000000000000000000000000000000000000000000000000000000000000000000000000000, -3055503637714103499638242468087 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
k : [1499999510307881412209368290569 / 1000000000000000000000000000000, -133974715708718321871232761413 / 1000000000000000000000000000000, 85559994462520092752046364047 / 100000000000000000000000000000]
s : [1000001469074437378282675255081 / 1000000000000000000000000000000, -53003121381999042038466561723 / 200000000000000000000000000000, 68466199667384568946483478851 / 40000000000000000000000000000]
g : [502544883817134970638579979889 / 1000000000000000000000000000000, 562371689734011156466044248137 / 1000000000000000000000000000000, 493090050716085871641467907013 / 250000000000000000000000000000]
j : [2212013323601943307322565361899 / 1000000000000000000000000000000, 4359489212973161393378138511 / 7812500000000000000000000000, 97470951589140204843236767979 / 100000000000000000000000000000]
f : [-363480378605353895469223757191 / 1000000000000000000000000000000, 639722040538996680007246909773 / 1000000000000000000000000000000, 295675852776698147043165422721 / 200000000000000000000000000000]
l : [1, -3264344261734102662830722663457 / 500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000, -1958119842040839934089138137941 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
b : [273479224981698854584567546283 / 200000000000000000000000000000, 5487319481725729007569324679 / 7812500000000000000000000000, 372562337705724731642838604097 / 250000000000000000000000000000]
d : [1 / 2, 13531646934131853855683174543 / 15625000000000000000000000000, 1543355015073658074549123058557 / 500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
n : [-182603813066598306565473278291 / 500000000000000000000000000000, 197050747611932758560067124543 / 250000000000000000000000000000, -247668849304575093059644724703 / 500000000000000000000000000000]
r : [117525839887307567570183 / 20000000000000000000000000000, -65520317261380869635525399483 / 250000000000000000000000000000, 1712106740494834100399661339869 / 1000000000000000000000000000000]
p : [-1209924378413210876548074708609 / 1000000000000000000000000000000, 283408625549462002872078412217 / 500000000000000000000000000000, 950916045387664925220363683939 / 1000000000000000000000000000000]
a : [100274172497201081363006798867 / 200000000000000000000000000000, 194931811116469709127519055137 / 250000000000000000000000000000, 996268411842046175221309901941 / 1000000000000000000000000000000]
t : [1 / 2, -66498430202187578986783639169 / 500000000000000000000000000000, 855752204275618063856916804653 / 1000000000000000000000000000000]
e : [-72930879987296691858553948549 / 200000000000000000000000000000, 107134699408858045006409860273 / 125000000000000000000000000000, 100457494572238684774253077499 / 200000000000000000000000000000]
i : [1977064848121185407068762314411 / 1000000000000000000000000000000, -26461126779668687401710318989 / 500000000000000000000000000000, 1730722314260785840250932252793 / 1000000000000000000000000000000]
o : [-195285621143608424598893073173 / 200000000000000000000000000000, 52718354612994778895034733751 / 250000000000000000000000000000, 46049492442940882155729079057 / 1000000000000000000000000000000]
q : [-15624938788545126060209157359 / 31250000000000000000000000000, -131040891201276888321100047201 / 1000000000000000000000000000000, 171211009411882659228324666161 / 200000000000000000000000000000]
c : [34150631560562221652695093427 / 25000000000000000000000000000, 788675052979453123222520509117 / 1000000000000000000000000000000, 246990469490426375675022257223 / 500000000000000000000000000000]
h : [85456035707620565244089825617 / 62500000000000000000000000000, 336628879911757629856290055671 / 1000000000000000000000000000000, 151310203743013572485751300821 / 62500000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 20
|E| = 54
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 3655250641005789138232089057166904572758791687298993174886403057351213836303412712471905911633076919533914652667008521 / 6919633691011516044417773430067514085049069089500973478595743386265247613229816250000000000000000000000000000000000000
Collision distance in [363401765619141696072843863277 / 500000000000000000000000000000, 145360706247656678429137545311 / 200000000000000000000000000000] ~ [0.7268, 0.7268]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [17 / 5000, 9 / 2500] ~ [0.0034, 0.0036]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 75842941544516093790532724355083268130597962903420806985269513247103758667826800693397091544851905612915129704666943530016149644523148625000239112377898829434373686312599227555961490263613560449810711163107972930016645680677244981150790154302852882393408156814681170277362319223359868695492862697209409175770232725659685213666591459730688514583694468471955764769856943124150936204846090678459648832964705882945845193484306534163067887172321662535898134426473 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [4354392654105624343589803487071 / 500000000000000000000000000000000000000000000000000000000000, 4854392654105624343589803487071 / 500000000000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [361250000000000000000000 / 3674234614174767147295926112059, 810000000000000000000000 / 7348469228349534294591852224117] ~ [0.0, 0.0]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-1 / 5000, 2000001 / 10000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [7348469228349534294591852224117 / 125000000000000000000000000000, 3674234614174767147295926112059 / 62500000000000000000000000000] ~ [58.78775, 58.78775]
LHS := (LHS NUM) / (LHS DEN) in [-25000000000000000000000000 / 7348469228349534294591852224117, 25000012500000000000000000 / 7348469228349534294591852224117] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [726803531238283392145687726554 / 4472135954999579392818347337463, 726803531238283392145687726555 / 4472135954999579392818347337462] ~ [0.16252, 0.16252]
Success: LHS < CD / |V| ^ .5
Success: existence proven