EL0025

lte_power_difference_functional

Any two witnesses for the same natural power difference have exactly the same value; no selected representation can change the valuation output.

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

∀ a. ∀ b. ∀ n. ∀ A. ∀ B. ∀ D. ∀ X. ∀ Y. ∀ E. Pow(a,n,A) → Pow(b,n,B) → A = B + D → Pow(a,n,X) → Pow(b,n,Y) → X = Y + E → D = E

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

Definition DAG

Pow(a,e,z) · 4

Actual proof prerequisites

pow_functional · checked external prerequisiteadd_left_cancel · checked external prerequisite
Original expanded first-order statement 
forall a b n A B D X Y E. (exists pa_b_olte_functional_A pa_c_olte_functional_A. ((forall pa_i_olte_functional_A_repeat. (exists pa_lt_olte_functional_A_repeat_bound. pa_lt_olte_functional_A_repeat_bound + S pa_i_olte_functional_A_repeat = n) -> (((exists pa_h_olte_functional_A_repeat_decoded. pa_h_olte_functional_A_repeat_decoded + S (a) = S ((S (pa_i_olte_functional_A_repeat)) * pa_c_olte_functional_A)) /\ exists pa_q_olte_functional_A_repeat_decoded. pa_b_olte_functional_A = pa_q_olte_functional_A_repeat_decoded * S ((S (pa_i_olte_functional_A_repeat)) * pa_c_olte_functional_A) + (a)))) /\ (exists pa_u_olte_functional_A_product pa_v_olte_functional_A_product. ((((exists pa_h_olte_functional_A_product_start. pa_h_olte_functional_A_product_start + S (1) = S ((S (0)) * pa_v_olte_functional_A_product)) /\ exists pa_q_olte_functional_A_product_start. pa_u_olte_functional_A_product = pa_q_olte_functional_A_product_start * S ((S (0)) * pa_v_olte_functional_A_product) + (1))) /\ ((((exists pa_h_olte_functional_A_product_terminal. pa_h_olte_functional_A_product_terminal + S (A) = S ((S (n)) * pa_v_olte_functional_A_product)) /\ exists pa_q_olte_functional_A_product_terminal. pa_u_olte_functional_A_product = pa_q_olte_functional_A_product_terminal * S ((S (n)) * pa_v_olte_functional_A_product) + (A))) /\ forall pa_i_olte_functional_A_product. (exists pa_lt_olte_functional_A_product_bound. pa_lt_olte_functional_A_product_bound + S pa_i_olte_functional_A_product = n) -> exists pa_p_olte_functional_A_product pa_r_olte_functional_A_product pa_s_olte_functional_A_product. ((((exists pa_h_olte_functional_A_product_factor. pa_h_olte_functional_A_product_factor + S (pa_p_olte_functional_A_product) = S ((S (pa_i_olte_functional_A_product)) * pa_c_olte_functional_A)) /\ exists pa_q_olte_functional_A_product_factor. pa_b_olte_functional_A = pa_q_olte_functional_A_product_factor * S ((S (pa_i_olte_functional_A_product)) * pa_c_olte_functional_A) + (pa_p_olte_functional_A_product))) /\ ((((exists pa_h_olte_functional_A_product_partial. pa_h_olte_functional_A_product_partial + S (pa_r_olte_functional_A_product) = S ((S (pa_i_olte_functional_A_product)) * pa_v_olte_functional_A_product)) /\ exists pa_q_olte_functional_A_product_partial. pa_u_olte_functional_A_product = pa_q_olte_functional_A_product_partial * S ((S (pa_i_olte_functional_A_product)) * pa_v_olte_functional_A_product) + (pa_r_olte_functional_A_product))) /\ ((((exists pa_h_olte_functional_A_product_successor. pa_h_olte_functional_A_product_successor + S (pa_s_olte_functional_A_product) = S ((S (S pa_i_olte_functional_A_product)) * pa_v_olte_functional_A_product)) /\ exists pa_q_olte_functional_A_product_successor. pa_u_olte_functional_A_product = pa_q_olte_functional_A_product_successor * S ((S (S pa_i_olte_functional_A_product)) * pa_v_olte_functional_A_product) + (pa_s_olte_functional_A_product))) /\ pa_s_olte_functional_A_product = pa_r_olte_functional_A_product * pa_p_olte_functional_A_product)))))))) -> (exists pa_b_olte_functional_B pa_c_olte_functional_B. ((forall pa_i_olte_functional_B_repeat. (exists pa_lt_olte_functional_B_repeat_bound. pa_lt_olte_functional_B_repeat_bound + S pa_i_olte_functional_B_repeat = n) -> (((exists pa_h_olte_functional_B_repeat_decoded. pa_h_olte_functional_B_repeat_decoded + S (b) = S ((S (pa_i_olte_functional_B_repeat)) * pa_c_olte_functional_B)) /\ exists pa_q_olte_functional_B_repeat_decoded. pa_b_olte_functional_B = pa_q_olte_functional_B_repeat_decoded * S ((S (pa_i_olte_functional_B_repeat)) * pa_c_olte_functional_B) + (b)))) /\ (exists pa_u_olte_functional_B_product pa_v_olte_functional_B_product. ((((exists pa_h_olte_functional_B_product_start. pa_h_olte_functional_B_product_start + S (1) = S ((S (0)) * pa_v_olte_functional_B_product)) /\ exists pa_q_olte_functional_B_product_start. pa_u_olte_functional_B_product = pa_q_olte_functional_B_product_start * S ((S (0)) * pa_v_olte_functional_B_product) + (1))) /\ ((((exists pa_h_olte_functional_B_product_terminal. pa_h_olte_functional_B_product_terminal + S (B) = S ((S (n)) * pa_v_olte_functional_B_product)) /\ exists pa_q_olte_functional_B_product_terminal. pa_u_olte_functional_B_product = pa_q_olte_functional_B_product_terminal * S ((S (n)) * pa_v_olte_functional_B_product) + (B))) /\ forall pa_i_olte_functional_B_product. (exists pa_lt_olte_functional_B_product_bound. pa_lt_olte_functional_B_product_bound + S pa_i_olte_functional_B_product = n) -> exists pa_p_olte_functional_B_product pa_r_olte_functional_B_product pa_s_olte_functional_B_product. ((((exists pa_h_olte_functional_B_product_factor. pa_h_olte_functional_B_product_factor + S (pa_p_olte_functional_B_product) = S ((S (pa_i_olte_functional_B_product)) * pa_c_olte_functional_B)) /\ exists pa_q_olte_functional_B_product_factor. pa_b_olte_functional_B = pa_q_olte_functional_B_product_factor * S ((S (pa_i_olte_functional_B_product)) * pa_c_olte_functional_B) + (pa_p_olte_functional_B_product))) /\ ((((exists pa_h_olte_functional_B_product_partial. pa_h_olte_functional_B_product_partial + S (pa_r_olte_functional_B_product) = S ((S (pa_i_olte_functional_B_product)) * pa_v_olte_functional_B_product)) /\ exists pa_q_olte_functional_B_product_partial. pa_u_olte_functional_B_product = pa_q_olte_functional_B_product_partial * S ((S (pa_i_olte_functional_B_product)) * pa_v_olte_functional_B_product) + (pa_r_olte_functional_B_product))) /\ ((((exists pa_h_olte_functional_B_product_successor. pa_h_olte_functional_B_product_successor + S (pa_s_olte_functional_B_product) = S ((S (S pa_i_olte_functional_B_product)) * pa_v_olte_functional_B_product)) /\ exists pa_q_olte_functional_B_product_successor. pa_u_olte_functional_B_product = pa_q_olte_functional_B_product_successor * S ((S (S pa_i_olte_functional_B_product)) * pa_v_olte_functional_B_product) + (pa_s_olte_functional_B_product))) /\ pa_s_olte_functional_B_product = pa_r_olte_functional_B_product * pa_p_olte_functional_B_product)))))))) -> A = B + D -> (exists pa_b_olte_functional_X pa_c_olte_functional_X. ((forall pa_i_olte_functional_X_repeat. (exists pa_lt_olte_functional_X_repeat_bound. pa_lt_olte_functional_X_repeat_bound + S pa_i_olte_functional_X_repeat = n) -> (((exists pa_h_olte_functional_X_repeat_decoded. pa_h_olte_functional_X_repeat_decoded + S (a) = S ((S (pa_i_olte_functional_X_repeat)) * pa_c_olte_functional_X)) /\ exists pa_q_olte_functional_X_repeat_decoded. pa_b_olte_functional_X = pa_q_olte_functional_X_repeat_decoded * S ((S (pa_i_olte_functional_X_repeat)) * pa_c_olte_functional_X) + (a)))) /\ (exists pa_u_olte_functional_X_product pa_v_olte_functional_X_product. ((((exists pa_h_olte_functional_X_product_start. pa_h_olte_functional_X_product_start + S (1) = S ((S (0)) * pa_v_olte_functional_X_product)) /\ exists pa_q_olte_functional_X_product_start. pa_u_olte_functional_X_product = pa_q_olte_functional_X_product_start * S ((S (0)) * pa_v_olte_functional_X_product) + (1))) /\ ((((exists pa_h_olte_functional_X_product_terminal. pa_h_olte_functional_X_product_terminal + S (X) = S ((S (n)) * pa_v_olte_functional_X_product)) /\ exists pa_q_olte_functional_X_product_terminal. pa_u_olte_functional_X_product = pa_q_olte_functional_X_product_terminal * S ((S (n)) * pa_v_olte_functional_X_product) + (X))) /\ forall pa_i_olte_functional_X_product. (exists pa_lt_olte_functional_X_product_bound. pa_lt_olte_functional_X_product_bound + S pa_i_olte_functional_X_product = n) -> exists pa_p_olte_functional_X_product pa_r_olte_functional_X_product pa_s_olte_functional_X_product. ((((exists pa_h_olte_functional_X_product_factor. pa_h_olte_functional_X_product_factor + S (pa_p_olte_functional_X_product) = S ((S (pa_i_olte_functional_X_product)) * pa_c_olte_functional_X)) /\ exists pa_q_olte_functional_X_product_factor. pa_b_olte_functional_X = pa_q_olte_functional_X_product_factor * S ((S (pa_i_olte_functional_X_product)) * pa_c_olte_functional_X) + (pa_p_olte_functional_X_product))) /\ ((((exists pa_h_olte_functional_X_product_partial. pa_h_olte_functional_X_product_partial + S (pa_r_olte_functional_X_product) = S ((S (pa_i_olte_functional_X_product)) * pa_v_olte_functional_X_product)) /\ exists pa_q_olte_functional_X_product_partial. pa_u_olte_functional_X_product = pa_q_olte_functional_X_product_partial * S ((S (pa_i_olte_functional_X_product)) * pa_v_olte_functional_X_product) + (pa_r_olte_functional_X_product))) /\ ((((exists pa_h_olte_functional_X_product_successor. pa_h_olte_functional_X_product_successor + S (pa_s_olte_functional_X_product) = S ((S (S pa_i_olte_functional_X_product)) * pa_v_olte_functional_X_product)) /\ exists pa_q_olte_functional_X_product_successor. pa_u_olte_functional_X_product = pa_q_olte_functional_X_product_successor * S ((S (S pa_i_olte_functional_X_product)) * pa_v_olte_functional_X_product) + (pa_s_olte_functional_X_product))) /\ pa_s_olte_functional_X_product = pa_r_olte_functional_X_product * pa_p_olte_functional_X_product)))))))) -> (exists pa_b_olte_functional_Y pa_c_olte_functional_Y. ((forall pa_i_olte_functional_Y_repeat. (exists pa_lt_olte_functional_Y_repeat_bound. pa_lt_olte_functional_Y_repeat_bound + S pa_i_olte_functional_Y_repeat = n) -> (((exists pa_h_olte_functional_Y_repeat_decoded. pa_h_olte_functional_Y_repeat_decoded + S (b) = S ((S (pa_i_olte_functional_Y_repeat)) * pa_c_olte_functional_Y)) /\ exists pa_q_olte_functional_Y_repeat_decoded. pa_b_olte_functional_Y = pa_q_olte_functional_Y_repeat_decoded * S ((S (pa_i_olte_functional_Y_repeat)) * pa_c_olte_functional_Y) + (b)))) /\ (exists pa_u_olte_functional_Y_product pa_v_olte_functional_Y_product. ((((exists pa_h_olte_functional_Y_product_start. pa_h_olte_functional_Y_product_start + S (1) = S ((S (0)) * pa_v_olte_functional_Y_product)) /\ exists pa_q_olte_functional_Y_product_start. pa_u_olte_functional_Y_product = pa_q_olte_functional_Y_product_start * S ((S (0)) * pa_v_olte_functional_Y_product) + (1))) /\ ((((exists pa_h_olte_functional_Y_product_terminal. pa_h_olte_functional_Y_product_terminal + S (Y) = S ((S (n)) * pa_v_olte_functional_Y_product)) /\ exists pa_q_olte_functional_Y_product_terminal. pa_u_olte_functional_Y_product = pa_q_olte_functional_Y_product_terminal * S ((S (n)) * pa_v_olte_functional_Y_product) + (Y))) /\ forall pa_i_olte_functional_Y_product. (exists pa_lt_olte_functional_Y_product_bound. pa_lt_olte_functional_Y_product_bound + S pa_i_olte_functional_Y_product = n) -> exists pa_p_olte_functional_Y_product pa_r_olte_functional_Y_product pa_s_olte_functional_Y_product. ((((exists pa_h_olte_functional_Y_product_factor. pa_h_olte_functional_Y_product_factor + S (pa_p_olte_functional_Y_product) = S ((S (pa_i_olte_functional_Y_product)) * pa_c_olte_functional_Y)) /\ exists pa_q_olte_functional_Y_product_factor. pa_b_olte_functional_Y = pa_q_olte_functional_Y_product_factor * S ((S (pa_i_olte_functional_Y_product)) * pa_c_olte_functional_Y) + (pa_p_olte_functional_Y_product))) /\ ((((exists pa_h_olte_functional_Y_product_partial. pa_h_olte_functional_Y_product_partial + S (pa_r_olte_functional_Y_product) = S ((S (pa_i_olte_functional_Y_product)) * pa_v_olte_functional_Y_product)) /\ exists pa_q_olte_functional_Y_product_partial. pa_u_olte_functional_Y_product = pa_q_olte_functional_Y_product_partial * S ((S (pa_i_olte_functional_Y_product)) * pa_v_olte_functional_Y_product) + (pa_r_olte_functional_Y_product))) /\ ((((exists pa_h_olte_functional_Y_product_successor. pa_h_olte_functional_Y_product_successor + S (pa_s_olte_functional_Y_product) = S ((S (S pa_i_olte_functional_Y_product)) * pa_v_olte_functional_Y_product)) /\ exists pa_q_olte_functional_Y_product_successor. pa_u_olte_functional_Y_product = pa_q_olte_functional_Y_product_successor * S ((S (S pa_i_olte_functional_Y_product)) * pa_v_olte_functional_Y_product) + (pa_s_olte_functional_Y_product))) /\ pa_s_olte_functional_Y_product = pa_r_olte_functional_Y_product * pa_p_olte_functional_Y_product)))))))) -> X = Y + E -> D = E

Complete tactic proof in conservative notation

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

41 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro n
  4. L4
    intro A
  5. L5
    intro B
  6. L6
    intro D
  7. L7
    intro X
  8. L8
    intro Y
  9. L9
    intro E
  10. L10
    intro hA
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hB
  2. L12
    intro hD
  3. L13
    intro hX
  4. L14
    intro hY
  5. L15
    intro hE
03Establish hAXL16–23

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

  1. L16
    have hAX : A = X
  2. L17
    specialize pow_functional (a)
  3. L18
    specialize pow_functional (n)
  4. L19
    specialize pow_functional (A)
  5. L20
    specialize pow_functional (X)
  6. L21
    apply pow_functional
  7. L22
    exact hA
  8. L23
    exact hX
04Establish hBYL24–33

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

  1. L24
    have hBY : B = Y
  2. L25
    specialize pow_functional (b)
  3. L26
    specialize pow_functional (n)
  4. L27
    specialize pow_functional (B)
  5. L28
    specialize pow_functional (Y)
  6. L29
    apply pow_functional
  7. L30
    exact hB
  8. L31
    exact hY
  9. L32
    specialize add_left_cancel (Y)
  10. L33
    specialize add_left_cancel (D)
05Use earlier factsL34–35

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

  1. L34
    specialize add_left_cancel (E)
  2. L35
    apply add_left_cancel
06Calculate and transport equalitiesL36–39

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

  1. L36
    trans X
  2. L37
    symm
  3. L38
    rewrite hAX at hD
  4. L39
    rewrite hBY at hD
07Use earlier factsL40–41

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

  1. L40
    exact hD
  2. L41
    exact hE

Library-wide reading audit

Original defined command ledger · 41 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro n
  4. 0004intro A
  5. 0005intro B
  6. 0006intro D
  7. 0007intro X
  8. 0008intro Y
  9. 0009intro E
  10. 0010intro hA
  11. 0011intro hB
  12. 0012intro hD
  13. 0013intro hX
  14. 0014intro hY
  15. 0015intro hE
  16. 0016have hAX : A = X
  17. 0017specialize pow_functional (a)
  18. 0018specialize pow_functional (n)
  19. 0019specialize pow_functional (A)
  20. 0020specialize pow_functional (X)
  21. 0021apply pow_functional
  22. 0022exact hA
  23. 0023exact hX
  24. 0024have hBY : B = Y
  25. 0025specialize pow_functional (b)
  26. 0026specialize pow_functional (n)
  27. 0027specialize pow_functional (B)
  28. 0028specialize pow_functional (Y)
  29. 0029apply pow_functional
  30. 0030exact hB
  31. 0031exact hY
  32. 0032specialize add_left_cancel (Y)
  33. 0033specialize add_left_cancel (D)
  34. 0034specialize add_left_cancel (E)
  35. 0035apply add_left_cancel
  36. 0036trans X
  37. 0037symm
  38. 0038rewrite hAX at hD
  39. 0039rewrite hBY at hD
  40. 0040exact hD
  41. 0041exact hE