PV0008 — prime_divisor_of_prime_power

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.

Exact expanded first-order arithmetic statement

forall p q k z. (~((p) = 1) /\ forall pvs_left_prime_power_base pvs_right_prime_power_base. (p) = pvs_left_prime_power_base * pvs_right_prime_power_base -> pvs_left_prime_power_base = 1 \/ pvs_right_prime_power_base = 1) -> (~((q) = 1) /\ forall pvs_left_prime_power_divisor pvs_right_prime_power_divisor. (q) = pvs_left_prime_power_divisor * pvs_right_prime_power_divisor -> pvs_left_prime_power_divisor = 1 \/ pvs_right_prime_power_divisor = 1) -> (exists pa_b_pvs_prime_power_value pa_c_pvs_prime_power_value. ((forall pa_i_pvs_prime_power_value_repeat. (exists pa_lt_pvs_prime_power_value_repeat_bound. pa_lt_pvs_prime_power_value_repeat_bound + S pa_i_pvs_prime_power_value_repeat = k) -> (((exists pa_h_pvs_prime_power_value_repeat_decoded. pa_h_pvs_prime_power_value_repeat_decoded + S (p) = S ((S (pa_i_pvs_prime_power_value_repeat)) * pa_c_pvs_prime_power_value)) /\ exists pa_q_pvs_prime_power_value_repeat_decoded. pa_b_pvs_prime_power_value = pa_q_pvs_prime_power_value_repeat_decoded * S ((S (pa_i_pvs_prime_power_value_repeat)) * pa_c_pvs_prime_power_value) + (p)))) /\ (exists pa_u_pvs_prime_power_value_product pa_v_pvs_prime_power_value_product. ((((exists pa_h_pvs_prime_power_value_product_start. pa_h_pvs_prime_power_value_product_start + S (1) = S ((S (0)) * pa_v_pvs_prime_power_value_product)) /\ exists pa_q_pvs_prime_power_value_product_start. pa_u_pvs_prime_power_value_product = pa_q_pvs_prime_power_value_product_start * S ((S (0)) * pa_v_pvs_prime_power_value_product) + (1))) /\ ((((exists pa_h_pvs_prime_power_value_product_terminal. pa_h_pvs_prime_power_value_product_terminal + S (z) = S ((S (k)) * pa_v_pvs_prime_power_value_product)) /\ exists pa_q_pvs_prime_power_value_product_terminal. pa_u_pvs_prime_power_value_product = pa_q_pvs_prime_power_value_product_terminal * S ((S (k)) * pa_v_pvs_prime_power_value_product) + (z))) /\ forall pa_i_pvs_prime_power_value_product. (exists pa_lt_pvs_prime_power_value_product_bound. pa_lt_pvs_prime_power_value_product_bound + S pa_i_pvs_prime_power_value_product = k) -> exists pa_p_pvs_prime_power_value_product pa_r_pvs_prime_power_value_product pa_s_pvs_prime_power_value_product. ((((exists pa_h_pvs_prime_power_value_product_factor. pa_h_pvs_prime_power_value_product_factor + S (pa_p_pvs_prime_power_value_product) = S ((S (pa_i_pvs_prime_power_value_product)) * pa_c_pvs_prime_power_value)) /\ exists pa_q_pvs_prime_power_value_product_factor. pa_b_pvs_prime_power_value = pa_q_pvs_prime_power_value_product_factor * S ((S (pa_i_pvs_prime_power_value_product)) * pa_c_pvs_prime_power_value) + (pa_p_pvs_prime_power_value_product))) /\ ((((exists pa_h_pvs_prime_power_value_product_partial. pa_h_pvs_prime_power_value_product_partial + S (pa_r_pvs_prime_power_value_product) = S ((S (pa_i_pvs_prime_power_value_product)) * pa_v_pvs_prime_power_value_product)) /\ exists pa_q_pvs_prime_power_value_product_partial. pa_u_pvs_prime_power_value_product = pa_q_pvs_prime_power_value_product_partial * S ((S (pa_i_pvs_prime_power_value_product)) * pa_v_pvs_prime_power_value_product) + (pa_r_pvs_prime_power_value_product))) /\ ((((exists pa_h_pvs_prime_power_value_product_successor. pa_h_pvs_prime_power_value_product_successor + S (pa_s_pvs_prime_power_value_product) = S ((S (S pa_i_pvs_prime_power_value_product)) * pa_v_pvs_prime_power_value_product)) /\ exists pa_q_pvs_prime_power_value_product_successor. pa_u_pvs_prime_power_value_product = pa_q_pvs_prime_power_value_product_successor * S ((S (S pa_i_pvs_prime_power_value_product)) * pa_v_pvs_prime_power_value_product) + (pa_s_pvs_prime_power_value_product))) /\ pa_s_pvs_prime_power_value_product = pa_r_pvs_prime_power_value_product * pa_p_pvs_prime_power_value_product)))))))) -> (exists pvs_factor_prime_power_divides. (z) = (q) * pvs_factor_prime_power_divides) -> q = p

Constructive proof overview

Generated structural guide

Every actual prime divisor of a witnessed prime power is its base prime.

The unchanged tactic script uses 6 declared prerequisites and contains 41 exact native proof lines.

Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

eq_decidable Stable theorem; checked-use authorized prime_nonzero Stable theorem; checked-use authorized one_le_of_ne_zero Stable theorem; checked-use authorized pow_nonzero_of_one_le Alpha theorem; checked-use authorized PV0007 prime_valuation_distinct_prime_power_zero PV0003 prime_valuation_nondivisor_of_zero

Direct dependents

PV0012 prime_valuation_support_append_full_power

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

41 script commands · 11 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.

Named ingredients (2)

prime valuation distinct prime power zero prime valuation nondivisor of zero

01Fix variables and assumptionsL1–8

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

L1
intro p
L2
intro q
L3
intro k
L4
intro z
L5
intro hp
L6
intro hq
L7
intro hpow
L8
intro hdiv

02Use earlier factsL9–10