Constructed slices · row and column tables · zero dimensions · Constructive arithmetic

Actual rectangular sums and finite Fubini

SignedRectangularSum(F,o,s,t,m,n,a) ∧ SignedRectangularSum(F,o,t,s,n,m,b) ⇒ a=b

Construct actual signed affine slices and row-sum tables, then prove equality of row-first and column-first totals by ordinary finite induction.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact certificate

Fully expanded arithmetic

Inspect all 1393 native tactic lines and 92 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem RS0020 and follow only the lemmas and conservative definitions supporting signed_rectangular_row_major_fubini.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G007 milestone → theorem and definition dependencies.
Major independently established statements: RS0007 signed_rectangular_slice_exists_extensionally_unique · RS001E signed_rectangular_fubini · RS0020 signed_rectangular_row_major_fubini.
Independently verified Alpha v34 checked-use theorem family: 32 dependency-curried kernel-checked theorem bodies · 92 proof prerequisites · 18 linked definitions · 34 definition-dependency arrows · 1393 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 217 bundle nodes; SHA-256 a6f62d8a0c89431b3596a0d15278643da6981afe166107cdc6aefa5433485395.
Exact mathematical boundary: Every slice, row table, column table and signed sum is an actual beta-coded witness. Entries are F((o+s*i)+t*j), for i<m and j<n. Zero dimensions and zero strides are allowed; separately certified endpoints are unused. Table uniqueness concerns values, not codes. No infinite-sum assertion is made.