EL001B

lte_odd_prime_power_difference_quotient

Construct the actual p-th powers and their geometric quotient p*u with a genuine p-nondivisible cofactor for every odd prime.

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

All displayed hypotheses are required. Powers and positive differences are actual existential outputs. The proof constructs second-order correction identities and iterates the prime step; no binomial expansion or LTE oracle is assumed. The 2-adic variants remain separate open targets.

Exact theorem in conservative defined notation

∀ p. ∀ a. ∀ b. ∀ d. ¬p = 1 ∧ (∀ x. ∀ y. p = x · y → x = 1 ∨ y = 1) → ¬p = 2 → a = b + d → Dvd(p,d) → ¬Dvd(p,b) → ∃ x. ∃ y. ∃ z. ∃ n. Pow(a,p,x) ∧ (Pow(b,p,y) ∧ (x = y + d · z ∧ (z = p · n ∧ ¬Dvd(p,n))))

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

Definition DAG

PowerDifferenceSecondOrder(a,b,d,k,A,B,R,T,Q,C,H) · 1Dvd(d,n) · 4Pow(a,e,z) · 2

Actual proof prerequisites

prime_is_succ_succ · checked external prerequisitelte_power_difference_second_order_existslte_odd_prime_quotient_unitlte_nondivisor_powerlte_power_exponent_eq_transport
Original expanded first-order statement 
forall p a b d. (~((p) = 1) /\ forall pvs_left_prime_step_prime pvs_right_prime_step_prime. (p) = pvs_left_prime_step_prime * pvs_right_prime_step_prime -> pvs_left_prime_step_prime = 1 \/ pvs_right_prime_step_prime = 1) -> ~(p = 2) -> a = b + d -> (exists olte_factor_prime_step_difference. (d) = (p) * olte_factor_prime_step_difference) -> ~(exists olte_factor_prime_step_base. (b) = (p) * olte_factor_prime_step_base) -> exists A B Q u. (((exists pa_b_olte_prime_step_A pa_c_olte_prime_step_A. ((forall pa_i_olte_prime_step_A_repeat. (exists pa_lt_olte_prime_step_A_repeat_bound. pa_lt_olte_prime_step_A_repeat_bound + S pa_i_olte_prime_step_A_repeat = p) -> (((exists pa_h_olte_prime_step_A_repeat_decoded. pa_h_olte_prime_step_A_repeat_decoded + S (a) = S ((S (pa_i_olte_prime_step_A_repeat)) * pa_c_olte_prime_step_A)) /\ exists pa_q_olte_prime_step_A_repeat_decoded. pa_b_olte_prime_step_A = pa_q_olte_prime_step_A_repeat_decoded * S ((S (pa_i_olte_prime_step_A_repeat)) * pa_c_olte_prime_step_A) + (a)))) /\ (exists pa_u_olte_prime_step_A_product pa_v_olte_prime_step_A_product. ((((exists pa_h_olte_prime_step_A_product_start. pa_h_olte_prime_step_A_product_start + S (1) = S ((S (0)) * pa_v_olte_prime_step_A_product)) /\ exists pa_q_olte_prime_step_A_product_start. pa_u_olte_prime_step_A_product = pa_q_olte_prime_step_A_product_start * S ((S (0)) * pa_v_olte_prime_step_A_product) + (1))) /\ ((((exists pa_h_olte_prime_step_A_product_terminal. pa_h_olte_prime_step_A_product_terminal + S (A) = S ((S (p)) * pa_v_olte_prime_step_A_product)) /\ exists pa_q_olte_prime_step_A_product_terminal. pa_u_olte_prime_step_A_product = pa_q_olte_prime_step_A_product_terminal * S ((S (p)) * pa_v_olte_prime_step_A_product) + (A))) /\ forall pa_i_olte_prime_step_A_product. (exists pa_lt_olte_prime_step_A_product_bound. pa_lt_olte_prime_step_A_product_bound + S pa_i_olte_prime_step_A_product = p) -> exists pa_p_olte_prime_step_A_product pa_r_olte_prime_step_A_product pa_s_olte_prime_step_A_product. ((((exists pa_h_olte_prime_step_A_product_factor. pa_h_olte_prime_step_A_product_factor + S (pa_p_olte_prime_step_A_product) = S ((S (pa_i_olte_prime_step_A_product)) * pa_c_olte_prime_step_A)) /\ exists pa_q_olte_prime_step_A_product_factor. pa_b_olte_prime_step_A = pa_q_olte_prime_step_A_product_factor * S ((S (pa_i_olte_prime_step_A_product)) * pa_c_olte_prime_step_A) + (pa_p_olte_prime_step_A_product))) /\ ((((exists pa_h_olte_prime_step_A_product_partial. pa_h_olte_prime_step_A_product_partial + S (pa_r_olte_prime_step_A_product) = S ((S (pa_i_olte_prime_step_A_product)) * pa_v_olte_prime_step_A_product)) /\ exists pa_q_olte_prime_step_A_product_partial. pa_u_olte_prime_step_A_product = pa_q_olte_prime_step_A_product_partial * S ((S (pa_i_olte_prime_step_A_product)) * pa_v_olte_prime_step_A_product) + (pa_r_olte_prime_step_A_product))) /\ ((((exists pa_h_olte_prime_step_A_product_successor. pa_h_olte_prime_step_A_product_successor + S (pa_s_olte_prime_step_A_product) = S ((S (S pa_i_olte_prime_step_A_product)) * pa_v_olte_prime_step_A_product)) /\ exists pa_q_olte_prime_step_A_product_successor. pa_u_olte_prime_step_A_product = pa_q_olte_prime_step_A_product_successor * S ((S (S pa_i_olte_prime_step_A_product)) * pa_v_olte_prime_step_A_product) + (pa_s_olte_prime_step_A_product))) /\ pa_s_olte_prime_step_A_product = pa_r_olte_prime_step_A_product * pa_p_olte_prime_step_A_product)))))))) /\ (((exists pa_b_olte_prime_step_B pa_c_olte_prime_step_B. ((forall pa_i_olte_prime_step_B_repeat. (exists pa_lt_olte_prime_step_B_repeat_bound. pa_lt_olte_prime_step_B_repeat_bound + S pa_i_olte_prime_step_B_repeat = p) -> (((exists pa_h_olte_prime_step_B_repeat_decoded. pa_h_olte_prime_step_B_repeat_decoded + S (b) = S ((S (pa_i_olte_prime_step_B_repeat)) * pa_c_olte_prime_step_B)) /\ exists pa_q_olte_prime_step_B_repeat_decoded. pa_b_olte_prime_step_B = pa_q_olte_prime_step_B_repeat_decoded * S ((S (pa_i_olte_prime_step_B_repeat)) * pa_c_olte_prime_step_B) + (b)))) /\ (exists pa_u_olte_prime_step_B_product pa_v_olte_prime_step_B_product. ((((exists pa_h_olte_prime_step_B_product_start. pa_h_olte_prime_step_B_product_start + S (1) = S ((S (0)) * pa_v_olte_prime_step_B_product)) /\ exists pa_q_olte_prime_step_B_product_start. pa_u_olte_prime_step_B_product = pa_q_olte_prime_step_B_product_start * S ((S (0)) * pa_v_olte_prime_step_B_product) + (1))) /\ ((((exists pa_h_olte_prime_step_B_product_terminal. pa_h_olte_prime_step_B_product_terminal + S (B) = S ((S (p)) * pa_v_olte_prime_step_B_product)) /\ exists pa_q_olte_prime_step_B_product_terminal. pa_u_olte_prime_step_B_product = pa_q_olte_prime_step_B_product_terminal * S ((S (p)) * pa_v_olte_prime_step_B_product) + (B))) /\ forall pa_i_olte_prime_step_B_product. (exists pa_lt_olte_prime_step_B_product_bound. pa_lt_olte_prime_step_B_product_bound + S pa_i_olte_prime_step_B_product = p) -> exists pa_p_olte_prime_step_B_product pa_r_olte_prime_step_B_product pa_s_olte_prime_step_B_product. ((((exists pa_h_olte_prime_step_B_product_factor. pa_h_olte_prime_step_B_product_factor + S (pa_p_olte_prime_step_B_product) = S ((S (pa_i_olte_prime_step_B_product)) * pa_c_olte_prime_step_B)) /\ exists pa_q_olte_prime_step_B_product_factor. pa_b_olte_prime_step_B = pa_q_olte_prime_step_B_product_factor * S ((S (pa_i_olte_prime_step_B_product)) * pa_c_olte_prime_step_B) + (pa_p_olte_prime_step_B_product))) /\ ((((exists pa_h_olte_prime_step_B_product_partial. pa_h_olte_prime_step_B_product_partial + S (pa_r_olte_prime_step_B_product) = S ((S (pa_i_olte_prime_step_B_product)) * pa_v_olte_prime_step_B_product)) /\ exists pa_q_olte_prime_step_B_product_partial. pa_u_olte_prime_step_B_product = pa_q_olte_prime_step_B_product_partial * S ((S (pa_i_olte_prime_step_B_product)) * pa_v_olte_prime_step_B_product) + (pa_r_olte_prime_step_B_product))) /\ ((((exists pa_h_olte_prime_step_B_product_successor. pa_h_olte_prime_step_B_product_successor + S (pa_s_olte_prime_step_B_product) = S ((S (S pa_i_olte_prime_step_B_product)) * pa_v_olte_prime_step_B_product)) /\ exists pa_q_olte_prime_step_B_product_successor. pa_u_olte_prime_step_B_product = pa_q_olte_prime_step_B_product_successor * S ((S (S pa_i_olte_prime_step_B_product)) * pa_v_olte_prime_step_B_product) + (pa_s_olte_prime_step_B_product))) /\ pa_s_olte_prime_step_B_product = pa_r_olte_prime_step_B_product * pa_p_olte_prime_step_B_product)))))))) /\ (((A = B + d * Q) /\ (((Q = p * u) /\ (~(exists olte_factor_prime_step_unit. (u) = (p) * olte_factor_prime_step_unit))))))))))

Complete tactic proof in conservative notation

All 90 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

90 script commands · 28 reading checkpoints · 3 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 (4)
lte power difference second order existslte odd prime quotient unitlte nondivisor powerlte power exponent eq transport
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro d
  5. L5
    intro hp
  6. L6
    intro hne
  7. L7
    intro ha
  8. L8
    intro hd
  9. L9
    intro hb
02Establish hindexL10–13

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

  1. L10
    have hindex : exists k. p = S (S k)
  2. L11
    specialize prime_is_succ_succ (p)
  3. L12
    apply prime_is_succ_succ
  4. L13
    exact hp
03Separate the logical casesL14–14

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

  1. L14
    cases hindex
04Establish hsecondL15–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lte power difference second order exists.

  1. L15
    have hsecond : ∃ A. ∃ B. ∃ R. ∃ T. ∃ Q. ∃ C. ∃ H. PowerDifferenceSecondOrder(a,b,d,x,A,B,R,T,Q,C,H)Definitions: PowerDifferenceSecondOrder(a,b,d,x,A,B,R,T,Q,C,H)Original native command in the exact edition
  2. L16
    specialize lte_power_difference_second_order_exists (a)
  3. L17
    specialize lte_power_difference_second_order_exists (b)
  4. L18
    specialize lte_power_difference_second_order_exists (d)
  5. L19
    specialize lte_power_difference_second_order_exists (x)
  6. L20
    apply lte_power_difference_second_order_exists
  7. L21
    exact ha
05Separate the logical casesL22–31

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

  1. L22
    cases hsecond
  2. L23
    cases hsecond_witness
  3. L24
    cases hsecond_witness_witness
  4. L25
    cases hsecond_witness_witness_witness
  5. L26
    cases hsecond_witness_witness_witness_witness
  6. L27
    cases hsecond_witness_witness_witness_witness_witness
  7. L28
    cases hsecond_witness_witness_witness_witness_witness_witness
  8. L29
    cases hsecond_witness_witness_witness_witness_witness_witness_witness
  9. L30
    cases hsecond_witness_witness_witness_witness_witness_witness_witness_right
  10. L31
    cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right
06Separate the logical casesL32–34

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

  1. L32
    cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right
  2. L33
    cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  3. L34
    cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
07Establish hunitL35–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lte odd prime quotient unit.

  1. L35
    have hunit : ∃ u. x5 = p · u ∧ ¬Dvd(p,u)Definitions: Dvd(p,u)Original native command in the exact edition
  2. L36
    specialize lte_odd_prime_quotient_unit (p)
  3. L37
    specialize lte_odd_prime_quotient_unit (d)
  4. L38
    specialize lte_odd_prime_quotient_unit (S x)
  5. L39
    specialize lte_odd_prime_quotient_unit (x3)
  6. L40
    specialize lte_odd_prime_quotient_unit (x4)
  7. L41
    specialize lte_odd_prime_quotient_unit (x5)
  8. L42
    specialize lte_odd_prime_quotient_unit (x6)
  9. L43
    specialize lte_odd_prime_quotient_unit (x7)
  10. L44
    apply lte_odd_prime_quotient_unit
08Use earlier factsL45–47

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

  1. L45
    exact hp
  2. L46
    exact hne
  3. L47
    exact hd
09Fix variables and assumptionsL48–48

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

  1. L48
    intro hdivR
10Use earlier factsL49–57

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

  1. L49
    specialize lte_nondivisor_power (p)
  2. L50
    specialize lte_nondivisor_power (b)
  3. L51
    specialize lte_nondivisor_power (S x)
  4. L52
    specialize lte_nondivisor_power (x3)
  5. L53
    apply lte_nondivisor_power
  6. L54
    exact hp
  7. L55
    exact hb
  8. L56
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_left
  9. L57
    exact hdivR
11Calculate and transport equalitiesL58–58

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

  1. L58
    rewrite hindex_witness
12Use earlier factsL59–59

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

  1. L59
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
13Calculate and transport equalitiesL60–60

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

  1. L60
    rewrite hindex_witness
14Use earlier factsL61–61

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

  1. L61
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
15Separate the logical casesL62–63

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

  1. L62
    cases hunit
  2. L63
    cases hunit_witness
16Construct an explicit witnessL64–67

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

  1. L64
    exists x1
  2. L65
    exists x2
  3. L66
    exists x5
  4. L67
    exists x8
17Separate the logical casesL68–68

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

  1. L68
    split
18Use earlier factsL69–73

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

  1. L69
    specialize lte_power_exponent_eq_transport (a)
  2. L70
    specialize lte_power_exponent_eq_transport (S (S x))
  3. L71
    specialize lte_power_exponent_eq_transport (p)
  4. L72
    specialize lte_power_exponent_eq_transport (x1)
  5. L73
    apply lte_power_exponent_eq_transport
19Calculate and transport equalitiesL74–74

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

  1. L74
    symm
20Use earlier factsL75–76

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

  1. L75
    exact hindex_witness
  2. L76
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_left
21Separate the logical casesL77–77

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

  1. L77
    split
22Use earlier factsL78–82

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

  1. L78
    specialize lte_power_exponent_eq_transport (b)
  2. L79
    specialize lte_power_exponent_eq_transport (S (S x))
  3. L80
    specialize lte_power_exponent_eq_transport (p)
  4. L81
    specialize lte_power_exponent_eq_transport (x2)
  5. L82
    apply lte_power_exponent_eq_transport
23Calculate and transport equalitiesL83–83

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

  1. L83
    symm
24Use earlier factsL84–85

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

  1. L84
    exact hindex_witness
  2. L85
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_left
25Separate the logical casesL86–86

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

  1. L86
    split
26Use earlier factsL87–87

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

  1. L87
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
27Separate the logical casesL88–88

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

  1. L88
    split
28Use earlier factsL89–90

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

  1. L89
    exact hunit_witness_left
  2. L90
    exact hunit_witness_right

Library-wide reading audit

Original defined command ledger · 90 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro d
  5. 0005intro hp
  6. 0006intro hne
  7. 0007intro ha
  8. 0008intro hd
  9. 0009intro hb
  10. 0010have hindex : exists k. p = S (S k)
  11. 0011specialize prime_is_succ_succ (p)
  12. 0012apply prime_is_succ_succ
  13. 0013exact hp
  14. 0014cases hindex
  15. 0015have hsecond : ∃ A. ∃ B. ∃ R. ∃ T. ∃ Q. ∃ C. ∃ H. PowerDifferenceSecondOrder(a,b,d,x,A,B,R,T,Q,C,H)
  16. 0016specialize lte_power_difference_second_order_exists (a)
  17. 0017specialize lte_power_difference_second_order_exists (b)
  18. 0018specialize lte_power_difference_second_order_exists (d)
  19. 0019specialize lte_power_difference_second_order_exists (x)
  20. 0020apply lte_power_difference_second_order_exists
  21. 0021exact ha
  22. 0022cases hsecond
  23. 0023cases hsecond_witness
  24. 0024cases hsecond_witness_witness
  25. 0025cases hsecond_witness_witness_witness
  26. 0026cases hsecond_witness_witness_witness_witness
  27. 0027cases hsecond_witness_witness_witness_witness_witness
  28. 0028cases hsecond_witness_witness_witness_witness_witness_witness
  29. 0029cases hsecond_witness_witness_witness_witness_witness_witness_witness
  30. 0030cases hsecond_witness_witness_witness_witness_witness_witness_witness_right
  31. 0031cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right
  32. 0032cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right
  33. 0033cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  34. 0034cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  35. 0035have hunit : ∃ u. x5 = p · u ∧ ¬Dvd(p,u)
  36. 0036specialize lte_odd_prime_quotient_unit (p)
  37. 0037specialize lte_odd_prime_quotient_unit (d)
  38. 0038specialize lte_odd_prime_quotient_unit (S x)
  39. 0039specialize lte_odd_prime_quotient_unit (x3)
  40. 0040specialize lte_odd_prime_quotient_unit (x4)
  41. 0041specialize lte_odd_prime_quotient_unit (x5)
  42. 0042specialize lte_odd_prime_quotient_unit (x6)
  43. 0043specialize lte_odd_prime_quotient_unit (x7)
  44. 0044apply lte_odd_prime_quotient_unit
  45. 0045exact hp
  46. 0046exact hne
  47. 0047exact hd
  48. 0048intro hdivR
  49. 0049specialize lte_nondivisor_power (p)
  50. 0050specialize lte_nondivisor_power (b)
  51. 0051specialize lte_nondivisor_power (S x)
  52. 0052specialize lte_nondivisor_power (x3)
  53. 0053apply lte_nondivisor_power
  54. 0054exact hp
  55. 0055exact hb
  56. 0056exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_left
  57. 0057exact hdivR
  58. 0058rewrite hindex_witness
  59. 0059exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  60. 0060rewrite hindex_witness
  61. 0061exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  62. 0062cases hunit
  63. 0063cases hunit_witness
  64. 0064exists x1
  65. 0065exists x2
  66. 0066exists x5
  67. 0067exists x8
  68. 0068split
  69. 0069specialize lte_power_exponent_eq_transport (a)
  70. 0070specialize lte_power_exponent_eq_transport (S (S x))
  71. 0071specialize lte_power_exponent_eq_transport (p)
  72. 0072specialize lte_power_exponent_eq_transport (x1)
  73. 0073apply lte_power_exponent_eq_transport
  74. 0074symm
  75. 0075exact hindex_witness
  76. 0076exact hsecond_witness_witness_witness_witness_witness_witness_witness_left
  77. 0077split
  78. 0078specialize lte_power_exponent_eq_transport (b)
  79. 0079specialize lte_power_exponent_eq_transport (S (S x))
  80. 0080specialize lte_power_exponent_eq_transport (p)
  81. 0081specialize lte_power_exponent_eq_transport (x2)
  82. 0082apply lte_power_exponent_eq_transport
  83. 0083symm
  84. 0084exact hindex_witness
  85. 0085exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_left
  86. 0086split
  87. 0087exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  88. 0088split
  89. 0089exact hunit_witness_left
  90. 0090exact hunit_witness_right