show/hide visualization coordinates
a : (0.04835393859239451, 0.7745428230475963, 0.969783860770882)
b : (0.9095126861576962, 0.27267338386762036, 0.8889588800474848)
c : (0.5188656371262543, 0.727525429742554, 0.08864363000759357)
d : (-0.42721778292716445, 1.0482877729723645, 0.13378431526765083)
e : (-0.8423946776398528, 0.3775907635642586, 0.7484335385387394)
f : (-0.5945872906583631, 0.5494523731097698, 1.7018773418757964)
g : (0.2596192221661454, 0.0374065242859955, 1.611653829693366)
h : (0.14677332432775958, -0.34399627848122244, 0.6941584861725616)
i : (0.8658038236839825, -0.20728757272944426, 0.012758551650100203)
j : (0.8904563275672706, 0.401120803433463, -0.7804825856260114)
k : (-0.0792390097372791, 0.6342279745425161, -0.7073252238136127)
l : (-0.8667720105534447, 0.23180655846867035, -0.24058249327503634)
m : (-0.779470853219405, -0.5491055195155405, 0.3779276799529545)
n : (-0.6074022335313951, -0.3863054386405606, 1.3494669348396333)
o : (-0.4046547203064544, -0.21805392985167033, 2.3141352071858137)
p : (-0.009658908724981985, -0.6078534760553542, -0.25763368428822686)
q : (0.749812711771859, -0.580743874082871, -0.907609012389837)
r : (1.228786991604161, -0.049624701710347885, -1.6065339468409223)
s : (0.24643613513473403, 0.0857546892842509, -1.4774633642602466)
t : (-0.7175109603922176, 0.054028591151557614, -1.2132675056204323)
u : (-0.9460012804115343, -0.6993074150760306, -0.5966014408993896)
v : (-0.17510211570704665, -0.785963180815944, -1.2276365081674077)
w : (0.5855910456768844, -0.7661763005116302, -1.8764464908214538)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['j', 's', 'r'], ['c', 'i', 'j'], ['b', 'g', 'a'], ['p', 'h', 'm'], ['c', 'k', 'j'], ['f', 'o', 'n'], ['p', 'u', 'v'], ['v', 'q', 'w'], ['p', 'v', 'q'], ['b', 'c', 'i'], ['o', 'n', 'g'], ['p', 'q', 'i'], ['h', 'n', 'm'], ['u', 'm', 'l'], ['f', 'n', 'e'], ['d', 'e', 'l'], ['t', 'v', 'u'], ['h', 'n', 'g'], ['e', 'm', 'l'], ['p', 'h', 'i'], ['j', 's', 'k'], ['b', 'h', 'g'], ['p', 'u', 'm'], ['f', 'g', 'a'], ['d', 'e', 'a'], ['q', 'r', 'w'], ['t', 'v', 's'], ['r', 'j', 'q'], ['f', 'e', 'a'], ['b', 'h', 'i'], ['n', 'e', 'm'], ['d', 'c', 'a'], ['b', 'c', 'a'], ['q', 'i', 'j'], ['u', 't', 'l'], ['f', 'o', 'g'], ['d', 'c', 'k'], ['t', 's', 'k'], ['r', 's', 'w'], ['t', 'k', 'l'], ['d', 'k', 'l'], ['v', 's', 'w']]
Coordinate Data:
h : [7000741363059307991 / 25000000000000000000, 80225195072929604361 / 100000000000000000000, -13716291291326493629 / 100000000000000000000]
e : [126919765648998467971 / 100000000000000000000, 8066490868381496749 / 100000000000000000000, -9571898263972139219 / 50000000000000000000]
p : [21823094378755694391 / 50000000000000000000, 106610914830342770461 / 100000000000000000000, 10182865719344042739 / 12500000000000000000]
q : [-32300973292172713211 / 100000000000000000000, 103899954633094444259 / 100000000000000000000, 2929209171298267227 / 2000000000000000000]
a : [946122600644343451 / 2500000000000000000, -31628715079952269487 / 100000000000000000000, -4127882875115854267 / 10000000000000000000]
i : [-43900084483385047429 / 100000000000000000000, 66554324497751784491 / 100000000000000000000, 27211851080459820819 / 50000000000000000000]
c : [-2301566456903060019 / 25000000000000000000, -673174393736200949 / 2500000000000000000, 11708798581292575471 / 25000000000000000000]
t : [28607848481058738653 / 25000000000000000000, 40422708109651593507 / 100000000000000000000, 88513153943986448463 / 50000000000000000000]
s : [18036684371539787397 / 100000000000000000000, 37250098296382267091 / 100000000000000000000, 101722946875977152509 / 50000000000000000000]
d : [21350519044432409889 / 25000000000000000000, -1180064201448581817 / 2000000000000000000, 21160562899582289209 / 50000000000000000000]
l : [64678749470178825877 / 50000000000000000000, 5661227844485080183 / 25000000000000000000, 2492431457919790343 / 3125000000000000000]
f : [102139026950849505457 / 100000000000000000000, -9119670086169622687 / 100000000000000000000, -5724408843082498599 / 5000000000000000000]
o : [41572884957829317111 / 50000000000000000000, 67630960209974389189 / 100000000000000000000, -175713963392651706621 / 100000000000000000000]
j : [-23182667435856935397 / 50000000000000000000, 114269737629221133 / 2000000000000000000, 133747815888530792121 / 100000000000000000000]
w : [-15878806682675244991 / 100000000000000000000, 1530539965949629707 / 1250000000000000000, 48668841281615006781 / 20000000000000000000]
k : [6325524857342637573 / 12500000000000000000, -1759723022944425399 / 10000000000000000000, 12643207970729093487 / 10000000000000000000]
u : [17160053240770829321 / 12500000000000000000, 7234769295775650831 / 6250000000000000000, 14419962676983576659 / 12500000000000000000]
m : [1507842290086921153 / 1250000000000000000, 50368059588180699661 / 50000000000000000000, 17906789330634213461 / 100000000000000000000]
n : [25855130309538176729 / 25000000000000000000, 84456111088863418701 / 100000000000000000000, -79247136158033667857 / 100000000000000000000]
v : [7523813681964731811 / 12500000000000000000, 7776367831650109039 / 6250000000000000000, 178463208142670433389 / 100000000000000000000]
b : [-48270970730756427191 / 100000000000000000000, 18558228838045320467 / 100000000000000000000, -33196330678818817701 / 100000000000000000000]
r : [-10024800159425361901 / 12500000000000000000, 12697009348960537619 / 25000000000000000000, 27044119001252738333 / 12500000000000000000]
g : [16718375668398646387 / 100000000000000000000, 42084914796207805761 / 100000000000000000000, -26366456410851737851 / 25000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 23
|E| = 63
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 1953124999999999999897051451803336889340314948154710440365763169991805343259247329470638822912595361379310643083362681 / 3906249999999999999912512377654957167520282974141059065397584617783498384464112500000000000000000000000000000000000000
Collision distance in [707106781186547524390127159921 / 1000000000000000000000000000000, 353553390593273762195063579961 / 500000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [613 / 2500, 1227 / 5000] ~ [0.2452, 0.2454]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 814520710785661564639929450658535494325339 / 12500000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1276339069985449880994259305779 / 5000000000000000000000000000000000000000000000000, 1276339069990449880994259305779 / 5000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [1878845000000000000000000000 / 3968626966596885885752423630459, 1254607500000000000000000000 / 2645751311064590590501615753639] ~ [0.00047, 0.00047]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-99999999999966974320119541 / 500000000000000000000000000000, 25000000000008263154407317 / 125000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [7937253933193771771504847260917 / 125000000000000000000000000000, 3968626966596885885752423630459 / 62500000000000000000000000000] ~ [63.49803, 63.49803]
LHS := (LHS NUM) / (LHS DEN) in [-99999999999966974320119541 / 31749015732775087086019389043668, 25000000000008263154407317 / 7937253933193771771504847260917] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524390127159921 / 4795831523312719541597438064163, 117851130197757920731687859987 / 799305253885453256932906344027] ~ [0.14744, 0.14744]
Success: LHS < CD / |V| ^ .5
Success: existence proven