Native PA with defined notation

Zero is a left identity for addition; unlike PA3, this needs induction.

One is a right identity for multiplication.

Every divisor of a prime is one or the prime itself.

A sum equal to zero has zero as its right addend.

No successor is zero (the reusable PA1 lemma).

Every consecutive beta range of length zero is vacuous.

Zero products have a zero factor: the 23-entry core capstone.

Every natural is either zero or the successor of a natural.

Addition is associative.

Multiplication distributes over addition on the right.

Multiplication is associative.

A right multiple of a multiple remains a multiple.

Zero annihilates multiplication on the left.

A successor can move through addition on the left.

Addition is commutative.

A successor can move through multiplication on the left.

Multiplication is commutative.

Extend a nonzero common multiple through the next positive natural.

A sum equal to zero has zero as its left addend.

Every finite initial interval has a nonzero common-multiple surrogate.

A right multiple of a bounded common multiple remains such a common multiple.

One is a left identity for multiplication.

A product is one only when both natural factors are one.

Every natural divisor of one equals one.

One is coprime to every natural in the expanded common-divisor relation.

Every natural number is below its successor.

Order witnesses compose by addition, so the defined order is transitive.

A product of two nonzero naturals is nonzero.

The right factor divides a product.

Every Gödel-beta decoding modulus is nonzero.

Successor order reflects to the underlying naturals.

A witnessed inequality is either equality or a witnessed strict inequality.

A witnessed strict inequality entails the corresponding weak inequality.

Adding a positive successor cannot leave a natural number fixed.

No natural is strictly below itself, with strict order fully expanded.

Two naturals are equal or strictly ordered in exactly one displayed direction.

A common right addend can be cancelled.

A common-factor difference is itself a multiple of that factor.

A common divisor of a dividend and divisor also divides the remainder.

Every beta-shaped successor modulus is coprime to its base c.

Multiplication distributes over addition on the left.

A common divisor of two ordered beta moduli divides the index gap times c.

The multiple relation is transitive.

Every natural number is a multiple of itself.

The defined order is reflexive; zero is its witness.

Only zero is less than or equal to zero.

Every dividend has a quotient and bounded remainder for a successor divisor.

Every positive divisor admits a quotient and a strictly bounded remainder.

Zero is a multiple of every natural number.

Every natural is the relational gcd of itself and zero.

A common divisor of a divisor and remainder divides their Euclidean linear step.

A relational gcd of divisor and remainder is a gcd of dividend and divisor.

Permute the outer entries of two additive pairs.

Transport balanced natural Bezout coefficients across one Euclidean division step.

Bounded Euclidean descent simultaneously constructs a relational gcd and balanced natural Bezout witnesses.

Every pair has a relational gcd together with balanced natural Bezout witnesses.

Coprime inputs admit balanced natural Bezout coefficients with result one.

Scale a balanced natural combination on the right.

Every common divisor of two inputs divides the result of a balanced natural combination.

Cancel a coprime factor from a divisibility witness (Gauss cancellation).

Beta moduli at an additive index gap dividing c are coprime.

Ordered bounded indices have coprime beta moduli when c is a common multiple of the bounded positive gaps.

Distinct indices in a bounded prefix have pairwise coprime beta moduli under a bounded common-multiple invariant.

Coprimality with a fixed right operand is closed under multiplication on the left.

Extend the accumulated target-modulus product for an exclusive prefix.

Every nonzero natural has a predecessor.

A balanced Bezout identity selects the right coefficient modulo the left modulus.

A balanced Bezout identity selects the left coefficient modulo the right modulus.

Balanced congruence is preserved by multiplication on the right.

Balanced congruence is preserved by multiplication on the left.

A multiple is balanced-congruent to zero.

Balanced natural congruence respects addition.

Balanced natural congruence is reflexive.

Balanced natural congruence is transitive.

The predecessor of a successor acts as minus one in balanced congruence.

Constructive binary CRT for positive coprime natural moduli using balanced congruence.

Balanced congruence descends from a multiple modulus to every divisor modulus.

One binary CRT extension preserves every old congruence whose modulus divides the accumulated product.

Every Gödel-beta position has a bounded decoded residue.

Every pair of natural numbers is comparable in the defined order.

A common left addend can be cancelled.

A strict upper bound prevents the lower term from containing that bound as an additive middle block.

A positive gap between quotients makes two bounded-remainder decompositions unequal.

Bounded quotient-remainder decompositions have unique quotients and remainders.

The decoded residue at a Gödel-beta position is unique.

Add the next source value to a target-base CRT code for an exclusive prefix.

Combine modulus-product and cross-base congruence updates for an exclusive prefix.

Fold an empty-based, exclusive beta prefix into another base with append readiness.

Adding on the left produces an explicit order witness.

Successor preserves the witness-defined order.

Every nonzero natural is at least one.

Right multiplication preserves the witness-defined order.

Scaling by a nonzero natural does not decrease a natural.

A weak inequality remains true after raising its upper bound by one.

A beta base is at most every beta modulus over that base.

The appended value fits every modulus after the same constructive scaled-base rebase.

Every decoded beta value is at most its code.

Adding on the right produces an explicit order witness.

An old beta value fits every modulus after a constructive scaled-base rebase.

Two balanced-congruent values below the same modulus are equal.

A bounded balanced residue has a directed quotient/remainder witness.

A bounded value congruent to a code is its expanded Gödel-beta value.

Rebase an arbitrary decoded prefix and append one exact natural value.

Recode a consecutive prefix and append its next value.

Every start and length admit a beta-coded consecutive range.

Every prime natural is nonzero.

A decoded entry of a Range prefix is its start plus its index.

Weak order followed by strict order remains strict.

Entries 1 through h in an odd half-range are nonzero and below p.

Bounded induction constructs a relational gcd whenever the right input is at most the bound.

Every pair of naturals has a relational greatest common divisor.

A relational gcd witness one implies expanded coprimality.

A prime dividing a product divides at least one factor (Euclid's lemma).

A divisor of a nonzero natural is bounded by that natural.

A strict inequality excludes the reverse weak inequality.

Any two naturals satisfy weak order in one direction or strict order in the other.

A directed quotient/remainder equation gives balanced congruence to its remainder.

A value below a successor is the predecessor or lies below it.

A value below a Gödel-beta modulus decodes to itself when used as the code.

Zero is below every natural number.

Every decoded beta prefix admits an exact beta-coded prefix-sum trace.

Every decoded beta prefix has a relational finite sum.

Every all-bits prefix has a relational count of its ones.

Adding the same right summand preserves the witness-defined order.

Adding the same left summand preserves the witness-defined order.

Balanced natural congruence is symmetric.

A prime is constructively either coprime to a natural or divides it.

A prime not dividing a natural is coprime to that natural.

Coprimality in its expanded common-divisor form is symmetric.

Balanced Bezout coefficients give a subtraction-free modular inverse.

A nonzero modulus turns balanced Bezout data into a natural modular inverse.

A coprime factor cancels from balanced congruence at nonzero modulus.

A nonzero residue factor cancels from congruence modulo a prime.

Equal decoded values in one consecutive range have equal indices.

A natural at least one is nonzero.

Successor is injective (the reusable PA2 lemma).

Every decoded beta factor prefix admits a beta-coded exact prefix-product trace.

Every finite decoded beta prefix has an exact relational product and a coded trace.

A successor sum decomposes into its prefix sum and final summand.

Dropping the final entry preserves the all-bits invariant.

The final entry of a nonempty all-bits prefix is zero or one.

A successor count is its prefix count plus a final zero-or-one bit.

Every constant beta prefix of length zero is vacuously Repeat.

Recode a constant prefix and append one more copy of its value.

Every value and length admit a beta-coded constant prefix.

Every base and exponent have a relational finite-product power.

The sum of an empty decoded prefix is zero.

An empty bit prefix contains zero ones.

The product of an empty decoded prefix is one.

A successor product decomposes into its prefix product and final decoded factor.

The relational zeroth power is one.

Every decoded entry of a Repeat prefix equals its repeated value.

A successor relational power is its predecessor power times the base.

Balanced natural congruence respects multiplication.

The empty decoded prefix is surjective onto the empty interval.

Equality of natural numbers is constructively decidable.

Occurrence of a value in a nonempty decoded prefix is constructively decidable.

A bounded successor prefix exposes a bounded final decoded value.

Recode a finite beta prefix while replacing one interior entry.

Swap a chosen interior beta entry with the last entry, given both decoded values.

Every explicitly decoded entry of a bounded prefix satisfies its value bound.

A swap-last recoding preserves boundedness of the full successor prefix.

Every decoded swapped entry reflects to one of the two moved entries or the original index.

A swap-last recoding preserves injectivity of the full successor prefix.

If a successor prefix omits its top value, its old prefix is bounded by the predecessor.

Injectivity of a successor prefix restricts to its old prefix.

A bounded injective successor sequence must place the new value last once its prefix is surjective.

A surjective prefix plus its new top value is surjective at successor length.

The available successor branch extends prefix surjectivity to the full prefix.

Surjectivity of a swapped successor prefix transports back to the original code.

The no-top branch of the constructive successor induction is complete.

Every bounded injective beta-coded prefix is surjective onto its finite interval.

A bounded injective successor reindexing fixed at its last position is bounded on the old prefix.

One-way extensional factor-prefix preservation transports Product without changing its trace.

Multiplication preserves equality in both arguments.

The fully expanded beta-coded Product relation is functional in its terminal product.

Replacing one factor balances the old and new finite products by the exchanged values.

Swapping an interior beta-coded factor with the last factor preserves the exact finite product.

Simultaneous interior/final swaps of an index code and target factors preserve alignment.

An even and an odd decomposition of the same natural are incompatible.

No odd natural is even.

Every natural has a constructive even-or-odd witness.

The successor of an even natural is odd.

No even natural is odd.

If a successor is even, its predecessor is odd.

The successor of an odd natural is even.

If a successor is odd, its predecessor is even.

The predecessor of a successor squares to one modulo that successor.

Powers of the predecessor of p alternate between one and the predecessor modulo p.

Repeat prefixes with one value preserve every decoded entry extensionally.

Relational powers have a unique natural value.

A successor power paired with its predecessor equals predecessor times base.

Balanced-congruent bases have congruent relational powers at every exponent.

Canonical bounded remainders constructively decide congruence.

Balanced congruence is constructively decidable at nonzero modulus.

Inclusive bounded search constructively decides square congruence.

A nonzero modulus admits a finite constructive residue search.

Expand a square while retaining an explicit quotient and remainder.

Absorb a second quotient into an existing residue equation.

Lift one quotient-and-remainder equation through squaring.

Existential wrapper for the generic square-residue lift.

Every square witness has an equivalent canonical bounded root.

Quadratic residuosity is constructively decidable at nonzero modulus.

A successor of a zero exponent gives the relational first power.

The relational first power of a natural is the natural itself.

A successor of exponent one gives the relational square.

The relational second power is exactly the square.

Relational powers turn addition of exponents into multiplication.

Iterated relational powers multiply their exponents.

Every natural has a beta-coded relational factorial value.

Every prime natural is the second successor of a natural.

A nonzero residue modulo a prime has a natural modular inverse.

A nonzero residue below a prime has a nonzero bounded inverse.

Every prime other than two is odd.

A successor factorial is its predecessor factorial times the successor.

The relational factorial of zero is one.

A fixed-point equation remains fixed after dropping an additive prefix.

Opposing additive witnesses force equality.

The witness-defined order is antisymmetric.

Two bounded inverses of the same residue are equal.

Two Range codes preserve every decoded entry extensionally.

The beta-coded relational factorial has a unique value.

Doubling commutes through multiplication on the right.

The product of two odd naturals is odd.

A product with an even right factor is even.

An even natural plus an odd natural is odd.

An odd natural plus an even natural is odd.

The sum of two even naturals is even.

The sum of two odd naturals is even.

Addition preserves equality in both arguments.

Two exact prefix-sum traces over one decoded prefix have equal endpoints.

Strict order followed by weak order remains strict.

Left multiplication preserves the witness-defined order.

A bounded remainder keeps its decomposition below the next divisor block.

Strict order is transitive.

The relational finite sum has a unique natural value.

The relational count of a fixed all-bits prefix is unique.

Multiplication by four is iterated doubling.

A nonzero common left factor can be cancelled.

The half witness in an odd decomposition is unique.

A product with an even left factor is even.

A prime cannot divide a distinct prime.

The reverse orientation is nondivisible as well.

Distinct primes are mutually nondivisible.

A residue strictly above h and below 2*h+1 has a positive reflected magnitude at most h.

A nonzero canonical product remainder has a positive half-range magnitude, with its sign recorded by a lower/reflected congruence disjunction.

A canonical nonzero remainder yields one explicit zero/one signed-half choice at its decoded source index.

A prime odd half-range and a nondivisible multiplier provide a signed choice at every decoded entry.

Append one pointwise signed choice simultaneously to the magnitude and zero/one sign beta prefixes.

Every bounded family of pointwise signed choices admits aligned beta-coded magnitude and sign prefixes.

The full prime odd half-range has beta-coded positive magnitudes and explicit reflection bits.

The sign projection of every encoded signed-half prefix is an AllBits prefix.

The encoded reflection bits have a native relational count of their ones.

Every decoded signed-prefix magnitude lies constructively in 1,...,h.

A nonzero prime residue multiplier is injective when two bounded sources have one modular target.

Equal lower signs or equal reflected signs force equality of the bounded source residues.

Opposite signed representatives cannot share one magnitude when their positive source sum is below p.

The positive signed-half magnitude prefix is injective over the full beta-coded half range.

Every positive bounded beta prefix can be recoded pointwise by removing one successor from each value.

The signed-half magnitude prefix admits a beta code of its 0,...,h-1 predecessors.

Append the selected 1/r factor while preserving every earlier decoded factor.

Every finite beta bit prefix admits a beta-coded 1/r sign-factor prefix.

Dropping the final position preserves the bit-to-sign-factor relation.

The product of 1/r sign factors is exactly r to the number of one bits.

For p=S r, the recoded sign product exists and equals the relational power r^e.

Append the product of the two final decoded values and preserve all earlier products.

Two beta prefixes admit a third beta prefix of their pointwise products.

Pointwise multiplication alignment restricts to the predecessor prefix.

Pointwise products of synchronized beta prefixes multiply their exact finite products.

The pointwise-product code has a Product equal to the product of the two source Products.

Signed magnitudes times their 1/r factors are pointwise congruent to the scaled source prefix.

Pointwise multiplication by a constant scales a finite product by its power.

The scaled canonical-source product is congruent to the product of signed magnitudes.

Removing one successor turns the positive 1,...,l range bound into the finite 0,...,l-1 bound.

Unique target decoding reflects every predecessor-code entry back to its source successor magnitude.

Injectivity of positive magnitudes transports to their uniquely decoded predecessor code.

The predecessor map aligns canonical factor 1+j with magnitude S j at every position.

A fixed-final reindex reduces successor product equality to equality of the two prefix products.

A bounded injective beta-coded reindexing preserves the exact finite product.

A magnitude permutation has exactly the product of the canonical half range.

The four Gauss product layers compose to A*P == P*r^e modulo p.

A finite product of factors pointwise coprime to m is coprime to m.

A product of positive residues below a prime is coprime to that prime.

The canonical half-range product is coprime to its odd prime modulus.

Coprimality of the half-range product constructively cancels P.

Gauss's signed half-range count controls a^h modulo the odd prime.

Every nonmultiple has a nonzero canonical remainder congruent to it.

Quadratic residuosity depends only on the balanced congruence class.

A congruent base has a relational power congruent to the supplied power.

A nonzero value strictly below a modulus is not divisible by it.

For a nonzero modulus, congruence to zero gives an explicit divisor witness.

Canonical nonzero products modulo a prime form a beta-coded index map.

Every decoded finite prefix can be recoded after successor-lifting its values.

The canonical multiplication-residue index map is bounded.

Multiplication by a nonzero prime residue is injective on 0,...,p-2.

A decoded entry of the range 1,...,l is the successor of its index.

A bounded residue map aligns the range 1,...,n with its successor lift.

The range and its successor-lifted residue map are pointwise congruent after scaling.

A nonzero multiplier modulo a prime induces a beta-coded residue reindexing.

Scaling the nonzero residues modulo a prime preserves their exact product modulo p.

The product 1*...*(p-1) is coprime to a prime p.

Fermat's theorem for the native predecessor exponent p-1.

A nonzero quadratic residue has half power one modulo an odd prime.

Multiplying an ordinary inverse by the target gives a scaled inverse.

A scaled inverse survives replacement by a congruent right factor.

A scaled inverse of a nonzero bounded target cannot be zero.

Every bounded nonzero prime residue has a bounded scaled inverse.

Append one actual scaled-inverse value to a zero-based source prefix.

Every bounded predecessor length has a beta-coded scaled-inverse prefix.

A prime predecessor interval has a full beta-coded scaled-inverse map.

Shifted orbit closure is vacuous on an empty order prefix.

Every empty beta prefix is bounded into every codomain.

Decoded-prefix injectivity is vacuous at length zero.

Zero codes witness the empty shifted, bounded, injective state.

The explicit adjacent scaled-orbit history is empty at zero pairs.

Move the newest pair from stored count to remaining count.

Expose a strict-prefix witness whenever at least one pair remains.

Bounded occurrence search either covers the target interval or returns an explicit omission.

Append one chosen source preimage to a beta-coded inverse-choice prefix.

Full finite coverage admits a beta-coded choice of one preimage for each target value.

Every inverse-choice prefix is bounded into the source domain.

A beta-coded choice of source preimages is injective by functionality of the source code.

A prefix shorter than the target interval cannot cover every target value.

Every beta-coded prefix shorter than n explicitly omits a value below n.

Every decoded scaled-inverse prefix entry satisfies its stored relation.

Every positive decoded mate has a predecessor inside the source bound.

The scaled-inverse relation is symmetric.

The bounded scaled inverse of a prime unit is unique.

A valid scaled inverse at a covered source is decoded by the prefix.

Decoding a scaled-inverse mate and decoding its predecessor returns the source residue.

On the bounded unit domain, fixed points are exactly square roots of a.

A negative QRes witness makes the scaled involution fixed-point-free.

A nonresidue scaled-inverse prefix has no decoded fixed point.

Choose an omitted source, decode its actual mate S j, and expose a distinct involutive pair.

Shifted orbit closure transfers omission across a decoded back edge.

Append two values at consecutive beta positions while preserving every old entry.

Every entry of a two-appended prefix is the second append, the first append, or an old entry.

Appending both zero-based sources preserves closure under actual-mate entries S j.

Appending two distinct values omitted by an injective old prefix preserves decoded-prefix injectivity.

Choose one omitted fixed-point-free scaled orbit and append its two sources adjacently.

A two-entry append remains bounded when the old prefix and both appended values are bounded.

The left position of an earlier pair lies below the doubled prefix.

The right position of an earlier pair lies below the doubled prefix.

Append one adjacent pair while retaining its raw At(i,S j) scaled edge.

Append one fixed-point-free scaled orbit and preserve iterable state plus history.

Normalize the two-entry successor length into the next doubled pair count.

Iterate exactly one adjacent scaled orbit for every stored pair.

At n=h+h, package a complete adjacent scaled-orbit order of length n.

A successor-lifted terminal scaled-orbit history has adjacent products congruent to a.

A product of length S(S k) decomposes into its k-prefix and its final two factors.

Adjacent fixed-target pairs multiply to the corresponding relational power.

A bounded injective order and its successor lift multiply to n factorial.

A prime is two or has exactly the doubled terminal PairOrder shape.

The relational factorial of one has value one.

Every nonzero prime residue index has a bounded inverse index.

Append one bounded zero-based inverse index to an inverse prefix.

Every length bounded by p-1 has a beta-coded inverse prefix.

A prime predecessor interval has a full beta-coded inverse map.

Orbit closure is vacuous on the empty decoded prefix.

The nonendpoint range invariant is vacuous on the empty prefix.

Arbitrary zero codes witness the empty PairOrder invariant state.

The adjacent inverse-pair witness invariant is vacuous at zero.

Rebalance one stored pair into the predecessor induction hypothesis.

Expose the exact one-orbit room equation in the successor case.

By temporarily appending both endpoints, finite omission constructively selects a missing nonendpoint value.

Every decoded inverse-prefix entry satisfies its stored inverse relation.

A bounded square root of one modulo a prime is one or the prime predecessor.

A fixed zero-based inverse index is zero or the last index.

A decoded inverse entry from a nonendpoint source is not fixed.

The bounded inverse-index relation is symmetric.

A bounded inverse index is unique.

A full inverse relation at a covered index is decoded by the prefix.

Decoding an inverse mate and decoding again returns the source index.

The zero index, representing residue one, is fixed by the full inverse prefix.

The last index, representing the predecessor of p, is fixed by the full inverse prefix.

The decoded mate of a nonendpoint inverse index is also a nonendpoint.

Choose an omitted nonendpoint index and extract its distinct, nonendpoint inverse mate together with both decoded directions.

Orbit closure turns omission of one endpoint of a decoded two-cycle into omission of its mate.

Appending both directions of a decoded two-cycle preserves orbit closure of the used prefix.

A two-entry append preserves the nonendpoint invariant when both appended values satisfy it.

Constructively choose one unused inverse orbit, append its two directions adjacently, and preserve the orbit-closed nonendpoint prefix invariants.

Thread decoded-prefix injectivity through one constructive fresh-orbit append.

Thread the complete bounded PairOrder state through one fresh inverse-orbit append.

A two-entry append preserves every old inverse pair and adds the new one.

Preserve the bounded PairOrder state and every adjacent inverse-pair witness through one append.

Iterate pair appends while retaining both bounded state and adjacent inverse history.

Specialize the paired iteration to a terminal n-2 prefix with full adjacency history.

The predecessor code covers every value 0,...,l-1 by constructive finite pigeonhole.

A bounded injective terminal prefix covers exactly every nonendpoint value below n = l+2.

The strengthened PairOrder state is complete at the exact terminal length n-2.

Every zero-based pair order has a beta code of successor-valued factors.

Successor-lifted adjacent inverse indices multiply to one modulo p.

Package a successor-valued factor code with adjacent unit pairs.

Adjacent inverse pairs multiply to one across an exact beta-coded even prefix.

The complete successor-lifted nonendpoint factor product is one modulo p.

A terminal PairOrder state decodes exactly positive values bounded by its length.

The predecessor map aligns canonical residues 2+j with successor-lifted PairOrder entries.

The lifted terminal product equals the product of the canonical nonendpoint range.

Package terminal PairOrder history, coverage, lifted product, and equality with residues 2,...,p-2.

Project the terminal PairOrder package to its canonical nonendpoint product modulo one.

A product of 2,...,l+1 is the factorial of l+1; the missing leading factor is one.

Restore the final factor l+2 after the leading unit has been absorbed.

Multiplying a residue-one product by n restores the predecessor residue n.

Wilson's factorial congruence for every prime, with p=2 handled before terminal pairing.

A completed terminal scaled pairing sends a^h to the predecessor p-1 modulo p.

A full nonresidue scaled-inverse prefix satisfies Euler's minus-one branch.

For a reduced nonzero nonresidue, a^((p-1)/2) is p-1 modulo p.

Every bounded nonzero input lands constructively in exactly the appropriate Euler endpoint.

A doubled predecessor cannot equal one.

For an odd-prime predecessor, the canonical residues one and p-1 are distinct.

For bounded nonzero inputs, quadratic residuosity is equivalent to the half-power residue one.

Euler's residue equivalence for an arbitrary nonmultiple representative.

For bounded nonzero inputs, nonresiduosity is equivalent to the half-power residue p-1.

Euler's nonresidue equivalence for an arbitrary nonmultiple representative.

Complete Euler criterion for every representative coprime to the prime.

An arbitrary prime unit is a quadratic residue exactly when its Gauss reflection count is even, and a nonresidue exactly when it is odd.

A constant prefix times 1,...,h decodes exactly as a*(1+i).

Append one quotient/remainder pair while preserving the decoded prefix.

Every finite beta source prefix has beta-coded quotients and bounded remainders for a nonzero modulus.

An odd-prime half range has exact scaled quotient/remainder codes.

The quotient code additionally carries its native finite floor sum.

The half of an odd modulus p=2h+1 is strictly below p.

A positive magnitude at most the odd half has a complement below the modulus.

The predecessor multiplier is congruent to the complementary remainder.

A bounded value congruent to an exact division input is its canonical remainder.

A Gauss signed congruence determines the exact canonical lower/reflected remainder branch.

Multiplication by an odd natural preserves and reflects evenness.

Multiplication by an odd natural preserves and reflects oddness.

An odd multiplier preserves both parity classes exactly.

An even sum has summands of the same parity.

A sum is even exactly when its summands have the same parity.

For odd divisor coefficient p, n=p*q+r is even exactly when q+r is even.

An odd sum has summands of opposite parity.

A sum is odd exactly when its summands have opposite parity.

For odd divisor coefficient p, n=p*q+r is odd exactly when q+r is odd.

An exact quotient-remainder equation with odd coefficient preserves the complete parity classification.

Every even natural is congruent to zero modulo two.

Every odd natural is congruent to one modulo two.

Naturals with the same constructive parity are congruent modulo two.

Odd scale and modulus transport an exact division equation to x == q+r modulo two.

Reflecting two remainders across an odd modulus flips parity.

A lower/reflected signed remainder changes q+r to q+m+s only by an even amount.

The generic Gauss-Eisenstein pointwise join: x == q+m+s modulo two.

Exact signed division data gives the Gauss--Eisenstein modulo-two relation.

Aligned Gauss and Eisenstein prefixes satisfy x == q+m+s modulo two pointwise.

Pointwise x==q+m+s congruence lifts to the four exact Sum endpoints.

The pointwise Gauss--Eisenstein congruence aggregates to exact terminal Sums.

The magnitude-predecessor code aligns positive magnitudes with the canonical half range.

Pointwise-equal decoded prefixes preserve an exact relational Sum.

Replacing one summand balances the old and new finite sums by the exchanged values.

Swapping an interior beta-coded summand with the last summand preserves the exact finite sum.

A fixed-final reindex reduces successor sum equality to equality of the two prefix sums.

A bounded injective beta-coded reindexing preserves the exact finite sum.

A positive magnitude permutation has exactly the canonical half-range Sum.

Gauss signed-half data makes the magnitude Sum equal the canonical half Sum.

Balanced congruence cancels a common additive left term constructively.

From x == q+x+s modulo two, cancel x and obtain 0 == q+s.

Cancel the exact Gauss magnitude Sum: 0 == quotient Sum + sign Sum modulo two.

Congruence to zero modulo two supplies an even witness.

If q+e is zero modulo two, q and e have the same parity and are congruent.

The Gauss sign BitCount is congruent modulo two to its orientation's quotient Sum.

One odd prime orientation has complete Gauss classification and a congruent exact Eisenstein quotient sum.

Distinct odd primes have no bounded positive point on q*x=p*y.

Every bounded half-rectangle cell has one exclusive orientation.

Every bounded lattice cell has a constructive exact indicator bit.

A fixed bounded row has a constructive exact bit choice in every column.

Append one exact orientation bit while preserving the previous row prefix.

Every finite family of exact cell choices has a beta-coded row prefix.

The beta-coded indicator projection contains only zero and one.

Every fixed half-rectangle row has an exact beta-coded indicator and BitCount witness.

Each bounded row has one semantic row-count witness.

Every prefix length at most h has semantic row-count choices.

Append one semantic row count while preserving all earlier rows.

Every finite family of semantic row counts has an outer beta prefix.

Every bounded initial set of rows has a semantic count prefix.

All h rows have one outer beta prefix of semantic counts.

The nested row counts have a native beta-sum rectangle total.

A bounded positive factor times a prime nondivisor cannot have zero remainder modulo that prime.

Distinct primes give the nondivisibility needed by the bounded scaled-remainder theorem.

An index below the divisor's own odd half has nonzero scaled remainder for a distinct prime multiplier.

The odd half-products differ by the explicit positive gap h+k+1.

A division row from the first odd half has quotient at most the second half.

A positive multiple lies below a nonintegral division value exactly through the quotient threshold.

A semantic row prefix is the exact initial segment cut out by its nonzero division quotient.

Every exact threshold prefix is an AllBits prefix.

Every decoded bit recovers its exact threshold semantics.

A length-k beta prefix consisting only of ones has BitCount k.

The BitCount of a bounded exact initial segment is its threshold.

A bounded exact initial-segment prefix has native BitCount q.

A semantic row BitCount is the quotient in its bounded nonzero division.

The semantic row count equals the quotient decoded by the scaled division prefix at that row.

The outer rectangle's semantic row witness is extensionally its decoded division quotient.

Every decoded quotient entry is the corresponding semantic rectangle entry.

The quotient Sum trace transports exactly to the semantic rectangle prefix.

The quotient floor-sum endpoint equals the independently summed semantic rectangle total.

Every decoded outer entry is semantically a BitCount of its row.

A fixed bounded index has one provenance-carrying bit in every swapped row.

Append one provenance-carrying swapped-row bit to a transposed column.

Every finite family of swapped-row cell choices has one beta-coded column.

Every decoded row bit recovers its exact strict-orientation meaning.

Every provenance-carrying transposed column is a zero/one prefix.

A decoded cell bit and its swapped-row transpose are exact complements.

Every decoded original-row bit and constructed column bit are exact complements.

Complementary decoded bit prefixes have counts summing to their length.

One semantic row and the constructed whole transposed column partition all k cells.

Every original row index has a fully witnessed complementary column count.

Append one fully witnessed column count to the outer count prefix.

Every bounded family of column-count witnesses has one outer beta prefix.

The provenance-carrying column counts have an exact relational outer Sum.

A constant beta prefix has exact relational sum length times value.

Every value and length admit a constant prefix with its exact sum.

Every decoded column-count outer entry recovers its full partition witness.

Decoded original-row and constructed-column counts partition the row width.

The decoded row and column counts add to the decoded entry of any constant-k prefix.

Pointwise sums of decoded entries induce exact addition of finite sums.

The original row total plus the constructed column-count total is exactly h*k.

Forget complement-partition provenance while retaining every genuine transposed-column count.

Every semantic zero-width rectangle has relational outer Sum zero.

A successor indicator row restricts to the same code's predecessor prefix.

A semantic successor row count is its restricted count plus its final decoded bit.

Every stored successor row constructively chooses an aligned reduced count and terminal bit.

Append aligned reduced-count and terminal-bit entries while preserving complete row provenance.

Any bounded family of successor-row splits has aligned β-coded reduced and terminal prefixes.

A semantic successor-width rectangle yields aligned reduced-count and terminal-bit β-prefixes.

The reduced-count code in a split prefix is itself a semantic predecessor-width rectangle prefix.

Every aligned decoded successor count is exactly its decoded reduced count plus terminal bit.

The successor outer Sum is exactly the reduced-row Sum plus the terminal-bit Sum.

A semantic column-count prefix restricts from successor length to predecessor length.

A decoded entry of any genuine transposed column has the exact Eisenstein cell orientation.

The exact orientation predicate determines its zero-or-one indicator uniquely.

Counts of extensionally identical semantic transposed columns are equal across arbitrary provenance codes.

Rebuild a counted column over another semantic outer code without changing its count.

Retarget every predecessor column count from the successor outer code to the reduced semantic rows.

The terminal-bit prefix and the constructed last column decode the same bit at every bounded row.

Every terminal-prefix decode transports extensionally to the constructed last-column code.

The terminal-bit Sum is exactly the relational count Sum of the constructed last column.

Any genuine transposed-column count total equals the swapped semantic row total.

The constructed complementary-column total is exactly the swapped semantic row total.

The two semantic Eisenstein row totals add exactly to the rectangle area.

For distinct odd primes, the two decoded finite quotient sums add exactly to h*k.

Distinct odd primes admit both Gauss classification counts, their mod-two quotient sums, and the exact Eisenstein sum identity.

Two oriented count/quotient congruences plus the exact floor-sum identity give e+f == h*k modulo two.

The half of a fixed odd number congruent to one modulo four is exactly even.

For a fixed odd decomposition, a modulo-four-one modulus is equivalent to an even half.

Congruence to one modulo two supplies an odd witness.

Balanced congruence modulo two preserves both parity predicates.

An even sum of Gauss counts gives equal cross-residue status.

Modulo-two equality with an even half product gives equal residue status.

A one-mod-four input forces equal cross-residue status.

Conditional one-mod-four reciprocity: the two cross-residue propositions have the same truth status.

The half of a fixed odd number congruent to three modulo four is exactly odd.

For a fixed odd decomposition, a modulo-four-three modulus is equivalent to an odd half.

An odd sum of Gauss counts gives opposite cross-residue status.

Modulo-two equality with an odd half product gives opposite residue status.

Two three-mod-four inputs force opposite cross-residue status.

Conditional three-mod-four reciprocity: exactly one cross-residue proposition holds.

The exact sign-free two-case quadratic-reciprocity endpoint.