HL001A

hensel_signed_blend_unit_coprime

An actual inverse of the integer derivative proves the recoded natural derivative coprime to the lifting base.

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. ∀ M. ∀ h. ∀ dp. ∀ dn. ∀ dg. M = S h → Dvd(p,M) → dg = dp + h · dn → SignedDerivativeUnit(p,dp,dn) → Coprime(dg,p)

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

Definition DAG

SignedDerivativeUnit(p,dp,dn) · 1Dvd(d,n) · 1Coprime(a,b) · 1ModEq(m,a,b) · 4

Actual proof prerequisites

hensel_signed_blend_mod_iffmod_inverse_implies_coprime · checked external prerequisiteadd_mul · checked external prerequisitemul_assoc · checked external prerequisite
Original expanded first-order statement 
forall p M h dp dn dg. M = S h -> (exists q. M = p * q) -> dg = dp + h * dn -> (exists sph_inverse_unit. ((exists hpl_gap_unit. hpl_gap_unit + S (sph_inverse_unit) = (p)) /\ (exists hgcrt_mod_left_hpl_unit hgcrt_mod_right_hpl_unit. (dp * sph_inverse_unit) + p * hgcrt_mod_left_hpl_unit = (1 + dn * sph_inverse_unit) + p * hgcrt_mod_right_hpl_unit))) -> (forall hmi_divisor_hpl_coprime. (exists hmi_left_factor_hpl_coprime. dg = 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 38 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

38 script commands · 7 reading checkpoints · 2 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 (1)
hensel signed blend mod iff
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro M
  3. L3
    intro h
  4. L4
    intro dp
  5. L5
    intro dn
  6. L6
    intro dg
  7. L7
    intro hM
  8. L8
    intro hdiv
  9. L9
    intro hdg
  10. L10
    intro hunit
02Separate the logical casesL11–12

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

  1. L11
    cases hunit
  2. L12
    cases hunit_witness
03Establish hproductL13–19

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

  1. L13
    have hproduct : dg * x = dp * x + h * (dn * x)
  2. L14
    rewrite hdg
  3. L15
    trans dp * x + (h * dn) * x
  4. L16
    apply add_mul
  5. L17
    congr
  6. L18
    refl
  7. L19
    apply mul_assoc
04Establish hiffL20–29

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

  1. L20
    have hiff : (ModEq(p,dg · x,1) → ModEq(p,dp · x,1 + dn · x)) ∧ (ModEq(p,dp · x,1 + dn · x) → ModEq(p,dg · x,1))Definitions: ModEq(p,dg · x,1)ModEq(p,dp · x,1 + dn · x)Original native command in the exact edition
  2. L21
    specialize hensel_signed_blend_mod_iff p
  3. L22
    specialize hensel_signed_blend_mod_iff M
  4. L23
    specialize hensel_signed_blend_mod_iff h
  5. L24
    specialize hensel_signed_blend_mod_iff (dp * x)
  6. L25
    specialize hensel_signed_blend_mod_iff (dn * x)
  7. L26
    specialize hensel_signed_blend_mod_iff (dg * x)
  8. L27
    specialize hensel_signed_blend_mod_iff 1
  9. L28
    apply hensel_signed_blend_mod_iff
  10. L29
    exact hM
05Use earlier factsL30–31

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

  1. L30
    exact hdiv
  2. L31
    exact hproduct
06Separate the logical casesL32–32

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

  1. L32
    cases hiff
07Use earlier factsL33–38

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

  1. L33
    specialize mod_inverse_implies_coprime dg
  2. L34
    specialize mod_inverse_implies_coprime p
  3. L35
    specialize mod_inverse_implies_coprime x
  4. L36
    apply mod_inverse_implies_coprime
  5. L37
    apply hiff_right
  6. L38
    exact hunit_witness_right

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro p
  2. 0002intro M
  3. 0003intro h
  4. 0004intro dp
  5. 0005intro dn
  6. 0006intro dg
  7. 0007intro hM
  8. 0008intro hdiv
  9. 0009intro hdg
  10. 0010intro hunit
  11. 0011cases hunit
  12. 0012cases hunit_witness
  13. 0013have hproduct : dg * x = dp * x + h * (dn * x)
  14. 0014rewrite hdg
  15. 0015trans dp * x + (h * dn) * x
  16. 0016apply add_mul
  17. 0017congr
  18. 0018refl
  19. 0019apply mul_assoc
  20. 0020have hiff : (ModEq(p,dg · x,1) → ModEq(p,dp · x,1 + dn · x)) ∧ (ModEq(p,dp · x,1 + dn · x) → ModEq(p,dg · x,1))
  21. 0021specialize hensel_signed_blend_mod_iff p
  22. 0022specialize hensel_signed_blend_mod_iff M
  23. 0023specialize hensel_signed_blend_mod_iff h
  24. 0024specialize hensel_signed_blend_mod_iff (dp * x)
  25. 0025specialize hensel_signed_blend_mod_iff (dn * x)
  26. 0026specialize hensel_signed_blend_mod_iff (dg * x)
  27. 0027specialize hensel_signed_blend_mod_iff 1
  28. 0028apply hensel_signed_blend_mod_iff
  29. 0029exact hM
  30. 0030exact hdiv
  31. 0031exact hproduct
  32. 0032cases hiff
  33. 0033specialize mod_inverse_implies_coprime dg
  34. 0034specialize mod_inverse_implies_coprime p
  35. 0035specialize mod_inverse_implies_coprime x
  36. 0036apply mod_inverse_implies_coprime
  37. 0037apply hiff_right
  38. 0038exact hunit_witness_right