Actual pointwise operations · signed values · distributivity · Constructive arithmetic

Signed weighted sums and linearity

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.

ArithAdd(F,G,H,l) ∧ SignedWeightedSum(W,F,l,a) ∧ SignedWeightedSum(W,G,l,b) ∧ SignedWeightedSum(W,H,l,c) ⇒ SignedAdd(a,b,c)

Construct real pointwise sum, product and scalar tables and prove algebraic laws for their actual finite signed sums, including empty windows.

Open the definition-aware map Read the final theorem See campaign milestone G007

Exact certificate

Fully expanded arithmetic

Inspect all 2117 native tactic lines and 121 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem WS0027 and follow only the lemmas and conservative definitions supporting signed_weighted_sum_add_linearity.

Trace prerequisites →
Zoom between mathematical scales: research checkpoint map → research domain → proof family → G007 milestone → theorem and definition dependencies.
Major independently established statements: WS0021 signed_weighted_sum_exists_unique · WS0028 signed_weighted_sum_scalar_linearity · WS0027 signed_weighted_sum_add_linearity.
Public research checkpoint, independently verified: 40 theorems in a complete dependency-closed HA bundle · 121 proof prerequisites · 18 linked definitions · 34 definition-dependency arrows · 2117 exact tactic lines. Not Alpha-enrolled; no Alpha checked-use authority; not Stable. Alpha v30 remains 3222 theorems and Stable remains 432. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 227 bundle nodes; SHA-256 e88ddec495a71d673e670299ea3943a5a996eecb1296fb746e107c8e0b81c967. Inspect the checkpoint receipt, literal bundle, and source files →
Exact mathematical boundary: All operation tables contain actual beta-coded entries and theorems compare represented signed values, not arbitrary encodings. The strict sum window is i<l; the separately certified endpoint i=l is unused. Rectangular row/column Fubini, divisor cancellation, convolution inversion and full G007 remain open.