show/hide visualization coordinates
a : (0.02971052839999988, -0.11882085176666668, 0.5678892978888889)
b : (0.40605657289999997, 0.34206042543333326, -0.23582215731111106)
c : (-0.4535949994000001, 0.6585346905333334, 0.16523047488888898)
d : (-0.5083446367000001, 0.4911810225333333, 1.1496060266888888)
e : (-0.9686572089000001, -0.1256983152666667, 0.5111921965888889)
f : (-0.42001648320000007, -0.21517067346666668, -0.32006471381111107)
g : (0.4640954113999999, -0.6531554235666667, -0.15722885711111106)
h : (1.1803710099, -0.1469079449666667, -0.637502484611111)
i : (0.27037980559999997, -0.2320229294666667, -1.043299783211111)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['d', 'e', 'c'], ['d', 'a', 'c'], ['g', 'f', 'a'], ['f', 'e', 'c'], ['h', 'i', 'b'], ['g', 'a', 'b'], ['g', 'f', 'i'], ['h', 'g', 'i'], ['d', 'a', 'e'], ['h', 'g', 'b'], ['f', 'i', 'b'], ['f', 'b', 'c'], ['a', 'b', 'c'], ['f', 'a', 'e']]
Coordinate Data:
f : [347394533 / 2500000000, 739332867 / 2000000000, 1244182543 / 5000000000]
a : [735856031 / 1250000000, 582520319 / 1250000000, 11367905203 / 10000000000]
e : [-32774633 / 80000000, 4591387917 / 10000000000, 1080093419 / 1000000000]
d : [506296597 / 10000000000, 2152036259 / 2000000000, 17185072491 / 10000000000]
i : [414677051 / 500000000, 141125671 / 400000000, -592998201 / 1250000000]
h : [17393453063 / 10000000000, 218964581 / 500000000, -343006311 / 5000000000]
g : [5115348539 / 5000000000, -341591583 / 5000000000, 4116723653 / 10000000000]
c : [105379297 / 1000000000, 497348719 / 400000000, 7341316973 / 10000000000]
b : [9650308693 / 10000000000, 2317243831 / 2500000000, 3330790651 / 10000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 9
|E| = 21
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 124999999910561544990684031030615965479794543241714274143929 / 249999999901975487050012775663056317360550000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [524 / 625, 4193 / 5000] ~ [0.8384, 0.8386]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 6006429255184994539859 / 10000000000000000000000000000000000000000
rho in [193752891 / 250000000000000000, 2693752891 / 250000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [2196608 / 229128785, 2511607 / 261861468] ~ [0.00959, 0.00959]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-19997 / 100000000, 1253 / 6250000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [458257569 / 12500000, 45825757 / 1250000] ~ [36.66061, 36.66061]
LHS := (LHS NUM) / (LHS DEN) in [-19997 / 3666060552, 358 / 65465367] ~ [-1e-05, 1e-05]
CD / |V| ^ .5 in [70710678 / 300000001, 70710679 / 300000000] ~ [0.2357, 0.2357]
Success: LHS < CD / |V| ^ .5
Success: existence proven