TS0031

beta_sorted_prime_prefix_divisor_equals_bounded_last

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

A prime dividing a sorted prime prefix equals its terminal factor whenever that terminal factor is bounded by the prime.

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 b c l r p q. ((~(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)) -> (forall ftsf_index_ftsp_prefix. (exists ftsf_gap_ftsp_prefix_bound. ftsf_gap_ftsp_prefix_bound + S ftsf_index_ftsp_prefix = (S l)) -> exists ftsf_factor_ftsp_prefix. ((((exists ff_h_ftsf_ftsp_prefix_entry. ff_h_ftsf_ftsp_prefix_entry + S (ftsf_factor_ftsp_prefix) = S ((S (ftsf_index_ftsp_prefix)) * c)) /\ exists ff_q_ftsf_ftsp_prefix_entry. b = ff_q_ftsf_ftsp_prefix_entry * S ((S (ftsf_index_ftsp_prefix)) * c) + (ftsf_factor_ftsp_prefix))) /\ ((~(ftsf_factor_ftsp_prefix = 1) /\ forall frm_prime_left_ftsf_ftsp_prefix_prime frm_prime_right_ftsf_ftsp_prefix_prime. ftsf_factor_ftsp_prefix = frm_prime_left_ftsf_ftsp_prefix_prime * frm_prime_right_ftsf_ftsp_prefix_prime -> frm_prime_left_ftsf_ftsp_prefix_prime = 1 \/ frm_prime_right_ftsf_ftsp_prefix_prime = 1)))) -> (forall ftsp_index_prefix. (exists ftsp_bound_prefix. ftsp_bound_prefix + S (S ftsp_index_prefix) = (S l)) -> exists ftsp_left_prefix ftsp_right_prefix. ((((exists ff_h_ftsp_prefix_left. ff_h_ftsp_prefix_left + S (ftsp_left_prefix) = S ((S (ftsp_index_prefix)) * c)) /\ exists ff_q_ftsp_prefix_left. b = ff_q_ftsp_prefix_left * S ((S (ftsp_index_prefix)) * c) + (ftsp_left_prefix))) /\ ((((exists ff_h_ftsp_prefix_right. ff_h_ftsp_prefix_right + S (ftsp_right_prefix) = S ((S (S ftsp_index_prefix)) * c)) /\ exists ff_q_ftsp_prefix_right. b = ff_q_ftsp_prefix_right * S ((S (S ftsp_index_prefix)) * c) + (ftsp_right_prefix))) /\ (exists ftsp_order_prefix. ftsp_order_prefix + ftsp_left_prefix = ftsp_right_prefix)))) -> (exists ff_u_ftsp_prefix ff_v_ftsp_prefix. ((((exists ff_h_ftsp_prefix_start. ff_h_ftsp_prefix_start + S (1) = S ((S (0)) * ff_v_ftsp_prefix)) /\ exists ff_q_ftsp_prefix_start. ff_u_ftsp_prefix = ff_q_ftsp_prefix_start * S ((S (0)) * ff_v_ftsp_prefix) + (1))) /\ ((((exists ff_h_ftsp_prefix_terminal. ff_h_ftsp_prefix_terminal + S (r) = S ((S (S l)) * ff_v_ftsp_prefix)) /\ exists ff_q_ftsp_prefix_terminal. ff_u_ftsp_prefix = ff_q_ftsp_prefix_terminal * S ((S (S l)) * ff_v_ftsp_prefix) + (r))) /\ forall ff_i_ftsp_prefix. (exists ff_lt_ftsp_prefix_bound. ff_lt_ftsp_prefix_bound + S ff_i_ftsp_prefix = S l) -> exists ff_p_ftsp_prefix ff_r_ftsp_prefix ff_s_ftsp_prefix. ((((exists ff_h_ftsp_prefix_factor. ff_h_ftsp_prefix_factor + S (ff_p_ftsp_prefix) = S ((S (ff_i_ftsp_prefix)) * c)) /\ exists ff_q_ftsp_prefix_factor. b = ff_q_ftsp_prefix_factor * S ((S (ff_i_ftsp_prefix)) * c) + (ff_p_ftsp_prefix))) /\ ((((exists ff_h_ftsp_prefix_partial. ff_h_ftsp_prefix_partial + S (ff_r_ftsp_prefix) = S ((S (ff_i_ftsp_prefix)) * ff_v_ftsp_prefix)) /\ exists ff_q_ftsp_prefix_partial. ff_u_ftsp_prefix = ff_q_ftsp_prefix_partial * S ((S (ff_i_ftsp_prefix)) * ff_v_ftsp_prefix) + (ff_r_ftsp_prefix))) /\ ((((exists ff_h_ftsp_prefix_successor. ff_h_ftsp_prefix_successor + S (ff_s_ftsp_prefix) = S ((S (S ff_i_ftsp_prefix)) * ff_v_ftsp_prefix)) /\ exists ff_q_ftsp_prefix_successor. ff_u_ftsp_prefix = ff_q_ftsp_prefix_successor * S ((S (S ff_i_ftsp_prefix)) * ff_v_ftsp_prefix) + (ff_s_ftsp_prefix))) /\ ff_s_ftsp_prefix = ff_r_ftsp_prefix * ff_p_ftsp_prefix)))))) -> (((exists ff_h_ftsp_prefix_last. ff_h_ftsp_prefix_last + S (q) = S ((S (l)) * c)) /\ exists ff_q_ftsp_prefix_last. b = ff_q_ftsp_prefix_last * S ((S (l)) * c) + (q))) -> (exists ftcn_factor_ftsp_suffix. (r) = (p) * ftcn_factor_ftsp_suffix) -> (exists ftsp_upper_gap. ftsp_upper_gap + q = p) -> q = p

Constructive proof overview

Generated structural guide

A prime dividing a sorted prime prefix equals its terminal factor whenever that terminal factor is bounded by the prime.

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

beta_prime_divisor_product_member Stable theorem; checked-use authorized beta_sorted_factor_le_last Stable theorem; checked-use authorized le_antisymm 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

43 script commands · 7 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–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro r
  5. L5
    intro p
  6. L6
    intro q
  7. L7
    intro hprime
  8. L8
    intro hallprime
  9. L9
    intro hsorted
  10. L10
    intro hproduct
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hlast
  2. L12
    intro hdivides
  3. L13
    intro hupper
03Establish hmemberL14–23

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

  1. L14
    have hmember : exists i. ((exists k. k + S i = S l) /\ (((exists ff_h_ftsp_prefix_member. ff_h_ftsp_prefix_member + S (p) = S ((S (i)) * c)) /\ exists ff_q_ftsp_prefix_member. b = ff_q_ftsp_prefix_member * S ((S (i)) * c) + (p))))
  2. L15
    specialize beta_prime_divisor_product_member b
  3. L16
    specialize beta_prime_divisor_product_member c
  4. L17
    specialize beta_prime_divisor_product_member (S l)
  5. L18
    specialize beta_prime_divisor_product_member r
  6. L19
    specialize beta_prime_divisor_product_member p
  7. L20
    apply beta_prime_divisor_product_member
  8. L21
    exact hprime
  9. L22
    exact hallprime
  10. L23
    exact hproduct
04Use earlier factsL24–24

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

  1. L24
    exact hdivides
05Separate the logical casesL25–26

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

  1. L25
    cases hmember
  2. L26
    cases hmember_witness
06Establish hlowerL27–36

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

  1. L27
    have hlower : exists k. k + p = q
  2. L28
    specialize beta_sorted_factor_le_last b
  3. L29
    specialize beta_sorted_factor_le_last c
  4. L30
    specialize beta_sorted_factor_le_last l
  5. L31
    specialize beta_sorted_factor_le_last x
  6. L32
    specialize beta_sorted_factor_le_last p
  7. L33
    specialize beta_sorted_factor_le_last q
  8. L34
    apply beta_sorted_factor_le_last
  9. L35
    exact hmember_witness_left
  10. L36
    exact hmember_witness_right
07Use earlier factsL37–43

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

  1. L37
    exact hlast
  2. L38
    exact hsorted
  3. L39
    specialize le_antisymm q
  4. L40
    specialize le_antisymm p
  5. L41
    apply le_antisymm
  6. L42
    exact hupper
  7. L43
    exact hlower

Library-wide reading audit

Original exact command ledger · 43 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro r
  5. 0005intro p
  6. 0006intro q
  7. 0007intro hprime
  8. 0008intro hallprime
  9. 0009intro hsorted
  10. 0010intro hproduct
  11. 0011intro hlast
  12. 0012intro hdivides
  13. 0013intro hupper
  14. 0014have hmember : exists i. ((exists k. k + S i = S l) /\ (((exists ff_h_ftsp_prefix_member. ff_h_ftsp_prefix_member + S (p) = S ((S (i)) * c)) /\ exists ff_q_ftsp_prefix_member. b = ff_q_ftsp_prefix_member * S ((S (i)) * c) + (p))))
  15. 0015specialize beta_prime_divisor_product_member b
  16. 0016specialize beta_prime_divisor_product_member c
  17. 0017specialize beta_prime_divisor_product_member (S l)
  18. 0018specialize beta_prime_divisor_product_member r
  19. 0019specialize beta_prime_divisor_product_member p
  20. 0020apply beta_prime_divisor_product_member
  21. 0021exact hprime
  22. 0022exact hallprime
  23. 0023exact hproduct
  24. 0024exact hdivides
  25. 0025cases hmember
  26. 0026cases hmember_witness
  27. 0027have hlower : exists k. k + p = q
  28. 0028specialize beta_sorted_factor_le_last b
  29. 0029specialize beta_sorted_factor_le_last c
  30. 0030specialize beta_sorted_factor_le_last l
  31. 0031specialize beta_sorted_factor_le_last x
  32. 0032specialize beta_sorted_factor_le_last p
  33. 0033specialize beta_sorted_factor_le_last q
  34. 0034apply beta_sorted_factor_le_last
  35. 0035exact hmember_witness_left
  36. 0036exact hmember_witness_right
  37. 0037exact hlast
  38. 0038exact hsorted
  39. 0039specialize le_antisymm q
  40. 0040specialize le_antisymm p
  41. 0041apply le_antisymm
  42. 0042exact hupper
  43. 0043exact hlower