show/hide visualization coordinates
a : (-1.1577871678487222, 0.3527847034925151, 0.5298583266984678)
b : (-1.0817110451085588, 0.7009144035704237, -0.40449606831045437)
c : (-0.8300395440976069, -0.2453583960177259, -0.20144621153015496)
d : (-0.3634133509321153, -0.23503647118457777, 0.682948187886542)
e : (-0.3072854245320749, 0.743304064855994, 0.8821953997061269)
f : (-0.9471209496349003, 1.3173956452089675, 0.3712850766706485)
g : (-1.8599024238343644, 0.9645708259248175, 0.16550697468853792)
h : (-0.16409009942365618, 1.0286232267514301, -0.17959892015231332)
i : (-0.28261214414128505, 0.2907384072695086, -0.8440374185056857)
j : (-0.24972167036151602, -0.708345183685822, -0.8714271066810539)
k : (-0.26893566368606936, -1.0248792332127414, 0.07695942736011108)
l : (0.49479766540574477, -0.747820803976733, 0.660011765339825)
m : (0.45524714371615727, 0.14059932979711598, 1.117335963408698)
n : (0.5891818621879226, 0.8839734396903299, 0.46200671491725376)
o : (-0.03177965366053043, 1.6579084141479896, 0.5862301070236222)
p : (0.6178477677763846, 0.4647983649341053, -0.44544605110415575)
q : (0.5242461982069626, -0.17312972183394865, -1.2098324077894322)
r : (0.6856068958102067, -1.0013479576419098, -0.6731599945389066)
s : (-0.060278645952928755, -1.6673006172077929, -0.6604393889778284)
t : (0.5545881973320224, -1.5901727877730756, 0.12441095532705138)
u : (1.307338816812328, -0.9320972177879951, 0.10700265096310502)
v : (1.0570604996302335, 0.010182710430360675, 0.3294196036112992)
w : (1.3187627363363656, -0.23030514575123667, -0.6052875860113052)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['h', 'f', 'o'], ['k', 's', 'j'], ['l', 'd', 'm'], ['v', 'n', 'm'], ['r', 'q', 'j'], ['h', 'n', 'p'], ['t', 'l', 'u'], ['h', 'i', 'p'], ['w', 'q', 'p'], ['e', 'a', 'd'], ['v', 'l', 'm'], ['f', 'b', 'g'], ['h', 'f', 'b'], ['v', 'u', 'l'], ['c', 'i', 'b'], ['c', 'a', 'd'], ['k', 'c', 'j'], ['o', 'e', 'f'], ['v', 'p', 'w'], ['k', 'l', 'd'], ['q', 'i', 'p'], ['t', 'l', 'k'], ['h', 'n', 'o'], ['b', 'a', 'g'], ['w', 'u', 'v'], ['r', 'u', 'w'], ['n', 'e', 'm'], ['r', 'u', 't'], ['i', 'c', 'j'], ['w', 'q', 'r'], ['c', 'k', 'd'], ['r', 't', 's'], ['n', 'o', 'e'], ['q', 'i', 'j'], ['h', 'i', 'b'], ['f', 'a', 'g'], ['r', 's', 'j'], ['e', 'd', 'm'], ['t', 's', 'k'], ['v', 'n', 'p'], ['c', 'b', 'a'], ['e', 'f', 'a']]
Coordinate Data:
s : [32051620283829807577 / 100000000000000000000, -111566966271028025473 / 100000000000000000000, -11859452547405329967 / 100000000000000000000]
m : [16720839850147682287 / 20000000000000000000, 2163219638420714873 / 3125000000000000000, 41479520672811828089 / 25000000000000000000]
p : [99864261656761138691 / 100000000000000000000, 20328586388632363617 / 20000000000000000000, 963988123996194023 / 10000000000000000000]
u : [168813366560355494011 / 100000000000000000000, -38046626329048246723 / 100000000000000000000, 64884751446688017953 / 100000000000000000000]
v : [143785534842146053937 / 100000000000000000000, 56181366492787341979 / 100000000000000000000, 21781611677876857611 / 25000000000000000000]
b : [-70091619631733195893 / 100000000000000000000, 5010181432271745829 / 4000000000000000000, 6867439759666040323 / 50000000000000000000]
t : [23384576153081230467 / 25000000000000000000, -103854183327556266583 / 100000000000000000000, 33312790941541327399 / 50000000000000000000]
d : [869074892955575319 / 50000000000000000000, 31659448331293499221 / 100000000000000000000, 24495861027806342999 / 20000000000000000000]
n : [96997671097914941073 / 100000000000000000000, 717802197093921303 / 500000000000000000, 5019257892105144713 / 5000000000000000000]
c : [-8984893906127601531 / 20000000000000000000, 15313627923989342069 / 50000000000000000000, 17019932598681007811 / 50000000000000000000]
i : [981827046499417579 / 10000000000000000000, 16847387235340428583 / 20000000000000000000, -15109627750095527839 / 50000000000000000000]
w : [42488939628189808261 / 25000000000000000000, 16066290437313805101 / 50000000000000000000, -6344272250752998451 / 100000000000000000000]
l : [21889812854924288547 / 25000000000000000000, -9809492473961010999 / 50000000000000000000, 7511603930272500939 / 6250000000000000000]
f : [-56632610084367357313 / 100000000000000000000, 93451329985324012199 / 50000000000000000000, 11414124252180295603 / 12500000000000000000]
j : [131073178429710799 / 1000000000000000000, -15671422918830920457 / 100000000000000000000, -16479112158863939051 / 50000000000000000000]
e : [3675471212957596447 / 50000000000000000000, 129493501935350667079 / 100000000000000000000, 17800503290123775033 / 12500000000000000000]
o : [34901519513069639943 / 100000000000000000000, 220953936864550264417 / 100000000000000000000, 5640374852636986573 / 5000000000000000000]
k : [11185918510515748453 / 100000000000000000000, -47324827871522858273 / 100000000000000000000, 3094021454319430967 / 5000000000000000000]
a : [-77699231905749537343 / 100000000000000000000, 5652597862437674093 / 6250000000000000000, 21434063804044859869 / 20000000000000000000]
r : [106640174460143363439 / 100000000000000000000, -44971700314439697697 / 100000000000000000000, -6565756551756571921 / 50000000000000000000]
h : [21670474936757064479 / 100000000000000000000, 158025418124894296953 / 100000000000000000000, 18112297167573091503 / 50000000000000000000]
g : [-36977689376078442787 / 25000000000000000000, 7581008902111651257 / 5000000000000000000, 70735183819231311481 / 100000000000000000000]
q : [45252052349909470437 / 50000000000000000000, 37850123266356409373 / 100000000000000000000, -6679875442856570739 / 10000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 23
|E| = 63
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 2222222222222222222182235990937081284695348455626326914842917097899238977334405912275207139621422618998143389281629761 / 4444444444444444444422673336366008859838600388784277976974809631117942538845480400000000000000000000000000000000000000
Collision distance in [141421356237309504879242894541 / 200000000000000000000000000000, 353553390593273762198107236353 / 500000000000000000000000000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [4719 / 10000, 4721 / 10000] ~ [0.4719, 0.4721]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 427665999488775151471230243517312086706573 / 10000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [2068008702807546580154615557331 / 10000000000000000000000000000000000000000000000000, 2068008702817546580154615557331 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [535311562500000000000000000 / 305278997430529683519417202343, 13929900625000000000000000000 / 7937253933193771771504847260917] ~ [0.00175, 0.00176]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999972185028239377 / 1000000000000000000000000000000, 100000000000013913380131653 / 500000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [7937253933193771771504847260917 / 125000000000000000000000000000, 3968626966596885885752423630459 / 62500000000000000000000000000] ~ [63.49803, 63.49803]
LHS := (LHS NUM) / (LHS DEN) in [-199999999999972185028239377 / 63498031465550174172038778087336, 33333333333337971126710551 / 10583005244258362362006463014556] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707106781186547524396214472705 / 4795831523312719541597438064163, 353553390593273762198107236353 / 2397915761656359770798719032081] ~ [0.14744, 0.14744]
Success: LHS < CD / |V| ^ .5
Success: existence proven