show/hide visualization coordinates
a : (-0.46490419714615383, 0.07983317668461531, 0.31802086616153846)
b : (-0.13640694694615385, -0.7935562367153846, -0.04153509493846147)
c : (-0.40627179394615387, -0.7177493279153846, 0.9183744199615385)
d : (-0.07172648984615382, 0.17055946808461536, 1.2329962922615385)
e : (0.38485910145384616, 0.5905469331846154, 0.44868759886153853)
f : (-0.15833408804615384, 0.7272769838846154, -0.3797120945384615)
g : (-0.5810916459461538, -0.1373540735153847, -0.6511696079384615)
h : (0.15998773385384615, -0.7150241215153845, -0.9933664350384614)
i : (0.4704207859538462, -0.047740064215384626, -0.3163410980384615)
j : (0.4907321285538462, -0.3883182633153847, 0.6236556782615386)
k : (0.9224982833538462, 0.27786991318461535, 1.2317439128615384)
l : (0.14591503125384617, 0.2610371696846153, -1.2104063276384616)
m : (-0.7556779025461539, 0.6926184424846153, -1.1809481102384616)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['b', 'a', 'c'], ['m', 'l', 'f'], ['m', 'g', 'f'], ['b', 'j', 'c'], ['i', 'l', 'f'], ['b', 'g', 'a'], ['g', 'a', 'f'], ['d', 'a', 'e'], ['b', 'h', 'g'], ['b', 'i', 'j'], ['i', 'h', 'l'], ['e', 'a', 'f'], ['k', 'e', 'j'], ['j', 'd', 'c'], ['b', 'i', 'h'], ['d', 'a', 'c'], ['m', 'g', 'l'], ['j', 'd', 'k'], ['l', 'h', 'g'], ['i', 'j', 'e'], ['k', 'd', 'e'], ['i', 'e', 'f']]
Coordinate Data:
k : [-6091167427 / 10000000000, 221559187 / 1000000000, -1537359209 / 2000000000]
m : [83520269 / 78125000, -1931893423 / 10000000000, 8220062093 / 5000000000]
b : [1124471219 / 2500000000, 12929853369 / 10000000000, 5045994033 / 10000000000]
f : [4717156287 / 10000000000, -2278478837 / 10000000000, 8427764029 / 10000000000]
e : [-89346951 / 1250000000, -91117833 / 1000000000, 28753419 / 2000000000]
c : [3598266673 / 5000000000, 12171784281 / 10000000000, -1138275279 / 2500000000]
a : [3891428689 / 5000000000, 839191847 / 2000000000, 725217211 / 5000000000]
h : [383484517 / 2500000000, 12144532217 / 10000000000, 7282153717 / 5000000000]
g : [4472365933 / 5000000000, 6367831737 / 10000000000, 11142339163 / 10000000000]
l : [837332547 / 5000000000, 476783861 / 2000000000, 418367659 / 250000000]
j : [-1773505879 / 10000000000, 1775494727 / 2000000000, -1605913699 / 10000000000]
d : [770216061 / 2000000000, 3288696321 / 10000000000, -7699319839 / 10000000000]
i : [-1570392453 / 10000000000, 1367922911 / 2500000000, 487128379 / 625000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 13
|E| = 33
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 3472222221146502033265267355955432109892038814951247300849 / 6944444445005829756047537291669138179381250000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [999 / 1250, 3997 / 5000] ~ [0.7992, 0.7994]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 2367100769418850159669 / 2000000000000000000000000000000000000000
rho in [108791101 / 100000000000000000, 1108791101 / 100000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [107892 / 15525845, 15976009 / 2297825056] ~ [0.00695, 0.00695]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-9997 / 50000000, 627 / 3125000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [71807033 / 1562500, 114891253 / 2500000] ~ [45.9565, 45.9565]
LHS := (LHS NUM) / (LHS DEN) in [-9997 / 2297825056, 627 / 143614066] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [35355339 / 180277564, 70710679 / 360555127] ~ [0.19612, 0.19612]
Success: LHS < CD / |V| ^ .5
Success: existence proven