HL0001

hensel_mod_add_zero_cancel

A known zero-congruent summand can be cancelled without subtraction.

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

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.

The derivative-nonzero criterion supplies no inverse or power witness: both are constructed. Roots may be arbitrary natural representatives of signed integer polynomials. Singular-root classification and p-adic completion are separate milestones.

Exact theorem in conservative defined notation

∀ m. ∀ a. ∀ q. ModEq(m,a + q,0) → ModEq(m,q,0) → ModEq(m,a,0)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ModEq(m,a,b) · 3

Actual proof prerequisites

mod_eq_add_cancel_right · checked external prerequisitemod_eq_trans · checked external prerequisitemod_eq_symm · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall m a q. (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. (a + q) + m * hgcrt_mod_left_hpl_mod = 0 + m * hgcrt_mod_right_hpl_mod) -> (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. q + m * hgcrt_mod_left_hpl_mod = 0 + m * hgcrt_mod_right_hpl_mod) -> (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. a + m * hgcrt_mod_left_hpl_mod = 0 + m * hgcrt_mod_right_hpl_mod)

Complete tactic proof in conservative notation

All 24 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

24 script commands · 4 reading checkpoints · 1 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–5

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

  1. L1
    intro m
  2. L2
    intro a
  3. L3
    intro q
  4. L4
    intro hsum
  5. L5
    intro hq
02Use earlier factsL6–15

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

  1. L6
    specialize mod_eq_add_cancel_right m
  2. L7
    specialize mod_eq_add_cancel_right a
  3. L8
    specialize mod_eq_add_cancel_right 0
  4. L9
    specialize mod_eq_add_cancel_right q
  5. L10
    apply mod_eq_add_cancel_right
  6. L11
    specialize mod_eq_trans m
  7. L12
    specialize mod_eq_trans (a + q)
  8. L13
    specialize mod_eq_trans 0
  9. L14
    specialize mod_eq_trans (0 + q)
  10. L15
    apply mod_eq_trans
03Use earlier factsL16–16

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

  1. L16
    exact hsum
04Establish heqL17–24

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

  1. L17
    have heq : 0 + q = q
  2. L18
    apply zero_add
  3. L19
    rewrite heq
  4. L20
    specialize mod_eq_symm m
  5. L21
    specialize mod_eq_symm q
  6. L22
    specialize mod_eq_symm 0
  7. L23
    apply mod_eq_symm
  8. L24
    exact hq

Library-wide reading audit

Original defined command ledger · 24 lines
  1. 0001intro m
  2. 0002intro a
  3. 0003intro q
  4. 0004intro hsum
  5. 0005intro hq
  6. 0006specialize mod_eq_add_cancel_right m
  7. 0007specialize mod_eq_add_cancel_right a
  8. 0008specialize mod_eq_add_cancel_right 0
  9. 0009specialize mod_eq_add_cancel_right q
  10. 0010apply mod_eq_add_cancel_right
  11. 0011specialize mod_eq_trans m
  12. 0012specialize mod_eq_trans (a + q)
  13. 0013specialize mod_eq_trans 0
  14. 0014specialize mod_eq_trans (0 + q)
  15. 0015apply mod_eq_trans
  16. 0016exact hsum
  17. 0017have heq : 0 + q = q
  18. 0018apply zero_add
  19. 0019rewrite heq
  20. 0020specialize mod_eq_symm m
  21. 0021specialize mod_eq_symm q
  22. 0022specialize mod_eq_symm 0
  23. 0023apply mod_eq_symm
  24. 0024exact hq