PV0004

prime_power_valuation_pow_value

The exact valuation of any witnessed nonnegative power is its exponent times the base valuation; zero powers are included.

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.

This is a shared constructive tool, not an additional major blueprint goal. The list covers every prime divisor, has no repeated primes, and contains actual prime-power values. One uses the empty support; zero is excluded.

Exact theorem in conservative defined notation

∀ p. ∀ a. ∀ k. ∀ e. ∀ z. ∀ f. Prime(p) → ¬a = 0 → BoundedPowerValuation(p,a,a,e) → Pow(a,k,z) → BoundedPowerValuation(p,z,z,f) → f = k · e

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

Definition DAG

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

Actual proof prerequisites

pow_zero · checked external prerequisiteprime_power_valuation_one_zero · checked external prerequisitemul_zero_left · checked external prerequisitepow_successor_decompose · checked external prerequisitepower_valuation_exists · checked external prerequisiteone_le_of_ne_zero · checked external prerequisitepow_nonzero_of_one_le · checked external prerequisitepower_valuation_value_eq_transport · checked external prerequisiteprime_power_valuation_mul · checked external prerequisitemul_succ_left · checked external prerequisite
Original expanded first-order statement 
forall p a k e z f. (~((p) = 1) /\ forall pvs_left_pow_domain pvs_right_pow_domain. (p) = pvs_left_pow_domain * pvs_right_pow_domain -> pvs_left_pow_domain = 1 \/ pvs_right_pow_domain = 1) -> ~(a = 0) -> (((exists bpd_gap_pvs_pow_base_selected_bound. bpd_gap_pvs_pow_base_selected_bound + (e) = (a)) /\ (exists bpvi_result_pvs_pow_base_selected. ((exists bpvi_b_pvs_pow_base_selected_power bpvi_c_pvs_pow_base_selected_power. ((forall bpvi_i_pvs_pow_base_selected_power. (exists bpvi_repeat_gap_pvs_pow_base_selected_power. bpvi_repeat_gap_pvs_pow_base_selected_power + S bpvi_i_pvs_pow_base_selected_power = e) -> (((exists bpvi_h_pvs_pow_base_selected_power_repeat. bpvi_h_pvs_pow_base_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_pow_base_selected_power)) * bpvi_c_pvs_pow_base_selected_power)) /\ exists bpvi_q_pvs_pow_base_selected_power_repeat. bpvi_b_pvs_pow_base_selected_power = bpvi_q_pvs_pow_base_selected_power_repeat * S ((S (bpvi_i_pvs_pow_base_selected_power)) * bpvi_c_pvs_pow_base_selected_power) + (p)))) /\ (exists bpvi_u_pvs_pow_base_selected_power bpvi_v_pvs_pow_base_selected_power. ((((exists bpvi_h_pvs_pow_base_selected_power_start. bpvi_h_pvs_pow_base_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_pow_base_selected_power)) /\ exists bpvi_q_pvs_pow_base_selected_power_start. bpvi_u_pvs_pow_base_selected_power = bpvi_q_pvs_pow_base_selected_power_start * S ((S (0)) * bpvi_v_pvs_pow_base_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_pow_base_selected_power_terminal. bpvi_h_pvs_pow_base_selected_power_terminal + S (bpvi_result_pvs_pow_base_selected) = S ((S (e)) * bpvi_v_pvs_pow_base_selected_power)) /\ exists bpvi_q_pvs_pow_base_selected_power_terminal. bpvi_u_pvs_pow_base_selected_power = bpvi_q_pvs_pow_base_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_pow_base_selected_power) + (bpvi_result_pvs_pow_base_selected))) /\ forall bpvi_j_pvs_pow_base_selected_power. (exists bpvi_product_gap_pvs_pow_base_selected_power. bpvi_product_gap_pvs_pow_base_selected_power + S bpvi_j_pvs_pow_base_selected_power = e) -> exists bpvi_factor_pvs_pow_base_selected_power bpvi_partial_pvs_pow_base_selected_power bpvi_successor_pvs_pow_base_selected_power. ((((exists bpvi_h_pvs_pow_base_selected_power_factor. bpvi_h_pvs_pow_base_selected_power_factor + S (bpvi_factor_pvs_pow_base_selected_power) = S ((S (bpvi_j_pvs_pow_base_selected_power)) * bpvi_c_pvs_pow_base_selected_power)) /\ exists bpvi_q_pvs_pow_base_selected_power_factor. bpvi_b_pvs_pow_base_selected_power = bpvi_q_pvs_pow_base_selected_power_factor * S ((S (bpvi_j_pvs_pow_base_selected_power)) * bpvi_c_pvs_pow_base_selected_power) + (bpvi_factor_pvs_pow_base_selected_power))) /\ ((((exists bpvi_h_pvs_pow_base_selected_power_partial. bpvi_h_pvs_pow_base_selected_power_partial + S (bpvi_partial_pvs_pow_base_selected_power) = S ((S (bpvi_j_pvs_pow_base_selected_power)) * bpvi_v_pvs_pow_base_selected_power)) /\ exists bpvi_q_pvs_pow_base_selected_power_partial. bpvi_u_pvs_pow_base_selected_power = bpvi_q_pvs_pow_base_selected_power_partial * S ((S (bpvi_j_pvs_pow_base_selected_power)) * bpvi_v_pvs_pow_base_selected_power) + (bpvi_partial_pvs_pow_base_selected_power))) /\ ((((exists bpvi_h_pvs_pow_base_selected_power_successor. bpvi_h_pvs_pow_base_selected_power_successor + S (bpvi_successor_pvs_pow_base_selected_power) = S ((S (S bpvi_j_pvs_pow_base_selected_power)) * bpvi_v_pvs_pow_base_selected_power)) /\ exists bpvi_q_pvs_pow_base_selected_power_successor. bpvi_u_pvs_pow_base_selected_power = bpvi_q_pvs_pow_base_selected_power_successor * S ((S (S bpvi_j_pvs_pow_base_selected_power)) * bpvi_v_pvs_pow_base_selected_power) + (bpvi_successor_pvs_pow_base_selected_power))) /\ bpvi_successor_pvs_pow_base_selected_power = bpvi_partial_pvs_pow_base_selected_power * bpvi_factor_pvs_pow_base_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_pow_base_selected. a = bpvi_result_pvs_pow_base_selected * bpvi_divisor_factor_pvs_pow_base_selected))) /\ forall bpd_candidate_pvs_pow_base. (exists bpd_gap_pvs_pow_base_candidate_bound. bpd_gap_pvs_pow_base_candidate_bound + (bpd_candidate_pvs_pow_base) = (a)) -> (exists bpvi_result_pvs_pow_base_candidate. ((exists bpvi_b_pvs_pow_base_candidate_power bpvi_c_pvs_pow_base_candidate_power. ((forall bpvi_i_pvs_pow_base_candidate_power. (exists bpvi_repeat_gap_pvs_pow_base_candidate_power. bpvi_repeat_gap_pvs_pow_base_candidate_power + S bpvi_i_pvs_pow_base_candidate_power = bpd_candidate_pvs_pow_base) -> (((exists bpvi_h_pvs_pow_base_candidate_power_repeat. bpvi_h_pvs_pow_base_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_pow_base_candidate_power)) * bpvi_c_pvs_pow_base_candidate_power)) /\ exists bpvi_q_pvs_pow_base_candidate_power_repeat. bpvi_b_pvs_pow_base_candidate_power = bpvi_q_pvs_pow_base_candidate_power_repeat * S ((S (bpvi_i_pvs_pow_base_candidate_power)) * bpvi_c_pvs_pow_base_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_pow_base_candidate_power bpvi_v_pvs_pow_base_candidate_power. ((((exists bpvi_h_pvs_pow_base_candidate_power_start. bpvi_h_pvs_pow_base_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_pow_base_candidate_power)) /\ exists bpvi_q_pvs_pow_base_candidate_power_start. bpvi_u_pvs_pow_base_candidate_power = bpvi_q_pvs_pow_base_candidate_power_start * S ((S (0)) * bpvi_v_pvs_pow_base_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_pow_base_candidate_power_terminal. bpvi_h_pvs_pow_base_candidate_power_terminal + S (bpvi_result_pvs_pow_base_candidate) = S ((S (bpd_candidate_pvs_pow_base)) * bpvi_v_pvs_pow_base_candidate_power)) /\ exists bpvi_q_pvs_pow_base_candidate_power_terminal. bpvi_u_pvs_pow_base_candidate_power = bpvi_q_pvs_pow_base_candidate_power_terminal * S ((S (bpd_candidate_pvs_pow_base)) * bpvi_v_pvs_pow_base_candidate_power) + (bpvi_result_pvs_pow_base_candidate))) /\ forall bpvi_j_pvs_pow_base_candidate_power. (exists bpvi_product_gap_pvs_pow_base_candidate_power. bpvi_product_gap_pvs_pow_base_candidate_power + S bpvi_j_pvs_pow_base_candidate_power = bpd_candidate_pvs_pow_base) -> exists bpvi_factor_pvs_pow_base_candidate_power bpvi_partial_pvs_pow_base_candidate_power bpvi_successor_pvs_pow_base_candidate_power. ((((exists bpvi_h_pvs_pow_base_candidate_power_factor. bpvi_h_pvs_pow_base_candidate_power_factor + S (bpvi_factor_pvs_pow_base_candidate_power) = S ((S (bpvi_j_pvs_pow_base_candidate_power)) * bpvi_c_pvs_pow_base_candidate_power)) /\ exists bpvi_q_pvs_pow_base_candidate_power_factor. bpvi_b_pvs_pow_base_candidate_power = bpvi_q_pvs_pow_base_candidate_power_factor * S ((S (bpvi_j_pvs_pow_base_candidate_power)) * bpvi_c_pvs_pow_base_candidate_power) + (bpvi_factor_pvs_pow_base_candidate_power))) /\ ((((exists bpvi_h_pvs_pow_base_candidate_power_partial. bpvi_h_pvs_pow_base_candidate_power_partial + S (bpvi_partial_pvs_pow_base_candidate_power) = S ((S (bpvi_j_pvs_pow_base_candidate_power)) * bpvi_v_pvs_pow_base_candidate_power)) /\ exists bpvi_q_pvs_pow_base_candidate_power_partial. bpvi_u_pvs_pow_base_candidate_power = bpvi_q_pvs_pow_base_candidate_power_partial * S ((S (bpvi_j_pvs_pow_base_candidate_power)) * bpvi_v_pvs_pow_base_candidate_power) + (bpvi_partial_pvs_pow_base_candidate_power))) /\ ((((exists bpvi_h_pvs_pow_base_candidate_power_successor. bpvi_h_pvs_pow_base_candidate_power_successor + S (bpvi_successor_pvs_pow_base_candidate_power) = S ((S (S bpvi_j_pvs_pow_base_candidate_power)) * bpvi_v_pvs_pow_base_candidate_power)) /\ exists bpvi_q_pvs_pow_base_candidate_power_successor. bpvi_u_pvs_pow_base_candidate_power = bpvi_q_pvs_pow_base_candidate_power_successor * S ((S (S bpvi_j_pvs_pow_base_candidate_power)) * bpvi_v_pvs_pow_base_candidate_power) + (bpvi_successor_pvs_pow_base_candidate_power))) /\ bpvi_successor_pvs_pow_base_candidate_power = bpvi_partial_pvs_pow_base_candidate_power * bpvi_factor_pvs_pow_base_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_pow_base_candidate. a = bpvi_result_pvs_pow_base_candidate * bpvi_divisor_factor_pvs_pow_base_candidate)) -> (exists bpd_gap_pvs_pow_base_maximal. bpd_gap_pvs_pow_base_maximal + (bpd_candidate_pvs_pow_base) = (e))) -> (exists pa_b_pvs_pow_source pa_c_pvs_pow_source. ((forall pa_i_pvs_pow_source_repeat. (exists pa_lt_pvs_pow_source_repeat_bound. pa_lt_pvs_pow_source_repeat_bound + S pa_i_pvs_pow_source_repeat = k) -> (((exists pa_h_pvs_pow_source_repeat_decoded. pa_h_pvs_pow_source_repeat_decoded + S (a) = S ((S (pa_i_pvs_pow_source_repeat)) * pa_c_pvs_pow_source)) /\ exists pa_q_pvs_pow_source_repeat_decoded. pa_b_pvs_pow_source = pa_q_pvs_pow_source_repeat_decoded * S ((S (pa_i_pvs_pow_source_repeat)) * pa_c_pvs_pow_source) + (a)))) /\ (exists pa_u_pvs_pow_source_product pa_v_pvs_pow_source_product. ((((exists pa_h_pvs_pow_source_product_start. pa_h_pvs_pow_source_product_start + S (1) = S ((S (0)) * pa_v_pvs_pow_source_product)) /\ exists pa_q_pvs_pow_source_product_start. pa_u_pvs_pow_source_product = pa_q_pvs_pow_source_product_start * S ((S (0)) * pa_v_pvs_pow_source_product) + (1))) /\ ((((exists pa_h_pvs_pow_source_product_terminal. pa_h_pvs_pow_source_product_terminal + S (z) = S ((S (k)) * pa_v_pvs_pow_source_product)) /\ exists pa_q_pvs_pow_source_product_terminal. pa_u_pvs_pow_source_product = pa_q_pvs_pow_source_product_terminal * S ((S (k)) * pa_v_pvs_pow_source_product) + (z))) /\ forall pa_i_pvs_pow_source_product. (exists pa_lt_pvs_pow_source_product_bound. pa_lt_pvs_pow_source_product_bound + S pa_i_pvs_pow_source_product = k) -> exists pa_p_pvs_pow_source_product pa_r_pvs_pow_source_product pa_s_pvs_pow_source_product. ((((exists pa_h_pvs_pow_source_product_factor. pa_h_pvs_pow_source_product_factor + S (pa_p_pvs_pow_source_product) = S ((S (pa_i_pvs_pow_source_product)) * pa_c_pvs_pow_source)) /\ exists pa_q_pvs_pow_source_product_factor. pa_b_pvs_pow_source = pa_q_pvs_pow_source_product_factor * S ((S (pa_i_pvs_pow_source_product)) * pa_c_pvs_pow_source) + (pa_p_pvs_pow_source_product))) /\ ((((exists pa_h_pvs_pow_source_product_partial. pa_h_pvs_pow_source_product_partial + S (pa_r_pvs_pow_source_product) = S ((S (pa_i_pvs_pow_source_product)) * pa_v_pvs_pow_source_product)) /\ exists pa_q_pvs_pow_source_product_partial. pa_u_pvs_pow_source_product = pa_q_pvs_pow_source_product_partial * S ((S (pa_i_pvs_pow_source_product)) * pa_v_pvs_pow_source_product) + (pa_r_pvs_pow_source_product))) /\ ((((exists pa_h_pvs_pow_source_product_successor. pa_h_pvs_pow_source_product_successor + S (pa_s_pvs_pow_source_product) = S ((S (S pa_i_pvs_pow_source_product)) * pa_v_pvs_pow_source_product)) /\ exists pa_q_pvs_pow_source_product_successor. pa_u_pvs_pow_source_product = pa_q_pvs_pow_source_product_successor * S ((S (S pa_i_pvs_pow_source_product)) * pa_v_pvs_pow_source_product) + (pa_s_pvs_pow_source_product))) /\ pa_s_pvs_pow_source_product = pa_r_pvs_pow_source_product * pa_p_pvs_pow_source_product)))))))) -> (((exists bpd_gap_pvs_pow_output_selected_bound. bpd_gap_pvs_pow_output_selected_bound + (f) = (z)) /\ (exists bpvi_result_pvs_pow_output_selected. ((exists bpvi_b_pvs_pow_output_selected_power bpvi_c_pvs_pow_output_selected_power. ((forall bpvi_i_pvs_pow_output_selected_power. (exists bpvi_repeat_gap_pvs_pow_output_selected_power. bpvi_repeat_gap_pvs_pow_output_selected_power + S bpvi_i_pvs_pow_output_selected_power = f) -> (((exists bpvi_h_pvs_pow_output_selected_power_repeat. bpvi_h_pvs_pow_output_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_pow_output_selected_power)) * bpvi_c_pvs_pow_output_selected_power)) /\ exists bpvi_q_pvs_pow_output_selected_power_repeat. bpvi_b_pvs_pow_output_selected_power = bpvi_q_pvs_pow_output_selected_power_repeat * S ((S (bpvi_i_pvs_pow_output_selected_power)) * bpvi_c_pvs_pow_output_selected_power) + (p)))) /\ (exists bpvi_u_pvs_pow_output_selected_power bpvi_v_pvs_pow_output_selected_power. ((((exists bpvi_h_pvs_pow_output_selected_power_start. bpvi_h_pvs_pow_output_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_pow_output_selected_power)) /\ exists bpvi_q_pvs_pow_output_selected_power_start. bpvi_u_pvs_pow_output_selected_power = bpvi_q_pvs_pow_output_selected_power_start * S ((S (0)) * bpvi_v_pvs_pow_output_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_pow_output_selected_power_terminal. bpvi_h_pvs_pow_output_selected_power_terminal + S (bpvi_result_pvs_pow_output_selected) = S ((S (f)) * bpvi_v_pvs_pow_output_selected_power)) /\ exists bpvi_q_pvs_pow_output_selected_power_terminal. bpvi_u_pvs_pow_output_selected_power = bpvi_q_pvs_pow_output_selected_power_terminal * S ((S (f)) * bpvi_v_pvs_pow_output_selected_power) + (bpvi_result_pvs_pow_output_selected))) /\ forall bpvi_j_pvs_pow_output_selected_power. (exists bpvi_product_gap_pvs_pow_output_selected_power. bpvi_product_gap_pvs_pow_output_selected_power + S bpvi_j_pvs_pow_output_selected_power = f) -> exists bpvi_factor_pvs_pow_output_selected_power bpvi_partial_pvs_pow_output_selected_power bpvi_successor_pvs_pow_output_selected_power. ((((exists bpvi_h_pvs_pow_output_selected_power_factor. bpvi_h_pvs_pow_output_selected_power_factor + S (bpvi_factor_pvs_pow_output_selected_power) = S ((S (bpvi_j_pvs_pow_output_selected_power)) * bpvi_c_pvs_pow_output_selected_power)) /\ exists bpvi_q_pvs_pow_output_selected_power_factor. bpvi_b_pvs_pow_output_selected_power = bpvi_q_pvs_pow_output_selected_power_factor * S ((S (bpvi_j_pvs_pow_output_selected_power)) * bpvi_c_pvs_pow_output_selected_power) + (bpvi_factor_pvs_pow_output_selected_power))) /\ ((((exists bpvi_h_pvs_pow_output_selected_power_partial. bpvi_h_pvs_pow_output_selected_power_partial + S (bpvi_partial_pvs_pow_output_selected_power) = S ((S (bpvi_j_pvs_pow_output_selected_power)) * bpvi_v_pvs_pow_output_selected_power)) /\ exists bpvi_q_pvs_pow_output_selected_power_partial. bpvi_u_pvs_pow_output_selected_power = bpvi_q_pvs_pow_output_selected_power_partial * S ((S (bpvi_j_pvs_pow_output_selected_power)) * bpvi_v_pvs_pow_output_selected_power) + (bpvi_partial_pvs_pow_output_selected_power))) /\ ((((exists bpvi_h_pvs_pow_output_selected_power_successor. bpvi_h_pvs_pow_output_selected_power_successor + S (bpvi_successor_pvs_pow_output_selected_power) = S ((S (S bpvi_j_pvs_pow_output_selected_power)) * bpvi_v_pvs_pow_output_selected_power)) /\ exists bpvi_q_pvs_pow_output_selected_power_successor. bpvi_u_pvs_pow_output_selected_power = bpvi_q_pvs_pow_output_selected_power_successor * S ((S (S bpvi_j_pvs_pow_output_selected_power)) * bpvi_v_pvs_pow_output_selected_power) + (bpvi_successor_pvs_pow_output_selected_power))) /\ bpvi_successor_pvs_pow_output_selected_power = bpvi_partial_pvs_pow_output_selected_power * bpvi_factor_pvs_pow_output_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_pow_output_selected. z = bpvi_result_pvs_pow_output_selected * bpvi_divisor_factor_pvs_pow_output_selected))) /\ forall bpd_candidate_pvs_pow_output. (exists bpd_gap_pvs_pow_output_candidate_bound. bpd_gap_pvs_pow_output_candidate_bound + (bpd_candidate_pvs_pow_output) = (z)) -> (exists bpvi_result_pvs_pow_output_candidate. ((exists bpvi_b_pvs_pow_output_candidate_power bpvi_c_pvs_pow_output_candidate_power. ((forall bpvi_i_pvs_pow_output_candidate_power. (exists bpvi_repeat_gap_pvs_pow_output_candidate_power. bpvi_repeat_gap_pvs_pow_output_candidate_power + S bpvi_i_pvs_pow_output_candidate_power = bpd_candidate_pvs_pow_output) -> (((exists bpvi_h_pvs_pow_output_candidate_power_repeat. bpvi_h_pvs_pow_output_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_pow_output_candidate_power)) * bpvi_c_pvs_pow_output_candidate_power)) /\ exists bpvi_q_pvs_pow_output_candidate_power_repeat. bpvi_b_pvs_pow_output_candidate_power = bpvi_q_pvs_pow_output_candidate_power_repeat * S ((S (bpvi_i_pvs_pow_output_candidate_power)) * bpvi_c_pvs_pow_output_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_pow_output_candidate_power bpvi_v_pvs_pow_output_candidate_power. ((((exists bpvi_h_pvs_pow_output_candidate_power_start. bpvi_h_pvs_pow_output_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_pow_output_candidate_power)) /\ exists bpvi_q_pvs_pow_output_candidate_power_start. bpvi_u_pvs_pow_output_candidate_power = bpvi_q_pvs_pow_output_candidate_power_start * S ((S (0)) * bpvi_v_pvs_pow_output_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_pow_output_candidate_power_terminal. bpvi_h_pvs_pow_output_candidate_power_terminal + S (bpvi_result_pvs_pow_output_candidate) = S ((S (bpd_candidate_pvs_pow_output)) * bpvi_v_pvs_pow_output_candidate_power)) /\ exists bpvi_q_pvs_pow_output_candidate_power_terminal. bpvi_u_pvs_pow_output_candidate_power = bpvi_q_pvs_pow_output_candidate_power_terminal * S ((S (bpd_candidate_pvs_pow_output)) * bpvi_v_pvs_pow_output_candidate_power) + (bpvi_result_pvs_pow_output_candidate))) /\ forall bpvi_j_pvs_pow_output_candidate_power. (exists bpvi_product_gap_pvs_pow_output_candidate_power. bpvi_product_gap_pvs_pow_output_candidate_power + S bpvi_j_pvs_pow_output_candidate_power = bpd_candidate_pvs_pow_output) -> exists bpvi_factor_pvs_pow_output_candidate_power bpvi_partial_pvs_pow_output_candidate_power bpvi_successor_pvs_pow_output_candidate_power. ((((exists bpvi_h_pvs_pow_output_candidate_power_factor. bpvi_h_pvs_pow_output_candidate_power_factor + S (bpvi_factor_pvs_pow_output_candidate_power) = S ((S (bpvi_j_pvs_pow_output_candidate_power)) * bpvi_c_pvs_pow_output_candidate_power)) /\ exists bpvi_q_pvs_pow_output_candidate_power_factor. bpvi_b_pvs_pow_output_candidate_power = bpvi_q_pvs_pow_output_candidate_power_factor * S ((S (bpvi_j_pvs_pow_output_candidate_power)) * bpvi_c_pvs_pow_output_candidate_power) + (bpvi_factor_pvs_pow_output_candidate_power))) /\ ((((exists bpvi_h_pvs_pow_output_candidate_power_partial. bpvi_h_pvs_pow_output_candidate_power_partial + S (bpvi_partial_pvs_pow_output_candidate_power) = S ((S (bpvi_j_pvs_pow_output_candidate_power)) * bpvi_v_pvs_pow_output_candidate_power)) /\ exists bpvi_q_pvs_pow_output_candidate_power_partial. bpvi_u_pvs_pow_output_candidate_power = bpvi_q_pvs_pow_output_candidate_power_partial * S ((S (bpvi_j_pvs_pow_output_candidate_power)) * bpvi_v_pvs_pow_output_candidate_power) + (bpvi_partial_pvs_pow_output_candidate_power))) /\ ((((exists bpvi_h_pvs_pow_output_candidate_power_successor. bpvi_h_pvs_pow_output_candidate_power_successor + S (bpvi_successor_pvs_pow_output_candidate_power) = S ((S (S bpvi_j_pvs_pow_output_candidate_power)) * bpvi_v_pvs_pow_output_candidate_power)) /\ exists bpvi_q_pvs_pow_output_candidate_power_successor. bpvi_u_pvs_pow_output_candidate_power = bpvi_q_pvs_pow_output_candidate_power_successor * S ((S (S bpvi_j_pvs_pow_output_candidate_power)) * bpvi_v_pvs_pow_output_candidate_power) + (bpvi_successor_pvs_pow_output_candidate_power))) /\ bpvi_successor_pvs_pow_output_candidate_power = bpvi_partial_pvs_pow_output_candidate_power * bpvi_factor_pvs_pow_output_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_pow_output_candidate. z = bpvi_result_pvs_pow_output_candidate * bpvi_divisor_factor_pvs_pow_output_candidate)) -> (exists bpd_gap_pvs_pow_output_maximal. bpd_gap_pvs_pow_output_maximal + (bpd_candidate_pvs_pow_output) = (f))) -> f = k * e

Complete tactic proof in conservative notation

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

98 script commands · 19 reading checkpoints · 6 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–3

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro k
02Induction on kL4–12

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction k
  2. L5
    intro e
  3. L6
    intro z
  4. L7
    intro f
  5. L8
    intro hp
  6. L9
    intro ha
  7. L10
    intro hbase
  8. L11
    intro hpow
  9. L12
    intro hval
03Establish hzL13–22

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

  1. L13
    have hz : z = 1
  2. L14
    specialize pow_zero (a)
  3. L15
    specialize pow_zero (0)
  4. L16
    specialize pow_zero (z)
  5. L17
    apply pow_zero
  6. L18
    refl
  7. L19
    exact hpow
  8. L20
    trans 0
  9. L21
    specialize prime_power_valuation_one_zero (p)
  10. L22
    specialize prime_power_valuation_one_zero (z)
04Use earlier factsL23–27

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

  1. L23
    specialize prime_power_valuation_one_zero (f)
  2. L24
    apply prime_power_valuation_one_zero
  3. L25
    exact hz
  4. L26
    exact hp
  5. L27
    exact hval
05Calculate and transport equalitiesL28–28

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

  1. L28
    symm
06Use earlier factsL29–29

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

  1. L29
    apply mul_zero_left
07Fix variables and assumptionsL30–37

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

  1. L30
    intro e
  2. L31
    intro z
  3. L32
    intro f
  4. L33
    intro hp
  5. L34
    intro ha
  6. L35
    intro hbase
  7. L36
    intro hpow
  8. L37
    intro hval
08Establish hprevL38–45

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

  1. L38
    have hprev : ∃ r. Pow(a,k,r) ∧ z = r · aDefinitions: Pow(a,k,r)Original native command in the exact edition
  2. L39
    specialize pow_successor_decompose (a)
  3. L40
    specialize pow_successor_decompose (k)
  4. L41
    specialize pow_successor_decompose (S k)
  5. L42
    specialize pow_successor_decompose (z)
  6. L43
    apply pow_successor_decompose
  7. L44
    refl
  8. L45
    exact hpow
09Separate the logical casesL46–47

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

  1. L46
    cases hprev
  2. L47
    cases hprev_witness
10Establish hvL48–51

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

  1. L48
    have hv : ∃ j. BoundedPowerValuation(p,x,x,j)Definitions: BoundedPowerValuation(p,x,x,j)Original native command in the exact edition
  2. L49
    specialize power_valuation_exists (p)
  3. L50
    specialize power_valuation_exists (x)
  4. L51
    apply power_valuation_exists
11Separate the logical casesL52–52

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

  1. L52
    cases hv
12Establish hindexL53–62

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

  1. L53
    have hindex : x1 = k * e
  2. L54
    specialize IH (e)
  3. L55
    specialize IH (x)
  4. L56
    specialize IH (x1)
  5. L57
    apply IH
  6. L58
    exact hp
  7. L59
    exact ha
  8. L60
    exact hbase
  9. L61
    exact hprev_witness_left
  10. L62
    exact hv_witness
13Establish hxL63–72

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

  1. L63
    have hx : ~(x = 0)
  2. L64
    intro hxzero
  3. L65
    specialize pow_nonzero_of_one_le (a)
  4. L66
    specialize pow_nonzero_of_one_le (k)
  5. L67
    specialize pow_nonzero_of_one_le (x)
  6. L68
    apply pow_nonzero_of_one_le
  7. L69
    specialize one_le_of_ne_zero (a)
  8. L70
    apply one_le_of_ne_zero
  9. L71
    exact ha
  10. L72
    exact hprev_witness_left
14Use earlier factsL73–73

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

  1. L73
    exact hxzero
15Establish hproductL74–83

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

  1. L74
    have hproduct : BoundedPowerValuation(p,x · a,x · a,f)Definitions: BoundedPowerValuation(p,x · a,x · a,f)Original native command in the exact edition
  2. L75
    specialize power_valuation_value_eq_transport (p)
  3. L76
    specialize power_valuation_value_eq_transport (z)
  4. L77
    specialize power_valuation_value_eq_transport (x * a)
  5. L78
    specialize power_valuation_value_eq_transport (f)
  6. L79
    apply power_valuation_value_eq_transport
  7. L80
    exact hprev_witness_right
  8. L81
    exact hval
  9. L82
    trans x1 + e
  10. L83
    specialize prime_power_valuation_mul (p)
16Use earlier factsL84–93

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

  1. L84
    specialize prime_power_valuation_mul (x)
  2. L85
    specialize prime_power_valuation_mul (a)
  3. L86
    specialize prime_power_valuation_mul (x1)
  4. L87
    specialize prime_power_valuation_mul (e)
  5. L88
    specialize prime_power_valuation_mul (f)
  6. L89
    apply prime_power_valuation_mul
  7. L90
    exact hp
  8. L91
    exact hx
  9. L92
    exact ha
  10. L93
    exact hv_witness
17Use earlier factsL94–95

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

  1. L94
    exact hbase
  2. L95
    exact hproduct
18Calculate and transport equalitiesL96–97

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

  1. L96
    rewrite hindex
  2. L97
    symm
19Use earlier factsL98–98

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

  1. L98
    apply mul_succ_left

Library-wide reading audit

Original defined command ledger · 98 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro k
  4. 0004induction k
  5. 0005intro e
  6. 0006intro z
  7. 0007intro f
  8. 0008intro hp
  9. 0009intro ha
  10. 0010intro hbase
  11. 0011intro hpow
  12. 0012intro hval
  13. 0013have hz : z = 1
  14. 0014specialize pow_zero (a)
  15. 0015specialize pow_zero (0)
  16. 0016specialize pow_zero (z)
  17. 0017apply pow_zero
  18. 0018refl
  19. 0019exact hpow
  20. 0020trans 0
  21. 0021specialize prime_power_valuation_one_zero (p)
  22. 0022specialize prime_power_valuation_one_zero (z)
  23. 0023specialize prime_power_valuation_one_zero (f)
  24. 0024apply prime_power_valuation_one_zero
  25. 0025exact hz
  26. 0026exact hp
  27. 0027exact hval
  28. 0028symm
  29. 0029apply mul_zero_left
  30. 0030intro e
  31. 0031intro z
  32. 0032intro f
  33. 0033intro hp
  34. 0034intro ha
  35. 0035intro hbase
  36. 0036intro hpow
  37. 0037intro hval
  38. 0038have hprev : ∃ r. Pow(a,k,r) ∧ z = r · a
  39. 0039specialize pow_successor_decompose (a)
  40. 0040specialize pow_successor_decompose (k)
  41. 0041specialize pow_successor_decompose (S k)
  42. 0042specialize pow_successor_decompose (z)
  43. 0043apply pow_successor_decompose
  44. 0044refl
  45. 0045exact hpow
  46. 0046cases hprev
  47. 0047cases hprev_witness
  48. 0048have hv : ∃ j. BoundedPowerValuation(p,x,x,j)
  49. 0049specialize power_valuation_exists (p)
  50. 0050specialize power_valuation_exists (x)
  51. 0051apply power_valuation_exists
  52. 0052cases hv
  53. 0053have hindex : x1 = k * e
  54. 0054specialize IH (e)
  55. 0055specialize IH (x)
  56. 0056specialize IH (x1)
  57. 0057apply IH
  58. 0058exact hp
  59. 0059exact ha
  60. 0060exact hbase
  61. 0061exact hprev_witness_left
  62. 0062exact hv_witness
  63. 0063have hx : ~(x = 0)
  64. 0064intro hxzero
  65. 0065specialize pow_nonzero_of_one_le (a)
  66. 0066specialize pow_nonzero_of_one_le (k)
  67. 0067specialize pow_nonzero_of_one_le (x)
  68. 0068apply pow_nonzero_of_one_le
  69. 0069specialize one_le_of_ne_zero (a)
  70. 0070apply one_le_of_ne_zero
  71. 0071exact ha
  72. 0072exact hprev_witness_left
  73. 0073exact hxzero
  74. 0074have hproduct : BoundedPowerValuation(p,x · a,x · a,f)
  75. 0075specialize power_valuation_value_eq_transport (p)
  76. 0076specialize power_valuation_value_eq_transport (z)
  77. 0077specialize power_valuation_value_eq_transport (x * a)
  78. 0078specialize power_valuation_value_eq_transport (f)
  79. 0079apply power_valuation_value_eq_transport
  80. 0080exact hprev_witness_right
  81. 0081exact hval
  82. 0082trans x1 + e
  83. 0083specialize prime_power_valuation_mul (p)
  84. 0084specialize prime_power_valuation_mul (x)
  85. 0085specialize prime_power_valuation_mul (a)
  86. 0086specialize prime_power_valuation_mul (x1)
  87. 0087specialize prime_power_valuation_mul (e)
  88. 0088specialize prime_power_valuation_mul (f)
  89. 0089apply prime_power_valuation_mul
  90. 0090exact hp
  91. 0091exact hx
  92. 0092exact ha
  93. 0093exact hv_witness
  94. 0094exact hbase
  95. 0095exact hproduct
  96. 0096rewrite hindex
  97. 0097symm
  98. 0098apply mul_succ_left