Prime-field arithmetic and finite tables — Exact Proof Explorer

Equality gives genuine balanced modular congruence.

Zero is a canonical representative at every prime, including two.

Every bounded representative represents itself, including zero.

Equality transports the dividend of an actual residue graph.

Balanced congruence transports canonical residues; no quotient oracle is assumed.

No two distinct representatives below p denote the same residue class.

The modulus itself has canonical residue zero, the characteristic-p boundary.

Construct the unique canonical add output for every pair of residues.

The actual bounded add graph is functional without any field-law premise.

Existence and uniqueness of canonical prime-field add are both proved.

Commutativity of actual canonical add, not an assumed table axiom.

Construct the unique canonical multiply output for every pair of residues.

The actual bounded multiply graph is functional without any field-law premise.

Existence and uniqueness of canonical prime-field multiply are both proved.

Commutativity of actual canonical multiply, not an assumed table axiom.

Both bracketings of three canonical add operands give the same actual result.

Both bracketings of three canonical multiply operands give the same actual result.

Actual left distributivity of multiplication over addition on bounded representatives.

Actual right distributivity of multiplication over addition on bounded representatives.

Natural zero is the actual additive identity, not an arbitrary chosen code.

Zero is also the left additive identity on every canonical representative.

Natural one is the actual multiplicative identity, including at p=2.

One is also the left multiplicative identity.

Multiplication by the actual zero representative produces zero.

Zero is absorbing on both sides of multiplication.

Additive cancellation follows from genuine balanced congruence cancellation and canonical bounds.

Construct a bounded additive inverse by actual signed floor division; the zero input is included.

Actual additive inverses are unique among canonical representatives.

Every element, including zero, has a unique actual additive inverse.

Every nonzero representative has an actual bounded multiplicative inverse, uniformly at every prime.

Multiplicative inverses are unique as bounded natural representatives.

Proved unique inverse existence has exactly the nonzero carrier domain, not an odd-prime or supplied-inverse premise.

Zero has no product equal to one; this follows from multiplication, not from the inverse definition's guard.

An actual inverse is itself nonzero, so reciprocal inversion has the correct domain.

Inversion is symmetric on the nonzero elements, with both domains proved.

Every nonzero canonical element is genuinely coprime to its prime modulus.

Cancellation by any nonzero element is proved, not assumed from a field certificate.

A zero canonical product has a zero factor, including the characteristic-two case.

The natural-number residue map preserves actual canonical add.

The natural-number residue map preserves actual canonical multiply.

No positive natural below p has residue zero; the modulus boundary is sharp.

Every prime has genuine canonical field arithmetic with distinct zero/one, total unique operations, both distributive laws, additive inverses and precisely nonzero multiplicative inverses.

Construct the actual bounded add value at every one of the p*p row-major indices.

Construct the actual bounded multiply value at every one of the p*p row-major indices.

Totalize only the inverse table by recording zero at zero; the nonzero branch constructs a genuine inverse.

The explicit zero convention and genuine nonzero inverses together define a functional total table operation.

Ordinary finite induction codes actual pointwise add witnesses; no choice axiom or unproved field law is introduced.

Ordinary finite induction codes actual pointwise multiply witnesses; no choice axiom or unproved field law is introduced.

Ordinary finite induction codes actual pointwise negate witnesses; no choice axiom or unproved field law is introduced.

Ordinary finite induction codes actual pointwise inverse witnesses; no choice axiom or unproved field law is introduced.

Construct every entry of the finite add table from primality alone.

Construct every entry of the finite multiply table from primality alone.

Construct every entry of the finite negate table from primality alone.

Construct every entry of the finite inverse table from primality alone.

Every prime has four actual finite beta-coded arithmetic tables; zero is only a totalized inverse-table convention.

Actual quotient/remainder uniqueness identifies both row-major coordinates of a add table entry.

Every decoded add table lookup has exactly the proved canonical arithmetic meaning.

Every genuine canonical add result occurs at its actual finite table index.

Actual quotient/remainder uniqueness identifies both row-major coordinates of a multiply table entry.

Every decoded multiply table lookup has exactly the proved canonical arithmetic meaning.

Every genuine canonical multiply result occurs at its actual finite table index.

Every decoded negate table lookup has its exact unary meaning, including the inverse-at-zero convention.

Every genuine negate value is stored at its actual unary table index.

Every decoded inverse table lookup has its exact unary meaning, including the inverse-at-zero convention.

Every genuine inverse value is stored at its actual unary table index.

The actual finite add table is symmetric under exchanging row and column.

Both parenthesizations of three actual add table lookups agree, with intermediate bounds proved.

The actual finite multiply table is symmetric under exchanging row and column.

Both parenthesizations of three actual multiply table lookups agree, with intermediate bounds proved.

The totalized inverse table really stores zero at zero, without claiming zero has an inverse.

Every nonzero inverse-table entry multiplies its input to the actual one representative.

Actual finite addition and multiplication table entries satisfy left distributivity, with all intermediate bounds derived.

Actual finite addition and multiplication table entries satisfy right distributivity, with all intermediate bounds derived.

Every decoded entry of the identity enumeration equals its actual index.

The actual p-entry enumeration is bounded, injective and onto every canonical field representative.

Exactly p canonical elements are witnessed by an actual finite bijection, not an external model count.

A genuine recoding preserving every one of the n+1 trace entries preserves all actual unit-addition steps.

Append the genuinely computed next unit sum to an actual finite beta history.

Ordinary induction proves that an actual n-step addition-of-one history has canonical residue n; the relation does not assume this invariant.

Every trace endpoint is a canonical representative, including the empty-history endpoint.

Construct an actual history of n additions of one for every natural n, including the empty history.

An actual repeated sum of n ones has canonical residue n.

Construct a genuine repeated-addition history ending at any supplied canonical residue; the trace invariant is proved, not assumed.

Any two actual histories of the same number of additions of one have identical endpoints.

Repeated addition is a total functional computation on every natural length, with an actual beta execution history.

The first positive number of additions of the actual identity one that returns zero is exactly p, including p=2.

For every prime construct all finite arithmetic tables, an exact p-element bijection, every field law, and characteristic p. This is the k=1 case only, not arbitrary prime-power extension fields.