FS005L

four_square_signed_common_zero_cancel

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Two modular zero balances with the same added natural term yield congruent remaining terms.

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 original first-admission records.

Exact expanded first-order arithmetic statement

forall k a b c. (exists ftcn_left_fssq_common_first ftcn_right_fssq_common_first. (a + c) + (k) * ftcn_left_fssq_common_first = (0) + (k) * ftcn_right_fssq_common_first) -> (exists ftcn_left_fssq_common_second ftcn_right_fssq_common_second. (b + c) + (k) * ftcn_left_fssq_common_second = (0) + (k) * ftcn_right_fssq_common_second) -> (exists ftcn_left_fssq_common_result ftcn_right_fssq_common_result. (a) + (k) * ftcn_left_fssq_common_result = (b) + (k) * ftcn_right_fssq_common_result)

Constructive proof overview

Generated structural guide

Two modular zero balances with the same added natural term yield congruent remaining terms.

The unchanged tactic script uses 3 declared prerequisites and contains 26 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Historical empty-context replay experiment only; that experiment persisted no certificate and granted no release authority. Current checked use follows separately sealed, independently verified proof bundles; there is no Stable promotion.

Proof neighborhood

Direct dependencies

mod_eq_symm Stable theorem; checked-use authorized mod_eq_trans Stable theorem; checked-use authorized mod_eq_add_cancel_right Alpha theorem; checked-use authorized

Direct dependents

FS005N four_square_signed_cross_negative FS005S four_square_signed_zero_cancel_right FS005X four_square_signed_partition_balance

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

26 script commands · 4 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

01Fix variables and assumptionsL1–6

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro k
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro hfirst
  6. L6
    intro hsecond
02Establish hreverseL7–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L7
    have hreverse : exists ftcn_left_fssq_common_reverse ftcn_right_fssq_common_reverse. (0) + (k) * ftcn_left_fssq_common_reverse = (b + c) + (k) * ftcn_right_fssq_common_reverse
  2. L8
    specialize mod_eq_symm k
  3. L9
    specialize mod_eq_symm (b + c)
  4. L10
    specialize mod_eq_symm 0
  5. L11
    apply mod_eq_symm
  6. L12
    exact hsecond
03Establish hequalL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq trans.

  1. L13
    have hequal : exists ftcn_left_fssq_common_equal ftcn_right_fssq_common_equal. (a + c) + (k) * ftcn_left_fssq_common_equal = (b + c) + (k) * ftcn_right_fssq_common_equal
  2. L14
    specialize mod_eq_trans k
  3. L15
    specialize mod_eq_trans (a + c)
  4. L16
    specialize mod_eq_trans 0
  5. L17
    specialize mod_eq_trans (b + c)
  6. L18
    apply mod_eq_trans
  7. L19
    exact hfirst
  8. L20
    exact hreverse
  9. L21
    specialize mod_eq_add_cancel_right k
  10. L22
    specialize mod_eq_add_cancel_right a
04Use earlier factsL23–26

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L23
    specialize mod_eq_add_cancel_right b
  2. L24
    specialize mod_eq_add_cancel_right c
  3. L25
    apply mod_eq_add_cancel_right
  4. L26
    exact hequal

Library-wide reading audit

Original exact command ledger · 26 lines
  1. 0001intro k
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro hfirst
  6. 0006intro hsecond
  7. 0007have hreverse : exists ftcn_left_fssq_common_reverse ftcn_right_fssq_common_reverse. (0) + (k) * ftcn_left_fssq_common_reverse = (b + c) + (k) * ftcn_right_fssq_common_reverse
  8. 0008specialize mod_eq_symm k
  9. 0009specialize mod_eq_symm (b + c)
  10. 0010specialize mod_eq_symm 0
  11. 0011apply mod_eq_symm
  12. 0012exact hsecond
  13. 0013have hequal : exists ftcn_left_fssq_common_equal ftcn_right_fssq_common_equal. (a + c) + (k) * ftcn_left_fssq_common_equal = (b + c) + (k) * ftcn_right_fssq_common_equal
  14. 0014specialize mod_eq_trans k
  15. 0015specialize mod_eq_trans (a + c)
  16. 0016specialize mod_eq_trans 0
  17. 0017specialize mod_eq_trans (b + c)
  18. 0018apply mod_eq_trans
  19. 0019exact hfirst
  20. 0020exact hreverse
  21. 0021specialize mod_eq_add_cancel_right k
  22. 0022specialize mod_eq_add_cancel_right a
  23. 0023specialize mod_eq_add_cancel_right b
  24. 0024specialize mod_eq_add_cancel_right c
  25. 0025apply mod_eq_add_cancel_right
  26. 0026exact hequal