FS005L · theorem body

four_square_signed_common_zero_cancel

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

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

historical independently replay-verified empty-context experiment; the experiment itself persisted no certificate and granted no release authority; current checked use follows separately sealed proof bundles; no Stable promotion.

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.

Statement with defined notation

∀ k. ∀ a. ∀ b. ∀ c. ModEq(k,a + c,0) → ModEq(k,b + c,0) → ModEq(k,a,b)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0008 ModEq

In local proof propositions

PD0008 ModEq
Exact expanded first-order 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)

Proof neighborhood

Direct theorem prerequisites

mod_eq_symm · Stable closed mod_eq_trans · Stable closed mod_eq_add_cancel_right · Alpha closed

Direct theorem dependents

FS005N four_square_signed_cross_negative FS005S four_square_signed_zero_cancel_right FS005X four_square_signed_partition_balance

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : ModEq(k,0,b + c)Definitions: ModEq(k,0,b + c)Original native command in the exact edition
  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 : ModEq(k,a + c,b + c)Definitions: ModEq(k,a + c,b + c)Original native command in the exact edition
  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 defined 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 : ModEq(k,0,b + c)
    Exact native replay linehave 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 : ModEq(k,a + c,b + c)
    Exact native replay linehave 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