show/hide visualization coordinates
a : (0.1737517005624999, -0.35566914831249996, -0.3631666978499999)
b : (0.4811939635625, -0.022015796312499947, 0.52798687795)
c : (-0.4517675992375001, -0.36445262581250004, 0.4169925526500001)
d : (-0.5268861225375001, -1.0656308009125, -0.2920253414499999)
e : (-0.7899175845375, -0.12185815371250003, -0.4922942609499999)
f : (-0.18506953303750007, 0.5043108490874999, -0.00028692934999985376)
g : (0.7650183532624999, 0.4488698954874999, -0.3073037187499999)
h : (0.5336768219624999, 0.9764457804875, 0.5100975177500001)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['a', 'g', 'b'], ['f', 'c', 'b'], ['f', 'e', 'c'], ['e', 'c', 'd'], ['g', 'h', 'b'], ['f', 'a', 'e'], ['a', 'e', 'd'], ['f', 'h', 'b'], ['f', 'g', 'h'], ['a', 'c', 'd'], ['a', 'c', 'b'], ['f', 'a', 'g']]
Coordinate Data:
b : [2237386239 / 2000000000, 2782328003 / 5000000000, 2947716873 / 2500000000]
e : [-762092143 / 5000000000, 285389527 / 625000000, 1588056103 / 10000000000]
g : [3506293773 / 2500000000, 2568378231 / 2500000000, 137518461 / 400000000]
d : [553065167 / 5000000000, -121787351 / 250000000, 1795372649 / 5000000000]
h : [11711759779 / 10000000000, 7774635887 / 5000000000, 1161197389 / 1000000000]
c : [1857315567 / 10000000000, 2140287711 / 10000000000, 10680924239 / 10000000000]
a : [1622501713 / 2000000000, 1114061243 / 5000000000, 1439665867 / 5000000000]
f : [4524296229 / 10000000000, 541396123 / 500000000, 6508129419 / 10000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 8
|E| = 18
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 499999999855289122962267654088484081106985982262149313372649 / 999999999859042455179781696486683248661000000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [1701 / 2000, 8507 / 10000] ~ [0.8505, 0.8507]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 2453915808602570121069 / 10000000000000000000000000000000000000000
rho in [99074029 / 200000000000000000, 2099074029 / 200000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [72335025 / 6788225104, 72369049 / 6788225088] ~ [0.01066, 0.01066]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-19999 / 100000000, 10021 / 50000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [106066017 / 3125000, 424264069 / 12500000] ~ [33.94113, 33.94113]
LHS := (LHS NUM) / (LHS DEN) in [-19999 / 3394112544, 10021 / 1697056272] ~ [-1e-05, 1e-05]
CD / |V| ^ .5 in [70710678 / 282842713, 70710679 / 282842712] ~ [0.25, 0.25]
Success: LHS < CD / |V| ^ .5
Success: existence proven