show/hide visualization coordinates
a : (0.5376232726193374, 0.18714792737005348, -0.7285401844990501)
b : (1.108990354685562, 0.4082796163212839, 0.061801788113251876)
c : (1.0829829427592144, -0.5273374481749025, -0.2902554844269305)
d : (0.14323122073254366, -0.718634546339951, -0.5735788353557566)
e : (-0.4540070541049395, 0.07896671665245714, -0.6580694759147104)
f : (-0.05254225808610136, 0.9939058839320578, -0.699449878707138)
g : (0.9403239715886871, 1.0983780528958147, -0.641984968689124)
h : (0.8104101732401543, 1.3262240330289683, 0.3230065412920877)
i : (0.31404165416390845, 0.5249941256517285, 0.657145627294181)
j : (0.8140386862038522, -0.34102956458017275, 0.6547092553260065)
k : (1.3113047131673838, -1.179678762171015, 0.4324615966023644)
l : (0.7612025214117804, -1.4722841392237658, -0.349695466873699)
m : (-0.22649331798402544, -1.5872266698901933, -0.24365234600199082)
n : (-0.8272118994588054, -0.794134918633421, -0.3443631198019875)
o : (-1.4254810884597269, 0.0021640574542081126, -0.43370470124071814)
p : (-0.9364821467670752, 0.8554846684401298, -0.25280702328414484)
q : (-0.18595834583609155, 1.2877625550600242, 0.24704280714050075)
r : (0.341969987307394, 1.8567570189352436, -0.38346252601988795)
s : (-0.6859583458360916, 0.5249941256517285, 0.657145627294181)
t : (-0.18595834583609155, -0.34103127813271006, 0.657145627294181)
u : (0.3136612286668328, -1.192864963692945, 0.49979362407088596)
v : (-0.6846329970868157, -1.2020677682047285, 0.5574473075268562)
w : (-1.168904254945803, -0.3311850941664177, 0.4735144958763718)
x : (-1.6461506721450838, 0.5424163718165266, 0.37834971298427067)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['h', 'q', 'r'], ['v', 'w', 't'], ['i', 'j', 't'], ['d', 'a', 'c'], ['m', 'l', 'd'], ['i', 's', 'q'], ['s', 'w', 'x'], ['s', 'q', 'p'], ['m', 'v', 'u'], ['k', 'l', 'u'], ['e', 'n', 'o'], ['q', 'f', 'r'], ['m', 'l', 'u'], ['b', 'a', 'c'], ['i', 's', 't'], ['j', 'u', 't'], ['k', 'j', 'u'], ['f', 'g', 'r'], ['s', 'x', 'p'], ['i', 'b', 'j'], ['s', 'w', 't'], ['n', 'v', 'w'], ['b', 'a', 'g'], ['q', 'f', 'p'], ['l', 'd', 'c'], ['e', 'f', 'a'], ['e', 'f', 'p'], ['h', 'i', 'b'], ['h', 'g', 'r'], ['v', 'u', 't'], ['p', 'o', 'x'], ['h', 'i', 'q'], ['n', 'm', 'd'], ['k', 'l', 'c'], ['m', 'n', 'v'], ['e', 'd', 'a'], ['k', 'j', 'c'], ['x', 'o', 'w'], ['e', 'o', 'p'], ['h', 'b', 'g'], ['n', 'o', 'w'], ['b', 'j', 'c'], ['n', 'e', 'd'], ['f', 'a', 'g']]
Coordinate Data:
i : [292712190607673254152398651219 / 10000000000000000000000000000000000000000000000000000000000000000000, -121025084629027729640890343393 / 10000000000000000000000000000000000000000000000000000000000000000000, 156388503034754187018762164597 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
x : [2450240407886240352647101083 / 1250000000000000000000000000, -17422246164798011387328794229 / 1000000000000000000000000000000, 278795914309910339336377228717 / 1000000000000000000000000000000]
o : [1391618194098908133528716277 / 800000000000000000000000000, 522830068197520446186914834419 / 1000000000000000000000000000000, 109085032853489920965860075573 / 100000000000000000000000000000]
g : [-626282317424778680605392134013 / 1000000000000000000000000000000, -71672990905510753751010707333 / 125000000000000000000000000000, 64956529799165257374410277473 / 50000000000000000000000000000]
w : [148294590910971148712336947477 / 100000000000000000000000000000, 856179219818146229343711104181 / 1000000000000000000000000000000, 36726226283561849355692160151 / 200000000000000000000000000000]
h : [-124092129769061481998847079779 / 250000000000000000000000000000, -80122990737723974563032879843 / 100000000000000000000000000000, 83534771500523324184672484791 / 250000000000000000000000000000]
p : [25010476018619672125425631433 / 20000000000000000000000000000, -165245271394200606684356805889 / 500000000000000000000000000000, 454976325289162942702648875929 / 500000000000000000000000000000]
s : [1, -171386569249618693147931338941 / 10000000000000000000000000000000000000000000000000000000000000000000, -3552053052384466199413542433 / 3125000000000000000000000000000000000000000000000000000000000000000000000000000000000]
u : [190212748537802888765918587 / 500000000000000000000000000000, 171785908934467341261863663539 / 100000000000000000000000000000, 157352003223295079584916166929 / 1000000000000000000000000000000]
j : [-99999406407988764459015260953 / 200000000000000000000000000000, 866023690231901268508978987371 / 1000000000000000000000000000000, 2436371968174444504514088599 / 1000000000000000000000000000000]
t : [1 / 2, 866025403784438646763723170753 / 1000000000000000000000000000000, -825947137551914801985809423367 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
k : [-3116447059385860874189815353 / 3125000000000000000000000000, 34093457756454871691832965301 / 20000000000000000000000000000, 44936806138363327335000795191 / 200000000000000000000000000000]
v : [998674651250724187602853177767 / 1000000000000000000000000000000, 172706189385645693720897420607 / 100000000000000000000000000000, 4984915988366241611702024317 / 50000000000000000000000000000]
c : [-768941288595305965208035495987 / 1000000000000000000000000000000, 105233157382663104904356456667 / 100000000000000000000000000000, 947401111721111556669852579331 / 1000000000000000000000000000000]
l : [-17886434689914877840860634633 / 40000000000000000000000000000, 199727826487549422395668404541 / 100000000000000000000000000000, 25171027354197003448634583553 / 25000000000000000000000000000]
m : [540534972147933943062916174951 / 1000000000000000000000000000000, 21122207955419219488619686417 / 10000000000000000000000000000, 9007979732961718144207480433 / 10000000000000000000000000000]
d : [170810433431364791580610569229 / 1000000000000000000000000000000, 124362867199167952722337607587 / 100000000000000000000000000000, 30768111566248441311825760233 / 25000000000000000000000000000]
a : [-55895404613857233703297618871 / 250000000000000000000000000000, 67569239656335012020728826111 / 200000000000000000000000000000, 69284290589661551540329820479 / 50000000000000000000000000000]
r : [-27928333143485515890596841319 / 1000000000000000000000000000000, -133176289328351505274078453419 / 100000000000000000000000000000, 13007601916425861468033621021 / 12500000000000000000000000000]
q : [1 / 2, -381384214704147841776813564281 / 500000000000000000000000000000, 102525705038420073710513133499 / 250000000000000000000000000000]
e : [768048708268847941269978917133 / 1000000000000000000000000000000, 223013704499635692737138792317 / 500000000000000000000000000000, 131521510320889142413272591453 / 100000000000000000000000000000]
b : [-794948700521653474165299202423 / 1000000000000000000000000000000, 58357254665222326907634505733 / 500000000000000000000000000000, 595343839180929162404689007743 / 1000000000000000000000000000000]
n : [7132834710141961213623639021 / 6250000000000000000000000000, 26382580885702990669365005929 / 20000000000000000000000000000, 25037718677404214100818242701 / 25000000000000000000000000000]
f : [22911494515625612259101535073 / 62500000000000000000000000000, -93782351656065859603688352481 / 200000000000000000000000000000, 135659550600131911997620414793 / 100000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 24
|E| = 66
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 560294196367976186219178910257980478726342060221838995661557192482078006682649110008584064824749327897185487430613368649 / 958777213857090504110790862869828264185200733807505850943188052400248508214712370000000000000000000000000000000000000000
Collision distance in [23889069372684434112959036167 / 31250000000000000000000000000, 152890043985180378322937831469 / 200000000000000000000000000000] ~ [0.76445, 0.76445]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [24958845131054246999 / 100000000000000000000, 24958845131054247001 / 100000000000000000000] ~ [0.24959, 0.24959]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 726992903606776822482970997726125081353954267691305863720769652850609050252221686530958048767070452478144855544413083674988896465246872669514270835838236299245834724922888202536166499909035613000148507184439989602694389775109057182385740741463110454247981935799818706357080299197307232877323 / 500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [3813116582552326900420265585993 / 100000000000000000000000000000000000000000000000000000000000, 3913116582552326900420265585993 / 100000000000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [622943950275950292054727966474900506001 / 1299846144741753657673581370922720000000000, 622943950275950292154563346999117494001 / 1299846144741753657673581370922560000000000] ~ [0.00048, 0.00048]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-8945753001 / 100000000000000000000, 1054247001 / 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 [-5591095625625000000 / 4062019202317980180229941784133, 658904375625000000 / 4062019202317980180229941784133] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [191112554981475472903672289336 / 1224744871391589049098642037353, 764450219925901891614689157345 / 4898979485566356196394568149411] ~ [0.15604, 0.15604]
Success: LHS < CD / |V| ^ .5
Success: existence proven