Signed arithmetic tables and finite sums — Exact Proof Explorer

Actual beta entries and their canonical signed balance produce a genuine table lookup.

Every lookup unpacks against any proved representation of its exact table code, with actual component witnesses.

Every actual pair of beta component streams gives canonical signed entries on every requested finite domain, including the zero endpoint.

Natural pairing constructs the table code itself, not merely an opaque validity witness.

A valid finite signed table always supplies its actual nested natural-pair packing.

Every index in the explicitly stated finite domain has an actual canonical signed lookup code.

Actual beta functionality and canonical signed balance make each lookup code literally unique.

The same packed table remains valid on every shorter finite domain, without a new encoding or changed entries.

Two genuine natural finite sums and their canonical signed balance construct the signed prefix sum.

Every signed sum unpacks into actual natural prefix sums against its proved table representation.

Both natural folds and signed normalization are genuinely constructed; no supplied sum or sign oracle is required.

The signed sum has a literally unique canonical result code, not a supposedly unique non-normalized signed pair.

The empty signed prefix sum is exactly canonical zero, regardless of the packed component streams.

The empty sum is constructed as an actual two-trace signed fold and only then identified with zero.

Canonical signed negation swaps arbitrary natural-component balances, not merely normalized representatives.

Opposite arbitrary component balances imply actual canonical SignedNegate, using its constructed inverse and literal functionality.

A canonical signed integer equal to its own additive inverse is zero; no characteristic-zero claim is assumed without proof.

The successor natural sum is genuinely constructed and identified with the previous sum plus the actual last beta entry.

Pointwise equality of canonical lookup values implies balanced integer equality of arbitrary component streams, without equating the components themselves.

Signed prefix sums are independent of all pointwise balanced positive/negative representatives, by the checked natural cross-sum theorem.

Swapping the actual positive/negative beta streams negates their signed sum, using the same genuine natural traces.

A genuine signed prefix sum, its actual next entry and canonical signed addition construct the successor sum.

Every successor signed sum supplies real predecessor and last-entry codes whose original SignedAdd graph gives its result.

Actual component streams construct a canonical lookup at any specified index; finite consumers retain their explicit index bounds.

Two real finite beta compositions are constructed before any permutation argument; no supplied composed table is assumed.

Real component composition implements the signed lookup pullback exactly, at every bounded target index.

Any actual finite signed table admits a genuinely beta-coded pullback along an actual beta map, with its new table code constructed.

All actual pullbacks of the same signed table and map agree in canonical value, even when their component representatives differ.

Original finite natural-sum permutation invariance preserves both actual component sums, hence their canonical signed result.

Any actual bounded injective beta permutation preserves the genuine signed sum, even for unrelated positive/negative representations of the pullback table.