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.

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

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

Definition DAG

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

Actual proof prerequisites

power_valuation_value_eq_transport · checked external prerequisiteprime_valuation_exponent_eq_transport · checked external prerequisite lte_valuation_product_exactpow_nonzero_of_one_le · checked external prerequisiteone_le_of_ne_zero · checked external prerequisiteprime_nonzero · checked external prerequisitelte_nondivisor_nonzero lte_prime_power_valuation_exact prime_valuation_zero_of_nondivisor · checked external prerequisite

Original expanded first-order 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)))

Complete tactic proof in conservative notation

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

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.

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 (3)

lte nondivisor nonzero lte valuation product exact 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