EL001A — lte_valuation_from_exact_cofactor

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 e P u X. (~((p) = 1) /\ forall pvs_left_cofactor_prime pvs_right_cofactor_prime. (p) = pvs_left_cofactor_prime * pvs_right_cofactor_prime -> pvs_left_cofactor_prime = 1 \/ pvs_right_cofactor_prime = 1) -> (exists pa_b_olte_cofactor_power pa_c_olte_cofactor_power. ((forall pa_i_olte_cofactor_power_repeat. (exists pa_lt_olte_cofactor_power_repeat_bound. pa_lt_olte_cofactor_power_repeat_bound + S pa_i_olte_cofactor_power_repeat = e) -> (((exists pa_h_olte_cofactor_power_repeat_decoded. pa_h_olte_cofactor_power_repeat_decoded + S (p) = S ((S (pa_i_olte_cofactor_power_repeat)) * pa_c_olte_cofactor_power)) /\ exists pa_q_olte_cofactor_power_repeat_decoded. pa_b_olte_cofactor_power = pa_q_olte_cofactor_power_repeat_decoded * S ((S (pa_i_olte_cofactor_power_repeat)) * pa_c_olte_cofactor_power) + (p)))) /\ (exists pa_u_olte_cofactor_power_product pa_v_olte_cofactor_power_product. ((((exists pa_h_olte_cofactor_power_product_start. pa_h_olte_cofactor_power_product_start + S (1) = S ((S (0)) * pa_v_olte_cofactor_power_product)) /\ exists pa_q_olte_cofactor_power_product_start. pa_u_olte_cofactor_power_product = pa_q_olte_cofactor_power_product_start * S ((S (0)) * pa_v_olte_cofactor_power_product) + (1))) /\ ((((exists pa_h_olte_cofactor_power_product_terminal. pa_h_olte_cofactor_power_product_terminal + S (P) = S ((S (e)) * pa_v_olte_cofactor_power_product)) /\ exists pa_q_olte_cofactor_power_product_terminal. pa_u_olte_cofactor_power_product = pa_q_olte_cofactor_power_product_terminal * S ((S (e)) * pa_v_olte_cofactor_power_product) + (P))) /\ forall pa_i_olte_cofactor_power_product. (exists pa_lt_olte_cofactor_power_product_bound. pa_lt_olte_cofactor_power_product_bound + S pa_i_olte_cofactor_power_product = e) -> exists pa_p_olte_cofactor_power_product pa_r_olte_cofactor_power_product pa_s_olte_cofactor_power_product. ((((exists pa_h_olte_cofactor_power_product_factor. pa_h_olte_cofactor_power_product_factor + S (pa_p_olte_cofactor_power_product) = S ((S (pa_i_olte_cofactor_power_product)) * pa_c_olte_cofactor_power)) /\ exists pa_q_olte_cofactor_power_product_factor. pa_b_olte_cofactor_power = pa_q_olte_cofactor_power_product_factor * S ((S (pa_i_olte_cofactor_power_product)) * pa_c_olte_cofactor_power) + (pa_p_olte_cofactor_power_product))) /\ ((((exists pa_h_olte_cofactor_power_product_partial. pa_h_olte_cofactor_power_product_partial + S (pa_r_olte_cofactor_power_product) = S ((S (pa_i_olte_cofactor_power_product)) * pa_v_olte_cofactor_power_product)) /\ exists pa_q_olte_cofactor_power_product_partial. pa_u_olte_cofactor_power_product = pa_q_olte_cofactor_power_product_partial * S ((S (pa_i_olte_cofactor_power_product)) * pa_v_olte_cofactor_power_product) + (pa_r_olte_cofactor_power_product))) /\ ((((exists pa_h_olte_cofactor_power_product_successor. pa_h_olte_cofactor_power_product_successor + S (pa_s_olte_cofactor_power_product) = S ((S (S pa_i_olte_cofactor_power_product)) * pa_v_olte_cofactor_power_product)) /\ exists pa_q_olte_cofactor_power_product_successor. pa_u_olte_cofactor_power_product = pa_q_olte_cofactor_power_product_successor * S ((S (S pa_i_olte_cofactor_power_product)) * pa_v_olte_cofactor_power_product) + (pa_s_olte_cofactor_power_product))) /\ pa_s_olte_cofactor_power_product = pa_r_olte_cofactor_power_product * pa_p_olte_cofactor_power_product)))))))) -> X = P * u -> ~(exists olte_factor_cofactor_unit. (u) = (p) * olte_factor_cofactor_unit) -> (((exists bpd_gap_pvs_cofactor_result_selected_bound. bpd_gap_pvs_cofactor_result_selected_bound + (e) = (X)) /\ (exists bpvi_result_pvs_cofactor_result_selected. ((exists bpvi_b_pvs_cofactor_result_selected_power bpvi_c_pvs_cofactor_result_selected_power. ((forall bpvi_i_pvs_cofactor_result_selected_power. (exists bpvi_repeat_gap_pvs_cofactor_result_selected_power. bpvi_repeat_gap_pvs_cofactor_result_selected_power + S bpvi_i_pvs_cofactor_result_selected_power = e) -> (((exists bpvi_h_pvs_cofactor_result_selected_power_repeat. bpvi_h_pvs_cofactor_result_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_cofactor_result_selected_power)) * bpvi_c_pvs_cofactor_result_selected_power)) /\ exists bpvi_q_pvs_cofactor_result_selected_power_repeat. bpvi_b_pvs_cofactor_result_selected_power = bpvi_q_pvs_cofactor_result_selected_power_repeat * S ((S (bpvi_i_pvs_cofactor_result_selected_power)) * bpvi_c_pvs_cofactor_result_selected_power) + (p)))) /\ (exists bpvi_u_pvs_cofactor_result_selected_power bpvi_v_pvs_cofactor_result_selected_power. ((((exists bpvi_h_pvs_cofactor_result_selected_power_start. bpvi_h_pvs_cofactor_result_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_cofactor_result_selected_power)) /\ exists bpvi_q_pvs_cofactor_result_selected_power_start. bpvi_u_pvs_cofactor_result_selected_power = bpvi_q_pvs_cofactor_result_selected_power_start * S ((S (0)) * bpvi_v_pvs_cofactor_result_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_cofactor_result_selected_power_terminal. bpvi_h_pvs_cofactor_result_selected_power_terminal + S (bpvi_result_pvs_cofactor_result_selected) = S ((S (e)) * bpvi_v_pvs_cofactor_result_selected_power)) /\ exists bpvi_q_pvs_cofactor_result_selected_power_terminal. bpvi_u_pvs_cofactor_result_selected_power = bpvi_q_pvs_cofactor_result_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_cofactor_result_selected_power) + (bpvi_result_pvs_cofactor_result_selected))) /\ forall bpvi_j_pvs_cofactor_result_selected_power. (exists bpvi_product_gap_pvs_cofactor_result_selected_power. bpvi_product_gap_pvs_cofactor_result_selected_power + S bpvi_j_pvs_cofactor_result_selected_power = e) -> exists bpvi_factor_pvs_cofactor_result_selected_power bpvi_partial_pvs_cofactor_result_selected_power bpvi_successor_pvs_cofactor_result_selected_power. ((((exists bpvi_h_pvs_cofactor_result_selected_power_factor. bpvi_h_pvs_cofactor_result_selected_power_factor + S (bpvi_factor_pvs_cofactor_result_selected_power) = S ((S (bpvi_j_pvs_cofactor_result_selected_power)) * bpvi_c_pvs_cofactor_result_selected_power)) /\ exists bpvi_q_pvs_cofactor_result_selected_power_factor. bpvi_b_pvs_cofactor_result_selected_power = bpvi_q_pvs_cofactor_result_selected_power_factor * S ((S (bpvi_j_pvs_cofactor_result_selected_power)) * bpvi_c_pvs_cofactor_result_selected_power) + (bpvi_factor_pvs_cofactor_result_selected_power))) /\ ((((exists bpvi_h_pvs_cofactor_result_selected_power_partial. bpvi_h_pvs_cofactor_result_selected_power_partial + S (bpvi_partial_pvs_cofactor_result_selected_power) = S ((S (bpvi_j_pvs_cofactor_result_selected_power)) * bpvi_v_pvs_cofactor_result_selected_power)) /\ exists bpvi_q_pvs_cofactor_result_selected_power_partial. bpvi_u_pvs_cofactor_result_selected_power = bpvi_q_pvs_cofactor_result_selected_power_partial * S ((S (bpvi_j_pvs_cofactor_result_selected_power)) * bpvi_v_pvs_cofactor_result_selected_power) + (bpvi_partial_pvs_cofactor_result_selected_power))) /\ ((((exists bpvi_h_pvs_cofactor_result_selected_power_successor. bpvi_h_pvs_cofactor_result_selected_power_successor + S (bpvi_successor_pvs_cofactor_result_selected_power) = S ((S (S bpvi_j_pvs_cofactor_result_selected_power)) * bpvi_v_pvs_cofactor_result_selected_power)) /\ exists bpvi_q_pvs_cofactor_result_selected_power_successor. bpvi_u_pvs_cofactor_result_selected_power = bpvi_q_pvs_cofactor_result_selected_power_successor * S ((S (S bpvi_j_pvs_cofactor_result_selected_power)) * bpvi_v_pvs_cofactor_result_selected_power) + (bpvi_successor_pvs_cofactor_result_selected_power))) /\ bpvi_successor_pvs_cofactor_result_selected_power = bpvi_partial_pvs_cofactor_result_selected_power * bpvi_factor_pvs_cofactor_result_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_cofactor_result_selected. X = bpvi_result_pvs_cofactor_result_selected * bpvi_divisor_factor_pvs_cofactor_result_selected))) /\ forall bpd_candidate_pvs_cofactor_result. (exists bpd_gap_pvs_cofactor_result_candidate_bound. bpd_gap_pvs_cofactor_result_candidate_bound + (bpd_candidate_pvs_cofactor_result) = (X)) -> (exists bpvi_result_pvs_cofactor_result_candidate. ((exists bpvi_b_pvs_cofactor_result_candidate_power bpvi_c_pvs_cofactor_result_candidate_power. ((forall bpvi_i_pvs_cofactor_result_candidate_power. (exists bpvi_repeat_gap_pvs_cofactor_result_candidate_power. bpvi_repeat_gap_pvs_cofactor_result_candidate_power + S bpvi_i_pvs_cofactor_result_candidate_power = bpd_candidate_pvs_cofactor_result) -> (((exists bpvi_h_pvs_cofactor_result_candidate_power_repeat. bpvi_h_pvs_cofactor_result_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_cofactor_result_candidate_power)) * bpvi_c_pvs_cofactor_result_candidate_power)) /\ exists bpvi_q_pvs_cofactor_result_candidate_power_repeat. bpvi_b_pvs_cofactor_result_candidate_power = bpvi_q_pvs_cofactor_result_candidate_power_repeat * S ((S (bpvi_i_pvs_cofactor_result_candidate_power)) * bpvi_c_pvs_cofactor_result_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_cofactor_result_candidate_power bpvi_v_pvs_cofactor_result_candidate_power. ((((exists bpvi_h_pvs_cofactor_result_candidate_power_start. bpvi_h_pvs_cofactor_result_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_cofactor_result_candidate_power)) /\ exists bpvi_q_pvs_cofactor_result_candidate_power_start. bpvi_u_pvs_cofactor_result_candidate_power = bpvi_q_pvs_cofactor_result_candidate_power_start * S ((S (0)) * bpvi_v_pvs_cofactor_result_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_cofactor_result_candidate_power_terminal. bpvi_h_pvs_cofactor_result_candidate_power_terminal + S (bpvi_result_pvs_cofactor_result_candidate) = S ((S (bpd_candidate_pvs_cofactor_result)) * bpvi_v_pvs_cofactor_result_candidate_power)) /\ exists bpvi_q_pvs_cofactor_result_candidate_power_terminal. bpvi_u_pvs_cofactor_result_candidate_power = bpvi_q_pvs_cofactor_result_candidate_power_terminal * S ((S (bpd_candidate_pvs_cofactor_result)) * bpvi_v_pvs_cofactor_result_candidate_power) + (bpvi_result_pvs_cofactor_result_candidate))) /\ forall bpvi_j_pvs_cofactor_result_candidate_power. (exists bpvi_product_gap_pvs_cofactor_result_candidate_power. bpvi_product_gap_pvs_cofactor_result_candidate_power + S bpvi_j_pvs_cofactor_result_candidate_power = bpd_candidate_pvs_cofactor_result) -> exists bpvi_factor_pvs_cofactor_result_candidate_power bpvi_partial_pvs_cofactor_result_candidate_power bpvi_successor_pvs_cofactor_result_candidate_power. ((((exists bpvi_h_pvs_cofactor_result_candidate_power_factor. bpvi_h_pvs_cofactor_result_candidate_power_factor + S (bpvi_factor_pvs_cofactor_result_candidate_power) = S ((S (bpvi_j_pvs_cofactor_result_candidate_power)) * bpvi_c_pvs_cofactor_result_candidate_power)) /\ exists bpvi_q_pvs_cofactor_result_candidate_power_factor. bpvi_b_pvs_cofactor_result_candidate_power = bpvi_q_pvs_cofactor_result_candidate_power_factor * S ((S (bpvi_j_pvs_cofactor_result_candidate_power)) * bpvi_c_pvs_cofactor_result_candidate_power) + (bpvi_factor_pvs_cofactor_result_candidate_power))) /\ ((((exists bpvi_h_pvs_cofactor_result_candidate_power_partial. bpvi_h_pvs_cofactor_result_candidate_power_partial + S (bpvi_partial_pvs_cofactor_result_candidate_power) = S ((S (bpvi_j_pvs_cofactor_result_candidate_power)) * bpvi_v_pvs_cofactor_result_candidate_power)) /\ exists bpvi_q_pvs_cofactor_result_candidate_power_partial. bpvi_u_pvs_cofactor_result_candidate_power = bpvi_q_pvs_cofactor_result_candidate_power_partial * S ((S (bpvi_j_pvs_cofactor_result_candidate_power)) * bpvi_v_pvs_cofactor_result_candidate_power) + (bpvi_partial_pvs_cofactor_result_candidate_power))) /\ ((((exists bpvi_h_pvs_cofactor_result_candidate_power_successor. bpvi_h_pvs_cofactor_result_candidate_power_successor + S (bpvi_successor_pvs_cofactor_result_candidate_power) = S ((S (S bpvi_j_pvs_cofactor_result_candidate_power)) * bpvi_v_pvs_cofactor_result_candidate_power)) /\ exists bpvi_q_pvs_cofactor_result_candidate_power_successor. bpvi_u_pvs_cofactor_result_candidate_power = bpvi_q_pvs_cofactor_result_candidate_power_successor * S ((S (S bpvi_j_pvs_cofactor_result_candidate_power)) * bpvi_v_pvs_cofactor_result_candidate_power) + (bpvi_successor_pvs_cofactor_result_candidate_power))) /\ bpvi_successor_pvs_cofactor_result_candidate_power = bpvi_partial_pvs_cofactor_result_candidate_power * bpvi_factor_pvs_cofactor_result_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_cofactor_result_candidate. X = bpvi_result_pvs_cofactor_result_candidate * bpvi_divisor_factor_pvs_cofactor_result_candidate)) -> (exists bpd_gap_pvs_cofactor_result_maximal. bpd_gap_pvs_cofactor_result_maximal + (bpd_candidate_pvs_cofactor_result) = (e)))

Constructive proof overview

Generated structural guide

An actual prime-power times a genuine nondivisor cofactor constructs its precise maximal valuation, including the unit boundary.

The unchanged tactic script uses 9 declared prerequisites and contains 63 exact native proof lines.

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

Proof neighborhood

Direct dependencies

power_valuation_value_eq_transport Alpha theorem; checked-use authorized prime_valuation_exponent_eq_transport Alpha theorem; checked-use authorized EL0018 lte_valuation_product_exact pow_nonzero_of_one_le Alpha theorem; checked-use authorized one_le_of_ne_zero Stable theorem; checked-use authorized prime_nonzero Stable theorem; checked-use authorized EL000B lte_nondivisor_nonzero EL0019 lte_prime_power_valuation_exact prime_valuation_zero_of_nondivisor Alpha theorem; checked-use authorized

Direct dependents

EL001E lte_odd_prime_power_step

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

63 script commands · 11 reading checkpoints · 1 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 (3)

lte valuation product exact lte nondivisor nonzero lte prime power valuation exact

01Fix variables and assumptionsL1–9

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

L1
intro p
L2
intro e
L3
intro P
L4
intro u
L5
intro X
L6
intro hp
L7
intro hpow
L8
intro hX
L9
intro hunit

02Establish huL10–19

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

L10
have hu : ~(u = 0)
L11
intro hz
L12
specialize lte_nondivisor_nonzero (p)
L13
specialize lte_nondivisor_nonzero (u)
L14
apply lte_nondivisor_nonzero
L15
exact hunit
L16
exact hz
L17
specialize power_valuation_value_eq_transport (p)
L18
specialize power_valuation_value_eq_transport (P * u)
L19
specialize power_valuation_value_eq_transport (X)

03Use earlier factsL20–21