EL0019

lte_prime_power_valuation_exact

The actual e-th power of a prime has exactly valuation e, including exponent zero.

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. ∀ e. ∀ P. ¬p = 1 ∧ (∀ x. ∀ y. p = x · y → x = 1 ∨ y = 1) → Pow(p,e,P) → BoundedPowerValuation(p,P,P,e)

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

Definition DAG

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

Actual proof prerequisites

prime_valuation_exponent_eq_transport · checked external prerequisiteprime_power_valuation_pow · checked external prerequisiteprime_nonzero · checked external prerequisitelte_prime_self_valuationmul_one · checked external prerequisite
Original expanded first-order statement 
forall p e P. (~((p) = 1) /\ forall pvs_left_prime_power_prime pvs_right_prime_power_prime. (p) = pvs_left_prime_power_prime * pvs_right_prime_power_prime -> pvs_left_prime_power_prime = 1 \/ pvs_right_prime_power_prime = 1) -> (exists pa_b_olte_prime_power_source pa_c_olte_prime_power_source. ((forall pa_i_olte_prime_power_source_repeat. (exists pa_lt_olte_prime_power_source_repeat_bound. pa_lt_olte_prime_power_source_repeat_bound + S pa_i_olte_prime_power_source_repeat = e) -> (((exists pa_h_olte_prime_power_source_repeat_decoded. pa_h_olte_prime_power_source_repeat_decoded + S (p) = S ((S (pa_i_olte_prime_power_source_repeat)) * pa_c_olte_prime_power_source)) /\ exists pa_q_olte_prime_power_source_repeat_decoded. pa_b_olte_prime_power_source = pa_q_olte_prime_power_source_repeat_decoded * S ((S (pa_i_olte_prime_power_source_repeat)) * pa_c_olte_prime_power_source) + (p)))) /\ (exists pa_u_olte_prime_power_source_product pa_v_olte_prime_power_source_product. ((((exists pa_h_olte_prime_power_source_product_start. pa_h_olte_prime_power_source_product_start + S (1) = S ((S (0)) * pa_v_olte_prime_power_source_product)) /\ exists pa_q_olte_prime_power_source_product_start. pa_u_olte_prime_power_source_product = pa_q_olte_prime_power_source_product_start * S ((S (0)) * pa_v_olte_prime_power_source_product) + (1))) /\ ((((exists pa_h_olte_prime_power_source_product_terminal. pa_h_olte_prime_power_source_product_terminal + S (P) = S ((S (e)) * pa_v_olte_prime_power_source_product)) /\ exists pa_q_olte_prime_power_source_product_terminal. pa_u_olte_prime_power_source_product = pa_q_olte_prime_power_source_product_terminal * S ((S (e)) * pa_v_olte_prime_power_source_product) + (P))) /\ forall pa_i_olte_prime_power_source_product. (exists pa_lt_olte_prime_power_source_product_bound. pa_lt_olte_prime_power_source_product_bound + S pa_i_olte_prime_power_source_product = e) -> exists pa_p_olte_prime_power_source_product pa_r_olte_prime_power_source_product pa_s_olte_prime_power_source_product. ((((exists pa_h_olte_prime_power_source_product_factor. pa_h_olte_prime_power_source_product_factor + S (pa_p_olte_prime_power_source_product) = S ((S (pa_i_olte_prime_power_source_product)) * pa_c_olte_prime_power_source)) /\ exists pa_q_olte_prime_power_source_product_factor. pa_b_olte_prime_power_source = pa_q_olte_prime_power_source_product_factor * S ((S (pa_i_olte_prime_power_source_product)) * pa_c_olte_prime_power_source) + (pa_p_olte_prime_power_source_product))) /\ ((((exists pa_h_olte_prime_power_source_product_partial. pa_h_olte_prime_power_source_product_partial + S (pa_r_olte_prime_power_source_product) = S ((S (pa_i_olte_prime_power_source_product)) * pa_v_olte_prime_power_source_product)) /\ exists pa_q_olte_prime_power_source_product_partial. pa_u_olte_prime_power_source_product = pa_q_olte_prime_power_source_product_partial * S ((S (pa_i_olte_prime_power_source_product)) * pa_v_olte_prime_power_source_product) + (pa_r_olte_prime_power_source_product))) /\ ((((exists pa_h_olte_prime_power_source_product_successor. pa_h_olte_prime_power_source_product_successor + S (pa_s_olte_prime_power_source_product) = S ((S (S pa_i_olte_prime_power_source_product)) * pa_v_olte_prime_power_source_product)) /\ exists pa_q_olte_prime_power_source_product_successor. pa_u_olte_prime_power_source_product = pa_q_olte_prime_power_source_product_successor * S ((S (S pa_i_olte_prime_power_source_product)) * pa_v_olte_prime_power_source_product) + (pa_s_olte_prime_power_source_product))) /\ pa_s_olte_prime_power_source_product = pa_r_olte_prime_power_source_product * pa_p_olte_prime_power_source_product)))))))) -> (((exists bpd_gap_pvs_prime_power_result_selected_bound. bpd_gap_pvs_prime_power_result_selected_bound + (e) = (P)) /\ (exists bpvi_result_pvs_prime_power_result_selected. ((exists bpvi_b_pvs_prime_power_result_selected_power bpvi_c_pvs_prime_power_result_selected_power. ((forall bpvi_i_pvs_prime_power_result_selected_power. (exists bpvi_repeat_gap_pvs_prime_power_result_selected_power. bpvi_repeat_gap_pvs_prime_power_result_selected_power + S bpvi_i_pvs_prime_power_result_selected_power = e) -> (((exists bpvi_h_pvs_prime_power_result_selected_power_repeat. bpvi_h_pvs_prime_power_result_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_prime_power_result_selected_power)) * bpvi_c_pvs_prime_power_result_selected_power)) /\ exists bpvi_q_pvs_prime_power_result_selected_power_repeat. bpvi_b_pvs_prime_power_result_selected_power = bpvi_q_pvs_prime_power_result_selected_power_repeat * S ((S (bpvi_i_pvs_prime_power_result_selected_power)) * bpvi_c_pvs_prime_power_result_selected_power) + (p)))) /\ (exists bpvi_u_pvs_prime_power_result_selected_power bpvi_v_pvs_prime_power_result_selected_power. ((((exists bpvi_h_pvs_prime_power_result_selected_power_start. bpvi_h_pvs_prime_power_result_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_prime_power_result_selected_power)) /\ exists bpvi_q_pvs_prime_power_result_selected_power_start. bpvi_u_pvs_prime_power_result_selected_power = bpvi_q_pvs_prime_power_result_selected_power_start * S ((S (0)) * bpvi_v_pvs_prime_power_result_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_prime_power_result_selected_power_terminal. bpvi_h_pvs_prime_power_result_selected_power_terminal + S (bpvi_result_pvs_prime_power_result_selected) = S ((S (e)) * bpvi_v_pvs_prime_power_result_selected_power)) /\ exists bpvi_q_pvs_prime_power_result_selected_power_terminal. bpvi_u_pvs_prime_power_result_selected_power = bpvi_q_pvs_prime_power_result_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_prime_power_result_selected_power) + (bpvi_result_pvs_prime_power_result_selected))) /\ forall bpvi_j_pvs_prime_power_result_selected_power. (exists bpvi_product_gap_pvs_prime_power_result_selected_power. bpvi_product_gap_pvs_prime_power_result_selected_power + S bpvi_j_pvs_prime_power_result_selected_power = e) -> exists bpvi_factor_pvs_prime_power_result_selected_power bpvi_partial_pvs_prime_power_result_selected_power bpvi_successor_pvs_prime_power_result_selected_power. ((((exists bpvi_h_pvs_prime_power_result_selected_power_factor. bpvi_h_pvs_prime_power_result_selected_power_factor + S (bpvi_factor_pvs_prime_power_result_selected_power) = S ((S (bpvi_j_pvs_prime_power_result_selected_power)) * bpvi_c_pvs_prime_power_result_selected_power)) /\ exists bpvi_q_pvs_prime_power_result_selected_power_factor. bpvi_b_pvs_prime_power_result_selected_power = bpvi_q_pvs_prime_power_result_selected_power_factor * S ((S (bpvi_j_pvs_prime_power_result_selected_power)) * bpvi_c_pvs_prime_power_result_selected_power) + (bpvi_factor_pvs_prime_power_result_selected_power))) /\ ((((exists bpvi_h_pvs_prime_power_result_selected_power_partial. bpvi_h_pvs_prime_power_result_selected_power_partial + S (bpvi_partial_pvs_prime_power_result_selected_power) = S ((S (bpvi_j_pvs_prime_power_result_selected_power)) * bpvi_v_pvs_prime_power_result_selected_power)) /\ exists bpvi_q_pvs_prime_power_result_selected_power_partial. bpvi_u_pvs_prime_power_result_selected_power = bpvi_q_pvs_prime_power_result_selected_power_partial * S ((S (bpvi_j_pvs_prime_power_result_selected_power)) * bpvi_v_pvs_prime_power_result_selected_power) + (bpvi_partial_pvs_prime_power_result_selected_power))) /\ ((((exists bpvi_h_pvs_prime_power_result_selected_power_successor. bpvi_h_pvs_prime_power_result_selected_power_successor + S (bpvi_successor_pvs_prime_power_result_selected_power) = S ((S (S bpvi_j_pvs_prime_power_result_selected_power)) * bpvi_v_pvs_prime_power_result_selected_power)) /\ exists bpvi_q_pvs_prime_power_result_selected_power_successor. bpvi_u_pvs_prime_power_result_selected_power = bpvi_q_pvs_prime_power_result_selected_power_successor * S ((S (S bpvi_j_pvs_prime_power_result_selected_power)) * bpvi_v_pvs_prime_power_result_selected_power) + (bpvi_successor_pvs_prime_power_result_selected_power))) /\ bpvi_successor_pvs_prime_power_result_selected_power = bpvi_partial_pvs_prime_power_result_selected_power * bpvi_factor_pvs_prime_power_result_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_prime_power_result_selected. P = bpvi_result_pvs_prime_power_result_selected * bpvi_divisor_factor_pvs_prime_power_result_selected))) /\ forall bpd_candidate_pvs_prime_power_result. (exists bpd_gap_pvs_prime_power_result_candidate_bound. bpd_gap_pvs_prime_power_result_candidate_bound + (bpd_candidate_pvs_prime_power_result) = (P)) -> (exists bpvi_result_pvs_prime_power_result_candidate. ((exists bpvi_b_pvs_prime_power_result_candidate_power bpvi_c_pvs_prime_power_result_candidate_power. ((forall bpvi_i_pvs_prime_power_result_candidate_power. (exists bpvi_repeat_gap_pvs_prime_power_result_candidate_power. bpvi_repeat_gap_pvs_prime_power_result_candidate_power + S bpvi_i_pvs_prime_power_result_candidate_power = bpd_candidate_pvs_prime_power_result) -> (((exists bpvi_h_pvs_prime_power_result_candidate_power_repeat. bpvi_h_pvs_prime_power_result_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_prime_power_result_candidate_power)) * bpvi_c_pvs_prime_power_result_candidate_power)) /\ exists bpvi_q_pvs_prime_power_result_candidate_power_repeat. bpvi_b_pvs_prime_power_result_candidate_power = bpvi_q_pvs_prime_power_result_candidate_power_repeat * S ((S (bpvi_i_pvs_prime_power_result_candidate_power)) * bpvi_c_pvs_prime_power_result_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_prime_power_result_candidate_power bpvi_v_pvs_prime_power_result_candidate_power. ((((exists bpvi_h_pvs_prime_power_result_candidate_power_start. bpvi_h_pvs_prime_power_result_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_prime_power_result_candidate_power)) /\ exists bpvi_q_pvs_prime_power_result_candidate_power_start. bpvi_u_pvs_prime_power_result_candidate_power = bpvi_q_pvs_prime_power_result_candidate_power_start * S ((S (0)) * bpvi_v_pvs_prime_power_result_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_prime_power_result_candidate_power_terminal. bpvi_h_pvs_prime_power_result_candidate_power_terminal + S (bpvi_result_pvs_prime_power_result_candidate) = S ((S (bpd_candidate_pvs_prime_power_result)) * bpvi_v_pvs_prime_power_result_candidate_power)) /\ exists bpvi_q_pvs_prime_power_result_candidate_power_terminal. bpvi_u_pvs_prime_power_result_candidate_power = bpvi_q_pvs_prime_power_result_candidate_power_terminal * S ((S (bpd_candidate_pvs_prime_power_result)) * bpvi_v_pvs_prime_power_result_candidate_power) + (bpvi_result_pvs_prime_power_result_candidate))) /\ forall bpvi_j_pvs_prime_power_result_candidate_power. (exists bpvi_product_gap_pvs_prime_power_result_candidate_power. bpvi_product_gap_pvs_prime_power_result_candidate_power + S bpvi_j_pvs_prime_power_result_candidate_power = bpd_candidate_pvs_prime_power_result) -> exists bpvi_factor_pvs_prime_power_result_candidate_power bpvi_partial_pvs_prime_power_result_candidate_power bpvi_successor_pvs_prime_power_result_candidate_power. ((((exists bpvi_h_pvs_prime_power_result_candidate_power_factor. bpvi_h_pvs_prime_power_result_candidate_power_factor + S (bpvi_factor_pvs_prime_power_result_candidate_power) = S ((S (bpvi_j_pvs_prime_power_result_candidate_power)) * bpvi_c_pvs_prime_power_result_candidate_power)) /\ exists bpvi_q_pvs_prime_power_result_candidate_power_factor. bpvi_b_pvs_prime_power_result_candidate_power = bpvi_q_pvs_prime_power_result_candidate_power_factor * S ((S (bpvi_j_pvs_prime_power_result_candidate_power)) * bpvi_c_pvs_prime_power_result_candidate_power) + (bpvi_factor_pvs_prime_power_result_candidate_power))) /\ ((((exists bpvi_h_pvs_prime_power_result_candidate_power_partial. bpvi_h_pvs_prime_power_result_candidate_power_partial + S (bpvi_partial_pvs_prime_power_result_candidate_power) = S ((S (bpvi_j_pvs_prime_power_result_candidate_power)) * bpvi_v_pvs_prime_power_result_candidate_power)) /\ exists bpvi_q_pvs_prime_power_result_candidate_power_partial. bpvi_u_pvs_prime_power_result_candidate_power = bpvi_q_pvs_prime_power_result_candidate_power_partial * S ((S (bpvi_j_pvs_prime_power_result_candidate_power)) * bpvi_v_pvs_prime_power_result_candidate_power) + (bpvi_partial_pvs_prime_power_result_candidate_power))) /\ ((((exists bpvi_h_pvs_prime_power_result_candidate_power_successor. bpvi_h_pvs_prime_power_result_candidate_power_successor + S (bpvi_successor_pvs_prime_power_result_candidate_power) = S ((S (S bpvi_j_pvs_prime_power_result_candidate_power)) * bpvi_v_pvs_prime_power_result_candidate_power)) /\ exists bpvi_q_pvs_prime_power_result_candidate_power_successor. bpvi_u_pvs_prime_power_result_candidate_power = bpvi_q_pvs_prime_power_result_candidate_power_successor * S ((S (S bpvi_j_pvs_prime_power_result_candidate_power)) * bpvi_v_pvs_prime_power_result_candidate_power) + (bpvi_successor_pvs_prime_power_result_candidate_power))) /\ bpvi_successor_pvs_prime_power_result_candidate_power = bpvi_partial_pvs_prime_power_result_candidate_power * bpvi_factor_pvs_prime_power_result_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_prime_power_result_candidate. P = bpvi_result_pvs_prime_power_result_candidate * bpvi_divisor_factor_pvs_prime_power_result_candidate)) -> (exists bpd_gap_pvs_prime_power_result_maximal. bpd_gap_pvs_prime_power_result_maximal + (bpd_candidate_pvs_prime_power_result) = (e)))

Complete tactic proof in conservative notation

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

27 script commands · 5 reading checkpoints · 0 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)
lte prime self valuation
01Fix variables and assumptionsL1–5

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

  1. L1
    intro p
  2. L2
    intro e
  3. L3
    intro P
  4. L4
    intro hp
  5. L5
    intro hpow
02Use earlier factsL6–15

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

  1. L6
    specialize prime_valuation_exponent_eq_transport (p)
  2. L7
    specialize prime_valuation_exponent_eq_transport (P)
  3. L8
    specialize prime_valuation_exponent_eq_transport (e * 1)
  4. L9
    specialize prime_valuation_exponent_eq_transport (e)
  5. L10
    apply prime_valuation_exponent_eq_transport
  6. L11
    apply mul_one
  7. L12
    specialize prime_power_valuation_pow (p)
  8. L13
    specialize prime_power_valuation_pow (p)
  9. L14
    specialize prime_power_valuation_pow (e)
  10. L15
    specialize prime_power_valuation_pow (1)
03Use earlier factsL16–18

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

  1. L16
    specialize prime_power_valuation_pow (P)
  2. L17
    apply prime_power_valuation_pow
  3. L18
    exact hp
04Fix variables and assumptionsL19–19

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

  1. L19
    intro hz
05Use earlier factsL20–27

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

  1. L20
    specialize prime_nonzero (p)
  2. L21
    apply prime_nonzero
  3. L22
    exact hp
  4. L23
    exact hz
  5. L24
    specialize lte_prime_self_valuation (p)
  6. L25
    apply lte_prime_self_valuation
  7. L26
    exact hp
  8. L27
    exact hpow

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro p
  2. 0002intro e
  3. 0003intro P
  4. 0004intro hp
  5. 0005intro hpow
  6. 0006specialize prime_valuation_exponent_eq_transport (p)
  7. 0007specialize prime_valuation_exponent_eq_transport (P)
  8. 0008specialize prime_valuation_exponent_eq_transport (e * 1)
  9. 0009specialize prime_valuation_exponent_eq_transport (e)
  10. 0010apply prime_valuation_exponent_eq_transport
  11. 0011apply mul_one
  12. 0012specialize prime_power_valuation_pow (p)
  13. 0013specialize prime_power_valuation_pow (p)
  14. 0014specialize prime_power_valuation_pow (e)
  15. 0015specialize prime_power_valuation_pow (1)
  16. 0016specialize prime_power_valuation_pow (P)
  17. 0017apply prime_power_valuation_pow
  18. 0018exact hp
  19. 0019intro hz
  20. 0020specialize prime_nonzero (p)
  21. 0021apply prime_nonzero
  22. 0022exact hp
  23. 0023exact hz
  24. 0024specialize lte_prime_self_valuation (p)
  25. 0025apply lte_prime_self_valuation
  26. 0026exact hp
  27. 0027exact hpow