HL0002

hensel_coprime_mod_transport

A derivative remains coprime to a nonzero modulus after any genuine congruence transport.

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

∀ p. ∀ d. ∀ e. ¬p = 0 → Coprime(d,p) → ModEq(p,d,e) → Coprime(e,p)

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

Definition DAG

Lt(a,b) · 1Coprime(a,b) · 2ModEq(m,a,b) · 2

Actual proof prerequisites

coprime_bounded_mod_inverse · checked external prerequisitemod_eq_mul_right · checked external prerequisitemod_eq_trans · checked external prerequisitemod_eq_symm · checked external prerequisitemod_inverse_implies_coprime · checked external prerequisite
Original expanded first-order statement 
forall p d e. ~(p = 0) -> (forall hmi_divisor_hpl_coprime. (exists hmi_left_factor_hpl_coprime. d = hmi_divisor_hpl_coprime * hmi_left_factor_hpl_coprime) -> (exists hmi_right_factor_hpl_coprime. p = hmi_divisor_hpl_coprime * hmi_right_factor_hpl_coprime) -> hmi_divisor_hpl_coprime = 1) -> (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. d + p * hgcrt_mod_left_hpl_mod = e + p * hgcrt_mod_right_hpl_mod) -> (forall hmi_divisor_hpl_coprime. (exists hmi_left_factor_hpl_coprime. e = hmi_divisor_hpl_coprime * hmi_left_factor_hpl_coprime) -> (exists hmi_right_factor_hpl_coprime. p = hmi_divisor_hpl_coprime * hmi_right_factor_hpl_coprime) -> hmi_divisor_hpl_coprime = 1)

Complete tactic proof in conservative notation

All 34 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

34 script commands · 5 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–6

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

  1. L1
    intro p
  2. L2
    intro d
  3. L3
    intro e
  4. L4
    intro hp
  5. L5
    intro hcop
  6. L6
    intro hmod
02Establish hinvL7–12

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

  1. L7
    have hinv : ∃ u. Lt(u,p) ∧ ModEq(p,d · u,1)Definitions: Lt(u,p)ModEq(p,d · u,1)Original native command in the exact edition
  2. L8
    specialize coprime_bounded_mod_inverse d
  3. L9
    specialize coprime_bounded_mod_inverse p
  4. L10
    apply coprime_bounded_mod_inverse
  5. L11
    exact hp
  6. L12
    exact hcop
03Separate the logical casesL13–14

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

  1. L13
    cases hinv
  2. L14
    cases hinv_witness
04Use earlier factsL15–24

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

  1. L15
    specialize mod_inverse_implies_coprime e
  2. L16
    specialize mod_inverse_implies_coprime p
  3. L17
    specialize mod_inverse_implies_coprime x
  4. L18
    apply mod_inverse_implies_coprime
  5. L19
    specialize mod_eq_trans p
  6. L20
    specialize mod_eq_trans (e * x)
  7. L21
    specialize mod_eq_trans (d * x)
  8. L22
    specialize mod_eq_trans 1
  9. L23
    apply mod_eq_trans
  10. L24
    specialize mod_eq_mul_right p
05Use earlier factsL25–34

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

  1. L25
    specialize mod_eq_mul_right e
  2. L26
    specialize mod_eq_mul_right d
  3. L27
    specialize mod_eq_mul_right x
  4. L28
    apply mod_eq_mul_right
  5. L29
    specialize mod_eq_symm p
  6. L30
    specialize mod_eq_symm d
  7. L31
    specialize mod_eq_symm e
  8. L32
    apply mod_eq_symm
  9. L33
    exact hmod
  10. L34
    exact hinv_witness_right

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro p
  2. 0002intro d
  3. 0003intro e
  4. 0004intro hp
  5. 0005intro hcop
  6. 0006intro hmod
  7. 0007have hinv : ∃ u. Lt(u,p) ∧ ModEq(p,d · u,1)
  8. 0008specialize coprime_bounded_mod_inverse d
  9. 0009specialize coprime_bounded_mod_inverse p
  10. 0010apply coprime_bounded_mod_inverse
  11. 0011exact hp
  12. 0012exact hcop
  13. 0013cases hinv
  14. 0014cases hinv_witness
  15. 0015specialize mod_inverse_implies_coprime e
  16. 0016specialize mod_inverse_implies_coprime p
  17. 0017specialize mod_inverse_implies_coprime x
  18. 0018apply mod_inverse_implies_coprime
  19. 0019specialize mod_eq_trans p
  20. 0020specialize mod_eq_trans (e * x)
  21. 0021specialize mod_eq_trans (d * x)
  22. 0022specialize mod_eq_trans 1
  23. 0023apply mod_eq_trans
  24. 0024specialize mod_eq_mul_right p
  25. 0025specialize mod_eq_mul_right e
  26. 0026specialize mod_eq_mul_right d
  27. 0027specialize mod_eq_mul_right x
  28. 0028apply mod_eq_mul_right
  29. 0029specialize mod_eq_symm p
  30. 0030specialize mod_eq_symm d
  31. 0031specialize mod_eq_symm e
  32. 0032apply mod_eq_symm
  33. 0033exact hmod
  34. 0034exact hinv_witness_right