show/hide visualization coordinates
a : (1.9867819149329193, -1.4789632461719107, -0.7165459125467794)
b : (1.7768581256152929, -0.5022148044920528, -0.6730202378880422)
c : (2.719569374375527, -0.8164956133162776, -0.5611136935498696)
d : (2.9085296038880695, -1.6638157030076557, -1.0574429162115648)
e : (2.7241224278436817, -1.6903522272814948, -0.07495128454094424)
f : (2.0451195408800156, -0.9933916881721331, 0.15570232245316928)
g : (1.1529370132432917, -1.1665508792411199, -0.26146219177123187)
h : (0.7946291327320281, -0.3163243243821777, -0.6471178259531013)
i : (1.3298278715594807, -0.2958083350982934, 0.19735917440937611)
j : (0.40807121940790747, -0.6835742213223414, 0.19887300901140414)
k : (-0.17108421287308878, -0.1689598340118892, -0.43338565453738453)
l : (0.5354151358896524, 0.3027462920392451, 0.09420509674968458)
m : (-0.279694371115714, -0.050200851147812586, 0.5535794601022374)
n : (-1.0703654261981927, 0.044011890682311594, -0.05136949801870205)
o : (-0.3516468514740077, 0.7392979592420369, -0.05594040746837914)
p : (-0.9633868863188542, 0.6576991665295798, 0.7308986909474886)
q : (-1.8779025156784606, 0.4024250980884006, 0.4170574673351486)
r : (-1.3105717382116557, 1.010873528783765, -0.13785360312863237)
s : (-1.6975420006077875, 1.3366533049188518, 0.7247712014547052)
t : (-2.6023627948767865, 0.9322468207751358, 0.8580180619840854)
u : (-2.2939572833464155, 1.1756021213310983, -0.061581980506674405)
v : (-2.5180055368755325, 1.8939097332616566, 0.5970807212862622)
w : (-3.2453417427913687, 1.3311858119930755, 0.2042400003877436)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['l', 'o', 'k'], ['r', 's', 'u'], ['i', 'f', 'g'], ['r', 'p', 'o'], ['i', 'h', 'l'], ['t', 'w', 'v'], ['p', 'm', 'n'], ['t', 's', 'q'], ['a', 'b', 'g'], ['a', 'f', 'e'], ['o', 'n', 'k'], ['i', 'j', 'l'], ['i', 'j', 'g'], ['r', 'u', 'q'], ['p', 'm', 'o'], ['a', 'b', 'c'], ['h', 'b', 'g'], ['h', 'j', 'g'], ['t', 'w', 'u'], ['d', 'e', 'c'], ['p', 's', 'q'], ['d', 'a', 'e'], ['a', 'f', 'g'], ['r', 'n', 'o'], ['q', 'p', 'n'], ['d', 'a', 'c'], ['v', 'w', 'u'], ['m', 'o', 'l'], ['m', 'n', 'k'], ['p', 's', 'r'], ['t', 'u', 'q'], ['h', 'k', 'j'], ['i', 'h', 'b'], ['k', 'm', 'j'], ['s', 'u', 'v'], ['e', 'f', 'c'], ['q', 'r', 'n'], ['t', 's', 'v'], ['i', 'b', 'f'], ['l', 'm', 'j'], ['h', 'l', 'k'], ['b', 'f', 'c']]
Coordinate Data:
u : [138605031562180814791 / 50000000000000000000, -29523303795815566261 / 50000000000000000000, 63804080436612551951 / 100000000000000000000]
b : [-6493573888590459379 / 5000000000000000000, 108735084990683982197 / 100000000000000000000, 62473953087374663693 / 50000000000000000000]
j : [700721284892934839 / 10000000000000000000, 25374205334742567129 / 20000000000000000000, 7551716296960940261 / 20000000000000000000]
r : [89435754305442838159 / 50000000000000000000, -42573748336897775361 / 100000000000000000000, 71431242698808355401 / 100000000000000000000]
w : [14893940362754278289 / 4000000000000000000, -7460497665782883237 / 10000000000000000000, 3722188234717075617 / 10000000000000000000]
n : [154850877409539372509 / 100000000000000000000, 54112415473247539391 / 100000000000000000000, 31391416093907658793 / 50000000000000000000]
i : [-42584226183113989477 / 50000000000000000000, 88094438051308046733 / 100000000000000000000, 4738745618125937817 / 12500000000000000000]
f : [-156697619298281460633 / 100000000000000000000, 19731596669836502423 / 12500000000000000000, 4207565014062818663 / 10000000000000000000]
a : [-75431928351785919151 / 50000000000000000000, 41281985831733951941 / 20000000000000000000, 25860094728124608603 / 20000000000000000000]
p : [36038255855401377363 / 25000000000000000000, -7256312111479275421 / 100000000000000000000, -15443986708803747637 / 100000000000000000000]
c : [-56035650661958145003 / 25000000000000000000, 2190049466767288533 / 1562500000000000000, 113757251740932067041 / 100000000000000000000]
m : [2368242871915359121 / 3125000000000000000, 63533689656259962713 / 100000000000000000000, 571984093930343719 / 25000000000000000000]
h : [-31648578483482702163 / 100000000000000000000, 5634127311231029497 / 6250000000000000000, 122357664981255236189 / 100000000000000000000]
g : [-2108730204206533677 / 3125000000000000000, 43792173116397677019 / 25000000000000000000, 83792101563068304313 / 100000000000000000000]
e : [-224597907994648065051 / 100000000000000000000, 227548827269628181269 / 100000000000000000000, 65141010840039537071 / 100000000000000000000]
t : [308050614277398764887 / 100000000000000000000, -17355538768017435343 / 50000000000000000000, -7038980953115855013 / 25000000000000000000]
l : [-1431794699811286039 / 25000000000000000000, 2823897533755419481 / 10000000000000000000, 24112686355488327853 / 50000000000000000000]
o : [20744754984280217579 / 25000000000000000000, -770809569136249147 / 5000000000000000000, 31619961566391512737 / 50000000000000000000]
q : [29450573294695771067 / 12500000000000000000, 3654218946527728403 / 20000000000000000000, 15940135652430258091 / 100000000000000000000]
s : [108784267425249431847 / 50000000000000000000, -75151725950406478569 / 100000000000000000000, -1853904719940675877 / 12500000000000000000]
d : [-60759656399771715403 / 25000000000000000000, 28111896855280531501 / 12500000000000000000, 163390174007101578121 / 100000000000000000000]
k : [64922756077028980339 / 100000000000000000000, 75409587942667621533 / 100000000000000000000, 12623055979960444949 / 12500000000000000000]
v : [74903722119318334227 / 25000000000000000000, -10224794436303669 / 7812500000000000, -206218974268110817 / 10000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 23
|E| = 63
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 499999999999999999959428686337487354950855857810413543498934657447058047661016976023376166113835623142498938380476830009 / 999999999999999999996100779369946923544722635151222873980587956975920796281085020000000000000000000000000000000000000000
Collision distance in [353553390593273762186767346883 / 500000000000000000000000000000, 707106781186547524373534693767 / 1000000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [2119 / 10000, 2121 / 10000] ~ [0.2119, 0.2121]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 30028100740139606033369588431193920070303 / 781250000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1960509345741016755194860213153 / 10000000000000000000000000000000000000000000000000, 1960509345751016755194860213153 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [107936562500000000000000000 / 305278997430529683519417202343, 937216875000000000000000000 / 2645751311064590590501615753639] ~ [0.00035, 0.00035]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-39999999999988261340488037 / 200000000000000000000000000000, 12500000000003671793420393 / 62500000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [7937253933193771771504847260917 / 125000000000000000000000000000, 3968626966596885885752423630459 / 62500000000000000000000000000] ~ [63.49803, 63.49803]
LHS := (LHS NUM) / (LHS DEN) in [-199999999999941306702440185 / 63498031465550174172038778087336, 25000000000007343586840786 / 7937253933193771771504847260917] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524373534693766 / 4795831523312719541597438064163, 707106781186547524373534693767 / 4795831523312719541597438064162] ~ [0.14744, 0.14744]
Success: LHS < CD / |V| ^ .5
Success: existence proven