Rigid-frame reduction (exact, gauge-free): for a candidate graph G with a K5 clique, in any R^4-realisation those 5 points form a regular unit 4-simplex (unique up to isometry), so WLOG pin them at s_i=e_i/sqrt2 in R^5 (hyperplane sum=1/sqrt2, affine dim 4); every other point is an affine combination p(lambda)=sum lambda_i s_i with sum lambda_i=1. Squared distances are exact rational quadratics: |p(lambda)-p(mu)|^2 = (1/2) sum (lambda_i-mu_i)^2 and |p(lambda)-s_j|^2 = (1/2)(sum lambda_i^2 - 2 lambda_j + 1). Hence G is R^4-realisable iff an explicit exact rational quadratic edge-distance system has a real solution (injectivity omitted only removes solutions, safe for non-realizability). Distance formulas verified symbolically.