show/hide visualization coordinates
a : (-0.7062520379253101, 0.6641544951397198, -0.21754889162065771)
b : (-1.1528540203021347, -0.2275597877744639, -0.1441165623376116)
c : (-1.143004147575173, 0.39280742605170876, 0.6401330790501384)
d : (-0.6366627858297016, 1.253521403612992, 0.5873138191502112)
e : (-0.23695961719010072, 1.5448566277594071, -0.2818013424659125)
f : (-0.23024764193940173, 0.9167824294972684, -1.0599258510540983)
g : (-0.6970836368331104, 0.034850597793582405, -0.9946541259399064)
h : (-1.1559382684751238, -0.8510027729838201, -0.9259792942838618)
i : (-0.7443484512538672, -1.1364751459766882, -0.06047403917700056)
j : (-0.6453947059874188, -0.47359789313524553, 0.6816862561521991)
k : (-0.14606628183116577, 0.39203977615502456, 0.7183270849548093)
l : (0.35393371816883423, 1.2171909796681664, 0.45540981404851544)
m : (0.589342680016806, 1.0244373208870063, -0.49718067913737407)
n : (0.26759296848231073, 0.10984256571197432, -0.742116501208774)
o : (-0.16597073309918264, -0.7894974867240214, -0.7987732462209474)
p : (0.15953521246156965, -1.5346837283842967, -0.21675662734753887)
q : (-0.14661768829377175, -1.3396862049325493, 0.7150407579282384)
r : (0.35393371816883423, -0.47398562762941404, 0.7183270849548093)
s : (0.8539337181688342, 0.39203977615502456, 0.7183270849548093)
t : (1.3115982676554987, 1.1068181398058021, 0.18952177957305993)
u : (1.1195826055950415, 0.21971634277339075, -0.23021669522446297)
v : (0.6446919026591033, -0.6603248019703067, -0.22768611758036383)
w : (0.828993271236323, -1.3253898049459087, 0.4959999658547304)
x : (1.324261953922311, -0.45685462655435277, 0.4771432469769892)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['m', 't', 'l'], ['e', 'd', 'l'], ['m', 'e', 'l'], ['i', 'j', 'q'], ['f', 'a', 'g'], ['s', 't', 'l'], ['a', 'e', 'd'], ['f', 'n', 'm'], ['b', 'a', 'g'], ['b', 'i', 'j'], ['u', 's', 't'], ['k', 'j', 'c'], ['b', 'h', 'g'], ['v', 'p', 'o'], ['m', 'f', 'e'], ['f', 'a', 'e'], ['n', 'o', 'g'], ['i', 'p', 'q'], ['w', 'p', 'v'], ['u', 'n', 'v'], ['u', 'x', 'v'], ['s', 'k', 'l'], ['b', 'c', 'j'], ['w', 'q', 'p'], ['m', 'u', 't'], ['a', 'd', 'c'], ['q', 'r', 'j'], ['k', 'd', 'c'], ['x', 's', 'r'], ['u', 's', 'x'], ['b', 'a', 'c'], ['i', 'h', 'o'], ['i', 'p', 'o'], ['m', 'u', 'n'], ['d', 'k', 'l'], ['w', 'q', 'r'], ['n', 'o', 'v'], ['w', 'x', 'v'], ['k', 'r', 'j'], ['w', 'x', 'r'], ['s', 'r', 'k'], ['b', 'i', 'h'], ['f', 'n', 'g'], ['o', 'h', 'g']]
Coordinate Data:
s : [179748494989076307561709898853 / 25000000000000000000000000000000000000000000000000000000000000000000, 486545888804795508072276341257 / 100000000000000000000000000000000000000000000000000000000000000000000, 43560568074039521386110707653 / 200000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
v : [52310453877432751710165441027 / 250000000000000000000000000000, 21047291562506625166735640107 / 20000000000000000000000000000, 946013202535173208382887150027 / 1000000000000000000000000000000]
r : [1 / 2, 866025403784438646763723170753 / 1000000000000000000000000000000, -208393497652787491155450998701 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
k : [1, -575992036223969895991065786487 / 100000000000000000000000000000000000000000000000000000000000000000000, -73648356945834964006959815583 / 500000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
h : [50246799666098954133648562063 / 25000000000000000000000000000, 124304254913884451539186100067 / 100000000000000000000000000000, 164430637923867125641642420713 / 100000000000000000000000000000]
d : [74529825199926787460801844303 / 50000000000000000000000000000, -430740813728983782228276575201 / 500000000000000000000000000000, 26202653160919626490913709701 / 200000000000000000000000000000]
m : [132295519076014138697283121997 / 500000000000000000000000000000, -126479508946396340343254473181 / 200000000000000000000000000000, 60775388204609172101063952979 / 50000000000000000000000000000]
p : [694398505707264541605504639137 / 1000000000000000000000000000000, 12042021903370757407495565547 / 6250000000000000000000000000, 467541856151174120586987872017 / 500000000000000000000000000000]
o : [25497611281700420480242512587 / 25000000000000000000000000000, 29538431571976146715586636187 / 25000000000000000000000000000, 75855016558787832052333351637 / 50000000000000000000000000000]
g : [77550867750097225087605374211 / 50000000000000000000000000000, 178594589180721081116718861663 / 500000000000000000000000000000, 171298121089471584398749623413 / 100000000000000000000000000000]
a : [156018575609414443875540104611 / 100000000000000000000000000000, -54422943796939061549784506763 / 200000000000000000000000000000, 935875976575467019918138156509 / 1000000000000000000000000000000]
w : [4988089386502244681974297901 / 200000000000000000000000000000, 171742958110093332992956771369 / 100000000000000000000000000000, 55581779775019740346560408841 / 250000000000000000000000000000]
t : [-228832274743332191175404332667 / 500000000000000000000000000000, -714778363650777583313361575189 / 1000000000000000000000000000000, 528805305381749444355876362709 / 1000000000000000000000000000000]
l : [1 / 2, -825151203513141864923644958833 / 1000000000000000000000000000000, 52583454181258779848314457551 / 200000000000000000000000000000]
n : [146585187421630866149852820849 / 250000000000000000000000000000, 282197210443050242199435502519 / 1000000000000000000000000000000, 3651108965408958577205903121 / 2500000000000000000000000000]
x : [-58791029469184599106508068699 / 125000000000000000000000000000, 53055900169336084988908607849 / 62500000000000000000000000000, 6029595949445504222573378357 / 25000000000000000000000000000]
f : [677613350067647480611995253 / 625000000000000000000000000, -262371326671121915445359498271 / 500000000000000000000000000000, 177825293600890772015086275787 / 100000000000000000000000000000]
e : [109089333535893492566535571429 / 100000000000000000000000000000, -57640842580219128211410755217 / 50000000000000000000000000000, 20002568548414438218261176417 / 20000000000000000000000000000]
b : [100339386923548443595716704329 / 50000000000000000000000000000, 619599563929488420092639914983 / 1000000000000000000000000000000, 862443647292420982144368053951 / 1000000000000000000000000000000]
i : [6393128677690805374197381829 / 4000000000000000000000000000, 76425746106585637806368619979 / 50000000000000000000000000000, 19470028103295248124416202953 / 25000000000000000000000000000]
u : [-66412221856551854781374647433 / 250000000000000000000000000000, 86161716690816897798508956599 / 500000000000000000000000000000, 948543780179272377382889510147 / 1000000000000000000000000000000]
q : [20011028129252120102774060919 / 20000000000000000000000000000, 173172598108757376361257884129 / 100000000000000000000000000000, 3286327026570997183656124413 / 1000000000000000000000000000000]
c : [1996937865744007339155692227 / 1000000000000000000000000000, -383824948342093279070681497 / 500000000000000000000000000000, 19548501476167742816909714689 / 250000000000000000000000000000]
j : [149932842415625296716921869391 / 100000000000000000000000000000, 432818834645135023654061672229 / 500000000000000000000000000000, 36640828802610250765054196447 / 1000000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 24
|E| = 66
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 314689266711360757129557770603248919471509843188895192464033378738817561707010524195243505857287622873471558717736681 / 624970044813332820293929946986889539407392614640557683473396288788545652235172218750000000000000000000000000000000000
Collision distance in [709596335904223652972615970551 / 1000000000000000000000000000000, 88699541988027956621576996319 / 125000000000000000000000000000] ~ [0.7096, 0.7096]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [9798377960868661999 / 100000000000000000000, 9798377960868662001 / 100000000000000000000] ~ [0.09798, 0.09798]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 151252914431555165312164545764345179831652974527103397497365210059566413473779610050925325424143323343322055857723469074675376845084577680728465458919802395423800060119945675628425045623057893595315245236943384017492336690570196902949903566080885691418081153900117061195183079523746862915033 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [972281191424178370237083564671 / 25000000000000000000000000000000000000000000000000000000000, 997281191424178370237083564671 / 25000000000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [96008210664036718772136857748506676001 / 1299846144741753657673581370922720000000000, 96008210664036718811330369591981324001 / 1299846144741753657673581370922560000000000] ~ [7e-05, 7e-05]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-9131338001 / 100000000000000000000, 868662001 / 100000000000000000000] ~ [-0.0, 0.0]
LHS DEN := 8 * |E| ^ .5 in [4062019202317980180229941784133 / 62500000000000000000000000000, 8124038404635960360459883568267 / 125000000000000000000000000000] ~ [64.99231, 64.99231]
LHS := (LHS NUM) / (LHS DEN) in [-5707086250625000000 / 4062019202317980180229941784133, 542913750625000000 / 4062019202317980180229941784133] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [709596335904223652972615970551 / 4898979485566356196394568149412, 709596335904223652972615970552 / 4898979485566356196394568149411] ~ [0.14485, 0.14485]
Success: LHS < CD / |V| ^ .5
Success: existence proven