Actual pointwise operations · signed values · distributivity
Construct real pointwise sum, product and scalar tables and prove algebraic laws for their actual finite signed sums, including empty windows.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
WS0001 signed_table_domain_resizeAn actual packed beta table has canonical entries on every finite domain; resizing the certificate never changes its streams.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0002 signed_table_lookup_anyEvery actual table supplies an actual signed value at any requested index, rather than a totality oracle.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0003 signed_table_add_lookupEvery supplied canonical lookup value satisfies the actual add graph, by lookup functionality and the witnessed pointwise entries.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0004 signed_table_add_restrictRestrict the strict pointwise window from S l to l while retaining genuine input and output table certificates.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0005 signed_table_add_emptyThe zero-length operation is empty on i<0 but still requires actual packed input and output tables.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0006 signed_table_add_extensional_uniqueOutputs of the same pointwise add operation agree in every represented value, not necessarily in their table codes or raw components.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0007 signed_table_multiply_lookupEvery supplied canonical lookup value satisfies the actual multiply graph, by lookup functionality and the witnessed pointwise entries.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0008 signed_table_multiply_restrictRestrict the strict pointwise window from S l to l while retaining genuine input and output table certificates.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0009 signed_table_multiply_emptyThe zero-length operation is empty on i<0 but still requires actual packed input and output tables.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS000A signed_table_multiply_extensional_uniqueOutputs of the same pointwise multiply operation agree in every represented value, not necessarily in their table codes or raw components.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS000B signed_table_scalar_lookupEvery supplied canonical lookup value satisfies the actual scalar graph, by lookup functionality and the witnessed pointwise entries.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS000C signed_table_scalar_restrictRestrict the strict pointwise window from S l to l while retaining genuine input and output table certificates.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS000D signed_table_scalar_emptyThe zero-length operation is empty on i<0 but still requires actual packed input and output tables.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS000E signed_table_scalar_extensional_uniqueOutputs of the same pointwise scalar operation agree in every represented value, not necessarily in their table codes or raw components.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS000F signed_table_add_extendThe actual pointwise add graph extends across a preserved strict prefix and a genuine new entry, without equating table codes.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0010 signed_table_add_existsOrdinary finite induction constructs both beta output streams and their actual packed table for pointwise add; no finite-choice or supplied-table oracle is used.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0011 signed_table_add_exists_extensionally_uniqueConstruct an actual pointwise add output and prove uniqueness of every represented entry; the raw table code is deliberately not claimed unique.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0012 signed_table_multiply_extendThe actual pointwise multiply graph extends across a preserved strict prefix and a genuine new entry, without equating table codes.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0013 signed_table_multiply_existsOrdinary finite induction constructs both beta output streams and their actual packed table for pointwise multiply; no finite-choice or supplied-table oracle is used.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0014 signed_table_multiply_exists_extensionally_uniqueConstruct an actual pointwise multiply output and prove uniqueness of every represented entry; the raw table code is deliberately not claimed unique.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0015 signed_table_scalar_extendThe actual pointwise scalar graph extends across a preserved strict prefix and a genuine new entry, without equating table codes.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0016 signed_table_scalar_existsOrdinary finite induction constructs both beta output streams and their actual packed table for pointwise scalar; no finite-choice or supplied-table oracle is used.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0017 signed_table_scalar_exists_extensionally_uniqueConstruct an actual pointwise scalar output and prove uniqueness of every represented entry; the raw table code is deliberately not claimed unique.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0018 signed_table_add_reassociateConstructing the other parenthesization and applying literal signed-add functionality proves reverse associativity.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0019 signed_table_add_medialThe actual four canonical signed summands may be regrouped across two prefix/last-entry pairs, with a genuinely constructed intermediate sum.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS001A signed_table_scalar_add_introAn actual sum of the two scalar products is the actual scalar multiple of the sum; no product witness or distributivity oracle is assumed.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS001B signed_prefix_sum_pointwise_addOrdinary 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.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS001C signed_prefix_sum_scalar_multiplyEvery 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.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS001D signed_prefix_sum_pointwise_add_values_existConstruct all actual signed prefix-sum values and prove their addition relation, including the empty-prefix boundary.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS001E signed_prefix_sum_scalar_multiply_values_existConstruct all actual signed prefix-sum values and prove their scalar product relation, including the empty-prefix boundary.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS001F signed_weighted_sum_existsConstruct the actual pointwise product table and both natural prefix-sum histories, then their canonical signed weighted-sum value.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0020 signed_weighted_sum_functionalEvery genuine product-table witness gives the same canonical signed weighted sum, even when its raw beta codes and representatives differ.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0021 signed_weighted_sum_exists_uniqueEvery two valid input tables have a genuinely constructed, literally unique canonical signed weighted-sum value.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0022 signed_weighted_sum_empty_valueThe empty weighted sum is canonical zero, regardless of the unused endpoint values of its valid table witnesses.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0023 signed_weighted_sum_empty_existsConstruct the real zero-length product table and signed fold; its output is then proved to be zero.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0024 signed_table_weighted_add_distributiveThe actual pointwise product tables distribute over a witnessed pointwise addition; every entry is constructed and checked against canonical signed scalar distributivity.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0025 signed_weighted_scalar_commuteConstruct the reordered product and identify its canonical value by signed multiplication associativity, commutativity and functionality.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0026 signed_table_weighted_scalar_commuteAn arbitrary signed scalar commutes with an actual table of pointwise weighted products, with the same strict prefix window and actual table witnesses.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0027 signed_weighted_sum_add_linearityActual signed weighted sums are additive in their value table, by genuine pointwise product distributivity and the proved prefix-sum induction.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableWS0028 signed_weighted_sum_scalar_linearityActual signed weighted sums commute with an arbitrary signed scalar; negative values, zero scalars and the empty prefix are included.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0ND0058 MatrixMinorFourCode(z,up,us,un,ut)One canonical injective doubled-Cantor code for all four signed-minor beta-code parameters.
Conservative definition · notation layer 0PD0001 Le(a,b)Witness-defined non-strict order on natural numbers.
Conservative definition · notation layer 0PD0013 BetaAt(b,c,i,x)x is the bounded beta-decoded value at index i.
Conservative definition · notation layer 0ND0142 SignedDecode(z,p,n)The original canonical integer code: even 2p denotes p, and odd 2k+1 denotes −(k+1). The decoded positive and negative parts are normalized.
Conservative definition · notation layer 0ND0143 SignedBalance(z,p,n)The original canonical code z represents the integer difference p−n; these supplied components need not be normalized.
Conservative definition · notation layer 1ND0251 ArithTable(N,F)An actual packed signed table with canonical signed entries through index N, including index zero. It contains no divisor transform or inversion hypothesis.
Conservative definition · notation layer 2ND0252 ArithAt(F,i,z)Two genuine beta entries of the packed table represent the unique canonical signed value z. Distinct component representations need not be equal.
Conservative definition · notation layer 2ND0254 ArithTableEqual(F,G,l)Pointwise equality of actual canonical signed lookups below l, not equality of table codes or their positive/negative components.
Conservative definition · notation layer 3ND0264 ArithExtend(F,G,l,z)A genuine output signed table through l preserves the represented source values at i<l and records the prescribed signed value z at l. Existence is proved by recoding both beta streams.
Conservative definition · notation layer 4ND0144 SignedAdd(a,b,c)Actual addition of original canonical signed codes, witnessed by their decoders and balanced equality.
Conservative definition · notation layer 1ND0266 ArithAdd(F,G,H,l)Three actual signed tables and witnessed SignedAdd entries at each i<l. The unused endpoint certified by ArithTable(l,...) is not included in the prefix sum.
Conservative definition · notation layer 3ND0145 SignedMul(a,b,c)Actual multiplication of original canonical signed codes; opposite-sign products remain on the negative side of the balance.
Conservative definition · notation layer 1ND0267 ArithMul(F,G,H,l)Three actual signed tables and witnessed SignedMul entries at each i<l; neither a finite-choice principle nor a product-of-sums identity is assumed.
Conservative definition · notation layer 3ND0268 ArithScale(a,F,G,l)Actual source and output tables with witnessed multiplication of every represented entry below l by the signed scalar a. Sum distributivity is a separate theorem.
Conservative definition · notation layer 3PD0015 Sum(b,c,l,z)z is the sum of a beta-coded prefix of length l.
Conservative definition · notation layer 1ND0253 SignedPrefixSum(F,l,z)The signed balance of two actual natural finite sums, at exactly the indices 0<=i<l. Existence, uniqueness and representation independence are proved separately.
Conservative definition · notation layer 2ND0272 SignedWeightedSum(W,F,l,z)An actual signed pointwise product table of weights W and values F, followed by its real signed prefix sum at indices i<l. No linearity, divisor cancellation or inversion is assumed in this graph.
Conservative definition · notation layer 4Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.