ND0157

SignedDifferenceSquare(p,n,s)

The natural value s of the integer square (p−n)², expressed as a subtraction-free balanced equality.

Conservative notation; not a theorem, primitive, or axiom.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Definition in prerequisite notation

p · p + n · n = s + (p · n + n · p)

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
((((p) * (p))) + (((n) * (n)))) = ((s) + (((((p) * (n))) + (((n) * (p))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

none — first-order arithmetic only

Definitions depending on this notation

GaussianSignedNorm(ap,an,bp,bn,N)RoundedSignedDivision(p,n,N,qp,qn,ep,en,t)

Checked theorems using this definition

GI0006 · gaussian_signed_square_existsGI0007 · gaussian_signed_square_functionalGI0008 · gaussian_signed_square_negatedGI0009 · gaussian_signed_square_integer_transportGI000D · gaussian_signed_square_productGI0010 · gaussian_signed_square_sum_compensationGI0011 · gaussian_signed_square_difference_compensationGI0012 · gaussian_signed_norm_existsGI0019 · gaussian_signed_square_lagrangeGI001A · gaussian_signed_norm_productGI001D · gaussian_signed_square_zero_iffGI001F · gaussian_signed_square_scaled