show/hide visualization coordinates
a : (-0.4856807925278869, 2.2094554042730286, -0.8817912182697459)
b : (-0.7949175061172679, 1.6251872574969124, -0.13145570156322495)
c : (-0.7938094218694179, 2.61931659002758, -0.023263084664339684)
d : (-0.9313769466398517, 3.1046261652247575, -0.8867153371661621)
e : (-0.01047658181570521, 3.006655526837066, -0.5094299384549718)
f : (0.07139908249784516, 2.1189921822003583, -0.056274157093209376)
g : (-0.012323388895455145, 1.3497733059526196, -0.6897509666197806)
h : (-0.6128132897165705, 0.655323588650595, -0.2933276207495036)
i : (-0.004880415815365136, 1.1865130928268985, 0.29680400141893604)
j : (0.3749061098323407, 0.5025527341231631, -0.32606068907034047)
k : (-0.2534143762658603, -0.2724935635680697, -0.3932663672860486)
l : (-0.14953500823760812, 0.2131529711144849, 0.47469476101917524)
m : (0.594117773269152, -0.35984882753754294, 0.13023942385802773)
n : (0.21169692802521278, -1.1560561301519476, -0.33859767832822685)
o : (-0.2474605173218849, -0.7820123474505816, 0.46717256746444336)
p : (0.6256504989141802, -1.2594513065253117, 0.5658092426155448)
q : (0.6717855795987158, -2.0095466293660476, -0.09390930417746723)
r : (-0.2008598335241467, -1.7718310285476844, 0.3326833306431464)
s : (0.5193539019672867, -2.204496512807415, 0.8749865243823762)
t : (1.0179767766439642, -2.858285382204926, 0.30583334368223214)
u : (0.03453593311372366, -2.731131473955453, 0.17669779128315888)
v : (0.3761254948846006, -3.1863956166124816, 0.9989210770759787)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['j', 'g', 'h'], ['n', 'o', 'k'], ['l', 'i', 'h'], ['f', 'b', 'i'], ['n', 'k', 'm'], ['l', 'j', 'i'], ['j', 'k', 'h'], ['s', 'p', 'r'], ['t', 'q', 's'], ['n', 'o', 'r'], ['u', 's', 'v'], ['t', 'q', 'u'], ['v', 't', 's'], ['b', 'i', 'h'], ['f', 'a', 'g'], ['n', 'q', 'p'], ['n', 'p', 'm'], ['b', 'g', 'h'], ['a', 'g', 'b'], ['l', 'o', 'm'], ['f', 'b', 'c'], ['f', 'g', 'i'], ['q', 'p', 's'], ['d', 'e', 'a'], ['n', 'q', 'r'], ['o', 'p', 'r'], ['u', 's', 'r'], ['d', 'e', 'c'], ['j', 'g', 'i'], ['d', 'a', 'c'], ['v', 't', 'u'], ['j', 'k', 'm'], ['a', 'b', 'c'], ['l', 'k', 'h'], ['o', 'p', 'm'], ['f', 'e', 'c'], ['l', 'j', 'm'], ['u', 'q', 'r'], ['l', 'o', 'k'], ['e', 'a', 'f']]
Coordinate Data:
e : [54385659965354337491 / 100000000000000000000, -258137790564218714399 / 100000000000000000000, 13641613394723012529 / 12500000000000000000]
n : [32168308981262540149 / 100000000000000000000, 158133375134682624493 / 100000000000000000000, 18409936229021922469 / 20000000000000000000]
t : [-24229837940306297043 / 50000000000000000000, 82089075084995111603 / 25000000000000000000, 13803289472031854737 / 50000000000000000000]
i : [53826043365320325267 / 100000000000000000000, -76123547163202001297 / 100000000000000000000, 28509513170393319403 / 100000000000000000000]
h : [57309665377720434069 / 50000000000000000000, -2300459674557165933 / 10000000000000000000, 43761337693618641329 / 50000000000000000000]
q : [-6920278088043878477 / 50000000000000000000, 121741212528046311999 / 50000000000000000000, 67580843730033644377 / 100000000000000000000]
u : [12471102118102862143 / 25000000000000000000, 31564090951503315801 / 10000000000000000000, 40520134183971036461 / 100000000000000000000]
s : [1402611587055142401 / 100000000000000000000, 262977413400229347537 / 100000000000000000000, -1831796195371918429 / 6250000000000000000]
d : [73237848223884495011 / 50000000000000000000, -16745928400186743701 / 6250000000000000000, 36715361757225786473 / 25000000000000000000]
v : [7862726147661877439 / 50000000000000000000, 361167323780736010643 / 100000000000000000000, -20851097197655471831 / 50000000000000000000]
o : [976050668949653803 / 1250000000000000000, 6036449843227300751 / 5000000000000000000, 11472656565842585083 / 100000000000000000000]
r : [73423985136198483433 / 100000000000000000000, 109855432487128153309 / 50000000000000000000, 996863209918891247 / 4000000000000000000]
p : [-9227048107634202649 / 100000000000000000000, 6738915710880761097 / 4000000000000000000, 201123631341556333 / 12500000000000000000]
a : [12738260129571562427 / 12500000000000000000, -178417778307814997019 / 100000000000000000000, 29273807027852304907 / 20000000000000000000]
k : [78679439410369839613 / 100000000000000000000, 34888559238147412129 / 50000000000000000000, 48758275020445890773 / 50000000000000000000]
c : [5308757758829024167 / 4000000000000000000, -43880779376654028653 / 20000000000000000000, 12103244355744178173 / 20000000000000000000]
m : [-6073775543131388943 / 100000000000000000000, 19628161218310534503 / 25000000000000000000, 22582985463242075443 / 50000000000000000000]
b : [66414876197755300461 / 50000000000000000000, -59995481815101690863 / 50000000000000000000, 1783387086715235493 / 2500000000000000000]
j : [15847390800549749393 / 100000000000000000000, -7727511292828466591 / 100000000000000000000, 90795982219320969431 / 100000000000000000000]
l : [6829150260754462979 / 10000000000000000000, 21212465008039360363 / 100000000000000000000, 1340054651296174917 / 12500000000000000000]
f : [1443690422937478251 / 3125000000000000000, -42342864025137000977 / 25000000000000000000, 63817329021607864529 / 100000000000000000000]
g : [6821292584166166509 / 12500000000000000000, -92449568475774111839 / 100000000000000000000, 6358250498713249083 / 5000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 4999999999999999999662988724238861428838608568058195434333851724339528950335611942614508445283009510081557757916769881 / 10000000000000000000108560945708961557991036200335776324111454933719688917753834400000000000000000000000000000000000000
Collision distance in [353553390593273762186587928609 / 500000000000000000000000000000, 707106781186547524373175857219 / 1000000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [2271 / 10000, 2273 / 10000] ~ [0.2271, 0.2273]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 3800169635310078803504220442513247602205253 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [60918824344224657989593455611 / 312500000000000000000000000000000000000000000000, 60918824344537157989593455611 / 312500000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [644680125000000000000000000 / 1549193338482966754071706159913, 807270156250000000000000000 / 1936491673103708442589632699891] ~ [0.00042, 0.00042]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-39999999999989370871343271 / 200000000000000000000000000000, 200000000000053192447020849 / 1000000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [1936491673103708442589632699891 / 31250000000000000000000000000, 1549193338482966754071706159913 / 25000000000000000000000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-66666666666648951452238785 / 20655911179772890054289415465504, 66666666666684397482340283 / 20655911179772890054289415465504] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524373175857218 / 4690415759823429554565630113545, 41594516540385148492539756307 / 275906809401378209092095889032] ~ [0.15076, 0.15076]
Success: LHS < CD / |V| ^ .5
Success: existence proven