SK0017

positive_power_prime_valuations_divisible

Every positive k-th power has every actual prime valuation divisible by k, with a constructed quotient valuation of its nonzero base.

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.

For n>1 the exponent gcd and a real beta table classify and witness all positive root degrees. The unit n=1 has a separate uniform certificate for every positive degree. Zero is excluded. NaturalSquarefreeDecomposition is deliberately distinct from the unrelated polynomial definition.

Exact theorem in conservative defined notation

∀ n. ∀ k. ∀ r. ¬n = 0 → ¬k = 0 → Pow(r,k,n) → PrimeValuationsDivisible(n,k)

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

Definition DAG

PrimeValuationsDivisible(n,k) · 1Pow(a,e,z) · 1BoundedPowerValuation(p,n,b,e) · 1

Actual proof prerequisites

positive_power_nonzero_basepower_valuation_exists · checked external prerequisiteprime_power_valuation_pow_value · checked external prerequisite
Original expanded first-order statement 
forall n k r. ~(n = 0) -> ~(k = 0) -> (exists pa_b_pvs_necessary_power pa_c_pvs_necessary_power. ((forall pa_i_pvs_necessary_power_repeat. (exists pa_lt_pvs_necessary_power_repeat_bound. pa_lt_pvs_necessary_power_repeat_bound + S pa_i_pvs_necessary_power_repeat = k) -> (((exists pa_h_pvs_necessary_power_repeat_decoded. pa_h_pvs_necessary_power_repeat_decoded + S (r) = S ((S (pa_i_pvs_necessary_power_repeat)) * pa_c_pvs_necessary_power)) /\ exists pa_q_pvs_necessary_power_repeat_decoded. pa_b_pvs_necessary_power = pa_q_pvs_necessary_power_repeat_decoded * S ((S (pa_i_pvs_necessary_power_repeat)) * pa_c_pvs_necessary_power) + (r)))) /\ (exists pa_u_pvs_necessary_power_product pa_v_pvs_necessary_power_product. ((((exists pa_h_pvs_necessary_power_product_start. pa_h_pvs_necessary_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_necessary_power_product)) /\ exists pa_q_pvs_necessary_power_product_start. pa_u_pvs_necessary_power_product = pa_q_pvs_necessary_power_product_start * S ((S (0)) * pa_v_pvs_necessary_power_product) + (1))) /\ ((((exists pa_h_pvs_necessary_power_product_terminal. pa_h_pvs_necessary_power_product_terminal + S (n) = S ((S (k)) * pa_v_pvs_necessary_power_product)) /\ exists pa_q_pvs_necessary_power_product_terminal. pa_u_pvs_necessary_power_product = pa_q_pvs_necessary_power_product_terminal * S ((S (k)) * pa_v_pvs_necessary_power_product) + (n))) /\ forall pa_i_pvs_necessary_power_product. (exists pa_lt_pvs_necessary_power_product_bound. pa_lt_pvs_necessary_power_product_bound + S pa_i_pvs_necessary_power_product = k) -> exists pa_p_pvs_necessary_power_product pa_r_pvs_necessary_power_product pa_s_pvs_necessary_power_product. ((((exists pa_h_pvs_necessary_power_product_factor. pa_h_pvs_necessary_power_product_factor + S (pa_p_pvs_necessary_power_product) = S ((S (pa_i_pvs_necessary_power_product)) * pa_c_pvs_necessary_power)) /\ exists pa_q_pvs_necessary_power_product_factor. pa_b_pvs_necessary_power = pa_q_pvs_necessary_power_product_factor * S ((S (pa_i_pvs_necessary_power_product)) * pa_c_pvs_necessary_power) + (pa_p_pvs_necessary_power_product))) /\ ((((exists pa_h_pvs_necessary_power_product_partial. pa_h_pvs_necessary_power_product_partial + S (pa_r_pvs_necessary_power_product) = S ((S (pa_i_pvs_necessary_power_product)) * pa_v_pvs_necessary_power_product)) /\ exists pa_q_pvs_necessary_power_product_partial. pa_u_pvs_necessary_power_product = pa_q_pvs_necessary_power_product_partial * S ((S (pa_i_pvs_necessary_power_product)) * pa_v_pvs_necessary_power_product) + (pa_r_pvs_necessary_power_product))) /\ ((((exists pa_h_pvs_necessary_power_product_successor. pa_h_pvs_necessary_power_product_successor + S (pa_s_pvs_necessary_power_product) = S ((S (S pa_i_pvs_necessary_power_product)) * pa_v_pvs_necessary_power_product)) /\ exists pa_q_pvs_necessary_power_product_successor. pa_u_pvs_necessary_power_product = pa_q_pvs_necessary_power_product_successor * S ((S (S pa_i_pvs_necessary_power_product)) * pa_v_pvs_necessary_power_product) + (pa_s_pvs_necessary_power_product))) /\ pa_s_pvs_necessary_power_product = pa_r_pvs_necessary_power_product * pa_p_pvs_necessary_power_product)))))))) -> (forall ppf_prime_necessary_valuations ppf_exponent_necessary_valuations. (~((ppf_prime_necessary_valuations) = 1) /\ forall pvs_left_necessary_valuationsdomain pvs_right_necessary_valuationsdomain. (ppf_prime_necessary_valuations) = pvs_left_necessary_valuationsdomain * pvs_right_necessary_valuationsdomain -> pvs_left_necessary_valuationsdomain = 1 \/ pvs_right_necessary_valuationsdomain = 1) -> (((exists bpd_gap_pvs_necessary_valuationsvaluation_selected_bound. bpd_gap_pvs_necessary_valuationsvaluation_selected_bound + (ppf_exponent_necessary_valuations) = (n)) /\ (exists bpvi_result_pvs_necessary_valuationsvaluation_selected. ((exists bpvi_b_pvs_necessary_valuationsvaluation_selected_power bpvi_c_pvs_necessary_valuationsvaluation_selected_power. ((forall bpvi_i_pvs_necessary_valuationsvaluation_selected_power. (exists bpvi_repeat_gap_pvs_necessary_valuationsvaluation_selected_power. bpvi_repeat_gap_pvs_necessary_valuationsvaluation_selected_power + S bpvi_i_pvs_necessary_valuationsvaluation_selected_power = ppf_exponent_necessary_valuations) -> (((exists bpvi_h_pvs_necessary_valuationsvaluation_selected_power_repeat. bpvi_h_pvs_necessary_valuationsvaluation_selected_power_repeat + S (ppf_prime_necessary_valuations) = S ((S (bpvi_i_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_c_pvs_necessary_valuationsvaluation_selected_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_selected_power_repeat. bpvi_b_pvs_necessary_valuationsvaluation_selected_power = bpvi_q_pvs_necessary_valuationsvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_c_pvs_necessary_valuationsvaluation_selected_power) + (ppf_prime_necessary_valuations)))) /\ (exists bpvi_u_pvs_necessary_valuationsvaluation_selected_power bpvi_v_pvs_necessary_valuationsvaluation_selected_power. ((((exists bpvi_h_pvs_necessary_valuationsvaluation_selected_power_start. bpvi_h_pvs_necessary_valuationsvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_selected_power_start. bpvi_u_pvs_necessary_valuationsvaluation_selected_power = bpvi_q_pvs_necessary_valuationsvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_necessary_valuationsvaluation_selected_power_terminal. bpvi_h_pvs_necessary_valuationsvaluation_selected_power_terminal + S (bpvi_result_pvs_necessary_valuationsvaluation_selected) = S ((S (ppf_exponent_necessary_valuations)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_selected_power_terminal. bpvi_u_pvs_necessary_valuationsvaluation_selected_power = bpvi_q_pvs_necessary_valuationsvaluation_selected_power_terminal * S ((S (ppf_exponent_necessary_valuations)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power) + (bpvi_result_pvs_necessary_valuationsvaluation_selected))) /\ forall bpvi_j_pvs_necessary_valuationsvaluation_selected_power. (exists bpvi_product_gap_pvs_necessary_valuationsvaluation_selected_power. bpvi_product_gap_pvs_necessary_valuationsvaluation_selected_power + S bpvi_j_pvs_necessary_valuationsvaluation_selected_power = ppf_exponent_necessary_valuations) -> exists bpvi_factor_pvs_necessary_valuationsvaluation_selected_power bpvi_partial_pvs_necessary_valuationsvaluation_selected_power bpvi_successor_pvs_necessary_valuationsvaluation_selected_power. ((((exists bpvi_h_pvs_necessary_valuationsvaluation_selected_power_factor. bpvi_h_pvs_necessary_valuationsvaluation_selected_power_factor + S (bpvi_factor_pvs_necessary_valuationsvaluation_selected_power) = S ((S (bpvi_j_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_c_pvs_necessary_valuationsvaluation_selected_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_selected_power_factor. bpvi_b_pvs_necessary_valuationsvaluation_selected_power = bpvi_q_pvs_necessary_valuationsvaluation_selected_power_factor * S ((S (bpvi_j_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_c_pvs_necessary_valuationsvaluation_selected_power) + (bpvi_factor_pvs_necessary_valuationsvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_necessary_valuationsvaluation_selected_power_partial. bpvi_h_pvs_necessary_valuationsvaluation_selected_power_partial + S (bpvi_partial_pvs_necessary_valuationsvaluation_selected_power) = S ((S (bpvi_j_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_selected_power_partial. bpvi_u_pvs_necessary_valuationsvaluation_selected_power = bpvi_q_pvs_necessary_valuationsvaluation_selected_power_partial * S ((S (bpvi_j_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power) + (bpvi_partial_pvs_necessary_valuationsvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_necessary_valuationsvaluation_selected_power_successor. bpvi_h_pvs_necessary_valuationsvaluation_selected_power_successor + S (bpvi_successor_pvs_necessary_valuationsvaluation_selected_power) = S ((S (S bpvi_j_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_selected_power_successor. bpvi_u_pvs_necessary_valuationsvaluation_selected_power = bpvi_q_pvs_necessary_valuationsvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_necessary_valuationsvaluation_selected_power)) * bpvi_v_pvs_necessary_valuationsvaluation_selected_power) + (bpvi_successor_pvs_necessary_valuationsvaluation_selected_power))) /\ bpvi_successor_pvs_necessary_valuationsvaluation_selected_power = bpvi_partial_pvs_necessary_valuationsvaluation_selected_power * bpvi_factor_pvs_necessary_valuationsvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_necessary_valuationsvaluation_selected. n = bpvi_result_pvs_necessary_valuationsvaluation_selected * bpvi_divisor_factor_pvs_necessary_valuationsvaluation_selected))) /\ forall bpd_candidate_pvs_necessary_valuationsvaluation. (exists bpd_gap_pvs_necessary_valuationsvaluation_candidate_bound. bpd_gap_pvs_necessary_valuationsvaluation_candidate_bound + (bpd_candidate_pvs_necessary_valuationsvaluation) = (n)) -> (exists bpvi_result_pvs_necessary_valuationsvaluation_candidate. ((exists bpvi_b_pvs_necessary_valuationsvaluation_candidate_power bpvi_c_pvs_necessary_valuationsvaluation_candidate_power. ((forall bpvi_i_pvs_necessary_valuationsvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_necessary_valuationsvaluation_candidate_power. bpvi_repeat_gap_pvs_necessary_valuationsvaluation_candidate_power + S bpvi_i_pvs_necessary_valuationsvaluation_candidate_power = bpd_candidate_pvs_necessary_valuationsvaluation) -> (((exists bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_repeat. bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_repeat + S (ppf_prime_necessary_valuations) = S ((S (bpvi_i_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_c_pvs_necessary_valuationsvaluation_candidate_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_repeat. bpvi_b_pvs_necessary_valuationsvaluation_candidate_power = bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_c_pvs_necessary_valuationsvaluation_candidate_power) + (ppf_prime_necessary_valuations)))) /\ (exists bpvi_u_pvs_necessary_valuationsvaluation_candidate_power bpvi_v_pvs_necessary_valuationsvaluation_candidate_power. ((((exists bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_start. bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_start. bpvi_u_pvs_necessary_valuationsvaluation_candidate_power = bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_terminal. bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_terminal + S (bpvi_result_pvs_necessary_valuationsvaluation_candidate) = S ((S (bpd_candidate_pvs_necessary_valuationsvaluation)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_terminal. bpvi_u_pvs_necessary_valuationsvaluation_candidate_power = bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_necessary_valuationsvaluation)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power) + (bpvi_result_pvs_necessary_valuationsvaluation_candidate))) /\ forall bpvi_j_pvs_necessary_valuationsvaluation_candidate_power. (exists bpvi_product_gap_pvs_necessary_valuationsvaluation_candidate_power. bpvi_product_gap_pvs_necessary_valuationsvaluation_candidate_power + S bpvi_j_pvs_necessary_valuationsvaluation_candidate_power = bpd_candidate_pvs_necessary_valuationsvaluation) -> exists bpvi_factor_pvs_necessary_valuationsvaluation_candidate_power bpvi_partial_pvs_necessary_valuationsvaluation_candidate_power bpvi_successor_pvs_necessary_valuationsvaluation_candidate_power. ((((exists bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_factor. bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_factor + S (bpvi_factor_pvs_necessary_valuationsvaluation_candidate_power) = S ((S (bpvi_j_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_c_pvs_necessary_valuationsvaluation_candidate_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_factor. bpvi_b_pvs_necessary_valuationsvaluation_candidate_power = bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_c_pvs_necessary_valuationsvaluation_candidate_power) + (bpvi_factor_pvs_necessary_valuationsvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_partial. bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_partial + S (bpvi_partial_pvs_necessary_valuationsvaluation_candidate_power) = S ((S (bpvi_j_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_partial. bpvi_u_pvs_necessary_valuationsvaluation_candidate_power = bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power) + (bpvi_partial_pvs_necessary_valuationsvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_successor. bpvi_h_pvs_necessary_valuationsvaluation_candidate_power_successor + S (bpvi_successor_pvs_necessary_valuationsvaluation_candidate_power) = S ((S (S bpvi_j_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power)) /\ exists bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_successor. bpvi_u_pvs_necessary_valuationsvaluation_candidate_power = bpvi_q_pvs_necessary_valuationsvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_necessary_valuationsvaluation_candidate_power)) * bpvi_v_pvs_necessary_valuationsvaluation_candidate_power) + (bpvi_successor_pvs_necessary_valuationsvaluation_candidate_power))) /\ bpvi_successor_pvs_necessary_valuationsvaluation_candidate_power = bpvi_partial_pvs_necessary_valuationsvaluation_candidate_power * bpvi_factor_pvs_necessary_valuationsvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_necessary_valuationsvaluation_candidate. n = bpvi_result_pvs_necessary_valuationsvaluation_candidate * bpvi_divisor_factor_pvs_necessary_valuationsvaluation_candidate)) -> (exists bpd_gap_pvs_necessary_valuationsvaluation_maximal. bpd_gap_pvs_necessary_valuationsvaluation_maximal + (bpd_candidate_pvs_necessary_valuationsvaluation) = (ppf_exponent_necessary_valuations))) -> (exists pvs_factor_necessary_valuationsdivides. (ppf_exponent_necessary_valuations) = (k) * pvs_factor_necessary_valuationsdivides))

Complete tactic proof in conservative notation

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

38 script commands · 8 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.

Named ingredients (1)
positive power nonzero base
01Fix variables and assumptionsL1–6

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

  1. L1
    intro n
  2. L2
    intro k
  3. L3
    intro r
  4. L4
    intro hn
  5. L5
    intro hk
  6. L6
    intro hpow
02Establish hrL7–16

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

  1. L7
    have hr : ~(r = 0)
  2. L8
    intro hz
  3. L9
    specialize positive_power_nonzero_base (n)
  4. L10
    specialize positive_power_nonzero_base (k)
  5. L11
    specialize positive_power_nonzero_base (r)
  6. L12
    apply positive_power_nonzero_base
  7. L13
    exact hn
  8. L14
    exact hk
  9. L15
    exact hpow
  10. L16
    exact hz
03Fix variables and assumptionsL17–20

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

  1. L17
    intro p
  2. L18
    intro e
  3. L19
    intro hp
  4. L20
    intro hval
04Establish hbaseL21–24

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

  1. L21
    have hbase : ∃ f. BoundedPowerValuation(p,r,r,f)Definitions: BoundedPowerValuation(p,r,r,f)Original native command in the exact edition
  2. L22
    specialize power_valuation_exists (p)
  3. L23
    specialize power_valuation_exists (r)
  4. L24
    apply power_valuation_exists
05Separate the logical casesL25–25

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

  1. L25
    cases hbase
06Construct an explicit witnessL26–26

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

  1. L26
    exists x
07Use earlier factsL27–36

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

  1. L27
    specialize prime_power_valuation_pow_value (p)
  2. L28
    specialize prime_power_valuation_pow_value (r)
  3. L29
    specialize prime_power_valuation_pow_value (k)
  4. L30
    specialize prime_power_valuation_pow_value (x)
  5. L31
    specialize prime_power_valuation_pow_value (n)
  6. L32
    specialize prime_power_valuation_pow_value (e)
  7. L33
    apply prime_power_valuation_pow_value
  8. L34
    exact hp
  9. L35
    exact hr
  10. L36
    exact hbase_witness
08Use earlier factsL37–38

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

  1. L37
    exact hpow
  2. L38
    exact hval

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro n
  2. 0002intro k
  3. 0003intro r
  4. 0004intro hn
  5. 0005intro hk
  6. 0006intro hpow
  7. 0007have hr : ~(r = 0)
  8. 0008intro hz
  9. 0009specialize positive_power_nonzero_base (n)
  10. 0010specialize positive_power_nonzero_base (k)
  11. 0011specialize positive_power_nonzero_base (r)
  12. 0012apply positive_power_nonzero_base
  13. 0013exact hn
  14. 0014exact hk
  15. 0015exact hpow
  16. 0016exact hz
  17. 0017intro p
  18. 0018intro e
  19. 0019intro hp
  20. 0020intro hval
  21. 0021have hbase : ∃ f. BoundedPowerValuation(p,r,r,f)
  22. 0022specialize power_valuation_exists (p)
  23. 0023specialize power_valuation_exists (r)
  24. 0024apply power_valuation_exists
  25. 0025cases hbase
  26. 0026exists x
  27. 0027specialize prime_power_valuation_pow_value (p)
  28. 0028specialize prime_power_valuation_pow_value (r)
  29. 0029specialize prime_power_valuation_pow_value (k)
  30. 0030specialize prime_power_valuation_pow_value (x)
  31. 0031specialize prime_power_valuation_pow_value (n)
  32. 0032specialize prime_power_valuation_pow_value (e)
  33. 0033apply prime_power_valuation_pow_value
  34. 0034exact hp
  35. 0035exact hr
  36. 0036exact hbase_witness
  37. 0037exact hpow
  38. 0038exact hval