Actual packed tables · witnessed reindexing · permutation invariance · Constructive arithmetic

Signed arithmetic tables and finite sums

PermutationPrefix(r,s,l) ∧ ArithReindex(F,G,r,s,l) ∧ SignedPrefixSum(F,l,u) ∧ SignedPrefixSum(G,l,v) ⇒ u=v

Construct finite signed tables, form their actual prefix sums, and prove that a witnessed permutation preserves the signed sum.

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 1410 native tactic lines and 73 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem SS001E and follow only the lemmas and conservative definitions supporting divisor_signed_sum_permutation_invariant.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G007 milestone → theorem and definition dependencies.
Major independently established statements: SS001B divisor_signed_table_reindex_exists · SS001E divisor_signed_sum_permutation_invariant.
Independently verified Alpha v34 checked-use theorem family: 30 dependency-curried kernel-checked theorem bodies · 73 proof prerequisites · 16 linked definitions · 27 definition-dependency arrows · 1410 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 214 bundle nodes; SHA-256 35bc01ab3f12cc09a5ed9aa3098225090dcc40ac241f9cbd669f99cef4737e57.
Exact mathematical boundary: These are actual signed-table and finite-sum foundations. Equality compares represented signed values, not arbitrary encodings. MatrixMinorFourCode is reused solely as generic nested pairing, without a matrix hypothesis. Full finite signed G007 is established separately in the Möbius-inversion family.