show/hide visualization coordinates
a : (0.47137358754364284, -0.4201080594011286, -0.10095123563682773)
b : (0.28581269409248616, -0.5814269322142042, 0.8683492214433942)
c : (0.16656627533580654, -1.3215287913349445, 0.20651122786813092)
d : (-0.2857381735169102, -0.8777823456964602, -0.5671229088730367)
e : (0.15854893061785585, -0.08851955366791289, -0.9910016818952838)
f : (0.34613164111862765, 0.5602239042126813, -0.2534756467085162)
g : (0.7858126940924861, 0.23672360931509087, 0.5843955431870256)
h : (-0.21418730590751384, 0.23672360931509087, 0.5843955431870256)
i : (-0.5750605556800993, -0.6702830204447338, 0.367348379717199)
j : (-0.5774832228491769, 0.04835067912956445, -0.32803621640206015)
k : (-0.3280002447401659, 0.7844802506893458, -0.9572194150883184)
l : (-0.5195890141995254, 0.9903976369980811, 0.0024116460142427076)
m : (0.28581269409248616, 1.1027490130995294, 0.5843955431870256)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['j', 'e', 'd'], ['m', 'f', 'l'], ['m', 'h', 'l'], ['g', 'a', 'f'], ['g', 'h', 'b'], ['j', 'e', 'k'], ['a', 'b', 'c'], ['i', 'c', 'd'], ['j', 'l', 'k'], ['f', 'a', 'e'], ['j', 'h', 'l'], ['f', 'l', 'k'], ['a', 'e', 'd'], ['f', 'e', 'k'], ['i', 'b', 'c'], ['g', 'm', 'f'], ['g', 'm', 'h'], ['a', 'c', 'd'], ['i', 'h', 'b'], ['g', 'a', 'b'], ['j', 'i', 'd'], ['j', 'i', 'h']]
Coordinate Data:
h : [-356114119393499991496311992447 / 500000000000000000000000000000000000000000000000000000000000000, -174781937162172856810569800527 / 100000000000000000000000000000000000000000000000000000000000000, 93908937869444756164243030301 / 500000000000000000000000000000000000000000000000000000000000000000000000000000]
m : [1 / 2, 866025403784438646763723170753 / 1000000000000000000000000000000, -51999064087459459055575591983 / 125000000000000000000000000000000000000000000000000000000000000000000000000000]
g : [1, -27449478636542948161132980041 / 10000000000000000000000000000000000000000000000000000000000000, 22817463680441993938027405063 / 100000000000000000000000000000000000000000000000000000000000000000000000000000]
b : [1 / 2, -16363010830585900129698352521 / 20000000000000000000000000000, 70988419564092162791801460053 / 250000000000000000000000000000]
a : [171390223362789155655552050897 / 250000000000000000000000000000, -656831668716219406390240375067 / 1000000000000000000000000000000, -685346778823853320841858960609 / 1000000000000000000000000000000]
f : [560318947026141519183439213321 / 1000000000000000000000000000000, 161750147448795232415710306137 / 500000000000000000000000000000, -418935594947770896925338401813 / 500000000000000000000000000000]
e : [93184059131342421474975514857 / 250000000000000000000000000000, -81310790745750944864834648349 / 250000000000000000000000000000, -19692465313528868323788103619 / 12500000000000000000000000000]
k : [-113812938832652089621543217663 / 1000000000000000000000000000000, 68469580171781865680378221537 / 125000000000000000000000000000, -6166459833101375981588725229 / 4000000000000000000000000000]
j : [-72659183388332592803914877607 / 200000000000000000000000000000, -94186465092763208409591350543 / 500000000000000000000000000000, -912431759589085717105685894411 / 1000000000000000000000000000000]
l : [-305401708292011637269585929293 / 1000000000000000000000000000000, 188418506920747561563786847863 / 250000000000000000000000000000, -290991948586391425220441454631 / 500000000000000000000000000000]
i : [-902183124431463553021635563 / 2500000000000000000000000000, -907006629759824615782216648509 / 1000000000000000000000000000000, -217047163469826547924386322659 / 1000000000000000000000000000000]
c : [380753581243320348498439055079 / 1000000000000000000000000000000, -155825240065003542483204681489 / 100000000000000000000000000000, -94471078829723669208480592301 / 250000000000000000000000000000]
d : [-71550867609396390331302115477 / 1000000000000000000000000000000, -55725297750577552766628644799 / 50000000000000000000000000000, -115151845206006239031203719717 / 100000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 13
|E| = 33
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 21060843925709131711498585540648692212592270913543492959647040689973871749049798175710075373163572534287784771560131361 / 39854464985186301327719774018323282982905088116003046082052681339998937355586544400000000000000000000000000000000000000
Collision distance in [363470691720167037245569875817 / 500000000000000000000000000000, 145388276688066814898227950327 / 200000000000000000000000000000] ~ [0.72694, 0.72694]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [72517952857689499999 / 100000000000000000000, 72517952857689500001 / 100000000000000000000] ~ [0.72518, 0.72518]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 6055712291247878339548014274145974532982831716269579714544329929368286136574999159325267859975956591561562538374342340864793885168385929188984168911546133884141750932284982233084917985115746783157845803747228961545775490084572276345848710646043310513449 / 62500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [2460835689607877566054451662911 / 250000000000000000000000000000000000000000000000000000000000, 2710835689607877566054451662911 / 250000000000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [5258853486670076719294242504534621000001 / 919130023446084585576097834915040000000000, 5258853486670076719584314315965379000001 / 919130023446084585576097834914880000000000] ~ [0.00572, 0.00572]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-2310500001 / 100000000000000000000, 7689500001 / 100000000000000000000] ~ [-0.0, 0.0]
LHS DEN := 8 * |E| ^ .5 in [2872281323269014329925305734109 / 62500000000000000000000000000, 5744562646538028659850611468219 / 125000000000000000000000000000] ~ [45.9565, 45.9565]
LHS := (LHS NUM) / (LHS DEN) in [-1444062500625000000 / 2872281323269014329925305734109, 4805937500625000000 / 2872281323269014329925305734109] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [726941383440334074491139751634 / 3605551275463989293119221267471, 145388276688066814898227950327 / 721110255092797858623844253494] ~ [0.20162, 0.20162]
Success: LHS < CD / |V| ^ .5
Success: existence proven