TS003S

prime_square_times_nonzero_strictly_increases

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

Multiplication of a nonzero natural by a prime square is strictly increasing in witnessed constructive order.

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. ((~(p = 1) /\ forall frm_prime_left_ftsv_prime frm_prime_right_ftsv_prime. p = frm_prime_left_ftsv_prime * frm_prime_right_ftsv_prime -> frm_prime_left_ftsv_prime = 1 \/ frm_prime_right_ftsv_prime = 1)) -> ~(q = 0) -> exists k. k + S q = (p * p) * q

Constructive proof overview

Generated structural guide

Multiplication of a nonzero natural by a prime square is strictly increasing in witnessed constructive order.

The unchanged tactic script uses 9 declared prerequisites and contains 46 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_two_le Alpha theorem; checked-use authorized succ_le_mul_of_two_le_right Alpha theorem; checked-use authorized prime_nonzero Stable theorem; checked-use authorized one_le_of_ne_zero Stable theorem; checked-use authorized mul_le_mul_left Stable theorem; checked-use authorized mul_one Stable theorem; checked-use authorized le_trans Stable theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized

Direct dependents

TS003C all_bad_prime_even_two_square_sufficiency_bounded TS003T three_mod_four_prime_two_square_norm_valuation_even_bounded

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

46 script commands · 13 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.

01Fix variables and assumptionsL1–4

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro hprime
  4. L4
    intro hquotient
02Establish htwoL5–8

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

  1. L5
    have htwo : exists k. k + 2 = p
  2. L6
    specialize prime_two_le p
  3. L7
    apply prime_two_le
  4. L8
    exact hprime
03Establish hfirstL9–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ le mul of two le right.

  1. L9
    have hfirst : exists k. k + S q = q * p
  2. L10
    specialize succ_le_mul_of_two_le_right q
  3. L11
    specialize succ_le_mul_of_two_le_right p
  4. L12
    apply succ_le_mul_of_two_le_right
  5. L13
    exact hquotient
  6. L14
    exact htwo
04Establish hpnonzeroL15–20

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

  1. L15
    have hpnonzero : ~(p = 0)
  2. L16
    specialize prime_nonzero p
  3. L17
    intro hpzero
  4. L18
    apply prime_nonzero
  5. L19
    exact hprime
  6. L20
    exact hpzero
05Establish honeL21–24

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

  1. L21
    have hone : exists k. k + 1 = p
  2. L22
    specialize one_le_of_ne_zero p
  3. L23
    apply one_le_of_ne_zero
  4. L24
    exact hpnonzero
06Establish hsecondL25–32

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

  1. L25
    have hsecond : exists k. k + (q * p) * 1 = (q * p) * p
  2. L26
    specialize mul_le_mul_left 1
  3. L27
    specialize mul_le_mul_left p
  4. L28
    specialize mul_le_mul_left (q * p)
  5. L29
    apply mul_le_mul_left
  6. L30
    exact hone
  7. L31
    specialize mul_one (q * p)
  8. L32
    rewrite mul_one at hsecond
07Establish hcombinedL33–39

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

  1. L33
    have hcombined : exists k. k + S q = (q * p) * p
  2. L34
    specialize le_trans (S q)
  3. L35
    specialize le_trans (q * p)
  4. L36
    specialize le_trans ((q * p) * p)
  5. L37
    apply le_trans
  6. L38
    exact hfirst
  7. L39
    exact hsecond
08Separate the logical casesL40–40

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

  1. L40
    cases hcombined
09Construct an explicit witnessL41–41

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

  1. L41
    exists x
10Calculate and transport equalitiesL42–42

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

  1. L42
    trans (q * p) * p
11Use earlier factsL43–43

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

  1. L43
    exact hcombined_witness
12Calculate and transport equalitiesL44–44

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

  1. L44
    trans q * (p * p)
13Use earlier factsL45–46

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

  1. L45
    apply mul_assoc
  2. L46
    apply mul_comm

Library-wide reading audit

Original exact command ledger · 46 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro hprime
  4. 0004intro hquotient
  5. 0005have htwo : exists k. k + 2 = p
  6. 0006specialize prime_two_le p
  7. 0007apply prime_two_le
  8. 0008exact hprime
  9. 0009have hfirst : exists k. k + S q = q * p
  10. 0010specialize succ_le_mul_of_two_le_right q
  11. 0011specialize succ_le_mul_of_two_le_right p
  12. 0012apply succ_le_mul_of_two_le_right
  13. 0013exact hquotient
  14. 0014exact htwo
  15. 0015have hpnonzero : ~(p = 0)
  16. 0016specialize prime_nonzero p
  17. 0017intro hpzero
  18. 0018apply prime_nonzero
  19. 0019exact hprime
  20. 0020exact hpzero
  21. 0021have hone : exists k. k + 1 = p
  22. 0022specialize one_le_of_ne_zero p
  23. 0023apply one_le_of_ne_zero
  24. 0024exact hpnonzero
  25. 0025have hsecond : exists k. k + (q * p) * 1 = (q * p) * p
  26. 0026specialize mul_le_mul_left 1
  27. 0027specialize mul_le_mul_left p
  28. 0028specialize mul_le_mul_left (q * p)
  29. 0029apply mul_le_mul_left
  30. 0030exact hone
  31. 0031specialize mul_one (q * p)
  32. 0032rewrite mul_one at hsecond
  33. 0033have hcombined : exists k. k + S q = (q * p) * p
  34. 0034specialize le_trans (S q)
  35. 0035specialize le_trans (q * p)
  36. 0036specialize le_trans ((q * p) * p)
  37. 0037apply le_trans
  38. 0038exact hfirst
  39. 0039exact hsecond
  40. 0040cases hcombined
  41. 0041exists x
  42. 0042trans (q * p) * p
  43. 0043exact hcombined_witness
  44. 0044trans q * (p * p)
  45. 0045apply mul_assoc
  46. 0046apply mul_comm