show/hide visualization coordinates
a : (0.5938375048017844, -0.231085985069573, 0.7385178184835827)
b : (0.3153713037373438, -0.9380795126145993, 0.08842803478122463)
c : (0.7500134556985311, -0.09966492926590631, -0.24042936009805388)
d : (1.2275101361754812, 0.47557108230606204, 0.42372457621811965)
e : (0.2512831380635011, 0.6779680456254668, 0.501289499968201)
f : (-0.38586672161845886, -0.08645994095773213, 0.5997268385934168)
g : (-0.05973158761318342, -0.9354860816777409, 1.0154075895808168)
h : (-0.37181942161470755, -1.6151985783675524, 0.3516364650868842)
i : (-0.6119173408501263, -0.8791200139807791, -0.28124688611547516)
j : (0.17106775152273612, -0.6365851039666379, -0.8540567695377957)
k : (0.3060283983428853, 0.34007755497006475, -1.0211366140690161)
l : (0.956928242985552, 0.8533297131010545, -0.4617605201768712)
m : (0.9061883177093134, 1.4204169831761195, 0.3603328371139978)
n : (0.10986542138608524, 1.3356917433420792, -0.2385757356468617)
o : (-0.601500654378411, 0.6674389089575047, -0.020868465239088585)
p : (-1.2017302404533958, -0.13117314358622412, 0.0232136573521049)
q : (-0.9873998003719113, -0.8839913678777667, 0.6455698123220753)
r : (-0.7422159837804798, -1.616614729944907, 1.2805091050383939)
s : (-0.5971296523121444, -0.0028924483623000707, -0.7629174971330228)
t : (-0.47017188332430415, 0.9681054853525813, -0.9655125059932138)
u : (0.4413896158939089, 1.3177523188407836, -1.18185188052942)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['t', 'n', 'o'], ['r', 'h', 'q'], ['p', 'q', 'f'], ['g', 'r', 'q'], ['s', 'p', 'o'], ['c', 'b', 'a'], ['u', 'l', 'n'], ['g', 'r', 'h'], ['c', 'k', 'l'], ['j', 'b', 'i'], ['m', 'l', 'n'], ['m', 'd', 'e'], ['m', 'e', 'n'], ['p', 'o', 'f'], ['a', 'e', 'f'], ['g', 'b', 'a'], ['i', 'h', 'q'], ['j', 'i', 's'], ['e', 'n', 'o'], ['t', 'u', 'n'], ['m', 'd', 'l'], ['i', 'p', 's'], ['u', 'k', 'l'], ['d', 'a', 'e'], ['t', 'k', 's'], ['c', 'a', 'd'], ['g', 'b', 'h'], ['t', 's', 'o'], ['g', 'a', 'f'], ['b', 'h', 'i'], ['i', 'p', 'q'], ['f', 'e', 'o'], ['j', 'b', 'c'], ['j', 'c', 'k'], ['j', 'k', 's'], ['d', 'c', 'l'], ['t', 'k', 'u'], ['g', 'q', 'f']]
Coordinate Data:
c : [6748420912670024817 / 5000000000000000000, 43898435859227436321 / 100000000000000000000, 7742420653620309773 / 25000000000000000000]
s : [254107452332940113 / 100000000000000000000, 26787841974794028671 / 50000000000000000000, -5319782772253912633 / 25000000000000000000]
f : [2138040052170149709 / 10000000000000000000, 1413091709063901711 / 3125000000000000000, 57492651241814156137 / 50000000000000000000]
d : [22839760787636935719 / 12500000000000000000, 101422037016424273057 / 100000000000000000000, 48692538123049296327 / 50000000000000000000]
h : [22785130522076630743 / 100000000000000000000, -53827464525468597411 / 50000000000000000000, 90176265132975042537 / 100000000000000000000]
r : [-14254525694500594649 / 100000000000000000000, -107796544208672641991 / 100000000000000000000, 183063529128126022899 / 100000000000000000000]
o : [-22874094286714923 / 12500000000000000000, 4824352787262741243 / 4000000000000000000, 13231443025094442053 / 25000000000000000000]
l : [155659896982102586249 / 100000000000000000000, 27839580019184706399 / 20000000000000000000, 8836566606599502243 / 100000000000000000000]
a : [59675411581862916197 / 50000000000000000000, 15378165139430382791 / 50000000000000000000, 64432200236322444517 / 50000000000000000000]
t : [12949884351116965831 / 100000000000000000000, 18834434665134525107 / 12500000000000000000, -1038465799375868983 / 2500000000000000000]
k : [90569912517835920459 / 100000000000000000000, 43936342141412272201 / 50000000000000000000, -1177526069565374839 / 2500000000000000000]
m : [150585904454478721111 / 100000000000000000000, 39181325420686000567 / 20000000000000000000, 45522951167843199373 / 50000000000000000000]
e : [85095386489897495597 / 100000000000000000000, 60830866674182371633 / 50000000000000000000, 21028313724221345971 / 20000000000000000000]
b : [91504203057281760461 / 100000000000000000000, -39943022475641860871 / 100000000000000000000, 31927711051204542447 / 50000000000000000000]
p : [-12041190272358440093 / 20000000000000000000, 8149522885439130929 / 20000000000000000000, 7166748044937139073 / 12500000000000000000]
g : [53993913922229036763 / 100000000000000000000, -3968367938195602667 / 10000000000000000000, 39138344395592078199 / 25000000000000000000]
u : [104106034272938285451 / 100000000000000000000, 185640160669896430469 / 100000000000000000000, -3948285589290960287 / 6250000000000000000]
j : [1926846195895524959 / 2500000000000000000, -9793581610845730793 / 100000000000000000000, -15196529164746476373 / 50000000000000000000]
i : [-19135334397894441 / 1562500000000000000, -17023536306129923263 / 50000000000000000000, 1075517200509564393 / 4000000000000000000]
q : [-38772907353643740837 / 100000000000000000000, -8633552000489649697 / 25000000000000000000, 119569599856494159581 / 100000000000000000000]
n : [35476807411077954113 / 50000000000000000000, 937170515600129959 / 500000000000000000, 31155045059600456283 / 100000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 21
|E| = 57
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 31249999999999999998232083790826947538317171453920615485461302901664271027053508234738256249843109962935731554699485481 / 62499999999999999999827314257772304139073346480498695733900205508667682657396430625000000000000000000000000000000000000
Collision distance in [353553390593273762190909765769 / 500000000000000000000000000000, 707106781186547524381819531539 / 1000000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [943 / 2500, 1887 / 5000] ~ [0.3772, 0.3774]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 31582765766793531870677303975858542681667 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1777154066669334436483156832201 / 10000000000000000000000000000000000000000000000000, 1777154066679334436483156832201 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [216890000000000000000000000 / 184142303299286577981382556267, 1483653750000000000000000000 / 1258305739211791616206114134491] ~ [0.00118, 0.00118]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-99999999999985779312168181 / 500000000000000000000000000000, 50000000000007114113981653 / 250000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [3774917217635374848618342403473 / 62500000000000000000000000000, 7549834435270749697236684806947 / 125000000000000000000000000000] ~ [60.39868, 60.39868]
LHS := (LHS NUM) / (LHS DEN) in [-99999999999985779312168181 / 30199337741082998788946739227784, 50000000000007114113981653 / 15099668870541499394473369613892] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524381819531538 / 4582575694955840006588047193729, 707106781186547524381819531539 / 4582575694955840006588047193728] ~ [0.1543, 0.1543]
Success: LHS < CD / |V| ^ .5
Success: existence proven