ND0163

GaussianSignedDivisionRemainder(ap,an,bp,bn,cp,cn,dp,dn,qp,qn,up,un,rp,rn,sp,sn,U,V)

The actual Gaussian coordinate equation A=B·Q+R, the two genuine squared norms U=N(R), V=N(B), and strict decrease U<V.

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

cp · qp + cn · qn + (dp · un + dn · up) + rp + an = ap + (cp · qn + cn · qp + (dp · up + dn · un) + rn) ∧ cp · up + cn · un + (dp · qp + dn · qn) + sp + bn = bp + (cp · un + cn · up + (dp · qn + dn · qp) + sn) ∧ (GaussianSignedNorm(rp,rn,sp,sn,U) ∧ (GaussianSignedNorm(cp,cn,dp,dn,V) ∧ Lt(U,V)))

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

Hygienic expanded first-order definition 
((((((((((((((cp) * (qp))) + (((cn) * (qn))))) + (((((dp) * (un))) + (((dn) * (up))))))) + (rp))) + (an)) = ((ap) + (((((((((cp) * (qn))) + (((cn) * (qp))))) + (((((dp) * (up))) + (((dn) * (un))))))) + (rn))))) /\ (((((((((((cp) * (up))) + (((cn) * (un))))) + (((((dp) * (qp))) + (((dn) * (qn))))))) + (sp))) + (bn)) = ((bp) + (((((((((cp) * (un))) + (((cn) * (up))))) + (((((dp) * (qn))) + (((dn) * (qp))))))) + (sn))))))) /\ ((exists ge_real_square_lowerlayerremainder ge_imaginary_square_lowerlayerremainder. ((((((rp) * (rp))) + (((rn) * (rn)))) = ((ge_real_square_lowerlayerremainder) + (((((rp) * (rn))) + (((rn) * (rp))))))) /\ ((((((sp) * (sp))) + (((sn) * (sn)))) = ((ge_imaginary_square_lowerlayerremainder) + (((((sp) * (sn))) + (((sn) * (sp))))))) /\ ((U) = ge_real_square_lowerlayerremainder + ge_imaginary_square_lowerlayerremainder)))) /\ ((exists ge_real_square_lowerlayerdivisor ge_imaginary_square_lowerlayerdivisor. ((((((cp) * (cp))) + (((cn) * (cn)))) = ((ge_real_square_lowerlayerdivisor) + (((((cp) * (cn))) + (((cn) * (cp))))))) /\ ((((((dp) * (dp))) + (((dn) * (dn)))) = ((ge_imaginary_square_lowerlayerdivisor) + (((((dp) * (dn))) + (((dn) * (dp))))))) /\ ((V) = ge_real_square_lowerlayerdivisor + ge_imaginary_square_lowerlayerdivisor)))) /\ (exists ge_gap_lowerlayerstrict. ge_gap_lowerlayerstrict + S (U) = (V)))))

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

Direct definition dependencies

GaussianSignedNorm(ap,an,bp,bn,N)Lt(a,b)

Definitions depending on this notation

none

Checked theorems using this definition

GI003A · gaussian_signed_euclidean_division_existsGI005D · gaussian_euclidean_division_exists