Half-open zero windows · constructed folds · exact padding · Constructive arithmetic

Actual signed finite support

Le(k,l) ∧ SignedZeroWindow(F,k,l) ∧ SignedPrefixSum(F,k,a) ∧ SignedPrefixSum(F,l,b) ⇒ a=b

Prove that a genuine zero tail does not alter an actual finite 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 312 native tactic lines and 25 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem ZS0008 and follow only the lemmas and conservative definitions supporting signed_prefix_sum_zero_padding_iff.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G007 milestone → theorem and definition dependencies.
Major independently established statements: ZS0004 signed_prefix_sum_zero_tail · ZS0007 signed_prefix_sum_last_value · ZS0008 signed_prefix_sum_zero_padding_iff.
Independently verified Alpha v34 checked-use theorem family: 8 dependency-curried kernel-checked theorem bodies · 25 proof prerequisites · 12 linked definitions · 17 definition-dependency arrows · 312 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 170 bundle nodes; SHA-256 99d889c64fb066f79247afa4310e0143f42bfffbc2cf56e4bd9be3735e0cac47.
Exact mathematical boundary: The zero window is half-open and its order hypothesis is essential. All folds retain actual beta-coded traces. These are support lemmas for the separately verified full inversion endpoint.