HL0025

hensel_prime_blended_nonzero_derivative_is_unit

A derivative nonzero modulo a genuine prime yields a bounded signed inverse through the actual natural blend dp+(p-1)*dn, with coprimality and both residue transports proved explicitly.

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. ∀ h. ∀ dp. ∀ dn. ∀ D. p = S h → D = dp + h · dn → Prime(p) → SignedDerivativeNonzero(p,dp,dn) → SignedDerivativeUnit(p,dp,dn)

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

Definition DAG

SignedDerivativeUnit(p,dp,dn) · 1SignedDerivativeNonzero(p,dp,dn) · 1Lt(a,b) · 1Prime(p) · 1Coprime(a,b) · 1ModEq(m,a,b) · 9

Actual proof prerequisites

hensel_signed_blend_zero_iffprime_not_divides_coprime · checked external prerequisitecoprime_symm · checked external prerequisitemultiple_implies_balanced_zero_congruence · checked external prerequisitecoprime_bounded_mod_inverse · checked external prerequisiteprime_nonzero · checked external prerequisitehensel_signed_blend_mod_iffmul_one · checked external prerequisiteadd_mul · checked external prerequisitemul_assoc · checked external prerequisite
Original expanded first-order statement 
forall p h dp dn D. p = S h -> D = dp + h * dn -> ((~(p = 1) /\ forall frm_prime_left_hsc_blended_prime frm_prime_right_hsc_blended_prime. p = frm_prime_left_hsc_blended_prime * frm_prime_right_hsc_blended_prime -> frm_prime_left_hsc_blended_prime = 1 \/ frm_prime_right_hsc_blended_prime = 1)) -> (~(exists hgcrt_mod_left_hpl_hsc_blended_nonzero hgcrt_mod_right_hpl_hsc_blended_nonzero. dp + p * hgcrt_mod_left_hpl_hsc_blended_nonzero = dn + p * hgcrt_mod_right_hpl_hsc_blended_nonzero)) -> (exists sph_inverse_hsc_blended_unit. ((exists hpl_gap_hsc_blended_unit. hpl_gap_hsc_blended_unit + S (sph_inverse_hsc_blended_unit) = (p)) /\ (exists hgcrt_mod_left_hpl_hsc_blended_unit hgcrt_mod_right_hpl_hsc_blended_unit. (dp * sph_inverse_hsc_blended_unit) + p * hgcrt_mod_left_hpl_hsc_blended_unit = (1 + dn * sph_inverse_hsc_blended_unit) + p * hgcrt_mod_right_hpl_hsc_blended_unit)))

Complete tactic proof in conservative notation

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

77 script commands · 19 reading checkpoints · 5 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.

Named ingredients (2)
hensel signed blend zero iffhensel signed blend mod iff
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro dp
  4. L4
    intro dn
  5. L5
    intro D
  6. L6
    intro hsucc
  7. L7
    intro hD
  8. L8
    intro hp
  9. L9
    intro hnonzero
02Establish hiffL10–18

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

  1. L10
    have hiff : (ModEq(p,D,0) → ModEq(p,dp,dn)) ∧ (ModEq(p,dp,dn) → ModEq(p,D,0))Definitions: ModEq(p,D,0)ModEq(p,dp,dn)Original native command in the exact edition
  2. L11
    specialize hensel_signed_blend_zero_iff (p)
  3. L12
    specialize hensel_signed_blend_zero_iff (p)
  4. L13
    specialize hensel_signed_blend_zero_iff (h)
  5. L14
    specialize hensel_signed_blend_zero_iff (dp)
  6. L15
    specialize hensel_signed_blend_zero_iff (dn)
  7. L16
    specialize hensel_signed_blend_zero_iff (D)
  8. L17
    apply hensel_signed_blend_zero_iff
  9. L18
    exact hsucc
03Construct an explicit witnessL19–19

Supply the displayed value, then prove that it has the required property.

  1. L19
    exists 1
04Calculate and transport equalitiesL20–20

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

  1. L20
    symm
05Use earlier factsL21–22

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

  1. L21
    apply mul_one
  2. L22
    exact hD
06Separate the logical casesL23–23

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

  1. L23
    cases hiff
07Establish hcopL24–33

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

  1. L24
  2. L25
    specialize coprime_symm (p)
  3. L26
    specialize coprime_symm (D)
  4. L27
    apply coprime_symm
  5. L28
    specialize prime_not_divides_coprime (p)
  6. L29
    specialize prime_not_divides_coprime (D)
  7. L30
    apply prime_not_divides_coprime
  8. L31
    exact hp
  9. L32
    intro hdiv
  10. L33
    apply hnonzero
08Use earlier factsL34–38

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

  1. L34
    apply hiff_left
  2. L35
    specialize multiple_implies_balanced_zero_congruence (p)
  3. L36
    specialize multiple_implies_balanced_zero_congruence (D)
  4. L37
    apply multiple_implies_balanced_zero_congruence
  5. L38
    exact hdiv
09Establish hinverseL39–48

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

  1. L39
    have hinverse : ∃ 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. L40
    specialize coprime_bounded_mod_inverse (D)
  3. L41
    specialize coprime_bounded_mod_inverse (p)
  4. L42
    apply coprime_bounded_mod_inverse
  5. L43
    intro hz
  6. L44
    specialize prime_nonzero (p)
  7. L45
    apply prime_nonzero
  8. L46
    exact hp
  9. L47
    exact hz
  10. L48
    exact hcop
10Separate the logical casesL49–50

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

  1. L49
    cases hinverse
  2. L50
    cases hinverse_witness
11Establish hproductL51–57

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

  1. L51
    have hproduct : D * x = dp * x + h * (dn * x)
  2. L52
    rewrite hD
  3. L53
    trans dp * x + (h * dn) * x
  4. L54
    apply add_mul
  5. L55
    congr
  6. L56
    refl
  7. L57
    apply mul_assoc
12Establish htransportL58–67

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

  1. L58
    have htransport : (ModEq(p,D · x,1) → ModEq(p,dp · x,1 + dn · x)) ∧ (ModEq(p,dp · x,1 + dn · x) → ModEq(p,D · x,1))Definitions: ModEq(p,D · x,1)ModEq(p,dp · x,1 + dn · x)Original native command in the exact edition
  2. L59
    specialize hensel_signed_blend_mod_iff (p)
  3. L60
    specialize hensel_signed_blend_mod_iff (p)
  4. L61
    specialize hensel_signed_blend_mod_iff (h)
  5. L62
    specialize hensel_signed_blend_mod_iff (dp * x)
  6. L63
    specialize hensel_signed_blend_mod_iff (dn * x)
  7. L64
    specialize hensel_signed_blend_mod_iff (D * x)
  8. L65
    specialize hensel_signed_blend_mod_iff (1)
  9. L66
    apply hensel_signed_blend_mod_iff
  10. L67
    exact hsucc
13Construct an explicit witnessL68–68

Supply the displayed value, then prove that it has the required property.

  1. L68
    exists 1
14Calculate and transport equalitiesL69–69

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

  1. L69
    symm
15Use earlier factsL70–71

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

  1. L70
    apply mul_one
  2. L71
    exact hproduct
16Separate the logical casesL72–72

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

  1. L72
    cases htransport
17Construct an explicit witnessL73–73

Supply the displayed value, then prove that it has the required property.

  1. L73
    exists x
18Separate the logical casesL74–74

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

  1. L74
    split
19Use earlier factsL75–77

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

  1. L75
    exact hinverse_witness_left
  2. L76
    apply htransport_left
  3. L77
    exact hinverse_witness_right

Library-wide reading audit

Original defined command ledger · 77 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro dp
  4. 0004intro dn
  5. 0005intro D
  6. 0006intro hsucc
  7. 0007intro hD
  8. 0008intro hp
  9. 0009intro hnonzero
  10. 0010have hiff : (ModEq(p,D,0) → ModEq(p,dp,dn)) ∧ (ModEq(p,dp,dn) → ModEq(p,D,0))
  11. 0011specialize hensel_signed_blend_zero_iff (p)
  12. 0012specialize hensel_signed_blend_zero_iff (p)
  13. 0013specialize hensel_signed_blend_zero_iff (h)
  14. 0014specialize hensel_signed_blend_zero_iff (dp)
  15. 0015specialize hensel_signed_blend_zero_iff (dn)
  16. 0016specialize hensel_signed_blend_zero_iff (D)
  17. 0017apply hensel_signed_blend_zero_iff
  18. 0018exact hsucc
  19. 0019exists 1
  20. 0020symm
  21. 0021apply mul_one
  22. 0022exact hD
  23. 0023cases hiff
  24. 0024have hcop : Coprime(D,p)
  25. 0025specialize coprime_symm (p)
  26. 0026specialize coprime_symm (D)
  27. 0027apply coprime_symm
  28. 0028specialize prime_not_divides_coprime (p)
  29. 0029specialize prime_not_divides_coprime (D)
  30. 0030apply prime_not_divides_coprime
  31. 0031exact hp
  32. 0032intro hdiv
  33. 0033apply hnonzero
  34. 0034apply hiff_left
  35. 0035specialize multiple_implies_balanced_zero_congruence (p)
  36. 0036specialize multiple_implies_balanced_zero_congruence (D)
  37. 0037apply multiple_implies_balanced_zero_congruence
  38. 0038exact hdiv
  39. 0039have hinverse : ∃ u. Lt(u,p) ∧ ModEq(p,D · u,1)
  40. 0040specialize coprime_bounded_mod_inverse (D)
  41. 0041specialize coprime_bounded_mod_inverse (p)
  42. 0042apply coprime_bounded_mod_inverse
  43. 0043intro hz
  44. 0044specialize prime_nonzero (p)
  45. 0045apply prime_nonzero
  46. 0046exact hp
  47. 0047exact hz
  48. 0048exact hcop
  49. 0049cases hinverse
  50. 0050cases hinverse_witness
  51. 0051have hproduct : D * x = dp * x + h * (dn * x)
  52. 0052rewrite hD
  53. 0053trans dp * x + (h * dn) * x
  54. 0054apply add_mul
  55. 0055congr
  56. 0056refl
  57. 0057apply mul_assoc
  58. 0058have htransport : (ModEq(p,D · x,1) → ModEq(p,dp · x,1 + dn · x)) ∧ (ModEq(p,dp · x,1 + dn · x) → ModEq(p,D · x,1))
  59. 0059specialize hensel_signed_blend_mod_iff (p)
  60. 0060specialize hensel_signed_blend_mod_iff (p)
  61. 0061specialize hensel_signed_blend_mod_iff (h)
  62. 0062specialize hensel_signed_blend_mod_iff (dp * x)
  63. 0063specialize hensel_signed_blend_mod_iff (dn * x)
  64. 0064specialize hensel_signed_blend_mod_iff (D * x)
  65. 0065specialize hensel_signed_blend_mod_iff (1)
  66. 0066apply hensel_signed_blend_mod_iff
  67. 0067exact hsucc
  68. 0068exists 1
  69. 0069symm
  70. 0070apply mul_one
  71. 0071exact hproduct
  72. 0072cases htransport
  73. 0073exists x
  74. 0074split
  75. 0075exact hinverse_witness_left
  76. 0076apply htransport_left
  77. 0077exact hinverse_witness_right