show/hide visualization coordinates
a : (0.7375722988929084, -0.7727169531996425, -0.2748718791568065)
b : (0.7511961596877655, -1.2634610217840914, 0.5963253715081758)
c : (0.5169744123559356, -1.7476746118864357, -0.24669145645970247)
d : (0.045236152671972674, -1.1467448539391416, -0.8919405869230862)
e : (0.2126963371631745, -0.1611833305554573, -0.8669291848071685)
f : (0.8796243551554311, 0.21584620881385952, -0.22423505439995767)
g : (1.2013583888202453, -0.37410411679851074, 0.5163362283889625)
h : (0.2531634850741775, -0.42820839597596083, 0.8293843899946078)
i : (-0.076765500681722, -1.0178556892521295, 0.09218500455660361)
j : (-0.7297968764489279, -0.6156448440947346, -0.5495131007089211)
k : (-0.45545190794587115, -0.5387103879447074, -1.508061966293747)
l : (-0.6752950775106807, 0.2836948092278784, -0.983353787913403)
m : (-0.022099871410572236, 0.6386282970972476, -0.31450534325891977)
n : (0.614619811209303, 0.9633349771399285, 0.3848898366644947)
o : (1.530802116021885, 0.5676125433529479, 0.44824391897979476)
p : (0.8351506434633987, 0.3290243361201305, 1.1258460855175352)
q : (-0.11927500196353252, 0.49845866036895903, 0.8801558392363109)
r : (-0.5964275204839419, -0.2039451220800444, 0.3519944998039707)
s : (-1.32939087968224, 0.12404296497080924, -0.24398245346307346)
t : (-0.9381934722831307, 1.0346075594326063, -0.37753659138788237)
u : (-0.3175861290332869, 1.3237054192439004, 0.3513453969729906)
v : (-1.0466153721336104, 0.667583854892463, 0.5463347697541558)
w : (-1.2714965509386809, 1.6237096968501281, 0.35858006339506654)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['a', 'f', 'e'], ['c', 'i', 'b'], ['t', 'w', 'u'], ['h', 'g', 'b'], ['c', 'a', 'd'], ['n', 'o', 'p'], ['j', 'i', 'r'], ['v', 'q', 'r'], ['e', 'k', 'l'], ['j', 's', 'r'], ['m', 't', 'l'], ['j', 'i', 'd'], ['a', 'g', 'b'], ['n', 'q', 'u'], ['v', 'q', 'u'], ['r', 'i', 'h'], ['q', 'h', 'p'], ['j', 's', 'l'], ['f', 'o', 'g'], ['a', 'e', 'd'], ['a', 'f', 'g'], ['o', 'f', 'n'], ['g', 'h', 'p'], ['e', 'd', 'k'], ['m', 'n', 'u'], ['j', 'k', 'l'], ['v', 't', 'w'], ['j', 'd', 'k'], ['m', 'f', 'e'], ['m', 't', 'u'], ['m', 'f', 'n'], ['c', 'i', 'd'], ['n', 'q', 'p'], ['h', 'i', 'b'], ['v', 's', 'r'], ['c', 'a', 'b'], ['v', 's', 't'], ['s', 't', 'l'], ['r', 'q', 'h'], ['v', 'w', 'u'], ['m', 'e', 'l'], ['g', 'o', 'p']]
Coordinate Data:
o : [210320671412398546391 / 100000000000000000000, 21980735708209724617 / 20000000000000000000, 96243701648931200483 / 100000000000000000000]
p : [140755524156549917801 / 100000000000000000000, 860448578177668933 / 1000000000000000000, 82001959151352625913 / 50000000000000000000]
a : [65498844849750449619 / 50000000000000000000, -12064635557105198919 / 50000000000000000000, 2991515229408884519 / 12500000000000000000]
j : [-3147845566936546039 / 20000000000000000000, -8422060203719613789 / 100000000000000000000, -3532000319940383861 / 100000000000000000000]
w : [-69909195283658026821 / 100000000000000000000, 215513393890766661203 / 100000000000000000000, 10909664511307297013 / 12500000000000000000]
s : [-4731164259875870751 / 6250000000000000000, 32773360351417385193 / 50000000000000000000, 13510532202322189131 / 50000000000000000000]
n : [118702440931140348447 / 100000000000000000000, 74737960959873346089 / 50000000000000000000, 89908293417401202207 / 100000000000000000000]
d : [61764075077407315587 / 100000000000000000000, -61532061188160315333 / 100000000000000000000, -37774748941356894529 / 100000000000000000000]
m : [27515236334576413307 / 50000000000000000000, 117005253915478600029 / 100000000000000000000, 19968775425059747177 / 100000000000000000000]
r : [-1201146119092068691 / 50000000000000000000, 16373955998874704317 / 50000000000000000000, 43309379865674396803 / 50000000000000000000]
g : [44344074673058639907 / 25000000000000000000, 7866006262951384487 / 50000000000000000000, 6440808286865498197 / 6250000000000000000]
v : [-47421077403150990107 / 100000000000000000000, 2398016193900002857 / 2000000000000000000, 106052786726367301403 / 100000000000000000000]
l : [-10289047940858014213 / 100000000000000000000, 8151190512854168797 / 10000000000000000000, -46916069040388574791 / 100000000000000000000]
b : [16545009472373325731 / 12500000000000000000, -9150459746581911023 / 12500000000000000000, 55525923450884654937 / 50000000000000000000]
u : [25481846906881363679 / 100000000000000000000, 92756483065071933177 / 50000000000000000000, 10819231181031348817 / 12500000000000000000]
e : [3925504676326375049 / 5000000000000000000, 1851204557510405763 / 5000000000000000000, -35273608729765127149 / 100000000000000000000]
k : [2339053803124587649 / 20000000000000000000, -728614588716888067 / 100000000000000000000, -49693443439211480103 / 50000000000000000000]
t : [-36578887418103019259 / 100000000000000000000, 156603180149014455259 / 100000000000000000000, 6832825306081743397 / 50000000000000000000]
q : [2832059975866050051 / 6250000000000000000, 20597658048529947859 / 20000000000000000000, 139434893674582807649 / 100000000000000000000]
i : [24781954871018927961 / 50000000000000000000, -48643144719459116983 / 100000000000000000000, 60637810206612082727 / 100000000000000000000]
h : [82556808317627806839 / 100000000000000000000, 10321584608157765333 / 100000000000000000000, 67178874375206255867 / 50000000000000000000]
c : [10893790104580359991 / 10000000000000000000, -24325007396577941419 / 20000000000000000000, 26750164104981477069 / 100000000000000000000]
f : [145202895325753165669 / 100000000000000000000, 74727045087139795669 / 100000000000000000000, 28995804310955960823 / 100000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 23
|E| = 63
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 114862327003797885931634734224950778488493670842180942361588370697325310725979672441323062185003661432731047795512657361 / 248739214028119024131481162561626050355274606950448902952002545947668517391798060000000000000000000000000000000000000000
Collision distance in [679542582570186296075169969751 / 1000000000000000000000000000000, 84942822821273287009396246219 / 125000000000000000000000000000] ~ [0.67954, 0.67954]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [1517 / 10000, 1519 / 10000] ~ [0.1517, 0.1519]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 8283178325109371345813841429244477494558349 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [719512783291121040464275969039 / 2500000000000000000000000000000000000000000000000, 719512783293621040464275969039 / 2500000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [719152812500000000000000000 / 3968626966596885885752423630459, 1442100625000000000000000000 / 7937253933193771771504847260917] ~ [0.00018, 0.00018]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999879690203151323 / 1000000000000000000000000000000, 200000000000120468412270123 / 1000000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [7937253933193771771504847260917 / 125000000000000000000000000000, 3968626966596885885752423630459 / 62500000000000000000000000000] ~ [63.49803, 63.49803]
LHS := (LHS NUM) / (LHS DEN) in [-66666666666626563401050441 / 21166010488516724724012926029112, 66666666666706822804090041 / 21166010488516724724012926029112] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [679542582570186296075169969751 / 4795831523312719541597438064163, 339771291285093148037584984876 / 2397915761656359770798719032081] ~ [0.14169, 0.14169]
Success: LHS < CD / |V| ^ .5
Success: existence proven