CG0009

linear_congruence_zero_modulus_nonzero_coefficient_unique

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

At modulus zero a nonzero coefficient has at most one natural solution; no bounded residue or finite-class formula is asserted.

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 expanded first-order arithmetic statement

forall a b x y. (~(a=0)) -> (exists hgcrt_mod_left_lcc_zero_unique_x hgcrt_mod_right_lcc_zero_unique_x. (a * x) + 0 * hgcrt_mod_left_lcc_zero_unique_x = b + 0 * hgcrt_mod_right_lcc_zero_unique_x) -> (exists hgcrt_mod_left_lcc_zero_unique_y hgcrt_mod_right_lcc_zero_unique_y. (a * y) + 0 * hgcrt_mod_left_lcc_zero_unique_y = b + 0 * hgcrt_mod_right_lcc_zero_unique_y) -> (x=y)

Constructive proof overview

Generated structural guide

At modulus zero a nonzero coefficient has at most one natural solution; no bounded residue or finite-class formula is asserted.

The unchanged tactic script uses 2 declared prerequisites and contains 32 exact native proof lines.

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

Proof neighborhood

Direct dependencies

mod_eq_zero_iff_eq Alpha theorem; checked-use authorized mul_left_cancel_nonzero Alpha theorem; checked-use authorized

Direct dependents

none

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

32 script commands · 9 reading checkpoints · 4 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–7

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro ha
  6. L6
    intro hx
  7. L7
    intro hy
02Establish he_xL8–11

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

  1. L8
    have he_x : (((exists hgcrt_mod_left_lcc_zero_x hgcrt_mod_right_lcc_zero_x. (a * x) + 0 * hgcrt_mod_left_lcc_zero_x = b + 0 * hgcrt_mod_right_lcc_zero_x) -> (a*x=b)) /\ (((a*x=b) -> (exists hgcrt_mod_left_lcc_zero_x hgcrt_mod_right_lcc_zero_x. (a * x) + 0 * hgcrt_mod_left_lcc_zero_x = b + 0 * hgcrt_mod_right_lcc_zero_x))))
  2. L9
    specialize mod_eq_zero_iff_eq (a*x)
  3. L10
    specialize mod_eq_zero_iff_eq (b)
  4. L11
    apply mod_eq_zero_iff_eq
03Separate the logical casesL12–12

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L12
    cases he_x
04Establish hxeqL13–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply he x left.

  1. L13
    have hxeq : a*x=b
  2. L14
    apply he_x_left
  3. L15
    exact hx
05Establish he_yL16–19

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

  1. L16
    have he_y : (((exists hgcrt_mod_left_lcc_zero_y hgcrt_mod_right_lcc_zero_y. (a * y) + 0 * hgcrt_mod_left_lcc_zero_y = b + 0 * hgcrt_mod_right_lcc_zero_y) -> (a*y=b)) /\ (((a*y=b) -> (exists hgcrt_mod_left_lcc_zero_y hgcrt_mod_right_lcc_zero_y. (a * y) + 0 * hgcrt_mod_left_lcc_zero_y = b + 0 * hgcrt_mod_right_lcc_zero_y))))
  2. L17
    specialize mod_eq_zero_iff_eq (a*y)
  3. L18
    specialize mod_eq_zero_iff_eq (b)
  4. L19
    apply mod_eq_zero_iff_eq
06Separate the logical casesL20–20

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L20
    cases he_y
07Establish hyeqL21–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply he y left.

  1. L21
    have hyeq : a*y=b
  2. L22
    apply he_y_left
  3. L23
    exact hy
  4. L24
    specialize mul_left_cancel_nonzero (a)
  5. L25
    specialize mul_left_cancel_nonzero (x)
  6. L26
    specialize mul_left_cancel_nonzero (y)
  7. L27
    apply mul_left_cancel_nonzero
  8. L28
    exact ha
  9. L29
    trans b
  10. L30
    exact hxeq
08Calculate and transport equalitiesL31–31

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L31
    symm
09Use earlier factsL32–32

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

  1. L32
    exact hyeq

Library-wide reading audit

Original exact command ledger · 32 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro x
  4. 0004intro y
  5. 0005intro ha
  6. 0006intro hx
  7. 0007intro hy
  8. 0008have he_x : (((exists hgcrt_mod_left_lcc_zero_x hgcrt_mod_right_lcc_zero_x. (a * x) + 0 * hgcrt_mod_left_lcc_zero_x = b + 0 * hgcrt_mod_right_lcc_zero_x) -> (a*x=b)) /\ (((a*x=b) -> (exists hgcrt_mod_left_lcc_zero_x hgcrt_mod_right_lcc_zero_x. (a * x) + 0 * hgcrt_mod_left_lcc_zero_x = b + 0 * hgcrt_mod_right_lcc_zero_x))))
  9. 0009specialize mod_eq_zero_iff_eq (a*x)
  10. 0010specialize mod_eq_zero_iff_eq (b)
  11. 0011apply mod_eq_zero_iff_eq
  12. 0012cases he_x
  13. 0013have hxeq : a*x=b
  14. 0014apply he_x_left
  15. 0015exact hx
  16. 0016have he_y : (((exists hgcrt_mod_left_lcc_zero_y hgcrt_mod_right_lcc_zero_y. (a * y) + 0 * hgcrt_mod_left_lcc_zero_y = b + 0 * hgcrt_mod_right_lcc_zero_y) -> (a*y=b)) /\ (((a*y=b) -> (exists hgcrt_mod_left_lcc_zero_y hgcrt_mod_right_lcc_zero_y. (a * y) + 0 * hgcrt_mod_left_lcc_zero_y = b + 0 * hgcrt_mod_right_lcc_zero_y))))
  17. 0017specialize mod_eq_zero_iff_eq (a*y)
  18. 0018specialize mod_eq_zero_iff_eq (b)
  19. 0019apply mod_eq_zero_iff_eq
  20. 0020cases he_y
  21. 0021have hyeq : a*y=b
  22. 0022apply he_y_left
  23. 0023exact hy
  24. 0024specialize mul_left_cancel_nonzero (a)
  25. 0025specialize mul_left_cancel_nonzero (x)
  26. 0026specialize mul_left_cancel_nonzero (y)
  27. 0027apply mul_left_cancel_nonzero
  28. 0028exact ha
  29. 0029trans b
  30. 0030exact hxeq
  31. 0031symm
  32. 0032exact hyeq