Lagrange’s Four-Square Theorem with defined notation

A canonical signed decoding has a zero positive/negative cross term.

The natural magnitude of a normalized signed coordinate squares to the sum of its positive and negative component squares.

Every canonical balanced signed coordinate has an explicit natural absolute magnitude with a constructive sign choice.

The product of two four-square norms expands constructively into four bounded natural square-times-norm blocks.

Hamilton's four signed product coordinates have canonical constructively chosen SignedBalance witnesses.

All four Hamilton-product coordinates have explicit natural absolute magnitudes and constructive sign choices.

Two adjacent natural summands exchange positions without disturbing their shared right tail.

The five additive square-gap contributions reorder without subtraction or a polynomial normalizer.

A natural square of a sum expands to its four ordered diagonal and cross contributions.

A larger coordinate and its base have squared sum equal to the gap square plus their two ordered cross products.

The opposite coordinate orientation has the same gap-square and ordered cross-term correction.

Either constructive absolute-difference branch transports coordinate squares to its magnitude square and cross correction.

Every canonical signed balance supplies a natural magnitude, constructive sign branch, and exact squared cross-term transport.

Two natural product factors interchange their middle terms; this is the bounded Euler cross-term cancellation primitive.

The square of a product is the product of the two natural coordinate squares.

Each of the four Hamilton signed coordinates independently satisfies its exact magnitude-square/cross-term balance.

Every Hamilton product has four explicit absolute coordinates with all four constructive squared cross-term corrections.

Canonical signed totality yields a natural absolute difference for any ordered pair, without importing another candidate module.

The six-variable Euler subclass with a two-square right factor is exactly the sum of two independently composed two-square norms.

Every four-square norm multiplied by any two-square norm has four explicitly constructed natural-square witnesses.

The actual odd-prime residue intersection supplies both square coordinates in the witnessed interval 0≤a,b≤h.

The half h of an odd prime p=2h+1 is constructively at least one.

The actual half-range seed norm a²+b²+1 is strictly smaller than the square of its odd prime modulus.

Every odd prime has an actual modular square seed with a strictly smaller natural multiplier.

Every prime other than two has a strictly prime-bounded constructive modular four-square seed.

Every prime, including two, has actual witnesses a²+b²+1=p·k with the constructive strict bound k<p.

The half of a constructively nonzero even multiplier is itself nonzero.

Every positive natural half is constructively strictly smaller than its doubled value.

Every represented nonzero even prime multiplier unconditionally descends to its nonzero strictly smaller represented half.

A proper odd prime multiplier descends constructively once its one explicitly centered signed quaternion quotient is represented.

Parity case distinction discharges the entire below-prime strict-descent obligation except for the single explicitly stated odd signed quaternion representation.

The conjugate quaternion's sixteen diagonal squares regroup into the exact row-major norm-product diagonal.

The all-positive conjugate scalar square decomposes into its four diagonal and six symmetric mixed blocks.

All conjugate scalar/vector coordinate squares separate into sixteen diagonal squares and exactly twelve same-sign mixed blocks.

The three conjugate vector corrections decompose into the twelve opposite-sign mixed blocks; the scalar correction vanishes.

Each of the twelve conjugate same-sign mixed blocks crosses its right factors into its unique opposite-sign correction block.

The complete subtraction-free conjugate quaternion compensation equation follows from sixteen diagonal and twelve explicitly crossed mixed blocks.

Each exact conjugate absolute coordinate independently satisfies its constructive natural square/cross-term balance.

Euler's full eight-variable conjugate quaternion identity holds for the all-positive scalar and all three exact two-positive/two-negative vector coordinates.

Every pair of natural four-square tuples has four explicit conjugate absolute coordinates satisfying the complete norm identity.

A genuinely covered interleaving of two bounded decoded beta prefixes remains bounded in their common finite codomain.

Two bounded injective equal-length prefixes whose covered interleaving overflows their finite codomain have an actual witnessed cross-family value collision.

Any two equally long beta-coded prefixes have an actual beta-coded even/odd interleaving with complete constructive source coverage.

Any two injective bounded equal-length decoded prefixes with combined length exceeding their codomain have an explicit actual common value.

The square of a nonzero natural multiplier remains nonzero constructively.

The product of two k-divisible norms exposes its exact common square factor k².

Four coordinates each divisible by k have a norm exactly divisible by the natural square k².

A nonzero natural square factor cancels without subtraction or division axioms.

An exact represented product of a prime multiple and a k-multiple descends through their common square factor.

A centered quaternion product whose four absolute coordinates are all k-divisible yields the exact four-square quotient p·r.

Every explicit centered nonzero quaternion certificate constructs a genuinely represented strictly smaller prime multiplier.

A modular seed x²+y²+1=p·k has a constructively nonzero multiplier because its left side is a successor.

Bounded constructive induction on a nonzero represented multiplier terminates at one under an explicit strictly decreasing quaternion step.

Every nonzero represented prime multiple descends all the way to a representation of the prime under the precise strict-step hypothesis.

A concrete modular square seed and the explicit strict multiplier step suffice for an actual representation of the prime.

All remaining three-modulo-four primes are represented once their modular square seeds and the decreasing quaternion step are supplied.

All-natural Lagrange follows by checked construction from exactly two explicit remaining premises: modular square seeds and strict centered-quaternion multiplier descent.

Every nonzero-modulus remainder has a complementary nonnegative residue and a decidable ordering between the two.

Every natural has a constructively chosen signed residue m with 2m≤k and either n=kq+m or n+m=kq.

Every four-coordinate natural quaternion admits four independent constructively chosen centered signed remainders.

A centered quaternion norm k·r strictly below k² forces its quotient r to be strictly smaller than k.

A pair of natural coordinates with matching constructive parity has an explicitly even sum.

Matching even or odd coordinate witnesses construct an explicitly even absolute difference without subtraction.

Multiplication by the two-square norm 1²+1² gives a fully explicit paired four-square doubling identity.

An actually represented double p·2 descends unconditionally to p when its four coordinates are supplied as two matching-parity pairs.

Any represented even multiplier with two constructively matching-parity coordinate pairs has a fully checked four-square half representation.

For an odd modulus 2h+1, the constructive centered bound m+m≤2h+1 implies the sharp half-range bound m≤h.

Two explicitly witnessed natural weak inequalities add constructively.

The square of the doubled odd half is exactly four copies of the half-square.

Four coordinates in the odd half interval have norm strictly below the square of the full odd modulus.

All four actual centered signed residues modulo any odd multiplier have norm strictly below its square, independently of their sign choices.

A zero natural four-square norm forces all four coordinates to vanish constructively.

A coordinate with centered magnitude zero is an actual natural multiple of the modulus in either signed-remainder branch.

A prime has no divisor k that is simultaneously nonunit and strictly smaller than the prime.

If all four coordinates of a represented prime multiple are k-divisible, square-factor cancellation makes k an actual divisor of the prime.

For a nonunit multiplier strictly below a prime, the centered quaternion norm quotient cannot vanish: otherwise all original coordinates would make the multiplier a forbidden prime divisor.

For every proper nonunit odd prime multiplier, any represented signed centered quotient automatically gives a nonzero strictly smaller represented multiplier.

Two products with fixed outer factors exchange their crossed middle factors.

The two mixed Hamilton products for the ab left-coordinate pair cancel exactly.

The two mixed Hamilton products for the ac left-coordinate pair cancel exactly.

The two mixed Hamilton products for the ad left-coordinate pair cancel exactly.

The two mixed Hamilton products for the bc left-coordinate pair cancel exactly.

The two mixed Hamilton products for the bd left-coordinate pair cancel exactly.

The two mixed Hamilton products for the cd left-coordinate pair cancel exactly.

All twelve mixed Hamilton-coordinate products cancel in six separately witnessed coordinate-pair blocks.

Eight additive terms are transposed as four independent magnitude/cross-term pairs.

Four exact signed-coordinate square balances aggregate into the sum of their natural squares plus their full cross correction.

Ordinary constructive additive cancellation turns all four signed cross corrections into an exact norm identity.

One left coordinate distributes into the four exact squared coordinate products of a quaternion norm.

The complete eight-variable quaternion norm product expands into exactly its sixteen squared coordinate products.

The exact eight-variable quaternion Euler identity follows constructively from its one remaining subtraction-free global compensation equality.

Six abstract additive entries are paired by a bounded explicit adjacent-swap proof.

A three-by-three square expansion separates its diagonal and its six ordered mixed products.

The twelve paired Hamilton mixed blocks are placed in their four signed-coordinate correction groups.

All sixteen Hamilton diagonal squares transpose from coordinate order into row-major norm order.

Two final additive entries exchange places while their common first entry is preserved.

A three-term natural square expands into three diagonal squares and three explicitly paired mixed blocks.

The two ordered products of one entry with a three-entry sum split into three exact symmetric pairs.

Both ordered occurrences of a mixed Hamilton product exchange their crossed right-hand factors constructively.

A singleton-square plus a triple-square decomposes into its four diagonal squares and three paired cross blocks.

A triple-square plus a singleton-square decomposes into its four diagonal squares and three paired cross blocks.

The sixteen exact Hamilton-coordinate diagonal squares are the sixteen row-major norm-product squares.

All eight positive/negative Hamilton-coordinate squares split exactly into sixteen diagonal squares plus twelve paired mixed blocks.

The complete four-coordinate signed correction splits into its twelve exact symmetric mixed-product blocks.

All twelve same-sign Hamilton mixed blocks become the twelve opposite-sign correction blocks by explicit crossed-factor swaps.

The exact previously missing global subtraction-free Hamilton compensation equation is proved without any remaining premise.

Euler's complete eight-variable quaternion four-square identity holds unconditionally for all constructively chosen natural absolute coordinates.

Every product of two arbitrary four-square natural norms has four explicitly constructed natural-square witnesses.

The class of constructively represented natural sums of four squares is closed under multiplication without any sign or compensation hypothesis.

The checked unconditional modular seed for every prime removes the entire seed hypothesis; only uniform strict multiplier descent remains.

The all-natural Lagrange four-square theorem follows from exactly one remaining explicit hypothesis: uniform strict prime-multiple descent.

Bounded constructive multiplier induction preserves k<p at every strictly decreasing step and reaches an actual representation of the prime.

An actual modular prime seed with multiplier strictly below the prime needs only the bounded strict-descent step to construct a four-square representation of the prime.

The checked unconditional bounded modular seed discharges every seed premise, so the exact below-prime strict step alone represents every prime.

The complete all-natural Lagrange conclusion follows from exactly the sharp bounded strict-multiplier descent hypothesis, with every prime seed already constructed.

The natural number 0 has four explicitly checked square witnesses.

The natural number 1 has four explicitly checked square witnesses.

The natural number 2 has four explicitly checked square witnesses.

The natural number 3 has four explicitly checked square witnesses.

The natural number 7 has four explicitly checked square witnesses.

The natural number 11 has four explicitly checked square witnesses.

Every constructive sum of two natural squares is a sum of four by adjoining two zero witnesses.

The exceptional prime two and every prime congruent to one modulo four already have explicit four-square witnesses.

Any witnessed solution of x² + y² + 1 = p·k gives an actual four-square representation of the prime multiple.

A modular four-square seed whose multiplier is one directly represents the prime itself.

Constructive prime trichotomy reduces representation of every prime exactly to the still-open three-modulo-four prime case.

Bounded constructive prime-factor descent proves every nonzero natural is a sum of four squares once every prime has such a representation.

All-natural Lagrange, including zero, follows constructively from the explicit universal prime-representation premise.

The full universal four-square theorem is reduced precisely to constructive representation of primes congruent to three modulo four.

Universal Lagrange is constructively equivalent to the one unresolved family of three-modulo-four prime representations.

The actual bounded modular prime seed, complete even branch, centered odd bounds, and terminating descent reduce representation of every prime to the single signed odd quaternion identity.

Universal Lagrange follows constructively from exactly one visible remaining hypothesis: representation of each odd signed centered quaternion quotient.

Every natural prime has an unconditionally constructed four-square representation, using the checked bounded seed, all sixteen signed quaternion cases, and terminating multiplier descent.

Lagrange's complete four-square theorem: every natural number has an unconditionally constructive, independently kernel-checked representation as a sum of four natural squares.

Every natural square has exactly the same residue modulo two as its coordinate.

The sum of two coordinate squares is congruent modulo two to their ordinary sum.

Three coordinate squares preserve their coordinate-sum parity.

Every four-square norm has the parity of the sum of all four coordinates.

An actually even represented norm forces the ordinary sum of its coordinates to be even.

If both original coordinate-pair sums are odd, one of the two crossed pairings has matching parity in each pair.

Every even sum of four naturals constructively selects one of the three partitions into two equal-parity pairs.

Every even four-square norm admits a witnessed choice of two equal-parity coordinate pairs.

Swapping the middle coordinates preserves an explicitly left-associated four-square norm.

The second crossed coordinate partition preserves the full natural four-square norm.

Every represented even natural n·2 has an actual four-square representation of n, with no coordinate-parity premise.

Four-square representability is unconditionally closed under division of represented doubles by two.

For every natural n, an actual four-square representation of n+n constructively produces one of n.

For an odd natural p=2h+1, its doubled half h+h is strictly below p.

Two inclusive odd half-ranges together have strictly more entries than the modulus.

The sum of two inclusive odd-half coordinates is strictly below the modulus.

A natural strictly below a modulus can be divisible by that modulus only when it is zero.

The ordered difference of two natural squares factors subtraction-free as their gap times their sum.

Congruent ordered squares force the prime modulus to divide the product of their gap and coordinate sum.

On the inclusive odd-prime half range, congruent squares of ordered coordinates have equal coordinates.

Squaring is constructively injective modulo every odd prime on its complete inclusive half range.

For every nonzero modulus and arbitrary finite length, canonical square residues are constructively encoded as one beta prefix.

Every canonical square-residue prefix is pointwise bounded by its modulus.

Equal canonical remainders of two natural squares give their balanced modular congruence.

The beta-coded square residues of the complete inclusive odd-prime half range form an actually injective bounded prefix.

Every bounded finite beta prefix admits a constructive beta-coded pointwise residue complement p-1-r.

Complement gaps below a modulus are symmetric after swapping the residue and its p-1 complement.

The pointwise predecessor complement of any bounded residue prefix is itself bounded by the modulus.

Taking p-1 residue complements preserves constructive injectivity of an arbitrary beta-coded finite prefix.

Two square residues whose canonical remainders are predecessor-complements yield an explicit divisor of their sum plus one.

Every odd prime has explicit natural square coordinates and a witnessed multiple satisfying a²+b²+1=p·k, obtained by constructive half-residue pigeonhole.

Every prime other than two has an actual witnessed modular four-square seed with no intersection or coding premise.

Every prime, including the exceptional prime two, admits explicit constructive witnesses a²+b²+1=p·k without any supplementary hypothesis.

When all four centered coordinate orientations are negative, every exact conjugate-quaternion positive/negative block is congruent modulo the multiplier.

A positive first orientation and three negative orientations make all four ordinary Hamilton quaternion blocks congruent modulo the multiplier.

An exact centered norm quotient supplies constructive balanced zero congruence for its complete four-square norm.

Constructive signed quaternion quotient for centered orientation mask 0000, using the exact four_square_signed_conjugate_positive_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 0001, using the exact four_square_signed_natural_negative_first_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 0010, using the exact four_square_signed_natural_negative_first_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 0011, using the exact four_square_signed_conjugate_mixed_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 0100, using the exact four_square_signed_natural_negative_first_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 0101, using the exact four_square_signed_conjugate_mixed_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 0110, using the exact four_square_signed_conjugate_mixed_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 0111, using the exact four_square_signed_natural_positive_first_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 1000, using the exact four_square_signed_natural_negative_first_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 1001, using the exact four_square_signed_conjugate_mixed_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 1010, using the exact four_square_signed_conjugate_mixed_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 1011, using the exact four_square_signed_natural_positive_first_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 1100, using the exact four_square_signed_conjugate_mixed_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 1101, using the exact four_square_signed_natural_positive_first_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 1110, using the exact four_square_signed_natural_positive_first_blocks surface.

Constructive signed quaternion quotient for centered orientation mask 1111, using the exact four_square_signed_conjugate_negative_blocks surface.

Any four individually k-divisible natural norm-product coordinates yield an explicit four-square representation of the exact quotient p·r.

Four signed absolute-coordinate blocks with actual modular balance construct every quotient coordinate and the represented prime-multiple quotient.

All sixteen actual centered sign patterns construct their signed quaternion quotient, yielding a genuine four-square representation without any orientation premise.

A nonnegative signed remainder directly gives balanced modular congruence.

Oppositely signed modular representatives nevertheless have congruent natural squares.

Every centered signed remainder has square congruent to the original coordinate, independently of either sign branch.

All sixteen independent sign patterns yield the same constructive modular congruence between original and centered four-square norms.

For every one of the sixteen centered sign patterns, a represented prime multiple yields an actual natural quotient of the centered four-square norm.

Any natural absolute value of a balanced signed expression congruent to zero has an actual divisibility witness.

The square of two natural addends separates its diagonal squares from its symmetric cross correction.

A four-addend square splits constructively into four diagonal squares and its six symmetric cross pairs.

A pair-versus-pair signed coordinate square decomposes into four diagonal squares and two symmetric cross pairs.

The symmetric cross product of two two-addend blocks decomposes into four independent symmetric coordinate pairs.

Each centered remainder constructively supplies its positive congruence or its opposite signed congruence.

Multiplying an opposite signed congruence preserves its subtraction-free zero balance.

Two modular zero balances with the same added natural term yield congruent remaining terms.

Two positive signed coordinate orientations have congruent crossed bilinear products.

Two negative signed coordinate orientations also have congruent crossed bilinear products.

Opposite signed coordinate orientations make the sum of their crossed bilinear products vanish modulo the multiplier.

Two independently vanishing signed blocks have vanishing sum modulo the multiplier.

Any two natural signed blocks that both vanish modulo the multiplier are congruent.

Swapping the two summands of a modular zero balance preserves that balance.

Cancel a separately vanishing natural tail from a subtraction-free modular zero balance.

The negative-positive orientation also makes the crossed bilinear sum vanish.

A positively oriented coordinate contributes its centered square modulo the multiplier.

A negatively oriented dot-product contribution and its centered square cancel modulo the multiplier.

A vanishing natural block can be prepended to any modular congruence.

Positive and negative signed dot-product groups balance when their combined centered square norm vanishes.

All four canonical signed quaternion blocks balance constructively modulo the multiplier under this exact orientation pattern.

All four canonical signed quaternion blocks balance constructively modulo the multiplier under this exact orientation pattern.

All four canonical signed quaternion blocks balance constructively modulo the multiplier under this exact orientation pattern.