Signed weighted sums and linearity — Exact Proof Explorer

An actual packed beta table has canonical entries on every finite domain; resizing the certificate never changes its streams.

Every actual table supplies an actual signed value at any requested index, rather than a totality oracle.

Every supplied canonical lookup value satisfies the actual add graph, by lookup functionality and the witnessed pointwise entries.

Restrict the strict pointwise window from S l to l while retaining genuine input and output table certificates.

The zero-length operation is empty on i<0 but still requires actual packed input and output tables.

Outputs of the same pointwise add operation agree in every represented value, not necessarily in their table codes or raw components.

Every supplied canonical lookup value satisfies the actual multiply graph, by lookup functionality and the witnessed pointwise entries.

Restrict the strict pointwise window from S l to l while retaining genuine input and output table certificates.

The zero-length operation is empty on i<0 but still requires actual packed input and output tables.

Outputs of the same pointwise multiply operation agree in every represented value, not necessarily in their table codes or raw components.

Every supplied canonical lookup value satisfies the actual scalar graph, by lookup functionality and the witnessed pointwise entries.

Restrict the strict pointwise window from S l to l while retaining genuine input and output table certificates.

The zero-length operation is empty on i<0 but still requires actual packed input and output tables.

Outputs of the same pointwise scalar operation agree in every represented value, not necessarily in their table codes or raw components.

The actual pointwise add graph extends across a preserved strict prefix and a genuine new entry, without equating table codes.

Ordinary finite induction constructs both beta output streams and their actual packed table for pointwise add; no finite-choice or supplied-table oracle is used.

Construct an actual pointwise add output and prove uniqueness of every represented entry; the raw table code is deliberately not claimed unique.

The actual pointwise multiply graph extends across a preserved strict prefix and a genuine new entry, without equating table codes.

Ordinary finite induction constructs both beta output streams and their actual packed table for pointwise multiply; no finite-choice or supplied-table oracle is used.

Construct an actual pointwise multiply output and prove uniqueness of every represented entry; the raw table code is deliberately not claimed unique.

The actual pointwise scalar graph extends across a preserved strict prefix and a genuine new entry, without equating table codes.

Ordinary finite induction constructs both beta output streams and their actual packed table for pointwise scalar; no finite-choice or supplied-table oracle is used.

Construct an actual pointwise scalar output and prove uniqueness of every represented entry; the raw table code is deliberately not claimed unique.

Constructing the other parenthesization and applying literal signed-add functionality proves reverse associativity.

The actual four canonical signed summands may be regrouped across two prefix/last-entry pairs, with a genuinely constructed intermediate sum.

An actual sum of the two scalar products is the actual scalar multiple of the sum; no product witness or distributivity oracle is assumed.

Ordinary prefix induction proves that the actual sum of a witnessed pointwise table addition is the canonical signed sum of the two actual prefix sums, including length zero.

Every actual prefix sum commutes with multiplication by an arbitrary canonical signed scalar, via genuine successor sums and distributivity; zero length and negative scalars are included.

Construct all actual signed prefix-sum values and prove their addition relation, including the empty-prefix boundary.

Construct all actual signed prefix-sum values and prove their scalar product relation, including the empty-prefix boundary.

Construct the actual pointwise product table and both natural prefix-sum histories, then their canonical signed weighted-sum value.

Every genuine product-table witness gives the same canonical signed weighted sum, even when its raw beta codes and representatives differ.

Every two valid input tables have a genuinely constructed, literally unique canonical signed weighted-sum value.

The empty weighted sum is canonical zero, regardless of the unused endpoint values of its valid table witnesses.

Construct the real zero-length product table and signed fold; its output is then proved to be zero.

The actual pointwise product tables distribute over a witnessed pointwise addition; every entry is constructed and checked against canonical signed scalar distributivity.

Construct the reordered product and identify its canonical value by signed multiplication associativity, commutativity and functionality.

An arbitrary signed scalar commutes with an actual table of pointwise weighted products, with the same strict prefix window and actual table witnesses.

Actual signed weighted sums are additive in their value table, by genuine pointwise product distributivity and the proved prefix-sum induction.

Actual signed weighted sums commute with an arbitrary signed scalar; negative values, zero scalars and the empty prefix are included.