HL0018

hensel_signed_blend_mod_iff

Natural recoding preserves every signed residue modulo every divisor of the selected final modulus.

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

∀ m. ∀ M. ∀ h. ∀ A. ∀ B. ∀ C. ∀ R. M = S h → Dvd(m,M) → C = A + h · B → (ModEq(m,C,R) → ModEq(m,A,R + B)) ∧ (ModEq(m,A,R + B) → ModEq(m,C,R))

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

Definition DAG

Dvd(d,n) · 1ModEq(m,a,b) · 6

Actual proof prerequisites

hensel_signed_blend_balancemultiple_mul_right · checked external prerequisitemultiple_implies_balanced_zero_congruence · checked external prerequisitemod_eq_add · checked external prerequisitemod_eq_refl · checked external prerequisitemod_eq_trans · checked external prerequisitemod_eq_symm · checked external prerequisitemod_eq_add_cancel_right · checked external prerequisite
Original expanded first-order statement 
forall m M h A B C R. M = S h -> (exists q. M = m * q) -> C = A + h * B -> (((exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. C + m * hgcrt_mod_left_hpl_mod = R + m * hgcrt_mod_right_hpl_mod) -> (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. A + m * hgcrt_mod_left_hpl_mod = (R + B) + m * hgcrt_mod_right_hpl_mod)) /\ ((exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. A + m * hgcrt_mod_left_hpl_mod = (R + B) + m * hgcrt_mod_right_hpl_mod) -> (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. C + m * hgcrt_mod_left_hpl_mod = R + m * hgcrt_mod_right_hpl_mod)))

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 · 15 reading checkpoints · 4 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 balance
01Fix variables and assumptionsL1–10

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

  1. L1
    intro m
  2. L2
    intro M
  3. L3
    intro h
  4. L4
    intro A
  5. L5
    intro B
  6. L6
    intro C
  7. L7
    intro R
  8. L8
    intro hM
  9. L9
    intro hdiv
  10. L10
    intro hC
02Establish hbalanceL11–17

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

  1. L11
    have hbalance : C + B = A + M * B
  2. L12
    rewrite hC
  3. L13
    rewrite hM
  4. L14
    specialize hensel_signed_blend_balance h
  5. L15
    specialize hensel_signed_blend_balance A
  6. L16
    specialize hensel_signed_blend_balance B
  7. L17
    apply hensel_signed_blend_balance
03Establish hmultipleL18–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply multiple implies balanced zero congruence.

  1. L18
    have hmultiple : ModEq(m,M · B,0)Definitions: ModEq(m,M · B,0)Original native command in the exact edition
  2. L19
    specialize multiple_implies_balanced_zero_congruence m
  3. L20
    specialize multiple_implies_balanced_zero_congruence (M * B)
  4. L21
    apply multiple_implies_balanced_zero_congruence
  5. L22
    specialize multiple_mul_right m
  6. L23
    specialize multiple_mul_right M
  7. L24
    specialize multiple_mul_right B
  8. L25
    apply multiple_mul_right
  9. L26
    exact hdiv
04Establish hdropL27–36

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

  1. L27
    have hdrop : ModEq(m,A + M · B,A + 0)Definitions: ModEq(m,A + M · B,A + 0)Original native command in the exact edition
  2. L28
    specialize mod_eq_add m
  3. L29
    specialize mod_eq_add A
  4. L30
    specialize mod_eq_add A
  5. L31
    specialize mod_eq_add (M * B)
  6. L32
    specialize mod_eq_add 0
  7. L33
    apply mod_eq_add
  8. L34
    specialize mod_eq_refl m
  9. L35
    specialize mod_eq_refl A
  10. L36
    apply mod_eq_refl
05Use earlier factsL37–37

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

  1. L37
    exact hmultiple
06Establish hzeroL38–40

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

  1. L38
    have hzero : A + 0 = A
  2. L39
    simp
  3. L40
    rewrite hzero at hdrop
07Separate the logical casesL41–41

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

  1. L41
    split
08Fix variables and assumptionsL42–42

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

  1. L42
    intro hsource
09Use earlier factsL43–52

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

  1. L43
    specialize mod_eq_trans m
  2. L44
    specialize mod_eq_trans A
  3. L45
    specialize mod_eq_trans (A + M * B)
  4. L46
    specialize mod_eq_trans (R + B)
  5. L47
    apply mod_eq_trans
  6. L48
    specialize mod_eq_symm m
  7. L49
    specialize mod_eq_symm (A + M * B)
  8. L50
    specialize mod_eq_symm A
  9. L51
    apply mod_eq_symm
  10. L52
    exact hdrop
10Calculate and transport equalitiesL53–53

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

  1. L53
    rewrite <- hbalance
11Use earlier factsL54–63

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

  1. L54
    specialize mod_eq_add m
  2. L55
    specialize mod_eq_add C
  3. L56
    specialize mod_eq_add R
  4. L57
    specialize mod_eq_add B
  5. L58
    specialize mod_eq_add B
  6. L59
    apply mod_eq_add
  7. L60
    exact hsource
  8. L61
    specialize mod_eq_refl m
  9. L62
    specialize mod_eq_refl B
  10. L63
    apply mod_eq_refl
12Fix variables and assumptionsL64–64

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

  1. L64
    intro hsource
13Use earlier factsL65–69

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

  1. L65
    specialize mod_eq_add_cancel_right m
  2. L66
    specialize mod_eq_add_cancel_right C
  3. L67
    specialize mod_eq_add_cancel_right R
  4. L68
    specialize mod_eq_add_cancel_right B
  5. L69
    apply mod_eq_add_cancel_right
14Calculate and transport equalitiesL70–70

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

  1. L70
    rewrite hbalance
15Use earlier factsL71–77

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

  1. L71
    specialize mod_eq_trans m
  2. L72
    specialize mod_eq_trans (A + M * B)
  3. L73
    specialize mod_eq_trans A
  4. L74
    specialize mod_eq_trans (R + B)
  5. L75
    apply mod_eq_trans
  6. L76
    exact hdrop
  7. L77
    exact hsource

Library-wide reading audit

Original defined command ledger · 77 lines
  1. 0001intro m
  2. 0002intro M
  3. 0003intro h
  4. 0004intro A
  5. 0005intro B
  6. 0006intro C
  7. 0007intro R
  8. 0008intro hM
  9. 0009intro hdiv
  10. 0010intro hC
  11. 0011have hbalance : C + B = A + M * B
  12. 0012rewrite hC
  13. 0013rewrite hM
  14. 0014specialize hensel_signed_blend_balance h
  15. 0015specialize hensel_signed_blend_balance A
  16. 0016specialize hensel_signed_blend_balance B
  17. 0017apply hensel_signed_blend_balance
  18. 0018have hmultiple : ModEq(m,M · B,0)
  19. 0019specialize multiple_implies_balanced_zero_congruence m
  20. 0020specialize multiple_implies_balanced_zero_congruence (M * B)
  21. 0021apply multiple_implies_balanced_zero_congruence
  22. 0022specialize multiple_mul_right m
  23. 0023specialize multiple_mul_right M
  24. 0024specialize multiple_mul_right B
  25. 0025apply multiple_mul_right
  26. 0026exact hdiv
  27. 0027have hdrop : ModEq(m,A + M · B,A + 0)
  28. 0028specialize mod_eq_add m
  29. 0029specialize mod_eq_add A
  30. 0030specialize mod_eq_add A
  31. 0031specialize mod_eq_add (M * B)
  32. 0032specialize mod_eq_add 0
  33. 0033apply mod_eq_add
  34. 0034specialize mod_eq_refl m
  35. 0035specialize mod_eq_refl A
  36. 0036apply mod_eq_refl
  37. 0037exact hmultiple
  38. 0038have hzero : A + 0 = A
  39. 0039simp
  40. 0040rewrite hzero at hdrop
  41. 0041split
  42. 0042intro hsource
  43. 0043specialize mod_eq_trans m
  44. 0044specialize mod_eq_trans A
  45. 0045specialize mod_eq_trans (A + M * B)
  46. 0046specialize mod_eq_trans (R + B)
  47. 0047apply mod_eq_trans
  48. 0048specialize mod_eq_symm m
  49. 0049specialize mod_eq_symm (A + M * B)
  50. 0050specialize mod_eq_symm A
  51. 0051apply mod_eq_symm
  52. 0052exact hdrop
  53. 0053rewrite <- hbalance
  54. 0054specialize mod_eq_add m
  55. 0055specialize mod_eq_add C
  56. 0056specialize mod_eq_add R
  57. 0057specialize mod_eq_add B
  58. 0058specialize mod_eq_add B
  59. 0059apply mod_eq_add
  60. 0060exact hsource
  61. 0061specialize mod_eq_refl m
  62. 0062specialize mod_eq_refl B
  63. 0063apply mod_eq_refl
  64. 0064intro hsource
  65. 0065specialize mod_eq_add_cancel_right m
  66. 0066specialize mod_eq_add_cancel_right C
  67. 0067specialize mod_eq_add_cancel_right R
  68. 0068specialize mod_eq_add_cancel_right B
  69. 0069apply mod_eq_add_cancel_right
  70. 0070rewrite hbalance
  71. 0071specialize mod_eq_trans m
  72. 0072specialize mod_eq_trans (A + M * B)
  73. 0073specialize mod_eq_trans A
  74. 0074specialize mod_eq_trans (R + B)
  75. 0075apply mod_eq_trans
  76. 0076exact hdrop
  77. 0077exact hsource