show/hide visualization coordinates
a : (0.5724575999797374, 0.5940278754380506, 0.6496634788825081)
b : (0.37055391277591365, 1.2409566840730524, -0.08567183079029528)
c : (-0.22192546529388235, 1.197504333167931, 0.7187410481237894)
d : (-0.28515840925065594, 0.24989479800564213, 1.0318508749706492)
e : (0.5573397650191716, -0.27809985402568566, 1.1387081338645797)
f : (1.313478674397762, -0.06482125977609382, 0.5200271248149451)
g : (0.965852080831789, 0.45644749803126766, -0.2593538048848315)
h : (0.15420460772953914, 0.603080830118883, -0.8247979182396491)
i : (-0.5504523367651076, 0.8591769191587835, -0.16307789908204828)
j : (-1.0931414772915335, 0.7097278456162257, 0.663453087131996)
k : (-1.1310965021681465, -0.2638250177651751, 0.8887401002696625)
l : (-0.24694779054974214, -0.6993185879091506, 0.7195467017377767)
m : (0.6431955195853107, -0.7629391613685157, 0.2683291155839206)
n : (1.3286809388474807, -0.4653132270752996, -0.3961470263617909)
o : (0.8955570406121995, 0.019410399224248642, -1.1560461610398676)
p : (-0.051591601636437, -0.18815482433413605, -1.4006399619746461)
q : (-0.79511011308445, 0.3257667276068981, -0.972779165003657)
r : (-1.0969054356948855, 0.027173655290717247, -0.06737220655058268)
s : (-1.0399616074674425, -0.9445282490577012, 0.16187178903591148)
t : (-0.13278356471063507, -1.288623557654265, -0.08025713807062718)
u : (0.4162117641137527, -0.7335159513276273, -0.7051248635352352)
v : (-0.5724575999797373, -0.5940278754380506, -0.6496634788825081)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['q', 'i', 'h'], ['j', 'i', 'c'], ['d', 'j', 'k'], ['v', 'q', 'p'], ['n', 'f', 'm'], ['j', 'r', 'i'], ['n', 'o', 'u'], ['v', 's', 'r'], ['n', 'f', 'g'], ['v', 't', 's'], ['u', 'n', 'm'], ['b', 'i', 'h'], ['f', 'a', 'g'], ['u', 'p', 'v'], ['q', 'p', 'h'], ['d', 'j', 'c'], ['b', 'g', 'h'], ['l', 't', 's'], ['o', 'g', 'h'], ['q', 'r', 'i'], ['s', 'k', 'r'], ['n', 'o', 'g'], ['b', 'i', 'c'], ['a', 'g', 'b'], ['l', 'd', 'k'], ['l', 'k', 's'], ['d', 'e', 'a'], ['l', 't', 'm'], ['j', 'k', 'r'], ['d', 'a', 'c'], ['v', 'q', 'r'], ['v', 't', 'u'], ['u', 't', 'm'], ['a', 'b', 'c'], ['o', 'p', 'h'], ['u', 'o', 'p'], ['e', 'a', 'f'], ['e', 'f', 'm'], ['l', 'e', 'm'], ['l', 'd', 'e']]
Coordinate Data:
e : [26274654644073580251 / 25000000000000000000, 730399816148844519 / 5000000000000000000, 158538096754475313187 / 100000000000000000000]
n : [728930943836500901 / 400000000000000000, -1028335245496125387 / 25000000000000000000, 2526290365919136847 / 50000000000000000000]
t : [36086285603313654801 / 100000000000000000000, -43222187019940527057 / 50000000000000000000, 18320784780477322961 / 50000000000000000000]
i : [-2840295801066799913 / 50000000000000000000, 4010489801294493429 / 3125000000000000000, 28359493459812537009 / 100000000000000000000]
h : [12957020569466216401 / 20000000000000000000, 102726064737433742323 / 100000000000000000000, -1181640889248360793 / 3125000000000000000]
q : [-15073184617033917923 / 50000000000000000000, 14998930897247053981 / 20000000000000000000, -52610633132348338857 / 100000000000000000000]
u : [3639432739430097421 / 4000000000000000000, -3093361340721726571 / 10000000000000000000, -25845202985506154807 / 100000000000000000000]
s : [-27315759336183543399 / 50000000000000000000, -52034843180224661029 / 100000000000000000000, 30427231135804258079 / 50000000000000000000]
d : [20848801149311565239 / 100000000000000000000, 16851865381527416327 / 25000000000000000000, 147852370865082303633 / 100000000000000000000]
v : [-3940558961798284237 / 50000000000000000000, -135878446546076867 / 800000000000000000, -10149532260116722067 / 50000000000000000000]
o : [138920346135597121221 / 100000000000000000000, 1774360865918812849 / 4000000000000000000, -70937332735969401591 / 100000000000000000000]
r : [-12065180299022279943 / 20000000000000000000, 11283836813654294741 / 25000000000000000000, 37930062712959092333 / 100000000000000000000]
p : [22102740955366731169 / 50000000000000000000, 23602499292131852209 / 100000000000000000000, -95396712829447242269 / 100000000000000000000]
a : [106610402072350901563 / 100000000000000000000, 25455192317337627369 / 25000000000000000000, 54816815628134085677 / 50000000000000000000]
k : [-63745008142437502859 / 100000000000000000000, 16035479949027950961 / 100000000000000000000, 66770646697491813013 / 50000000000000000000]
c : [27172095544988926929 / 100000000000000000000, 81084207521169268341 / 50000000000000000000, 116541388180396305943 / 100000000000000000000]
m : [113684194032908234143 / 100000000000000000000, -16937967205653060237 / 50000000000000000000, 1787504873160235513 / 2500000000000000000]
b : [17284006670393705239 / 20000000000000000000, 20814206266606337001 / 12500000000000000000, 18050050144493917081 / 50000000000000000000]
j : [-59949505654776177461 / 100000000000000000000, 7086922892948001971 / 6250000000000000000, 111012592081216956283 / 100000000000000000000]
l : [24669863019402949829 / 100000000000000000000, -137569385326848047 / 500000000000000000, 116621953541795042259 / 100000000000000000000]
f : [90356254757076681843 / 50000000000000000000, 8983963936984018579 / 25000000000000000000, 12083749481188984323 / 12500000000000000000]
g : [145949850157556065089 / 100000000000000000000, 220156828821680559 / 250000000000000000, 9365951439767106619 / 50000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 33023422696745149649042370755946471011753686767398260512851702692604572188315804362408129823167864160907266632804591041 / 50688104787495193347839335208649990345578414947562997012594056450271064946266422500000000000000000000000000000000000000
Collision distance in [807156995456309788769913053703 / 1000000000000000000000000000000, 100894624432038723596239131713 / 125000000000000000000000000000] ~ [0.80716, 0.80716]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [87 / 200, 272 / 625] ~ [0.435, 0.4352]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 138012816064538295272647551511457778729437 / 4000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [464375952328327490842713640341 / 2500000000000000000000000000000000000000000000000, 464375952330827490842713640341 / 2500000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [2365312500000000000000000000 / 1549193338482966754071706159913, 2959360000000000000000000000 / 1936491673103708442589632699891] ~ [0.00153, 0.00153]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999973551171621371 / 1000000000000000000000000000000, 50000000000006615247189909 / 250000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [1936491673103708442589632699891 / 31250000000000000000000000000, 1549193338482966754071706159913 / 25000000000000000000000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-66666666666657850390540457 / 20655911179772890054289415465504, 5555555555556290583021101 / 1721325931647740837857451288792] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [807156995456309788769913053703 / 4690415759823429554565630113545, 100894624432038723596239131713 / 586301969977928694320703764193] ~ [0.17209, 0.17209]
Success: LHS < CD / |V| ^ .5
Success: existence proven