show/hide visualization coordinates
a : (0.6241834977825946, 0.5468451094349308, 0.7111638748544682)
b : (0.9390964816581449, -0.20120557948382234, 0.12699782021351563)
c : (0.6373441716851946, 0.659830726339386, -0.2823455851081177)
d : (0.1538502367791813, 1.3222690136240765, 0.2898511734010734)
e : (-0.3112472408443041, 0.7722377893211612, 0.9835009327177674)
f : (0.31403886102226497, 0.35336757356315573, 1.6419574864579156)
g : (0.7047006555077737, -0.37798248755438146, 1.0829311450099148)
h : (1.0919117290231148, -1.1080337188588893, 0.5198212230427477)
i : (0.5408737883562892, -1.008418764444825, -0.30869193243684256)
j : (0.6773907197178746, -0.17083699173045896, -0.8376719901595098)
k : (0.39964340298721274, 0.6953797375557852, -1.253033285845036)
l : (-0.2565699022433169, 1.0070415024801256, -0.5658280455254723)
m : (-0.8338456120969365, 1.1766127581688632, 0.2329199397972727)
n : (-0.9002268326313282, 0.19593627895099275, 0.4169503086748201)
o : (-0.28311556656618997, -0.22235840048508015, 1.0834360522965087)
p : (0.09988985292678138, -1.0025158443997804, 0.5888036520804549)
q : (-0.4156066758516812, -1.2863214624387245, -0.21972445502955062)
r : (-0.12349965848219546, -0.7448858886055121, -1.0080904929785501)
s : (0.24030861135028042, -0.16503652498069477, -1.7370748949415786)
t : (-0.453656294561101, 0.1932439334366814, -1.112536807648544)
u : (-1.1438904803869732, 0.5530697357537986, -0.48476124209654015)
v : (-0.8248587298302422, -0.3899201948093357, -0.3899523132277726)
w : (-0.8767150153024369, -0.798318300837453, 0.521377436451054)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['e', 'n', 'o'], ['j', 'k', 's'], ['i', 'b', 'h'], ['p', 'o', 'w'], ['r', 'j', 's'], ['o', 'p', 'g'], ['a', 'c', 'd'], ['i', 'p', 'h'], ['b', 'g', 'h'], ['a', 'b', 'g'], ['r', 'j', 'i'], ['v', 'n', 'w'], ['c', 'j', 'b'], ['k', 't', 's'], ['w', 'p', 'q'], ['m', 'u', 'l'], ['a', 'b', 'c'], ['c', 'k', 'l'], ['v', 'n', 'u'], ['r', 'v', 'q'], ['m', 'd', 'l'], ['n', 'u', 'm'], ['v', 'u', 't'], ['i', 'j', 'b'], ['f', 'a', 'g'], ['r', 'v', 't'], ['k', 't', 'l'], ['u', 't', 'l'], ['c', 'd', 'l'], ['v', 'w', 'q'], ['r', 'i', 'q'], ['p', 'g', 'h'], ['e', 'm', 'd'], ['c', 'j', 'k'], ['e', 'n', 'm'], ['r', 't', 's'], ['f', 'o', 'g'], ['n', 'w', 'o'], ['e', 'f', 'a'], ['e', 'a', 'd'], ['p', 'i', 'q'], ['e', 'f', 'o']]
Coordinate Data:
e : [17439193267672693589 / 20000000000000000000, -20996282138371349551 / 100000000000000000000, -2458852142735905943 / 6250000000000000000]
q : [97631909839101181501 / 100000000000000000000, 46214910759404302559 / 25000000000000000000, 40490452245478654991 / 50000000000000000000]
g : [-14398823296844315599 / 100000000000000000000, 1880514910983658347 / 2000000000000000000, -24642327756494621849 / 50000000000000000000]
i : [991931709152071773 / 50000000000000000000, 31413874647645452473 / 20000000000000000000, 22469413057921624671 / 25000000000000000000]
d : [8137243715202986919 / 20000000000000000000, -37999702284331445997 / 50000000000000000000, 1501167082394745193 / 5000000000000000000]
u : [42615072573157593521 / 25000000000000000000, 92052321836490993 / 10000000000000000000, 26871145799414065089 / 25000000000000000000]
w : [17967842973022094911 / 12500000000000000000, 27211865375498014993 / 20000000000000000000, 1717678835724209411 / 25000000000000000000]
t : [25359217927510790363 / 25000000000000000000, 7380620690015326183 / 20000000000000000000, 21282767469107080973 / 12500000000000000000]
o : [84382798910552058597 / 100000000000000000000, 19615834210563195223 / 25000000000000000000, -49335146241648621057 / 100000000000000000000]
v : [34639278809239323661 / 25000000000000000000, 95219516274678341321 / 100000000000000000000, 12250461288847438119 / 12500000000000000000]
b : [-9459601477970356039 / 25000000000000000000, 76348054742126997487 / 100000000000000000000, 46308676966650677913 / 100000000000000000000]
f : [6166839037926641451 / 25000000000000000000, 20890739437429195221 / 100000000000000000000, -52593644828894655993 / 50000000000000000000]
c : [-3831587457293198221 / 50000000000000000000, -1219446980024229401 / 12500000000000000000, 87243017498814011501 / 100000000000000000000]
p : [11520564240313730783 / 25000000000000000000, 156479081233722809743 / 100000000000000000000, 1280937799567481 / 1000000000000000000]
m : [139455803463626722693 / 100000000000000000000, -61433779023141551439 / 100000000000000000000, 8929116252068742899 / 25000000000000000000]
l : [81728232478264751299 / 100000000000000000000, -44476653454267775873 / 100000000000000000000, 115591263540549479639 / 100000000000000000000]
j : [-1458478714731798977 / 12500000000000000000, 9163899495848832869 / 12500000000000000000, 28555131600790644031 / 20000000000000000000]
h : [-2124797225935137417 / 4000000000000000000, 83515434339816847533 / 50000000000000000000, 3513168341863737473 / 50000000000000000000]
a : [-3173553762163202227 / 50000000000000000000, 771492925125845447 / 50000000000000000000, -6053964248722289841 / 50000000000000000000]
n : [2921878510341317729 / 2000000000000000000, 18316934449322747001 / 50000000000000000000, 8656714060260116617 / 50000000000000000000]
r : [68421208102152612907 / 100000000000000000000, 32679021413573996857 / 25000000000000000000, 4994297133933039093 / 3125000000000000000]
k : [16106901955211788661 / 100000000000000000000, -3327619240458437997 / 25000000000000000000, 46077946893126457769 / 25000000000000000000]
s : [16020190559452510331 / 50000000000000000000, 18182787322953561899 / 25000000000000000000, 232715948482160126291 / 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 = 140615034829168175909892564517330309771240370240295692468583368248632293787727174516245348095484176587853325444864287761 / 235154226299591548697782213620339279753748485126522846513871687652918518745501850000000000000000000000000000000000000000
Collision distance in [154656964110747701581009451867 / 200000000000000000000000000000, 96660602569217313488130907417 / 125000000000000000000000000000] ~ [0.77328, 0.77328]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [4803 / 10000, 961 / 2000] ~ [0.4803, 0.4805]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 2868953527908988578493441365964688668318877 / 50000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1197696440653680113142618589007 / 5000000000000000000000000000000000000000000000000, 1197696440658680113142618589007 / 5000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [7209002812500000000000000000 / 3968626966596885885752423630459, 14430015625000000000000000000 / 7937253933193771771504847260917] ~ [0.00182, 0.00182]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-49999999999992086226194089 / 250000000000000000000000000000, 200000000000031668276608421 / 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 [-49999999999992086226194089 / 15874507866387543543009694521834, 200000000000031668276608421 / 63498031465550174172038778087336] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [773284820553738507905047259335 / 4795831523312719541597438064163, 386642410276869253952523629668 / 2397915761656359770798719032081] ~ [0.16124, 0.16124]
Success: LHS < CD / |V| ^ .5
Success: existence proven