8 vertices

bcdefg aghfc abfed ace adcf aecbhg afhb bgf

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