HL001A

hensel_signed_blend_unit_coprime

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 38 exact native proof lines.

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

Proof neighborhood

Direct dependencies

HL0018 hensel_signed_blend_mod_iff mod_inverse_implies_coprime Stable theorem; checked-use authorized add_mul Stable theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized

Direct dependents

HL001F beta_signed_horner_hensel_iterated_exists_unique

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

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.

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 : (((exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. (dg * x) + p * hgcrt_mod_left_hpl_mod = 1 + p * hgcrt_mod_right_hpl_mod) -> (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. (dp * x) + p * hgcrt_mod_left_hpl_mod = (1 + dn * x) + p * hgcrt_mod_right_hpl_mod)) /\ ((exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. (dp * x) + p * hgcrt_mod_left_hpl_mod = (1 + dn * x) + p * hgcrt_mod_right_hpl_mod) -> (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. (dg * x) + p * hgcrt_mod_left_hpl_mod = 1 + p * hgcrt_mod_right_hpl_mod)))
  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 exact 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 : (((exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. (dg * x) + p * hgcrt_mod_left_hpl_mod = 1 + p * hgcrt_mod_right_hpl_mod) -> (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. (dp * x) + p * hgcrt_mod_left_hpl_mod = (1 + dn * x) + p * hgcrt_mod_right_hpl_mod)) /\ ((exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. (dp * x) + p * hgcrt_mod_left_hpl_mod = (1 + dn * x) + p * hgcrt_mod_right_hpl_mod) -> (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. (dg * x) + p * hgcrt_mod_left_hpl_mod = 1 + p * hgcrt_mod_right_hpl_mod)))
  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