Actual pointwise operations · signed values · distributivity
Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.
Construct real pointwise sum, product and scalar tables and prove algebraic laws for their actual finite signed sums, including empty windows.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
WS0001 signed_table_domain_resizeAn actual packed beta table has canonical entries on every finite domain; resizing the certificate never changes its streams.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS0002 signed_table_lookup_anyEvery actual table supplies an actual signed value at any requested index, rather than a totality oracle.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS0003 signed_table_add_lookupEvery supplied canonical lookup value satisfies the actual add graph, by lookup functionality and the witnessed pointwise entries.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS0004 signed_table_add_restrictRestrict the strict pointwise window from S l to l while retaining genuine input and output table certificates.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS0005 signed_table_add_emptyThe zero-length operation is empty on i<0 but still requires actual packed input and output tables.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS0007 signed_table_multiply_lookupEvery supplied canonical lookup value satisfies the actual multiply graph, by lookup functionality and the witnessed pointwise entries.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS0008 signed_table_multiply_restrictRestrict the strict pointwise window from S l to l while retaining genuine input and output table certificates.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS0009 signed_table_multiply_emptyThe zero-length operation is empty on i<0 but still requires actual packed input and output tables.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS000B signed_table_scalar_lookupEvery supplied canonical lookup value satisfies the actual scalar graph, by lookup functionality and the witnessed pointwise entries.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS000C signed_table_scalar_restrictRestrict the strict pointwise window from S l to l while retaining genuine input and output table certificates.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS000D signed_table_scalar_emptyThe zero-length operation is empty on i<0 but still requires actual packed input and output tables.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS0018 signed_table_add_reassociateConstructing the other parenthesization and applying literal signed-add functionality proves reverse associativity.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS001F signed_weighted_sum_existsConstruct the actual pointwise product table and both natural prefix-sum histories, then their canonical signed weighted-sum value.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS0021 signed_weighted_sum_exists_uniqueEvery two valid input tables have a genuinely constructed, literally unique canonical signed weighted-sum value.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS0022 signed_weighted_sum_empty_valueThe empty weighted sum is canonical zero, regardless of the unused endpoint values of its valid table witnesses.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS0023 signed_weighted_sum_empty_existsConstruct the real zero-length product table and signed fold; its output is then proved to be zero.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not StableWS0025 signed_weighted_scalar_commuteConstruct the reordered product and identify its canonical value by signed multiplication associativity, commutativity and functionality.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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.