show/hide visualization coordinates
a : (-0.822424715878584, 0.8492870847555758, 0.13845791535114638)
b : (-0.8683802445525186, 0.20478618044034047, -0.6247633328601065)
c : (-1.6020018298599696, 0.2286505495647826, 0.05437572613832453)
d : (-1.1928549320883866, 0.3989005637843499, 0.9508207878694529)
e : (-0.2601122318116791, 0.7593140504636473, 0.9604734403643972)
f : (0.12625840422161172, 1.1654566545927452, 0.1323635945574141)
g : (-0.3737415957783883, 1.067716206651303, -0.7281285929935283)
h : (0.12625840422161172, 0.20169080286686447, -0.7281285929935283)
i : (-0.37278179056620564, -0.6627344759777474, -0.6670727064587121)
j : (-1.3197364117506971, -0.6430005788587128, -0.3463118629602708)
k : (-1.3599178369326579, -0.5392210786686875, 0.6474764788966133)
l : (-0.42282516182150887, -0.20079295485542592, 0.7330552336507364)
m : (0.5119272125860814, 0.15238731028454244, 0.7718069930305839)
n : (0.6727097473132105, 1.1195600515134658, 0.9685958777533995)
o : (1.0200882939695235, 0.7171798811004334, 0.12159036196183948)
p : (0.6262584042216117, 1.067716206651303, -0.7281285929935283)
q : (1.1262582391655, 0.201690898162055, -0.7287031468962721)
r : (0.6262686296666542, -0.6641516634239528, -0.7106186524501422)
s : (0.1423641055088975, -1.439701102367005, -0.3052059253993352)
t : (-0.6056974887930784, -1.0440212569690837, 0.2275616703459986)
u : (0.33715188722022893, -0.7601848472052581, 0.40212382730935337)
v : (1.1723678967185003, -0.27070562236534146, 0.15147605467233693)
w : (1.6244381707251865, -0.6618204093821514, -0.650185775987147)
x : (1.0881248442950573, -1.2480024507580443, -0.0429307799090245)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['b', 'i', 'h'], ['m', 'n', 'o'], ['g', 'p', 'f'], ['a', 'b', 'c'], ['q', 'p', 'o'], ['h', 'q', 'r'], ['i', 'h', 'r'], ['n', 'o', 'f'], ['s', 'i', 't'], ['m', 'v', 'o'], ['p', 'o', 'f'], ['x', 's', 'r'], ['j', 'b', 'i'], ['a', 'g', 'f'], ['l', 'k', 't'], ['x', 'v', 'u'], ['l', 'k', 'd'], ['s', 'i', 'r'], ['a', 'e', 'f'], ['p', 'h', 'q'], ['d', 'k', 'c'], ['m', 'l', 'e'], ['t', 's', 'u'], ['v', 'x', 'w'], ['a', 'e', 'd'], ['e', 'n', 'f'], ['a', 'd', 'c'], ['m', 'e', 'n'], ['j', 'k', 't'], ['v', 'q', 'o'], ['x', 's', 'u'], ['m', 'l', 'u'], ['x', 'w', 'r'], ['b', 'g', 'h'], ['m', 'v', 'u'], ['j', 'i', 't'], ['h', 'g', 'p'], ['w', 'q', 'r'], ['j', 'b', 'c'], ['a', 'b', 'g'], ['j', 'k', 'c'], ['l', 'e', 'd'], ['v', 'w', 'q'], ['l', 'u', 't']]
Coordinate Data:
p : [95187161869919764047897219671 / 2500000000000000000000000000000000000000000000000000000000000000000, -57485336255956086258626209527 / 6250000000000000000000000000000000000000000000000000000000000000000, 62759056666546839236176754943 / 500000000000000000000000000000000000000000000000000000000000000000000000000000]
g : [1, -39535887291540527616755514799 / 1250000000000000000000000000000000000000000000000000000000000000000, -33151568602900503116034986109 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000]
v : [-341318432810555418662762921 / 625000000000000000000000000, 16730272862708056995844409419 / 12500000000000000000000000000, -17592092953317304273839198351 / 20000000000000000000000000000]
j : [194599481597230882733670748477 / 100000000000000000000000000000, 171071678551001579716013508897 / 100000000000000000000000000000, -5965886406769648548818189741 / 15625000000000000000000000000]
s : [483894298712714200866652504897 / 1000000000000000000000000000000, 250741730901830798647330296439 / 100000000000000000000000000000, -105730666898548269570662114463 / 250000000000000000000000000000]
r : [-5112722521232717028580607 / 500000000000000000000000000000, 86593393503762791537485671821 / 50000000000000000000000000000, -875497027169305550538316493 / 50000000000000000000000000000]
e : [443185318016645390318586485867 / 500000000000000000000000000000, 308402156187655686961294226839 / 1000000000000000000000000000000, -3377204066715850881305084981 / 2000000000000000000000000000]
c : [111413011704079073894683535007 / 50000000000000000000000000000, 839065657086520448761452399097 / 1000000000000000000000000000000, -9781303989148159584825142737 / 12500000000000000000000000000]
a : [144868312010019567061419813247 / 100000000000000000000000000000, 27303640236965912928216120563 / 125000000000000000000000000000, -433293254172337331953159707049 / 500000000000000000000000000000]
i : [99904019478781734112545131957 / 100000000000000000000000000000, 21630633532863131420636976709 / 12500000000000000000000000000, -61055886534816161793984775667 / 1000000000000000000000000000000]
w : [-124772470812946843008854309179 / 125000000000000000000000000000, 172953661603345447927280769693 / 100000000000000000000000000000, -15588563401276244369661213059 / 200000000000000000000000000000]
h : [1 / 2, 866025403784438646763723170753 / 1000000000000000000000000000000, -27118994258617228019578809769 / 200000000000000000000000000000000000000000000000000000000000000000000000000000]
t : [61597794650734500306832779149 / 50000000000000000000000000000, 52793436590509671740203181421 / 25000000000000000000000000000, -59730641458720429003043955291 / 62500000000000000000000000000]
f : [1 / 2, -48870223970721096717791213877 / 500000000000000000000000000000, -172098437510188479746157002001 / 200000000000000000000000000000]
m : [7145699477220640365664800081 / 62500000000000000000000000000, 915328896366760570714259739983 / 1000000000000000000000000000000, -74996779301205608956324925479 / 50000000000000000000000000000]
q : [-124999958735972064641111683283 / 250000000000000000000000000000, 433012654244624050726478335043 / 500000000000000000000000000000, 574553902743841341724048403 / 1000000000000000000000000000000]
d : [90955666815499910605307216847 / 50000000000000000000000000000, 668815642866953211301707640509 / 1000000000000000000000000000000, -167894938086298124381196059237 / 100000000000000000000000000000]
l : [26227089151078016304739405643 / 25000000000000000000000000000, 63425458075336444826470230937 / 50000000000000000000000000000, -36529595666106617164969061981 / 25000000000000000000000000000]
n : [-46451343091598803810232952393 / 1000000000000000000000000000000, -51843844862162762918730756051 / 1000000000000000000000000000000, -84836223537346393649013785243 / 50000000000000000000000000000]
u : [144553258500691401424392217933 / 500000000000000000000000000000, 182790105385656129511575384799 / 100000000000000000000000000000, -22605048406057635043188932849 / 20000000000000000000000000000]
o : [-4922873621848897514973539541 / 12500000000000000000000000000, 87634081387717419300899468397 / 250000000000000000000000000000, -169943790991073556837427426767 / 200000000000000000000000000000]
b : [149463864877413027770089770779 / 100000000000000000000000000000, 431465013105481316255186777897 / 500000000000000000000000000000, -103365260133421671604694393363 / 1000000000000000000000000000000]
k : [99308812057713479486427134277 / 50000000000000000000000000000, 160693728531999047875144028237 / 100000000000000000000000000000, -137560507189014154994150405391 / 100000000000000000000000000000]
x : [-11546661001836139392000112299 / 25000000000000000000000000000, 46314373148186949167389980043 / 20000000000000000000000000000, -85649726635562968589554870597 / 125000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 24
|E| = 66
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 8428219284900736228179279953729901058655180171656366252997113022264165869611212835777806248045580750446101319083888961 / 15474283800128887546355669436561245084939334538657997791715729948664806190513200312500000000000000000000000000000000000
Collision distance in [369005329611383581060882244307 / 500000000000000000000000000000, 147602131844553432424352897723 / 200000000000000000000000000000] ~ [0.73801, 0.73801]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [10581162938003139999 / 100000000000000000000, 10581162938003140001 / 100000000000000000000] ~ [0.10581, 0.10581]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 256129320947922030082353439067725710061523271085067144143631544098343973522831177435279268017775159213522565740783620489865195985797987819829779218289675955286264508203662644297674630427576312420911994622208866704746624483671071968224935190627808779346887621970672311248393 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1600404076937827692693283795877 / 100000000000000000000000000000000000000000000000000, 1600404077037827692693283795877 / 100000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [111961009120571241526088323983593720001 / 1299846144741753657673581370922720000000000, 111961009120571241568412975735606280001 / 1299846144741753657673581370922560000000000] ~ [9e-05, 9e-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 [-1996860001 / 100000000000000000000, 8003140001 / 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 [-1248037500625000000 / 4062019202317980180229941784133, 5001962500625000000 / 4062019202317980180229941784133] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [123001776537127860353627414769 / 816496580927726032732428024902, 738010659222767162121764488615 / 4898979485566356196394568149411] ~ [0.15065, 0.15065]
Success: LHS < CD / |V| ^ .5
Success: existence proven