show/hide visualization coordinates
a : (-0.7766955497529413, -0.5749980675235294, -0.41814315342941183)
b : (-0.7735135339529413, -0.6350861131235294, 0.5800448555705882)
c : (-1.0384405426529413, 0.21843404587647064, 0.13136120517058825)
d : (-0.31723926975294126, 0.3023983697764706, -0.5562569420294119)
e : (0.2139555576470587, -0.5448361610235294, -0.5511869163294119)
f : (-0.19003470865294125, -1.2422824142235296, 0.0407257365705882)
g : (-1.1820673816529412, -1.3681858263235296, 0.036309107270588226)
h : (0.20429760544705872, -0.44355407022352933, 0.4951870203705882)
i : (-0.4045985285529412, 0.23586043217647062, 0.9046274090705881)
j : (-0.3598036706529413, 0.9491843432764706, 0.2052259375705882)
k : (0.20118078724705873, 1.1565912232764706, -0.5961970619294119)
l : (0.6243120918470587, 0.3005562609764706, -0.8931213656294119)
m : (0.9736577921470587, -0.12225187862352938, -0.056945033229411746)
n : (0.8001600408470587, -1.1026571523235296, 0.03635035527058822)
o : (0.4802358471470587, 0.5168767457764706, 0.5330120715705882)
p : (0.4748632826470587, 1.4906912365764706, 0.30573146787058825)
q : (1.0697301806470587, 0.8632590256764706, -0.19672469372941176)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['l', 'e', 'm'], ['d', 'k', 'l'], ['h', 'o', 'i'], ['i', 'j', 'c'], ['d', 'e', 'a'], ['d', 'e', 'l'], ['f', 'e', 'a'], ['k', 'l', 'q'], ['i', 'o', 'j'], ['b', 'f', 'g'], ['j', 'k', 'p'], ['d', 'c', 'a'], ['b', 'f', 'h'], ['h', 'm', 'n'], ['b', 'i', 'c'], ['k', 'q', 'p'], ['b', 'c', 'a'], ['b', 'g', 'a'], ['j', 'd', 'c'], ['e', 'm', 'n'], ['q', 'o', 'p'], ['h', 'o', 'm'], ['f', 'h', 'n'], ['f', 'e', 'n'], ['b', 'h', 'i'], ['d', 'k', 'j'], ['l', 'm', 'q'], ['q', 'o', 'm'], ['f', 'g', 'a'], ['j', 'o', 'p']]
Coordinate Data:
c : [2066617791 / 1250000000, 1859160009 / 5000000000, 1771630691 / 5000000000]
n : [-1853063507 / 10000000000, 1058077 / 625000, 4493369881 / 10000000000]
l : [-94584017 / 10000000000, 2897097867 / 10000000000, 1378808709 / 1000000000]
b : [13883672241 / 10000000000, 1531690201 / 1250000000, -471787561 / 5000000000]
e : [160359253 / 400000000, 11351022087 / 10000000000, 10368742597 / 10000000000]
d : [9320929599 / 10000000000, 2878676779 / 10000000000, 5209721427 / 5000000000]
h : [4105560847 / 10000000000, 10338201179 / 10000000000, -9499677 / 1000000000]
i : [10194522187 / 10000000000, 708811231 / 2000000000, -4189400657 / 10000000000]
o : [134617843 / 1000000000, 733893019 / 10000000000, -236623641 / 5000000000]
p : [55996163 / 400000000, -9004251889 / 10000000000, 359911751 / 2000000000]
f : [2012220997 / 2500000000, 18325484619 / 10000000000, 1112404017 / 2500000000]
q : [-909752981 / 2000000000, -136496489 / 500000000, 6824120371 / 10000000000]
k : [4136729029 / 10000000000, -1415812939 / 2500000000, 10818844053 / 10000000000]
m : [-179402051 / 500000000, 7125179263 / 10000000000, 2713161883 / 5000000000]
a : [13915492399 / 10000000000, 91036259 / 78125000, 1129788121 / 1250000000]
j : [1218321701 / 1250000000, -897295739 / 2500000000, 1402307029 / 5000000000]
g : [8984605359 / 5000000000, 979225937 / 500000000, 4493782361 / 10000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 17
|E| = 45
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 708616779925692700594911333965206691215941463623187369 / 1417233560068870964452271082889093660687500000000000000
Collision distance in [35355339 / 50000000, 70710679 / 100000000] ~ [0.70711, 0.70711]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [2737 / 5000, 1369 / 2500] ~ [0.5474, 0.5476]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 5202722914378479690527 / 5000000000000000000000000000000000000000
rho in [102007087 / 100000000000000000, 1102007087 / 100000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [7491169 / 2683281576, 1874161 / 670820393] ~ [0.00279, 0.00279]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-19991 / 100000000, 20109 / 100000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [670820393 / 12500000, 335410197 / 6250000] ~ [53.66563, 53.66563]
LHS := (LHS NUM) / (LHS DEN) in [-19991 / 5366563144, 20109 / 5366563144] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [70710678 / 412310563, 70710679 / 412310562] ~ [0.1715, 0.1715]
Success: LHS < CD / |V| ^ .5
Success: existence proven