show/hide visualization coordinates
a : (-0.10736530040588108, 0.10479267668524708, 0.554526481181347)
b : (-0.9363987882211556, -0.44893471363086135, 0.47649153199476035)
c : (-0.03851728841404389, -0.889094227268413, 0.4682202045024174)
d : (0.790768885602788, -0.3309291680850166, 0.49535336302332056)
e : (0.7077052597049538, 0.6598777882904376, 0.38857317173901296)
f : (-0.20125235478569237, 1.049345631857134, 0.23987598317452974)
g : (-1.005008886311356, 0.5455112208408167, 0.5563034224172033)
h : (-1.8079630524940913, 0.007991364672460782, 0.29874369879074403)
i : (-1.1835038134186837, -0.18915162020384976, -0.4570243226599004)
j : (-0.6728395477116419, -1.032822578926909, -0.2913701010499393)
k : (0.3137893196088314, -1.0551085129181337, -0.4528223085791607)
l : (0.8566929933883588, -1.3173573092159683, 0.34497539124017884)
m : (1.685889738554582, -0.7589967395906786, 0.37078686336912836)
n : (1.6122682493146487, 0.23616572607265332, 0.43583717664256505)
o : (1.3067486357948361, 0.6693891179459047, -0.41208691104957)
p : (0.3137893196088314, 0.6734540586411938, -0.5304730278731454)
q : (-0.6860234863877347, 0.6733459821329205, -0.5498209291738373)
r : (-1.1182775920427765, 1.3776067686418894, 0.013360331816022808)
s : (-1.9015624060122116, 0.9841356161004183, 0.49465582558523946)
t : (-1.6789588395955701, 0.6791010975752558, -0.4313039979096648)
u : (-0.18621068039116864, -0.19257134514324478, -0.5304730278731454)
v : (0.8137893196088314, -0.19257134514324478, -0.5304730278731454)
w : (1.3123169803217059, -1.0591250636702494, -0.5069183168545439)
x : (1.8101233346836396, -0.19405442565976275, -0.4449374745804173)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['s', 'g', 'h'], ['e', 'd', 'a'], ['e', 'd', 'n'], ['k', 'v', 'u'], ['f', 'q', 'r'], ['q', 'p', 'u'], ['l', 'd', 'c'], ['b', 'g', 'a'], ['w', 'x', 'v'], ['s', 'g', 'r'], ['b', 'i', 'j'], ['f', 'p', 'e'], ['f', 'e', 'a'], ['o', 'x', 'n'], ['b', 'c', 'j'], ['i', 't', 'h'], ['q', 't', 'r'], ['x', 'm', 'n'], ['x', 'o', 'v'], ['f', 'g', 'a'], ['k', 'u', 'j'], ['w', 'l', 'm'], ['m', 'd', 'n'], ['d', 'c', 'a'], ['w', 'x', 'm'], ['l', 'd', 'm'], ['i', 'q', 'u'], ['t', 's', 'h'], ['i', 'q', 't'], ['k', 'c', 'j'], ['o', 'e', 'n'], ['i', 'j', 'u'], ['b', 'g', 'h'], ['f', 'g', 'r'], ['o', 'p', 'v'], ['k', 'w', 'v'], ['u', 'p', 'v'], ['s', 't', 'r'], ['f', 'q', 'p'], ['k', 'l', 'c'], ['b', 'i', 'h'], ['k', 'w', 'l'], ['b', 'c', 'a'], ['o', 'p', 'e']]
Coordinate Data:
u : [-39615786869702563778080413133 / 2000000000000000000000000000000000000000000000000000000000000000000, 164273052719905308726924144433 / 5000000000000000000000000000000000000000000000000000000000000000000, 33518173491158238011899599407 / 200000000000000000000000000000000000000000000000000000000000000000000000000000000000]
a : [78845379985287564322704622243 / 1000000000000000000000000000000, 148682010914245921308907646897 / 500000000000000000000000000000, 27124987726362309082129731589 / 25000000000000000000000000000]
d : [61061222874622287463989599327 / 62500000000000000000000000000, -8647363933860737623573057821 / 62500000000000000000000000000, 102582639089646588717862090971 / 100000000000000000000000000000]
p : [1 / 2, 866025403784438646763723170753 / 1000000000000000000000000000000, 270083982964652494939634860467 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000]
i : [-99729313302751499042441527967 / 100000000000000000000000000000, 1709862469697504650138212423 / 500000000000000000000000000000, 18362176303311259443031553051 / 250000000000000000000000000000]
l : [3259073980561023457131954071 / 3125000000000000000000000000, -112478596407272367204312976113 / 100000000000000000000000000000, 437724209556662147602341530827 / 500000000000000000000000000000]
x : [3119271898554388020099120311 / 1562500000000000000000000000, -1483080516517969195451300679 / 1000000000000000000000000000000, 85535553292728085991594189893 / 1000000000000000000000000000000]
q : [-124953201499141515704381868519 / 250000000000000000000000000000, 173183465455233075880336173453 / 200000000000000000000000000000, -9673950650345909719292853003 / 500000000000000000000000000000]
f : [-7520837197261861733090927249 / 500000000000000000000000000000, 62095848850018928447066970867 / 50000000000000000000000000000, 770349011047675119180683794339 / 1000000000000000000000000000000]
r : [-466033455825803915049800231439 / 500000000000000000000000000000, 157017811378513405269658424211 / 100000000000000000000000000000, 33989584980573013047869831823 / 62500000000000000000000000000]
s : [-171535172562104282172093886009 / 100000000000000000000000000000, 117670696124366305564676628817 / 100000000000000000000000000000, 102512885345838487578361209731 / 100000000000000000000000000000]
m : [187210041894575055966584964559 / 100000000000000000000000000000, -566425394447433775604008100233 / 1000000000000000000000000000000, 225314972810568460407944319001 / 250000000000000000000000000000]
v : [1, -139122156368987907267544756299 / 5000000000000000000000000000000000000000000000000000000000000000000, -82258802084722940840538371759 / 250000000000000000000000000000000000000000000000000000000000000000000000000000000000]
k : [1 / 2, -862537167774888872872665944857 / 1000000000000000000000000000000, 38825359646992338275371838547 / 500000000000000000000000000000]
g : [-818798205920187230331591660577 / 1000000000000000000000000000000, 738082565984061504130363475527 / 1000000000000000000000000000000, 54338822514517441818454426241 / 50000000000000000000000000000]
b : [-750188107829986985102390595557 / 1000000000000000000000000000000, -256363368487616567988616321229 / 1000000000000000000000000000000, 25174113996697643745478480103 / 25000000000000000000000000000]
h : [-162175237210292259284542731779 / 100000000000000000000000000000, 200562709815705557526140054123 / 1000000000000000000000000000000, 829216726663889455950140343447 / 1000000000000000000000000000000]
j : [-486628867320473233238001867029 / 1000000000000000000000000000000, -840251233783664125043992194697 / 1000000000000000000000000000000, 239102926823206147557697941041 / 1000000000000000000000000000000]
e : [55869746256007649520937528869 / 62500000000000000000000000000, 852449133433682471970145441909 / 1000000000000000000000000000000, 57440387475759899692325004523 / 62500000000000000000000000000]
w : [29970553214257489386969431501 / 20000000000000000000000000000, -34662148741080188047241366533 / 40000000000000000000000000000, 11777355509300747033695424053 / 500000000000000000000000000000]
c : [73846695988562374888226249701 / 500000000000000000000000000000, -696522882125168223728019260119 / 1000000000000000000000000000000, 998693232375562843566850521261 / 1000000000000000000000000000000]
o : [37323982904650123580634234197 / 25000000000000000000000000000, 861960463089149559719323900813 / 1000000000000000000000000000000, 118386116823575407969947550369 / 1000000000000000000000000000000]
t : [-37318703980110036316516701053 / 25000000000000000000000000000, 871672442718500593187210279409 / 1000000000000000000000000000000, 99169029963480614641754811427 / 1000000000000000000000000000000]
n : [179847892970581752491683422397 / 100000000000000000000000000000, 428737071215898092313390120421 / 1000000000000000000000000000000, 966310204515710468225472609393 / 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 = 44345197759387420613161108659390899211297485908553752595956116696329496972260491288411400883999511815151476650023689 / 77387973160714253577088454478422444380100577847225763193089773563482097242958906250000000000000000000000000000000000
Collision distance in [378491879458697713626752603277 / 500000000000000000000000000000, 151396751783479085450701041311 / 200000000000000000000000000000] ~ [0.75698, 0.75698]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [17025941153008191999 / 100000000000000000000, 17025941153008192001 / 100000000000000000000] ~ [0.17026, 0.17026]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 203867095830607954091734661550668473374862489358915094818490381704203787675717409998484701314350537196140146653628176836862096622741734223210722346789848311965906088988460243197616150534677612916788233916503433473947196746397962020100343766013546406870849332577994504554850895893 / 500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [504810726696907603077542492343 / 25000000000000000000000000000000000000000000000000000000000, 529810726696907603077542492343 / 25000000000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [289882672145697922394798936802847616001 / 1299846144741753657673581370922720000000000, 289882672145697922462902701414880384001 / 1299846144741753657673581370922560000000000] ~ [0.00022, 0.00022]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-6991808001 / 100000000000000000000, 3008192001 / 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 [-4369880000625000000 / 4062019202317980180229941784133, 1880120000625000000 / 4062019202317980180229941784133] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [126163959819565904542250867759 / 816496580927726032732428024902, 756983758917395427253505206555 / 4898979485566356196394568149411] ~ [0.15452, 0.15452]
Success: LHS < CD / |V| ^ .5
Success: existence proven