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

Signed arithmetic tables and finite sums

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.

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

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: research checkpoint map → 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.
Public research checkpoint, independently verified: 30 theorems in a complete dependency-closed HA bundle · 73 proof prerequisites · 16 linked definitions · 27 definition-dependency arrows · 1410 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 214 bundle nodes; SHA-256 35bc01ab3f12cc09a5ed9aa3098225090dcc40ac241f9cbd669f99cef4737e57. Inspect the checkpoint receipt, literal bundle, and source files →
Exact mathematical boundary: These are genuine signed-table and finite-sum foundations, not full divisor-sum cancellation or Möbius inversion. G007 remains open. The historical MatrixMinorFourCode definition is reused solely as generic nested pairing of four beta parameters; no matrix-specific hypothesis is imported. Equality is equality of represented signed values, not equality of arbitrary component codes.