show/hide visualization coordinates
a : (0.6607299931698826, -0.19855122562274885, 0.6078564252627764)
b : (0.5733545704079565, -0.9724879873017436, -0.019349620960476877)
c : (1.2487063498865596, -0.2571812193326021, -0.19889404903504904)
d : (1.2903733642658377, 0.5479542725512346, 0.3927314233896001)
e : (0.46154406761043487, 0.729734459491037, 0.9218797585866795)
f : (-0.2269949813689358, 0.01090948539685932, 1.0178205457894562)
g : (0.017146745540664865, -0.9364998803591946, 0.8109140189245226)
h : (-0.4003767069749734, -1.1965777864093172, -0.0597372599374596)
i : (0.0996232930250266, -0.9865422096994781, -0.8999069193016652)
j : (1.0991674835947358, -0.9834156318203979, -0.8698796715238337)
k : (0.5985412911206162, -0.12114150000581458, -0.9464089927822403)
l : (1.1156824099676008, 0.6551930633250899, -0.5860345916720858)
m : (0.6334836381696233, 1.231256089600305, 0.07399247916301444)
n : (0.16024778245254956, 1.6790773176452323, 0.8326122604606433)
o : (-0.49121817980053284, 0.9713386914770111, 1.1059218597344054)
p : (-0.9169063173547699, 0.39783114778746687, 0.4060085030417425)
q : (-0.8881122853497475, -0.5887264952183517, 0.5668653361191643)
r : (-1.400237624734882, -1.180378738312537, -0.05577040008723111)
s : (-0.9003767069749734, -0.9865422096994781, -0.8999069193016652)
t : (-0.4003767069749734, -0.12051680591503955, -0.8999069193016652)
u : (0.11589581567078489, 0.6709034177995968, -0.5726200239690533)
v : (-0.3634732332010655, 1.1863232476178998, 0.13769519761483517)
w : (-0.8838209475529786, 0.6827419397195086, -0.5519743772571359)
x : (-1.2026031145944374, -0.2347014427145412, -0.31390806295727325)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['w', 'p', 'x'], ['q', 'h', 'g'], ['i', 't', 'k'], ['u', 'k', 'l'], ['f', 'a', 'g'], ['m', 'd', 'l'], ['s', 'x', 't'], ['a', 'e', 'd'], ['b', 'a', 'g'], ['b', 'i', 'j'], ['k', 'j', 'c'], ['f', 'q', 'g'], ['b', 'h', 'g'], ['f', 'e', 'o'], ['v', 'p', 'o'], ['w', 'u', 't'], ['f', 'a', 'e'], ['q', 'r', 'x'], ['w', 'p', 'v'], ['i', 'j', 'k'], ['w', 'x', 't'], ['k', 'c', 'l'], ['m', 'e', 'd'], ['f', 'p', 'o'], ['i', 's', 'h'], ['b', 'c', 'j'], ['a', 'd', 'c'], ['u', 'm', 'l'], ['u', 'w', 'v'], ['q', 'p', 'x'], ['x', 's', 'r'], ['m', 'n', 'e'], ['b', 'a', 'c'], ['n', 'e', 'o'], ['i', 's', 't'], ['m', 'n', 'v'], ['u', 't', 'k'], ['n', 'o', 'v'], ['q', 'r', 'h'], ['m', 'u', 'v'], ['s', 'r', 'h'], ['d', 'c', 'l'], ['b', 'i', 'h'], ['f', 'q', 'p']]
Coordinate Data:
s : [-34766786803803235957682269051 / 200000000000000000000000000000000000000000000000000000, -260774079705310807856621747491 / 5000000000000000000000000000000000000000000000000000000, -99247059077973200700821108311 / 50000000000000000000000000000000000000000000000000000000000000000000000]
v : [134225868443476964792606511131 / 250000000000000000000000000000, 1697551138529201738309774517 / 781250000000000000000000000, 103760211691650038030205773187 / 100000000000000000000000000000]
r : [-62482614719988583310517659051 / 125000000000000000000000000000, -193836528613058818340790453129 / 1000000000000000000000000000000, 168827303842886818128146948159 / 200000000000000000000000000000]
k : [14989179980955895004669745637 / 10000000000000000000000000000, 865400709693663557133583016039 / 1000000000000000000000000000000, -46502073480575054916574328923 / 1000000000000000000000000000000]
h : [249999999999999999999998759691 / 500000000000000000000000000000, -42007115341967835443264351407 / 200000000000000000000000000000, 13127650927565712425049991419 / 15625000000000000000000000000]
m : [153386034514459671787337142117 / 100000000000000000000000000000, 221779829929978350942139085751 / 100000000000000000000000000000, 243474849616169902100889669207 / 250000000000000000000000000000]
d : [219075007124081122276881733829 / 100000000000000000000000000000, 76724824112535639949928637539 / 50000000000000000000000000000, 32315958567281635641458389121 / 25000000000000000000000000000]
p : [-16529610379796452804895826961 / 1000000000000000000000000000000, 4326166742146702977266123043 / 3125000000000000000000000000, 65295771117170388598524257461 / 50000000000000000000000000000]
o : [12786203974201268075877558051 / 31250000000000000000000000000, 97894045058824458340305151361 / 50000000000000000000000000000, 40116575580721409729342723511 / 20000000000000000000000000000]
g : [458761726257819124483071928219 / 500000000000000000000000000000, 50042329340283537316388447497 / 1000000000000000000000000000000, 171082093822618780797618921899 / 100000000000000000000000000000]
a : [78055335007242803965244409689 / 50000000000000000000000000000, 787990984076729287409183120989 / 1000000000000000000000000000000, 75388167228222076109799105709 / 50000000000000000000000000000]
w : [8277879710997412654600695281 / 500000000000000000000000000000, 41732103735474670428206177453 / 25000000000000000000000000000, 347932542044529223044836525347 / 1000000000000000000000000000000]
t : [499999999999999999999999979989 / 1000000000000000000000000000000, 866025403784438646763723309723 / 1000000000000000000000000000000, 528902256852520650113502489593 / 100000000000000000000000000000000000000000000000000000000000000000000000]
l : [201605911694257432464403728937 / 100000000000000000000000000000, 164173527302456809267014715683 / 100000000000000000000000000000, 7846808190739484998477538711 / 25000000000000000000000000000]
x : [-3777830095243300862403435771 / 12500000000000000000000000000, 375920383492468453988681577279 / 500000000000000000000000000000, 292999428172195992795023970277 / 500000000000000000000000000000]
n : [106062448942752285778245920077 / 100000000000000000000000000000, 53312390546894208739670516177 / 20000000000000000000000000000, 173251917976230857511808683603 / 100000000000000000000000000000]
f : [134676345121207518499422669427 / 200000000000000000000000000000, 997451695096337489056703403371 / 1000000000000000000000000000000, 19177274650911215793808127593 / 10000000000000000000000000000]
e : [34048019364635205594602049599 / 25000000000000000000000000000, 171627666919051523951886788739 / 100000000000000000000000000000, 182178667788834459087646875679 / 100000000000000000000000000000]
b : [5894925109531719151318202381 / 4000000000000000000000000000, 3513555599433636268025160571 / 250000000000000000000000000000, 44027864917059419357972399271 / 50000000000000000000000000000]
i : [20000000000000000000000003877 / 20000000000000000000000000000, -868155480824532091933886962037 / 10000000000000000000000000000000000000000000000000000000, -1290656791866636417332270843 / 390625000000000000000000000000000000000000000000000000000000000000000]
u : [20325450452915166983595363123 / 20000000000000000000000000000, 41436140687476872715323451931 / 25000000000000000000000000000, 327286895332611848791312398793 / 1000000000000000000000000000000]
q : [6132210812612926764740373533 / 500000000000000000000000000000, 397815714481126344321058031471 / 1000000000000000000000000000000, 73338612771041474993410677489 / 50000000000000000000000000000]
c : [214908305686153267040384252131 / 100000000000000000000000000000, 22792530948964878447964789133 / 31250000000000000000000000000, 350506435133308117459958101953 / 500000000000000000000000000000]
j : [99977209528485450502235873887 / 50000000000000000000000000000, 3126577879080210664555577187 / 1000000000000000000000000000000, 30027247777831454217321344059 / 1000000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 24
|E| = 66
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 562495854106807631312753670926178414039914700839037679740176806023202198873017749993166481479952378512834394670100617001 / 936477780670129999492879226235367900906710541786726295423610823649382002485898540000000000000000000000000000000000000000
Collision distance in [775016456197549141615321944661 / 1000000000000000000000000000000, 387508228098774570807660972331 / 500000000000000000000000000000] ~ [0.77502, 0.77502]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [42066483672656539999 / 100000000000000000000, 42066483672656540001 / 100000000000000000000] ~ [0.42066, 0.42066]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 106323369843990460438846030501262494858939522738105976835434887456294579477301014986026732505191777242178341197053676987892645536562538300567412312997526441335284866714823292808939312797301060213816155792467031334385268394387698181092830615299 / 50000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [145824119982937294898395650167 / 100000000000000000000000000000000000000000000000000, 145824120082937294898395650167 / 100000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [1769589048581879261880327837426286920001 / 1299846144741753657673581370922720000000000, 1769589048581879262048593772116913080001 / 1299846144741753657673581370922560000000000] ~ [0.00136, 0.00136]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-7343460001 / 100000000000000000000, 2656540001 / 100000000000000000000] ~ [-0.0, 0.0]
LHS DEN := 8 * |E| ^ .5 in [4062019202317980180229941784133 / 62500000000000000000000000000, 8124038404635960360459883568267 / 125000000000000000000000000000] ~ [64.99231, 64.99231]
LHS := (LHS NUM) / (LHS DEN) in [-4589662500625000000 / 4062019202317980180229941784133, 1660337500625000000 / 4062019202317980180229941784133] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [775016456197549141615321944661 / 4898979485566356196394568149412, 59616650476734549355024764974 / 376844575812796630491889857647] ~ [0.1582, 0.1582]
Success: LHS < CD / |V| ^ .5
Success: existence proven