TS002X

distinct_prime_power_valuation_zero

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

The prime-power valuation of a distinct prime factor is exactly zero.

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 e. ((~(p = 1) /\ forall frm_prime_left_ftsp_p frm_prime_right_ftsp_p. p = frm_prime_left_ftsp_p * frm_prime_right_ftsp_p -> frm_prime_left_ftsp_p = 1 \/ frm_prime_right_ftsp_p = 1)) -> ((~(q = 1) /\ forall frm_prime_left_ftsp_q frm_prime_right_ftsp_q. q = frm_prime_left_ftsp_q * frm_prime_right_ftsp_q -> frm_prime_left_ftsp_q = 1 \/ frm_prime_right_ftsp_q = 1)) -> ~(p = q) -> (((exists bpv_gap_ftsp_distinct_exponent_bound. bpv_gap_ftsp_distinct_exponent_bound + e = q) /\ (exists bpv_result_ftsp_distinct_selected. ((exists ff_b_ftsp_distinct_selected_power ff_c_ftsp_distinct_selected_power. ((forall ff_i_ftsp_distinct_selected_power_repeat. (exists ff_lt_ftsp_distinct_selected_power_repeat_bound. ff_lt_ftsp_distinct_selected_power_repeat_bound + S ff_i_ftsp_distinct_selected_power_repeat = e) -> (((exists ff_h_ftsp_distinct_selected_power_repeat_decoded. ff_h_ftsp_distinct_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_distinct_selected_power_repeat)) * ff_c_ftsp_distinct_selected_power)) /\ exists ff_q_ftsp_distinct_selected_power_repeat_decoded. ff_b_ftsp_distinct_selected_power = ff_q_ftsp_distinct_selected_power_repeat_decoded * S ((S (ff_i_ftsp_distinct_selected_power_repeat)) * ff_c_ftsp_distinct_selected_power) + (p)))) /\ (exists ff_u_ftsp_distinct_selected_power_product ff_v_ftsp_distinct_selected_power_product. ((((exists ff_h_ftsp_distinct_selected_power_product_start. ff_h_ftsp_distinct_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_distinct_selected_power_product)) /\ exists ff_q_ftsp_distinct_selected_power_product_start. ff_u_ftsp_distinct_selected_power_product = ff_q_ftsp_distinct_selected_power_product_start * S ((S (0)) * ff_v_ftsp_distinct_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_distinct_selected_power_product_terminal. ff_h_ftsp_distinct_selected_power_product_terminal + S (bpv_result_ftsp_distinct_selected) = S ((S (e)) * ff_v_ftsp_distinct_selected_power_product)) /\ exists ff_q_ftsp_distinct_selected_power_product_terminal. ff_u_ftsp_distinct_selected_power_product = ff_q_ftsp_distinct_selected_power_product_terminal * S ((S (e)) * ff_v_ftsp_distinct_selected_power_product) + (bpv_result_ftsp_distinct_selected))) /\ forall ff_i_ftsp_distinct_selected_power_product. (exists ff_lt_ftsp_distinct_selected_power_product_bound. ff_lt_ftsp_distinct_selected_power_product_bound + S ff_i_ftsp_distinct_selected_power_product = e) -> exists ff_p_ftsp_distinct_selected_power_product ff_r_ftsp_distinct_selected_power_product ff_s_ftsp_distinct_selected_power_product. ((((exists ff_h_ftsp_distinct_selected_power_product_factor. ff_h_ftsp_distinct_selected_power_product_factor + S (ff_p_ftsp_distinct_selected_power_product) = S ((S (ff_i_ftsp_distinct_selected_power_product)) * ff_c_ftsp_distinct_selected_power)) /\ exists ff_q_ftsp_distinct_selected_power_product_factor. ff_b_ftsp_distinct_selected_power = ff_q_ftsp_distinct_selected_power_product_factor * S ((S (ff_i_ftsp_distinct_selected_power_product)) * ff_c_ftsp_distinct_selected_power) + (ff_p_ftsp_distinct_selected_power_product))) /\ ((((exists ff_h_ftsp_distinct_selected_power_product_partial. ff_h_ftsp_distinct_selected_power_product_partial + S (ff_r_ftsp_distinct_selected_power_product) = S ((S (ff_i_ftsp_distinct_selected_power_product)) * ff_v_ftsp_distinct_selected_power_product)) /\ exists ff_q_ftsp_distinct_selected_power_product_partial. ff_u_ftsp_distinct_selected_power_product = ff_q_ftsp_distinct_selected_power_product_partial * S ((S (ff_i_ftsp_distinct_selected_power_product)) * ff_v_ftsp_distinct_selected_power_product) + (ff_r_ftsp_distinct_selected_power_product))) /\ ((((exists ff_h_ftsp_distinct_selected_power_product_successor. ff_h_ftsp_distinct_selected_power_product_successor + S (ff_s_ftsp_distinct_selected_power_product) = S ((S (S ff_i_ftsp_distinct_selected_power_product)) * ff_v_ftsp_distinct_selected_power_product)) /\ exists ff_q_ftsp_distinct_selected_power_product_successor. ff_u_ftsp_distinct_selected_power_product = ff_q_ftsp_distinct_selected_power_product_successor * S ((S (S ff_i_ftsp_distinct_selected_power_product)) * ff_v_ftsp_distinct_selected_power_product) + (ff_s_ftsp_distinct_selected_power_product))) /\ ff_s_ftsp_distinct_selected_power_product = ff_r_ftsp_distinct_selected_power_product * ff_p_ftsp_distinct_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_distinct_selected_divides. q = bpv_result_ftsp_distinct_selected * bpv_factor_ftsp_distinct_selected_divides)))) /\ forall bpv_candidate_ftsp_distinct. (exists bpv_gap_ftsp_distinct_candidate_bound. bpv_gap_ftsp_distinct_candidate_bound + bpv_candidate_ftsp_distinct = q) -> (exists bpv_result_ftsp_distinct_candidate. ((exists ff_b_ftsp_distinct_candidate_power ff_c_ftsp_distinct_candidate_power. ((forall ff_i_ftsp_distinct_candidate_power_repeat. (exists ff_lt_ftsp_distinct_candidate_power_repeat_bound. ff_lt_ftsp_distinct_candidate_power_repeat_bound + S ff_i_ftsp_distinct_candidate_power_repeat = bpv_candidate_ftsp_distinct) -> (((exists ff_h_ftsp_distinct_candidate_power_repeat_decoded. ff_h_ftsp_distinct_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_distinct_candidate_power_repeat)) * ff_c_ftsp_distinct_candidate_power)) /\ exists ff_q_ftsp_distinct_candidate_power_repeat_decoded. ff_b_ftsp_distinct_candidate_power = ff_q_ftsp_distinct_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_distinct_candidate_power_repeat)) * ff_c_ftsp_distinct_candidate_power) + (p)))) /\ (exists ff_u_ftsp_distinct_candidate_power_product ff_v_ftsp_distinct_candidate_power_product. ((((exists ff_h_ftsp_distinct_candidate_power_product_start. ff_h_ftsp_distinct_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_distinct_candidate_power_product)) /\ exists ff_q_ftsp_distinct_candidate_power_product_start. ff_u_ftsp_distinct_candidate_power_product = ff_q_ftsp_distinct_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_distinct_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_distinct_candidate_power_product_terminal. ff_h_ftsp_distinct_candidate_power_product_terminal + S (bpv_result_ftsp_distinct_candidate) = S ((S (bpv_candidate_ftsp_distinct)) * ff_v_ftsp_distinct_candidate_power_product)) /\ exists ff_q_ftsp_distinct_candidate_power_product_terminal. ff_u_ftsp_distinct_candidate_power_product = ff_q_ftsp_distinct_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_distinct)) * ff_v_ftsp_distinct_candidate_power_product) + (bpv_result_ftsp_distinct_candidate))) /\ forall ff_i_ftsp_distinct_candidate_power_product. (exists ff_lt_ftsp_distinct_candidate_power_product_bound. ff_lt_ftsp_distinct_candidate_power_product_bound + S ff_i_ftsp_distinct_candidate_power_product = bpv_candidate_ftsp_distinct) -> exists ff_p_ftsp_distinct_candidate_power_product ff_r_ftsp_distinct_candidate_power_product ff_s_ftsp_distinct_candidate_power_product. ((((exists ff_h_ftsp_distinct_candidate_power_product_factor. ff_h_ftsp_distinct_candidate_power_product_factor + S (ff_p_ftsp_distinct_candidate_power_product) = S ((S (ff_i_ftsp_distinct_candidate_power_product)) * ff_c_ftsp_distinct_candidate_power)) /\ exists ff_q_ftsp_distinct_candidate_power_product_factor. ff_b_ftsp_distinct_candidate_power = ff_q_ftsp_distinct_candidate_power_product_factor * S ((S (ff_i_ftsp_distinct_candidate_power_product)) * ff_c_ftsp_distinct_candidate_power) + (ff_p_ftsp_distinct_candidate_power_product))) /\ ((((exists ff_h_ftsp_distinct_candidate_power_product_partial. ff_h_ftsp_distinct_candidate_power_product_partial + S (ff_r_ftsp_distinct_candidate_power_product) = S ((S (ff_i_ftsp_distinct_candidate_power_product)) * ff_v_ftsp_distinct_candidate_power_product)) /\ exists ff_q_ftsp_distinct_candidate_power_product_partial. ff_u_ftsp_distinct_candidate_power_product = ff_q_ftsp_distinct_candidate_power_product_partial * S ((S (ff_i_ftsp_distinct_candidate_power_product)) * ff_v_ftsp_distinct_candidate_power_product) + (ff_r_ftsp_distinct_candidate_power_product))) /\ ((((exists ff_h_ftsp_distinct_candidate_power_product_successor. ff_h_ftsp_distinct_candidate_power_product_successor + S (ff_s_ftsp_distinct_candidate_power_product) = S ((S (S ff_i_ftsp_distinct_candidate_power_product)) * ff_v_ftsp_distinct_candidate_power_product)) /\ exists ff_q_ftsp_distinct_candidate_power_product_successor. ff_u_ftsp_distinct_candidate_power_product = ff_q_ftsp_distinct_candidate_power_product_successor * S ((S (S ff_i_ftsp_distinct_candidate_power_product)) * ff_v_ftsp_distinct_candidate_power_product) + (ff_s_ftsp_distinct_candidate_power_product))) /\ ff_s_ftsp_distinct_candidate_power_product = ff_r_ftsp_distinct_candidate_power_product * ff_p_ftsp_distinct_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_distinct_candidate_divides. q = bpv_result_ftsp_distinct_candidate * bpv_factor_ftsp_distinct_candidate_divides))) -> (exists bpv_gap_ftsp_distinct_maximal. bpv_gap_ftsp_distinct_maximal + bpv_candidate_ftsp_distinct = e)) -> e = 0

Constructive proof overview

Generated structural guide

The prime-power valuation of a distinct prime factor is exactly zero.

The unchanged tactic script uses 3 declared prerequisites and contains 26 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

eq_decidable Stable theorem; checked-use authorized power_valuation_nonzero_exponent_divides_base Alpha theorem; checked-use authorized TS002W prime_divisor_of_prime_forces_equality

Direct dependents

TS0035 distinct_prime_factor_even_valuation_reflects_prefix

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

26 script commands · 7 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 (1)
prime divisor of prime forces equality
01Fix variables and assumptionsL1–7

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro e
  4. L4
    intro hp
  5. L5
    intro hq
  6. L6
    intro hdistinct
  7. L7
    intro hvaluation
02Use earlier factsL8–9

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

  1. L8
    specialize eq_decidable e
  2. L9
    specialize eq_decidable 0
03Separate the logical casesL10–10

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

  1. L10
    cases eq_decidable
04Use earlier factsL11–11

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

  1. L11
    exact eq_decidable_left
05Separate the logical casesL12–12

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

  1. L12
    exfalso
06Establish hdividesL13–22

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

  1. L13
    have hdivides : exists ftcn_factor_ftsp_prime_divides_prime. (q) = (p) * ftcn_factor_ftsp_prime_divides_prime
  2. L14
    specialize power_valuation_nonzero_exponent_divides_base p
  3. L15
    specialize power_valuation_nonzero_exponent_divides_base q
  4. L16
    specialize power_valuation_nonzero_exponent_divides_base e
  5. L17
    apply power_valuation_nonzero_exponent_divides_base
  6. L18
    exact hvaluation
  7. L19
    exact eq_decidable_right
  8. L20
    apply hdistinct
  9. L21
    specialize prime_divisor_of_prime_forces_equality p
  10. L22
    specialize prime_divisor_of_prime_forces_equality q
07Use earlier factsL23–26

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

  1. L23
    apply prime_divisor_of_prime_forces_equality
  2. L24
    exact hp
  3. L25
    exact hq
  4. L26
    exact hdivides

Library-wide reading audit

Original exact command ledger · 26 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro e
  4. 0004intro hp
  5. 0005intro hq
  6. 0006intro hdistinct
  7. 0007intro hvaluation
  8. 0008specialize eq_decidable e
  9. 0009specialize eq_decidable 0
  10. 0010cases eq_decidable
  11. 0011exact eq_decidable_left
  12. 0012exfalso
  13. 0013have hdivides : exists ftcn_factor_ftsp_prime_divides_prime. (q) = (p) * ftcn_factor_ftsp_prime_divides_prime
  14. 0014specialize power_valuation_nonzero_exponent_divides_base p
  15. 0015specialize power_valuation_nonzero_exponent_divides_base q
  16. 0016specialize power_valuation_nonzero_exponent_divides_base e
  17. 0017apply power_valuation_nonzero_exponent_divides_base
  18. 0018exact hvaluation
  19. 0019exact eq_decidable_right
  20. 0020apply hdistinct
  21. 0021specialize prime_divisor_of_prime_forces_equality p
  22. 0022specialize prime_divisor_of_prime_forces_equality q
  23. 0023apply prime_divisor_of_prime_forces_equality
  24. 0024exact hp
  25. 0025exact hq
  26. 0026exact hdivides