show/hide visualization coordinates
a : (-0.2301683012177318, 0.49434090507582634, 0.847019456100766)
b : (0.5664088914253147, 0.7280558958078835, 1.4045515890474125)
c : (0.3540760599641237, 1.2630813763553874, 0.5868337258154871)
d : (-0.4366876066670522, 1.023062903983293, 0.023731642302928346)
e : (-1.0266998114456813, 0.2606350486242422, 0.289418231322508)
f : (-0.3120175722705175, -0.4200188751102123, 0.4504757772881201)
g : (0.4872025322182216, -0.184556525749919, 1.0034718953710051)
h : (1.0226085917804593, 0.5209310261865553, 0.5391146347981592)
i : (0.48306598601791045, 0.7605248031272382, -0.26803380174759595)
j : (-0.316397932872599, 0.387637811510571, -0.7390037942899027)
k : (-1.218797249981618, 0.7735285950628761, -0.5472649728411306)
l : (-1.8226682134525154, 0.02664522974977096, -0.2688675984007436)
m : (-1.0928909184018898, -0.6433859603324256, -0.13291428308394904)
n : (-0.34779323798327033, -1.3009539179565004, -0.021407208237123776)
o : (0.4131896963519358, -1.0935680056966488, 0.5933253002954317)
p : (1.0516241829209783, -0.42413134585249146, 0.21351486755822907)
q : (1.37320811857097, 0.31759103708157804, -0.3750696030035313)
r : (0.5558599428170943, -0.10031587067651604, -0.7716749181972132)
s : (-0.30275159001153995, -0.6122507911298484, -0.7450502507982909)
t : (-1.1407579221233617, -0.12218105999731554, -0.9850024251334654)
u : (0.5377696144960364, -1.0271578397365593, -0.3966593126417405)
v : (1.4026167398647305, -0.6275144403267844, -0.700508951525359)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['d', 'a', 'e'], ['d', 'a', 'c'], ['t', 'l', 'm'], ['d', 'k', 'j'], ['g', 'b', 'h'], ['p', 'o', 'u'], ['s', 't', 'm'], ['r', 'i', 'j'], ['t', 'k', 'j'], ['v', 'q', 'r'], ['n', 's', 'm'], ['t', 'k', 'l'], ['r', 'q', 'i'], ['d', 'e', 'k'], ['f', 'o', 'n'], ['a', 'g', 'f'], ['t', 's', 'j'], ['a', 'f', 'e'], ['e', 'm', 'f'], ['e', 'l', 'm'], ['b', 'h', 'c'], ['o', 'n', 'u'], ['s', 'r', 'u'], ['s', 'n', 'u'], ['p', 'q', 'v'], ['s', 'r', 'j'], ['p', 'g', 'h'], ['a', 'b', 'c'], ['a', 'g', 'b'], ['p', 'g', 'o'], ['p', 'q', 'h'], ['e', 'k', 'l'], ['f', 'n', 'm'], ['v', 'r', 'u'], ['i', 'h', 'c'], ['f', 'o', 'g'], ['d', 'i', 'j'], ['p', 'v', 'u'], ['i', 'q', 'h'], ['d', 'i', 'c']]
Coordinate Data:
b : [2511775067210140529 / 100000000000000000000, -21441948462823684039 / 100000000000000000000, -19581637370553430907 / 20000000000000000000]
u : [215028110405518631 / 4000000000000000000, 3081588501832412051 / 2000000000000000000, 82212903316148143559 / 100000000000000000000]
k : [181032389207903416309 / 100000000000000000000, -6497304597080737497 / 25000000000000000000, 12159183667010894519 / 12500000000000000000]
j : [45396228748500756689 / 50000000000000000000, 6299929983453783531 / 50000000000000000000, 2911183787024108953 / 2500000000000000000]
i : [10846065607950565773 / 100000000000000000000, -3086104899344895639 / 12500000000000000000, 34675176113366847689 / 50000000000000000000]
f : [90354421436793360861 / 100000000000000000000, 93365528628985889691 / 100000000000000000000, -500121135367582917 / 20000000000000000000]
t : [34645691284415557513 / 20000000000000000000, 12716349423539244003 / 20000000000000000000, 70523607282660312383 / 50000000000000000000]
s : [8942782321089560851 / 10000000000000000000, 22517744046189902121 / 20000000000000000000, 117051997131803180851 / 100000000000000000000]
a : [41084747165757396413 / 50000000000000000000, 385910122076406167 / 20000000000000000000, -105387433895256243 / 250000000000000000]
d : [51410712438223418847 / 50000000000000000000, -25471324640182327001 / 50000000000000000000, 8034761564336252447 / 20000000000000000000]
m : [168441756049930595081 / 100000000000000000000, 2314044743024144443 / 2000000000000000000, 55838400360368997447 / 100000000000000000000]
q : [-625345181178842933 / 800000000000000000, 19604537409806859303 / 100000000000000000000, 80053932352327225179 / 100000000000000000000]
g : [10432410987919456359 / 100000000000000000000, 8727411711619571043 / 12500000000000000000, -7225027185640803843 / 12500000000000000000]
v : [-40554504888365718961 / 50000000000000000000, 11411508515064309363 / 10000000000000000000, 56298933602254999369 / 50000000000000000000]
p : [-11502438520589055537 / 25000000000000000000, 23444193925803452137 / 25000000000000000000, 1059774264807559497 / 5000000000000000000]
h : [-10777048742076078883 / 25000000000000000000, -182365375172715469 / 25000000000000000000, -710280714240114207 / 6250000000000000000]
l : [120709742777496568907 / 50000000000000000000, 4869911814298756647 / 10000000000000000000, 13886746378409692183 / 20000000000000000000]
e : [20227830669288719057 / 12500000000000000000, 5060027251108089011 / 20000000000000000000, 2721029783944660039 / 20000000000000000000]
c : [23745058213329243771 / 100000000000000000000, -1498889930351481593 / 2000000000000000000, -16136400529574611137 / 100000000000000000000]
n : [23482997002017161399 / 25000000000000000000, 181459032913614721411 / 100000000000000000000, 357501543005491789 / 800000000000000000]
o : [8916847287274015827 / 50000000000000000000, 80360220843814767799 / 50000000000000000000, -3357111595513814413 / 20000000000000000000]
r : [22291687050201131 / 625000000000000000, 7674403523202032903 / 12500000000000000000, 23942892774339083007 / 20000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 22
|E| = 60
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 138627749326122619195654982801004686821633089902773424872295584266543035551892901763467278329890093326743813762940140369 / 243550401970742709602646251385789455484384358917792542441467259336533429976407580000000000000000000000000000000000000000
Collision distance in [37722517194544114274268947519 / 50000000000000000000000000000, 754450343890882285485378950381 / 1000000000000000000000000000000] ~ [0.75445, 0.75445]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [913 / 10000, 183 / 2000] ~ [0.0913, 0.0915]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 8962141632422141236504231675671215880122199 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [2993683622633183534199010674163 / 10000000000000000000000000000000000000000000000000, 2993683622643183534199010674163 / 10000000000000000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [104196125000000000000000000 / 1549193338482966754071706159913, 14535156250000000000000000 / 215165741455967604732181411099] ~ [7e-05, 7e-05]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-199999999999797254875378847 / 1000000000000000000000000000000, 8000000000008127570165563 / 40000000000000000000000000000] ~ [-0.0002, 0.0002]
LHS DEN := 8 * |E| ^ .5 in [1936491673103708442589632699891 / 31250000000000000000000000000, 1549193338482966754071706159913 / 25000000000000000000000000000] ~ [61.96773, 61.96773]
LHS := (LHS NUM) / (LHS DEN) in [-199999999999797254875378847 / 61967733539318670162868246396512, 200000000000203189254139075 / 61967733539318670162868246396512] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [150890068778176457097075790076 / 938083151964685910913126022709, 754450343890882285485378950381 / 4690415759823429554565630113544] ~ [0.16085, 0.16085]
Success: LHS < CD / |V| ^ .5
Success: existence proven