TS0030

prime_square_divisibility_forces_suffix_prime_divisor

Dependency-curried candidate body; not Alpha-enrolled; no checked-use authority

If a prime square divides a product with one terminal prime factor, that same prime divides the remaining prefix product.

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 r n. ((~(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)) -> n = r * p -> (exists ftcn_factor_ftsp_square. (n) = (p * p) * ftcn_factor_ftsp_square) -> (exists ftcn_factor_ftsp_suffix. (r) = (p) * ftcn_factor_ftsp_suffix)

Constructive proof overview

Generated structural guide

If a prime square divides a product with one terminal prime factor, that same prime divides the remaining prefix product.

The unchanged tactic script uses 4 declared prerequisites and contains 29 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

prime_nonzero Stable theorem; checked-use authorized mul_left_cancel_nonzero Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized

Direct dependents

TS0032 even_valuation_sorted_terminal_prime_has_equal_predecessor

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This dependency-curried candidate body does not grant checked theorem use or Stable membership.

Read the argument

Proof checkpoints

29 script commands · 6 reading checkpoints · 2 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.

01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro r
  3. L3
    intro n
  4. L4
    intro hprime
  5. L5
    intro hproduct
  6. L6
    intro hsquare
02Separate the logical casesL7–7

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

  1. L7
    cases hsquare
03Establish hpnonzeroL8–13

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

  1. L8
    have hpnonzero : ~(p = 0)
  2. L9
    specialize prime_nonzero p
  3. L10
    intro hpzero
  4. L11
    apply prime_nonzero
  5. L12
    exact hprime
  6. L13
    exact hpzero
04Establish hbalanceL14–22

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

  1. L14
    have hbalance : p * r = p * (p * x)
  2. L15
    trans r * p
  3. L16
    apply mul_comm
  4. L17
    trans n
  5. L18
    symm
  6. L19
    exact hproduct
  7. L20
    trans (p * p) * x
  8. L21
    exact hsquare_witness
  9. L22
    apply mul_assoc
05Construct an explicit witnessL23–23

Supply the displayed value, then prove that it has the required property.

  1. L23
    exists x
06Use earlier factsL24–29

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

  1. L24
    specialize mul_left_cancel_nonzero p
  2. L25
    specialize mul_left_cancel_nonzero r
  3. L26
    specialize mul_left_cancel_nonzero (p * x)
  4. L27
    apply mul_left_cancel_nonzero
  5. L28
    exact hpnonzero
  6. L29
    exact hbalance

Library-wide reading audit

Original exact command ledger · 29 lines
  1. 0001intro p
  2. 0002intro r
  3. 0003intro n
  4. 0004intro hprime
  5. 0005intro hproduct
  6. 0006intro hsquare
  7. 0007cases hsquare
  8. 0008have hpnonzero : ~(p = 0)
  9. 0009specialize prime_nonzero p
  10. 0010intro hpzero
  11. 0011apply prime_nonzero
  12. 0012exact hprime
  13. 0013exact hpzero
  14. 0014have hbalance : p * r = p * (p * x)
  15. 0015trans r * p
  16. 0016apply mul_comm
  17. 0017trans n
  18. 0018symm
  19. 0019exact hproduct
  20. 0020trans (p * p) * x
  21. 0021exact hsquare_witness
  22. 0022apply mul_assoc
  23. 0023exists x
  24. 0024specialize mul_left_cancel_nonzero p
  25. 0025specialize mul_left_cancel_nonzero r
  26. 0026specialize mul_left_cancel_nonzero (p * x)
  27. 0027apply mul_left_cancel_nonzero
  28. 0028exact hpnonzero
  29. 0029exact hbalance