show/hide visualization coordinates
a : (0.7880695027576932, 0.21361520570025172, -0.10190674038732839)
b : (0.7457084510757599, -0.5645572321060228, 0.5247137175766933)
c : (1.0420015892542172, -0.6995257270145182, -0.4207987792473822)
d : (1.0173579293497725, 0.06579544973015616, -1.0639754163018236)
e : (0.8180047056429136, 0.9883224537697929, -0.7335178259587734)
f : (0.42068482929682416, 1.1008040643718981, 0.1772427370525399)
g : (0.3659289671809993, 0.31908670367358194, 0.7984671438065012)
h : (-0.0997534799315638, -0.5271254517133658, 1.057435957617414)
i : (0.31800138610055506, -1.4102389433814668, 0.8439144534538724)
j : (0.18799680305289068, -1.109913527106856, -0.10102123363074855)
k : (0.16674752047237873, -0.3781652921499519, -0.7822649408510569)
l : (0.1375230648244723, 0.49257903971863637, -1.2731317656730339)
m : (0.9725138295701996, 0.8289969526775577, -1.7085779858078622)
n : (-0.15313392057189723, 1.205547556136716, -0.6350138992589225)
o : (-0.5557682835155203, 0.8902783688762469, 0.22434103866900146)
p : (-0.06775752023830939, 1.1855656811822421, 1.0457123908092472)
q : (-0.5997534799315638, 0.3388999520710728, 1.057435957617414)
r : (-1.0997534799315638, -0.5271254517133658, 1.057435957617414)
s : (-0.5997534799315638, -1.197168248839351, 0.5087624207855508)
t : (-0.6797844017431003, -0.6740568271954501, -0.33973595405066126)
u : (-0.5486113570579634, 0.28905386642576403, -0.5747070675529271)
v : (-1.0816275941281561, 0.03975983242836212, 0.2338386489237816)
w : (-1.4948415815974738, -0.87042842554193, 0.20535118479108783)
show/hide computer existence proof
(see shape-existence, preprint)
Attempting to prove existence
Starting realization:
Abstract data:
mode: maximal_simplices
data: [['j', 'b', 'i'], ['t', 'v', 'w'], ['h', 'b', 'g'], ['l', 'k', 'd'], ['j', 'i', 's'], ['j', 'k', 't'], ['h', 'i', 's'], ['r', 'v', 'q'], ['h', 'g', 'q'], ['o', 'f', 'n'], ['u', 'k', 'l'], ['d', 'k', 'c'], ['v', 'o', 'q'], ['a', 'e', 'f'], ['a', 'b', 'c'], ['o', 'f', 'p'], ['p', 'g', 'q'], ['j', 'k', 'c'], ['e', 'f', 'n'], ['h', 'r', 's'], ['t', 'u', 'k'], ['j', 't', 's'], ['a', 'f', 'g'], ['l', 'e', 'n'], ['l', 'u', 'n'], ['w', 'r', 'v'], ['a', 'b', 'g'], ['u', 'o', 'n'], ['a', 'd', 'c'], ['r', 'w', 's'], ['t', 'w', 's'], ['h', 'b', 'i'], ['m', 'e', 'l'], ['j', 'b', 'c'], ['m', 'e', 'd'], ['o', 'p', 'q'], ['t', 'u', 'v'], ['f', 'p', 'g'], ['a', 'e', 'd'], ['h', 'r', 'q'], ['l', 'm', 'd'], ['u', 'v', 'o']]
Coordinate Data:
r : [-21136307503907831148164958761 / 2000000000000000000000000000000000000000000000000000000000000000000, 79931858365796395352067825933 / 5000000000000000000000000000000000000000000000000000000000000000000, 78610682434029767034661766283 / 200000000000000000000000000000000000000000000000000000000000000000000000000000000]
g : [73284122355628152202956299963 / 50000000000000000000000000000, 423106077693473850664177519677 / 500000000000000000000000000000, -64742203452728191133023105223 / 250000000000000000000000000000]
b : [184546193100732375324460867593 / 100000000000000000000000000000, -18715890196328542343413608351 / 500000000000000000000000000000, -33295140002545042428238641057 / 62500000000000000000000000000]
n : [59163722459979160550130834507 / 62500000000000000000000000000, 173267300785008155753156628277 / 100000000000000000000000000000, -33848997137526729755961747161 / 20000000000000000000000000000]
v : [2265735725425969235832839369 / 125000000000000000000000000000, 22675411365669115269324861789 / 40000000000000000000000000000, -823597308693632305904288769093 / 1000000000000000000000000000000]
q : [1 / 2, 866025403784438646763723170753 / 1000000000000000000000000000000, -15979057661627212425351384669 / 50000000000000000000000000000000000000000000000000000000000000000000000000000000]
j : [128775028298445451396558444243 / 100000000000000000000000000000, -58278807539349016685131807 / 100000000000000000000000000, -115845719124816245118899086627 / 100000000000000000000000000000]
p : [51599797984662724514316057651 / 50000000000000000000000000000, 171269113289560775865055648941 / 100000000000000000000000000000, -2930891702041679939303302919 / 250000000000000000000000000000]
i : [70887743301605947989699781437 / 50000000000000000000000000000, -55194593229256311374184643683 / 62500000000000000000000000000, -213521504163541518399497842659 / 1000000000000000000000000000000]
e : [191775818557447751206458499643 / 100000000000000000000000000000, 151544790548315865468927501379 / 100000000000000000000000000000, -179095378357618729759183547707 / 100000000000000000000000000000]
m : [207226730950176321692021140121 / 100000000000000000000000000000, 27122448087818468701716700931 / 20000000000000000000000000000, -276601394342527621017091889933 / 100000000000000000000000000000]
h : [1, -109870808947709339348276350387 / 5000000000000000000000000000000000000000000000000000000000000000000, -34310294286819214702256615351 / 125000000000000000000000000000000000000000000000000000000000000000000000000000000]
o : [543985196416043467419288374391 / 1000000000000000000000000000000, 70870191029480630033795281813 / 50000000000000000000000000000, -104136864868551558666458741729 / 125000000000000000000000000000]
l : [123727654475603617993586196113 / 100000000000000000000000000000, 25492612285800053536535562343 / 25000000000000000000000000000, -46611354465808952786052108527 / 20000000000000000000000000000]
k : [31662525010098565193297315739 / 25000000000000000000000000000, 148960159563413864287545028959 / 1000000000000000000000000000000, -183970089846847074499630683189 / 100000000000000000000000000000]
t : [26248067386778969478420033243 / 62500000000000000000000000000, -146931375482084344944218631657 / 1000000000000000000000000000000, -34929297791701877180584074831 / 25000000000000000000000000000]
f : [1900547886535484873353642287 / 1250000000000000000000000000, 81396475804263204844102991551 / 50000000000000000000000000000, -880193220564873999809659089789 / 1000000000000000000000000000000]
c : [26771938364822261695332414537 / 12500000000000000000000000000, -172400275301152426631494362107 / 1000000000000000000000000000000, -36955868421619901342291682209 / 25000000000000000000000000000]
a : [188782298268925703053008131553 / 100000000000000000000000000000, 148148131482723495632331006851 / 200000000000000000000000000000, -57967134900237120495784563919 / 50000000000000000000000000000]
u : [551142122873600395411078669609 / 1000000000000000000000000000000, 816179318139129839260387579729 / 1000000000000000000000000000000, -40803575629258527963065687533 / 25000000000000000000000000000]
d : [26463892616016703679584054771 / 12500000000000000000000000000, 592920901443521978152863769437 / 1000000000000000000000000000000, -212141137391923766081426476019 / 100000000000000000000000000000]
s : [1 / 2, -167510699281496285430367129441 / 250000000000000000000000000000, -68584192103982897037012265207 / 125000000000000000000000000000]
w : [-98772025416477507120804916993 / 250000000000000000000000000000, -85825743457141050814255614201 / 250000000000000000000000000000, -426042386413163033973227695887 / 500000000000000000000000000000]
Desired square lengths:
default : 1
Checking inequality 1:
d = 3
|V| = 23
|E| = 63
Success: d|V| >= |E|
Checking self-intersection:
Square collision distance = 1953112456917618123900936195354158601967536978166432713000493455389786295312981041626753320939623275487675173190618001 / 3906249370353613608353335679885271659099846801543686307951932886474544688625197695312500000000000000000000000000000000
Collision distance in [707104567631367 / 1000000000000000, 88388070953921 / 125000000000000] ~ [0.7071, 0.7071]
Success: starting realization non-self-intersecting
Checking inequality 2:
sigma_min in [20112678478849465999 / 100000000000000000000, 20112678478849466001 / 100000000000000000000] ~ [0.20113, 0.20113]
Success: sigma_min > 0
Checking inequality 3:
rho_squared = 460843235501029392809521722670462143714867494378458576053501513365436582771616044204110863198410702004538086573995104547221925332478961630311174279474483021347987052757103391399455871244092454395040365614331188173037427695703094997602576308015889105191086527000774286818981781 / 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
rho in [848567943932811 / 1250000000000000000000000000000000000000, 1250000000848567943932811 / 1250000000000000000000000000000000000000] ~ [0.0, 0.0]
sigma_min ^ 2 / (16 * E ^ .5) in [404519835593574469516481731527457068001 / 1269960629311003520000000000000000000000000, 404519835593574469596932445442854932001 / 1269960629311003360000000000000000000000000] ~ [0.00032, 0.00032]
Success: rho < sigma_min ^ 2 / (16 * E ^ .5)
Checking inequality 4:
LHS NUM := sigma_min - [sigma_min ^ 2 - 16 * rho * |E| ^ .5 ] ^ .5 in [-1150534001 / 100000000000000000000, 8849466001 / 100000000000000000000] ~ [-0.0, 0.0]
LHS DEN := 8 * |E| ^ .5 in [7937253933193771 / 125000000000000, 1984313483298443 / 31250000000000] ~ [63.49803, 63.49803]
LHS := (LHS NUM) / (LHS DEN) in [-1150534001 / 6349803146555016800000, 8849466001 / 6349803146555016800000] ~ [-0.0, 0.0]
CD / |V| ^ .5 in [707104567631367 / 4795831523312720, 707104567631368 / 4795831523312719] ~ [0.14744, 0.14744]
Success: LHS < CD / |V| ^ .5
Success: existence proven