TH0009

hensel_correction_exists

Every coprime derivative at a nonzero modulus has an actual strictly bounded subtraction-free root correction.

Alpha v34 checked-use · first admitted v25 · 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.

Historical partial components only: this chapter proves exact natural polynomial Taylor remainders, bounded corrections, and one-step divisibility lifts. G095 is now closed in the separate Alpha-v27 hensel-lifting branch for integer polynomials, unrestricted input roots, unique canonical representatives, and every positive prime power. Full G095 proof · Alpha v27

Exact theorem in conservative defined notation

∀ d. ∀ p. ∀ q. ¬p = 0 → Coprime(d,p) → ∃ x. HenselCorrection(d,p,q,x)

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

Definition DAG

HenselCorrection(d,p,q,t) · 1Coprime(a,b) · 1

Actual proof prerequisites

nonzero_is_succ · checked external prerequisitecoprime_to_is_gcd_one · checked external prerequisiteone_mul · checked external prerequisitelinear_congruence_nonzero_modulus_bounded_constructor · checked external prerequisitehensel_predecessor_annihilates_residuemod_eq_refl · checked external prerequisitemod_eq_add · checked external prerequisitemod_eq_trans · checked external prerequisite
Original expanded first-order statement 
forall d p q. ~(p = 0) -> (forall hmi_divisor_pth_correction. (exists hmi_left_factor_pth_correction. d = hmi_divisor_pth_correction * hmi_left_factor_pth_correction) -> (exists hmi_right_factor_pth_correction. p = hmi_divisor_pth_correction * hmi_right_factor_pth_correction) -> hmi_divisor_pth_correction = 1) -> exists t. (((exists ff_lt_pth_correction_exists_bound. ff_lt_pth_correction_exists_bound + S t = p) /\ (exists hgcrt_mod_left_pth_correction_exists_annihilation hgcrt_mod_right_pth_correction_exists_annihilation. (q + d * t) + p * hgcrt_mod_left_pth_correction_exists_annihilation = 0 + p * hgcrt_mod_right_pth_correction_exists_annihilation)))

Complete unchanged native tactic proof

All 61 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

61 script commands · 17 reading checkpoints · 8 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 predecessor annihilates residue
01Fix variables and assumptionsL1–5

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

  1. L1
    intro d
  2. L2
    intro p
  3. L3
    intro q
  4. L4
    intro hp
  5. L5
    intro hcop
02Establish hsuccessorL6–9

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

  1. L6
    have hsuccessor : exists k. p = S k
  2. L7
    specialize nonzero_is_succ p
  3. L8
    apply nonzero_is_succ
  4. L9
    exact hp
03Separate the logical casesL10–10

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

  1. L10
    cases hsuccessor
04Establish hgcdL11–15

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

  1. L11
    have hgcd : (((exists r. d = 1 * r) /\ (exists s. p = 1 * s)) /\ forall j. (exists u. d = j * u) -> (exists v. p = j * v) -> exists w. 1 = j * w)
  2. L12
    specialize coprime_to_is_gcd_one d
  3. L13
    specialize coprime_to_is_gcd_one p
  4. L14
    apply coprime_to_is_gcd_one
  5. L15
    exact hcop
05Establish hdivisorL16–16

Establish this local claim before using it. It is not an additional assumption.

  1. L16
    have hdivisor : exists w. x * q = 1 * w
06Construct an explicit witnessL17–17

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

  1. L17
    exists x * q
07Calculate and transport equalitiesL18–18

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

  1. L18
    symm
08Use earlier factsL19–19

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

  1. L19
    apply one_mul
09Establish hsolutionL20–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply linear congruence nonzero modulus bounded constructor.

  1. L20
    have hsolution : exists t. ((exists h. h + S t = p) /\ (exists hgcrt_mod_left_pth_correction_solution hgcrt_mod_right_pth_correction_solution. (d * t) + p * hgcrt_mod_left_pth_correction_solution = (x * q) + p * hgcrt_mod_right_pth_correction_solution))
  2. L21
    specialize linear_congruence_nonzero_modulus_bounded_constructor d
  3. L22
    specialize linear_congruence_nonzero_modulus_bounded_constructor p
  4. L23
    specialize linear_congruence_nonzero_modulus_bounded_constructor (x * q)
  5. L24
    specialize linear_congruence_nonzero_modulus_bounded_constructor 1
  6. L25
    apply linear_congruence_nonzero_modulus_bounded_constructor
  7. L26
    exact hgcd
  8. L27
    exact hp
  9. L28
    exact hdivisor
10Separate the logical casesL29–30

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

  1. L29
    cases hsolution
  2. L30
    cases hsolution_witness
11Establish hsameL31–34

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

  1. L31
    have hsame : exists hgcrt_mod_left_pth_correction_same hgcrt_mod_right_pth_correction_same. q + p * hgcrt_mod_left_pth_correction_same = q + p * hgcrt_mod_right_pth_correction_same
  2. L32
    specialize mod_eq_refl p
  3. L33
    specialize mod_eq_refl q
  4. L34
    apply mod_eq_refl
12Establish hsumL35–43

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

  1. L35
    have hsum : exists hgcrt_mod_left_pth_correction_sum hgcrt_mod_right_pth_correction_sum. (q + d * x1) + p * hgcrt_mod_left_pth_correction_sum = (q + x * q) + p * hgcrt_mod_right_pth_correction_sum
  2. L36
    specialize mod_eq_add p
  3. L37
    specialize mod_eq_add q
  4. L38
    specialize mod_eq_add q
  5. L39
    specialize mod_eq_add (d * x1)
  6. L40
    specialize mod_eq_add (x * q)
  7. L41
    apply mod_eq_add
  8. L42
    exact hsame
  9. L43
    exact hsolution_witness_right
13Establish hnegativeL44–49

Establish this local claim before using it. It is not an additional assumption.

  1. L44
    have hnegative : exists hgcrt_mod_left_pth_correction_negative hgcrt_mod_right_pth_correction_negative. (q + x * q) + p * hgcrt_mod_left_pth_correction_negative = 0 + p * hgcrt_mod_right_pth_correction_negative
  2. L45
    specialize hensel_predecessor_annihilates_residue x
  3. L46
    specialize hensel_predecessor_annihilates_residue q
  4. L47
    rewrite <- hsuccessor_witness at hensel_predecessor_annihilates_residue
  5. L48
    rewrite <- hsuccessor_witness at hensel_predecessor_annihilates_residue
  6. L49
    exact hensel_predecessor_annihilates_residue
14Establish hresultL50–57

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

  1. L50
    have hresult : exists hgcrt_mod_left_pth_correction_final hgcrt_mod_right_pth_correction_final. (q + d * x1) + p * hgcrt_mod_left_pth_correction_final = 0 + p * hgcrt_mod_right_pth_correction_final
  2. L51
    specialize mod_eq_trans p
  3. L52
    specialize mod_eq_trans (q + d * x1)
  4. L53
    specialize mod_eq_trans (q + x * q)
  5. L54
    specialize mod_eq_trans 0
  6. L55
    apply mod_eq_trans
  7. L56
    exact hsum
  8. L57
    exact hnegative
15Construct an explicit witnessL58–58

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

  1. L58
    exists x1
16Separate the logical casesL59–59

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

  1. L59
    split
17Use earlier factsL60–61

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

  1. L60
    exact hsolution_witness_left
  2. L61
    exact hresult

Library-wide reading audit

Original defined command ledger · 61 lines
  1. 0001intro d
  2. 0002intro p
  3. 0003intro q
  4. 0004intro hp
  5. 0005intro hcop
  6. 0006have hsuccessor : exists k. p = S k
  7. 0007specialize nonzero_is_succ p
  8. 0008apply nonzero_is_succ
  9. 0009exact hp
  10. 0010cases hsuccessor
  11. 0011have hgcd : (((exists r. d = 1 * r) /\ (exists s. p = 1 * s)) /\ forall j. (exists u. d = j * u) -> (exists v. p = j * v) -> exists w. 1 = j * w)
  12. 0012specialize coprime_to_is_gcd_one d
  13. 0013specialize coprime_to_is_gcd_one p
  14. 0014apply coprime_to_is_gcd_one
  15. 0015exact hcop
  16. 0016have hdivisor : exists w. x * q = 1 * w
  17. 0017exists x * q
  18. 0018symm
  19. 0019apply one_mul
  20. 0020have hsolution : exists t. ((exists h. h + S t = p) /\ (exists hgcrt_mod_left_pth_correction_solution hgcrt_mod_right_pth_correction_solution. (d * t) + p * hgcrt_mod_left_pth_correction_solution = (x * q) + p * hgcrt_mod_right_pth_correction_solution))
  21. 0021specialize linear_congruence_nonzero_modulus_bounded_constructor d
  22. 0022specialize linear_congruence_nonzero_modulus_bounded_constructor p
  23. 0023specialize linear_congruence_nonzero_modulus_bounded_constructor (x * q)
  24. 0024specialize linear_congruence_nonzero_modulus_bounded_constructor 1
  25. 0025apply linear_congruence_nonzero_modulus_bounded_constructor
  26. 0026exact hgcd
  27. 0027exact hp
  28. 0028exact hdivisor
  29. 0029cases hsolution
  30. 0030cases hsolution_witness
  31. 0031have hsame : exists hgcrt_mod_left_pth_correction_same hgcrt_mod_right_pth_correction_same. q + p * hgcrt_mod_left_pth_correction_same = q + p * hgcrt_mod_right_pth_correction_same
  32. 0032specialize mod_eq_refl p
  33. 0033specialize mod_eq_refl q
  34. 0034apply mod_eq_refl
  35. 0035have hsum : exists hgcrt_mod_left_pth_correction_sum hgcrt_mod_right_pth_correction_sum. (q + d * x1) + p * hgcrt_mod_left_pth_correction_sum = (q + x * q) + p * hgcrt_mod_right_pth_correction_sum
  36. 0036specialize mod_eq_add p
  37. 0037specialize mod_eq_add q
  38. 0038specialize mod_eq_add q
  39. 0039specialize mod_eq_add (d * x1)
  40. 0040specialize mod_eq_add (x * q)
  41. 0041apply mod_eq_add
  42. 0042exact hsame
  43. 0043exact hsolution_witness_right
  44. 0044have hnegative : exists hgcrt_mod_left_pth_correction_negative hgcrt_mod_right_pth_correction_negative. (q + x * q) + p * hgcrt_mod_left_pth_correction_negative = 0 + p * hgcrt_mod_right_pth_correction_negative
  45. 0045specialize hensel_predecessor_annihilates_residue x
  46. 0046specialize hensel_predecessor_annihilates_residue q
  47. 0047rewrite <- hsuccessor_witness at hensel_predecessor_annihilates_residue
  48. 0048rewrite <- hsuccessor_witness at hensel_predecessor_annihilates_residue
  49. 0049exact hensel_predecessor_annihilates_residue
  50. 0050have hresult : exists hgcrt_mod_left_pth_correction_final hgcrt_mod_right_pth_correction_final. (q + d * x1) + p * hgcrt_mod_left_pth_correction_final = 0 + p * hgcrt_mod_right_pth_correction_final
  51. 0051specialize mod_eq_trans p
  52. 0052specialize mod_eq_trans (q + d * x1)
  53. 0053specialize mod_eq_trans (q + x * q)
  54. 0054specialize mod_eq_trans 0
  55. 0055apply mod_eq_trans
  56. 0056exact hsum
  57. 0057exact hnegative
  58. 0058exists x1
  59. 0059split
  60. 0060exact hsolution_witness_left
  61. 0061exact hresult