HL0025

hensel_prime_blended_nonzero_derivative_is_unit

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

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.

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

Constructive proof overview

Generated structural guide

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.

The unchanged tactic script uses 10 declared prerequisites and contains 77 exact native proof lines.

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

Proof neighborhood

Direct dependencies

HL0019 hensel_signed_blend_zero_iff prime_not_divides_coprime Stable theorem; checked-use authorized coprime_symm Stable theorem; checked-use authorized multiple_implies_balanced_zero_congruence Alpha theorem; checked-use authorized coprime_bounded_mod_inverse Stable theorem; checked-use authorized prime_nonzero Stable theorem; checked-use authorized HL0018 hensel_signed_blend_mod_iff mul_one Stable theorem; checked-use authorized add_mul Stable theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized

Direct dependents

HL0026 hensel_prime_signed_nonzero_derivative_is_unit

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

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.

Named ingredients (2)
hensel signed blend zero iffhensel signed blend mod iff

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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
  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
    have hcop : forall hmi_divisor_hpl_hsc_blended_coprime. (exists hmi_left_factor_hpl_hsc_blended_coprime. D = hmi_divisor_hpl_hsc_blended_coprime * hmi_left_factor_hpl_hsc_blended_coprime) -> (exists hmi_right_factor_hpl_hsc_blended_coprime. p = hmi_divisor_hpl_hsc_blended_coprime * hmi_right_factor_hpl_hsc_blended_coprime) -> hmi_divisor_hpl_hsc_blended_coprime = 1
  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 : exists u. ((exists hpl_gap_hsc_bound. hpl_gap_hsc_bound + S (u) = (p)) /\ (exists hgcrt_mod_left_hpl_hsc_natural_inverse hgcrt_mod_right_hpl_hsc_natural_inverse. (D * u) + p * hgcrt_mod_left_hpl_hsc_natural_inverse = 1 + p * hgcrt_mod_right_hpl_hsc_natural_inverse))
  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
  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 exact 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 : (((exists hgcrt_mod_left_hpl_hsc_zero_forward hgcrt_mod_right_hpl_hsc_zero_forward. D + p * hgcrt_mod_left_hpl_hsc_zero_forward = 0 + p * hgcrt_mod_right_hpl_hsc_zero_forward) -> (exists hgcrt_mod_left_hpl_hsc_zero_signed hgcrt_mod_right_hpl_hsc_zero_signed. dp + p * hgcrt_mod_left_hpl_hsc_zero_signed = dn + p * hgcrt_mod_right_hpl_hsc_zero_signed)) /\ ((exists hgcrt_mod_left_hpl_hsc_zero_reverse hgcrt_mod_right_hpl_hsc_zero_reverse. dp + p * hgcrt_mod_left_hpl_hsc_zero_reverse = dn + p * hgcrt_mod_right_hpl_hsc_zero_reverse) -> (exists hgcrt_mod_left_hpl_hsc_zero_blended hgcrt_mod_right_hpl_hsc_zero_blended. D + p * hgcrt_mod_left_hpl_hsc_zero_blended = 0 + p * hgcrt_mod_right_hpl_hsc_zero_blended)))
  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 : forall hmi_divisor_hpl_hsc_blended_coprime. (exists hmi_left_factor_hpl_hsc_blended_coprime. D = hmi_divisor_hpl_hsc_blended_coprime * hmi_left_factor_hpl_hsc_blended_coprime) -> (exists hmi_right_factor_hpl_hsc_blended_coprime. p = hmi_divisor_hpl_hsc_blended_coprime * hmi_right_factor_hpl_hsc_blended_coprime) -> hmi_divisor_hpl_hsc_blended_coprime = 1
  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 : exists u. ((exists hpl_gap_hsc_bound. hpl_gap_hsc_bound + S (u) = (p)) /\ (exists hgcrt_mod_left_hpl_hsc_natural_inverse hgcrt_mod_right_hpl_hsc_natural_inverse. (D * u) + p * hgcrt_mod_left_hpl_hsc_natural_inverse = 1 + p * hgcrt_mod_right_hpl_hsc_natural_inverse))
  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 : (((exists hgcrt_mod_left_hpl_hsc_inverse_forward hgcrt_mod_right_hpl_hsc_inverse_forward. (D * x) + p * hgcrt_mod_left_hpl_hsc_inverse_forward = 1 + p * hgcrt_mod_right_hpl_hsc_inverse_forward) -> (exists hgcrt_mod_left_hpl_hsc_inverse_signed hgcrt_mod_right_hpl_hsc_inverse_signed. (dp * x) + p * hgcrt_mod_left_hpl_hsc_inverse_signed = (1 + dn * x) + p * hgcrt_mod_right_hpl_hsc_inverse_signed)) /\ ((exists hgcrt_mod_left_hpl_hsc_inverse_reverse hgcrt_mod_right_hpl_hsc_inverse_reverse. (dp * x) + p * hgcrt_mod_left_hpl_hsc_inverse_reverse = (1 + dn * x) + p * hgcrt_mod_right_hpl_hsc_inverse_reverse) -> (exists hgcrt_mod_left_hpl_hsc_inverse_blended hgcrt_mod_right_hpl_hsc_inverse_blended. (D * x) + p * hgcrt_mod_left_hpl_hsc_inverse_blended = 1 + p * hgcrt_mod_right_hpl_hsc_inverse_blended)))
  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