show/hide visualization coordinates
a : (-0.12691276976250004, -0.37577205652499995, -0.85023340535)
b : (-0.5258342004625001, 0.11929486367500008, -0.07837173614999998)
c : (0.23527793013749998, 0.5190280769750001, -0.58917667195)
d : (0.7768346525375, -0.3060188857249999, -0.42788865084999994)
e : (0.015722521837500003, -0.7057520989249999, 0.08291628515000005)
f : (-0.38319890896250003, -0.21068517892499994, 0.85477795445)
g : (-0.36980244706250004, 0.770857245075, 0.6640032061500001)
h : (0.37791322173749997, 0.18904803437500006, 0.34397301855000006)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['a', 'e', 'b'], ['h', 'c', 'b'], ['f', 'h', 'e'], ['g', 'h', 'b'], ['h', 'e', 'd'], ['a', 'e', 'd'], ['f', 'e', 'b'], ['h', 'c', 'd'], ['f', 'g', 'h'], ['a', 'c', 'd'], ['a', 'c', 'b'], ['f', 'g', 'b']]
Coordinate Data:
b : [-644285251 / 5000000000, 1115271101 / 2000000000, 3534658723 / 10000000000]
e : [4126996721 / 10000000000, -2674114121 / 10000000000, 643442367 / 1250000000]
g : [33968379 / 1250000000, 12091979319 / 10000000000, 5479204073 / 5000000000]
d : [2934529507 / 2500000000, 1323218011 / 10000000000, 4936197 / 1250000000]
h : [193722593 / 250000000, 1568471803 / 2500000000, 775810627 / 1000000000]
c : [1580637701 / 2500000000, 4786843819 / 5000000000, -314678127 / 2000000000]
a : [540128761 / 2000000000, 625686303 / 10000000000, -4183957969 / 10000000000]
f : [137782413 / 10000000000, 2276555079 / 10000000000, 12866155629 / 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 = 499999999841510733998097589684629740165595232825586677150729 / 999999999962142997059030078366758308283700000000000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [9817 / 10000, 9819 / 10000] ~ [0.9817, 0.9819]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 7295617699528534594439 / 10000000000000000000000000000000000000000
rho in [854143881 / 1000000000000000000, 10854143881 / 1000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [96373489 / 6788225104, 1190281 / 83805248] ~ [0.0142, 0.0142]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-9999 / 50000000, 10019 / 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 [-1111 / 188561808, 10019 / 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