show/hide visualization coordinates
a : (0.45562349766645405, -0.8691115038610218, 0.7186621644037218)
b : (-0.27325099145248394, -0.23606512976557295, 0.979419268537458)
c : (-0.49759262119823583, -1.171083499548192, 0.7048077587057077)
d : (0.21744813709826616, -1.7547736323402834, 0.3200707799060162)
e : (1.1708198500163203, -1.4533466922277576, 0.33504331416362854)
f : (1.03297564995222, -0.5303560246672081, -0.024243763400844665)
g : (0.5780884345594063, 0.11492207373716301, 0.5895100936068413)
h : (-0.01632934865216462, 0.7202499337351123, 1.118892451560093)
i : (-0.8262855877921691, 0.49392148988873685, 0.5778320795273059)
j : (-0.7802520192499467, -0.4006768719293539, 0.13333834323886617)
k : (-0.35881608432834244, -1.2053186139809504, -0.28492403817371725)
l : (0.6150648186471533, -1.3136396524146292, -0.4844798936435144)
m : (0.4659835369165325, -0.38933166613343095, -0.8358052669576995)
n : (0.8287342268654397, 0.3974528115469188, -0.3364235265798089)
o : (0.45158733798160067, 1.06528934779834, 0.3052575352047394)
p : (-0.4502812759909089, 1.4201685461528724, 0.5516185664303556)
q : (-1.3048593373594504, 1.2137797482178, 0.07506846296325809)
r : (-0.9386572748973918, 0.42163808468207276, -0.4132015794716482)
s : (-0.5340164630834675, -0.38933166613343095, -0.8358052669576995)
t : (-0.03401646308346751, -1.16062037463066, -1.2296500690621277)
u : (-0.03401646308346751, 0.47669373765100764, -0.8358052669576995)
v : (0.5222740784789578, 1.2902601397021836, -0.666540554682258)
w : (0.16160315070565234, 1.9645697606691606, -0.022162546886744572)
x : (-0.45182878871650783, 1.2947096538511225, -0.44047904547423017)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['w', 'p', 'x'], ['m', 't', 'l'], ['e', 'd', 'l'], ['u', 'x', 'r'], ['f', 'a', 'g'], ['s', 'r', 'j'], ['a', 'e', 'd'], ['f', 'n', 'm'], ['b', 'a', 'g'], ['b', 'i', 'j'], ['k', 'j', 'c'], ['p', 'h', 'o'], ['b', 'h', 'g'], ['s', 't', 'k'], ['f', 'a', 'e'], ['q', 'r', 'x'], ['n', 'o', 'g'], ['i', 'p', 'q'], ['w', 'v', 'o'], ['u', 'n', 'v'], ['k', 's', 'j'], ['f', 'e', 'l'], ['u', 'x', 'v'], ['f', 'm', 'l'], ['b', 'c', 'j'], ['i', 'r', 'j'], ['a', 'd', 'c'], ['w', 'p', 'o'], ['q', 'p', 'x'], ['i', 'r', 'q'], ['k', 'd', 'c'], ['m', 's', 't'], ['u', 's', 'r'], ['b', 'a', 'c'], ['i', 'p', 'h'], ['m', 'u', 'n'], ['m', 'u', 's'], ['d', 'k', 'l'], ['n', 'o', 'v'], ['w', 'x', 'v'], ['t', 'k', 'l'], ['b', 'i', 'h'], ['f', 'n', 'g'], ['o', 'h', 'g']]
Coordinate Data:
s : [-9252702150422335666693891281 / 625000000000000000000000000000000000000000000000000000000000, -12163072980910839124569095861 / 1000000000000000000000000000000000000000000000000000000000000, -410902518498130621102703785823 / 500000000000000000000000000000000000000000000000000000000000000000000000000000]
v : [52814527078121270339868767553 / 50000000000000000000000000000, 167959180583561445514805855669 / 100000000000000000000000000000, 33852942455088308290097871449 / 200000000000000000000000000000]
r : [-80928162362784870539496284557 / 200000000000000000000000000000, 101371218851937961347063570333 / 125000000000000000000000000000, 422603687486051296132814223321 / 1000000000000000000000000000000]
k : [87600189377562543008320393301 / 500000000000000000000000000000, -12749796060117491758155320189 / 15625000000000000000000000000, 550881228783982301779954111209 / 1000000000000000000000000000000]
h : [103537422886260567027409279091 / 200000000000000000000000000000, 110958159986854325843710980187 / 100000000000000000000000000000, 1221686074073620352650442221 / 625000000000000000000000000]
m : [1, -747385731271711932169840967099 / 100000000000000000000000000000000000000000000000000000000000000, 671518588863581112426927873979 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000]
d : [751464600181733637901929958663 / 1000000000000000000000000000000, -136544196620685242922644269267 / 100000000000000000000000000000, 115587604686371573566712511043 / 100000000000000000000000000000]
p : [83735187092558607072558601557 / 1000000000000000000000000000000, 180950021228630335289219340103 / 100000000000000000000000000000, 69371191669402755045095430011 / 50000000000000000000000000000]
o : [985603801065068165228042626973 / 1000000000000000000000000000000, 145462101393177095180492886701 / 100000000000000000000000000000, 57053140108121950668809418229 / 50000000000000000000000000000]
g : [111210489764287386826868463829 / 100000000000000000000000000000, 504253739870593913563297503493 / 1000000000000000000000000000000, 14253153605645408019397633891 / 10000000000000000000000000000]
a : [989639960749921552535844594643 / 1000000000000000000000000000000, -95955967545518177840147994937 / 200000000000000000000000000000, 77723371568071061658813312979 / 50000000000000000000000000000]
w : [347809806894559916023458637257 / 500000000000000000000000000000, 117695071340129576959327345661 / 50000000000000000000000000000, 406821360035477456833589375441 / 500000000000000000000000000000]
t : [1 / 2, -192822177124307297772092393637 / 250000000000000000000000000000, -196922401052214102214424119587 / 500000000000000000000000000000]
x : [51367296479349798125326229 / 625000000000000000000000000, 168404131998455342482047081949 / 100000000000000000000000000000, 197663110741734681209453194181 / 500000000000000000000000000000]
n : [34068767248722679838175242649 / 25000000000000000000000000000, 786784477680349805855785611957 / 1000000000000000000000000000000, 499381740377890608937111021793 / 1000000000000000000000000000000]
l : [57454064086531040510196921017 / 50000000000000000000000000000, -46215399314059910982830868569 / 50000000000000000000000000000, 175662686657092568227558135167 / 500000000000000000000000000000]
f : [156699211303568735071309595851 / 100000000000000000000000000000, -141024358533777135623571356837 / 1000000000000000000000000000000, 811561503556854905976580167497 / 1000000000000000000000000000000]
e : [170483631309978763165617952507 / 100000000000000000000000000000, -106401502609432654087093406839 / 100000000000000000000000000000, 117084858112132794795975075249 / 100000000000000000000000000000]
b : [260765471630983580919392435687 / 1000000000000000000000000000000, 153266536367857992105779219827 / 1000000000000000000000000000000, 90761226774757873148586284879 / 50000000000000000000000000000]
i : [-292269124708701518951169420699 / 1000000000000000000000000000000, 883253156022167756093622626597 / 1000000000000000000000000000000, 70681867324250266522483820267 / 50000000000000000000000000000]
u : [1 / 2, 866025403784438646763723170753 / 1000000000000000000000000000000, 150286448104701957877811282481 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000]
q : [-19271071856899570582172622569 / 25000000000000000000000000000, 80155570717561549485916148347 / 50000000000000000000000000000, 910873729920957628072993179631 / 1000000000000000000000000000000]
c : [36423841885231697624073427391 / 1000000000000000000000000000000, -39087591670738051008573500317 / 50000000000000000000000000000, 154061302566340713442441707433 / 100000000000000000000000000000]
j : [-246235556166479199273774564673 / 1000000000000000000000000000000, -11345205795922975941478117029 / 1000000000000000000000000000000, 484571805098282834278914454107 / 500000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 24
|E| = 66
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 561090651641629273793026160272634890683922789168342097631143945075503150801417518480163734137829679769544945453527674009 / 954861295999047628696582395534037648369820982791989942928362995104655948743084940000000000000000000000000000000000000000
Collision distance in [383280192291886804005831426933 / 500000000000000000000000000000, 766560384583773608011662853867 / 1000000000000000000000000000000] ~ [0.76656, 0.76656]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [50191217468015579999 / 100000000000000000000, 50191217468015580001 / 100000000000000000000] ~ [0.50191, 0.50191]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 571069988035170883536867398479640251993181201110016008118222861030052863271647709066869862523444633630591135532476861825843318173367387991047144282437774028383632790223936472382075088313470500053626569994894333733351766655467387532820328995856045982900957 / 500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [1689778074238109652980276741819 / 50000000000000000000000000000000000000000000000000000000000, 1739778074238109652980276741819 / 50000000000000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [2519158310921632289259920687800368840001 / 1299846144741753657673581370922720000000000, 2519158310921632289460685557672431160001 / 1299846144741753657673581370922560000000000] ~ [0.00194, 0.00194]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-1984420001 / 100000000000000000000, 8015580001 / 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 [-1240262500625000000 / 4062019202317980180229941784133, 385364423125000000 / 312463015562921552325380137241] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [127760064097295601335277142311 / 816496580927726032732428024902, 766560384583773608011662853867 / 4898979485566356196394568149411] ~ [0.15647, 0.15647]
Success: LHS < CD / |V| ^ .5
Success: existence proven