HL0002

hensel_coprime_mod_transport

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

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

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 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)

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 declared prerequisites and contains 34 exact native proof lines.

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

Proof neighborhood

Direct dependencies

coprime_bounded_mod_inverse Stable theorem; checked-use authorized mod_eq_mul_right Stable theorem; checked-use authorized mod_eq_trans Stable theorem; checked-use authorized mod_eq_symm Stable theorem; checked-use authorized mod_inverse_implies_coprime Stable theorem; checked-use authorized

Direct dependents

HL0009 beta_horner_simple_canonical_representative HL000D beta_horner_simple_root_at_congruent_point

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

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.

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 : exists u. ((exists hpl_gap_bound. hpl_gap_bound + S (u) = (p)) /\ (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. (d * u) + p * hgcrt_mod_left_hpl_mod = 1 + p * hgcrt_mod_right_hpl_mod))
  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 exact 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 : exists u. ((exists hpl_gap_bound. hpl_gap_bound + S (u) = (p)) /\ (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. (d * u) + p * hgcrt_mod_left_hpl_mod = 1 + p * hgcrt_mod_right_hpl_mod))
  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