Actual rectangular sums and finite Fubini — Exact Proof Explorer

Every actual slice lookup is the identical canonical signed value at its explicitly computed source index.

Restrict only the strict slice window, retaining the same actual output streams and source packing.

A zero-length affine slice still requires real packed source and output tables; its strict entry window is empty.

Two slices of the same window agree in their represented signed entries, not necessarily their codes or component streams.

A preserved actual prefix and one real source lookup extend the slice without changing any earlier represented value.

Ordinary induction constructs the affine output by actual two-beta extension, including zero length and zero stride.

Construct an affine slice and prove extensional uniqueness, with no supplied slice, function, or finite-choice oracle.

Construct an actual affine slice and actual positive/negative prefix-sum traces; the result is not a supplied sum oracle.

The canonical signed affine-sum value is independent of every permissible slice encoding.

Every actual empty affine sum is the canonical signed zero, irrespective of offset or stride.

A valid source actually admits an empty slice and its zero sum, rather than merely a vacuous uniqueness assertion.

A successor affine sum decomposes into its actual prefix sum and actual last source entry with the original SignedAdd relation.

Extend both beta streams by the actual next source value and append the actual signed sum; no output slice is assumed.

Any two actual consecutive affine sums and their true intervening source value satisfy the signed addition law.

Every finite affine window of a genuine source table has a constructed and literally unique canonical signed sum.

Each actual row-table entry is the actual signed sum of the corresponding affine source slice.

Removing the last row preserves every actual earlier row sum and the same output encoding.

Zero rows impose no fictitious row values but still certify genuine source and row-table packings.

All genuine row-sum tables agree entrywise in canonical signed values, without identifying arbitrary beta encodings.

A preserved row-table prefix extends by one actually proved slice sum, never by an assumed finite-choice table.

Ordinary induction computes each finite slice sum and appends its actual signed value to construct the entire row-sum table.

Construct a genuine row-sum table and prove its precise extensional uniqueness at every i<m.

Construct the whole row-sum table and then its actual finite sum; both finite dimensions are arbitrary.

All actual representations of the same rectangular sum have the identical canonical signed result.

Every genuine source and every finite affine rectangle admit a constructed, unique signed double-sum value.

A rectangle with zero rows has actual signed total zero, including when its column count is nonzero.

Induction proves the sum of any actual table of empty row sums is zero; a positive number of zero-length rows is not silently discarded.

A rectangle with zero columns has actual signed total zero for every row count.

Appending one real grid row adds its actual entries pointwise to the actual column-sum table, using only the elementary equality of the two coordinate expressions.

Ordinary row-count induction proves finite signed Fubini for arbitrary affine grids, including both zero dimensions, by constructing the missing prefix column table and applying actual signed sum linearity.

Construct actual row and column sum tables and actual signed sum traces sharing one canonical value; no supplied slice, table, sum, or permutation witness is required.

Every actual row-major m-by-n signed beta table has constructed row and column sums with exactly the same total, including zero rows or columns.