MV0011

mobius_prime_factor_list_append

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

The beta extension theorem constructs a new actual prime list with one more occurrence and product n*p; no sorted or preselected factorization is supplied.

Exact expanded first-order arithmetic statement

forall n b c l p. ((~(n = 0) /\ ((exists ff_u_fsat_mps_append_source_product ff_v_fsat_mps_append_source_product. ((((exists ff_h_fsat_mps_append_source_product_start. ff_h_fsat_mps_append_source_product_start + S (1) = S ((S (0)) * ff_v_fsat_mps_append_source_product)) /\ exists ff_q_fsat_mps_append_source_product_start. ff_u_fsat_mps_append_source_product = ff_q_fsat_mps_append_source_product_start * S ((S (0)) * ff_v_fsat_mps_append_source_product) + (1))) /\ ((((exists ff_h_fsat_mps_append_source_product_terminal. ff_h_fsat_mps_append_source_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_mps_append_source_product)) /\ exists ff_q_fsat_mps_append_source_product_terminal. ff_u_fsat_mps_append_source_product = ff_q_fsat_mps_append_source_product_terminal * S ((S (l)) * ff_v_fsat_mps_append_source_product) + (n))) /\ forall ff_i_fsat_mps_append_source_product. (exists ff_lt_fsat_mps_append_source_product_bound. ff_lt_fsat_mps_append_source_product_bound + S ff_i_fsat_mps_append_source_product = l) -> exists ff_p_fsat_mps_append_source_product ff_r_fsat_mps_append_source_product ff_s_fsat_mps_append_source_product. ((((exists ff_h_fsat_mps_append_source_product_factor. ff_h_fsat_mps_append_source_product_factor + S (ff_p_fsat_mps_append_source_product) = S ((S (ff_i_fsat_mps_append_source_product)) * c)) /\ exists ff_q_fsat_mps_append_source_product_factor. b = ff_q_fsat_mps_append_source_product_factor * S ((S (ff_i_fsat_mps_append_source_product)) * c) + (ff_p_fsat_mps_append_source_product))) /\ ((((exists ff_h_fsat_mps_append_source_product_partial. ff_h_fsat_mps_append_source_product_partial + S (ff_r_fsat_mps_append_source_product) = S ((S (ff_i_fsat_mps_append_source_product)) * ff_v_fsat_mps_append_source_product)) /\ exists ff_q_fsat_mps_append_source_product_partial. ff_u_fsat_mps_append_source_product = ff_q_fsat_mps_append_source_product_partial * S ((S (ff_i_fsat_mps_append_source_product)) * ff_v_fsat_mps_append_source_product) + (ff_r_fsat_mps_append_source_product))) /\ ((((exists ff_h_fsat_mps_append_source_product_successor. ff_h_fsat_mps_append_source_product_successor + S (ff_s_fsat_mps_append_source_product) = S ((S (S ff_i_fsat_mps_append_source_product)) * ff_v_fsat_mps_append_source_product)) /\ exists ff_q_fsat_mps_append_source_product_successor. ff_u_fsat_mps_append_source_product = ff_q_fsat_mps_append_source_product_successor * S ((S (S ff_i_fsat_mps_append_source_product)) * ff_v_fsat_mps_append_source_product) + (ff_s_fsat_mps_append_source_product))) /\ ff_s_fsat_mps_append_source_product = ff_r_fsat_mps_append_source_product * ff_p_fsat_mps_append_source_product)))))) /\ (forall ftsf_index_fsat_mps_append_source_primes. (exists ftsf_gap_fsat_mps_append_source_primes_bound. ftsf_gap_fsat_mps_append_source_primes_bound + S ftsf_index_fsat_mps_append_source_primes = (l)) -> exists ftsf_factor_fsat_mps_append_source_primes. ((((exists ff_h_ftsf_fsat_mps_append_source_primes_entry. ff_h_ftsf_fsat_mps_append_source_primes_entry + S (ftsf_factor_fsat_mps_append_source_primes) = S ((S (ftsf_index_fsat_mps_append_source_primes)) * c)) /\ exists ff_q_ftsf_fsat_mps_append_source_primes_entry. b = ff_q_ftsf_fsat_mps_append_source_primes_entry * S ((S (ftsf_index_fsat_mps_append_source_primes)) * c) + (ftsf_factor_fsat_mps_append_source_primes))) /\ ((~(ftsf_factor_fsat_mps_append_source_primes = 1) /\ forall frm_prime_left_ftsf_fsat_mps_append_source_primes_prime frm_prime_right_ftsf_fsat_mps_append_source_primes_prime. ftsf_factor_fsat_mps_append_source_primes = frm_prime_left_ftsf_fsat_mps_append_source_primes_prime * frm_prime_right_ftsf_fsat_mps_append_source_primes_prime -> frm_prime_left_ftsf_fsat_mps_append_source_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_mps_append_source_primes_prime = 1))))))) -> (~((p) = 1) /\ forall pvs_left_append_prime pvs_right_append_prime. (p) = pvs_left_append_prime * pvs_right_append_prime -> pvs_left_append_prime = 1 \/ pvs_right_append_prime = 1) -> exists d e. ((~(n * p = 0) /\ ((exists ff_u_fsat_mps_append_target_product ff_v_fsat_mps_append_target_product. ((((exists ff_h_fsat_mps_append_target_product_start. ff_h_fsat_mps_append_target_product_start + S (1) = S ((S (0)) * ff_v_fsat_mps_append_target_product)) /\ exists ff_q_fsat_mps_append_target_product_start. ff_u_fsat_mps_append_target_product = ff_q_fsat_mps_append_target_product_start * S ((S (0)) * ff_v_fsat_mps_append_target_product) + (1))) /\ ((((exists ff_h_fsat_mps_append_target_product_terminal. ff_h_fsat_mps_append_target_product_terminal + S (n * p) = S ((S (S l)) * ff_v_fsat_mps_append_target_product)) /\ exists ff_q_fsat_mps_append_target_product_terminal. ff_u_fsat_mps_append_target_product = ff_q_fsat_mps_append_target_product_terminal * S ((S (S l)) * ff_v_fsat_mps_append_target_product) + (n * p))) /\ forall ff_i_fsat_mps_append_target_product. (exists ff_lt_fsat_mps_append_target_product_bound. ff_lt_fsat_mps_append_target_product_bound + S ff_i_fsat_mps_append_target_product = S l) -> exists ff_p_fsat_mps_append_target_product ff_r_fsat_mps_append_target_product ff_s_fsat_mps_append_target_product. ((((exists ff_h_fsat_mps_append_target_product_factor. ff_h_fsat_mps_append_target_product_factor + S (ff_p_fsat_mps_append_target_product) = S ((S (ff_i_fsat_mps_append_target_product)) * e)) /\ exists ff_q_fsat_mps_append_target_product_factor. d = ff_q_fsat_mps_append_target_product_factor * S ((S (ff_i_fsat_mps_append_target_product)) * e) + (ff_p_fsat_mps_append_target_product))) /\ ((((exists ff_h_fsat_mps_append_target_product_partial. ff_h_fsat_mps_append_target_product_partial + S (ff_r_fsat_mps_append_target_product) = S ((S (ff_i_fsat_mps_append_target_product)) * ff_v_fsat_mps_append_target_product)) /\ exists ff_q_fsat_mps_append_target_product_partial. ff_u_fsat_mps_append_target_product = ff_q_fsat_mps_append_target_product_partial * S ((S (ff_i_fsat_mps_append_target_product)) * ff_v_fsat_mps_append_target_product) + (ff_r_fsat_mps_append_target_product))) /\ ((((exists ff_h_fsat_mps_append_target_product_successor. ff_h_fsat_mps_append_target_product_successor + S (ff_s_fsat_mps_append_target_product) = S ((S (S ff_i_fsat_mps_append_target_product)) * ff_v_fsat_mps_append_target_product)) /\ exists ff_q_fsat_mps_append_target_product_successor. ff_u_fsat_mps_append_target_product = ff_q_fsat_mps_append_target_product_successor * S ((S (S ff_i_fsat_mps_append_target_product)) * ff_v_fsat_mps_append_target_product) + (ff_s_fsat_mps_append_target_product))) /\ ff_s_fsat_mps_append_target_product = ff_r_fsat_mps_append_target_product * ff_p_fsat_mps_append_target_product)))))) /\ (forall ftsf_index_fsat_mps_append_target_primes. (exists ftsf_gap_fsat_mps_append_target_primes_bound. ftsf_gap_fsat_mps_append_target_primes_bound + S ftsf_index_fsat_mps_append_target_primes = (S l)) -> exists ftsf_factor_fsat_mps_append_target_primes. ((((exists ff_h_ftsf_fsat_mps_append_target_primes_entry. ff_h_ftsf_fsat_mps_append_target_primes_entry + S (ftsf_factor_fsat_mps_append_target_primes) = S ((S (ftsf_index_fsat_mps_append_target_primes)) * e)) /\ exists ff_q_ftsf_fsat_mps_append_target_primes_entry. d = ff_q_ftsf_fsat_mps_append_target_primes_entry * S ((S (ftsf_index_fsat_mps_append_target_primes)) * e) + (ftsf_factor_fsat_mps_append_target_primes))) /\ ((~(ftsf_factor_fsat_mps_append_target_primes = 1) /\ forall frm_prime_left_ftsf_fsat_mps_append_target_primes_prime frm_prime_right_ftsf_fsat_mps_append_target_primes_prime. ftsf_factor_fsat_mps_append_target_primes = frm_prime_left_ftsf_fsat_mps_append_target_primes_prime * frm_prime_right_ftsf_fsat_mps_append_target_primes_prime -> frm_prime_left_ftsf_fsat_mps_append_target_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_mps_append_target_primes_prime = 1)))))))

Constructive proof overview

Generated structural guide

The beta extension theorem constructs a new actual prime list with one more occurrence and product n*p; no sorted or preselected factorization is supplied.

The unchanged tactic script uses 5 declared prerequisites and contains 53 exact native proof lines.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Proof neighborhood

Direct dependencies

beta_factor_prefix_product_append Alpha theorem; checked-use authorized mul_ne_zero Alpha theorem; checked-use authorized prime_nonzero Alpha theorem; checked-use authorized all_prime_transport Alpha theorem; checked-use authorized all_prime_succ_intro Alpha theorem; checked-use authorized

Direct dependents

MV0015 mobius_fresh_prime_negates

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. The literal dependency-closed bundle is checked by original HA and the independently compiled Lean verifier. Public delivery grants no Alpha checked-use authority or Stable membership.

Read the argument

Proof checkpoints

53 script commands · 15 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–7

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

  1. L1
    intro n
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro l
  5. L5
    intro p
  6. L6
    intro hf
  7. L7
    intro hp
02Separate the logical casesL8–9

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

  1. L8
    cases hf
  2. L9
    cases hf_right
03Establish hextL10–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta factor prefix product append.

  1. L10
    have hext : ∃ d. ∃ e. BetaAt(d,e,l,p) ∧ ((∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(d,e,x,y)) ∧ Product(d,e,S l,n · p))Definitions: LtBetaAtProduct
  2. L11
    specialize beta_factor_prefix_product_append (b)
  3. L12
    specialize beta_factor_prefix_product_append (c)
  4. L13
    specialize beta_factor_prefix_product_append (l)
  5. L14
    specialize beta_factor_prefix_product_append (n)
  6. L15
    specialize beta_factor_prefix_product_append (p)
  7. L16
    apply beta_factor_prefix_product_append
  8. L17
    exact hf_right_left
04Separate the logical casesL18–21

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

  1. L18
    cases hext
  2. L19
    cases hext_witness
  3. L20
    cases hext_witness_witness
  4. L21
    cases hext_witness_witness_right
05Construct an explicit witnessL22–23

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

  1. L22
    exists x
  2. L23
    exists x1
06Separate the logical casesL24–24

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

  1. L24
    split
07Fix variables and assumptionsL25–25

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

  1. L25
    intro hz
08Use earlier factsL26–29

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

  1. L26
    specialize mul_ne_zero (n)
  2. L27
    specialize mul_ne_zero (p)
  3. L28
    apply mul_ne_zero
  4. L29
    exact hf_left
09Fix variables and assumptionsL30–30

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

  1. L30
    intro hpz
10Use earlier factsL31–35

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

  1. L31
    specialize prime_nonzero (p)
  2. L32
    apply prime_nonzero
  3. L33
    exact hp
  4. L34
    exact hpz
  5. L35
    exact hz
11Separate the logical casesL36–36

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

  1. L36
    split
12Use earlier factsL37–46

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

  1. L37
    exact hext_witness_witness_right_right
  2. L38
    specialize all_prime_succ_intro (x)
  3. L39
    specialize all_prime_succ_intro (x1)
  4. L40
    specialize all_prime_succ_intro (l)
  5. L41
    specialize all_prime_succ_intro (p)
  6. L42
    apply all_prime_succ_intro
  7. L43
    specialize all_prime_transport (b)
  8. L44
    specialize all_prime_transport (c)
  9. L45
    specialize all_prime_transport (x)
  10. L46
    specialize all_prime_transport (x1)
13Use earlier factsL47–50

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

  1. L47
    specialize all_prime_transport (l)
  2. L48
    apply all_prime_transport
  3. L49
    exact hf_right_right
  4. L50
    exact hext_witness_witness_right_left
14Separate the logical casesL51–51

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

  1. L51
    split
15Use earlier factsL52–53

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

  1. L52
    exact hext_witness_witness_left
  2. L53
    exact hp

Library-wide reading audit

Original exact command ledger · 53 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro l
  5. 0005intro p
  6. 0006intro hf
  7. 0007intro hp
  8. 0008cases hf
  9. 0009cases hf_right
  10. 0010have hext : exists d e. ((((exists ff_h_pvs_append_last. ff_h_pvs_append_last + S (p) = S ((S (l)) * e)) /\ exists ff_q_pvs_append_last. d = ff_q_pvs_append_last * S ((S (l)) * e) + (p))) /\ (((forall pfp_i_append_preserved pfp_a_append_preserved. (exists pfp_gap_append_preservedbound. pfp_gap_append_preservedbound + S (pfp_i_append_preserved) = (l)) -> (((exists ff_h_pfp_append_preservedold. ff_h_pfp_append_preservedold + S (pfp_a_append_preserved) = S ((S (pfp_i_append_preserved)) * c)) /\ exists ff_q_pfp_append_preservedold. b = ff_q_pfp_append_preservedold * S ((S (pfp_i_append_preserved)) * c) + (pfp_a_append_preserved))) -> (((exists ff_h_pfp_append_preservednew. ff_h_pfp_append_preservednew + S (pfp_a_append_preserved) = S ((S (pfp_i_append_preserved)) * e)) /\ exists ff_q_pfp_append_preservednew. d = ff_q_pfp_append_preservednew * S ((S (pfp_i_append_preserved)) * e) + (pfp_a_append_preserved)))) /\ (exists ff_u_fsat_append_product ff_v_fsat_append_product. ((((exists ff_h_fsat_append_product_start. ff_h_fsat_append_product_start + S (1) = S ((S (0)) * ff_v_fsat_append_product)) /\ exists ff_q_fsat_append_product_start. ff_u_fsat_append_product = ff_q_fsat_append_product_start * S ((S (0)) * ff_v_fsat_append_product) + (1))) /\ ((((exists ff_h_fsat_append_product_terminal. ff_h_fsat_append_product_terminal + S (n * p) = S ((S (S l)) * ff_v_fsat_append_product)) /\ exists ff_q_fsat_append_product_terminal. ff_u_fsat_append_product = ff_q_fsat_append_product_terminal * S ((S (S l)) * ff_v_fsat_append_product) + (n * p))) /\ forall ff_i_fsat_append_product. (exists ff_lt_fsat_append_product_bound. ff_lt_fsat_append_product_bound + S ff_i_fsat_append_product = S l) -> exists ff_p_fsat_append_product ff_r_fsat_append_product ff_s_fsat_append_product. ((((exists ff_h_fsat_append_product_factor. ff_h_fsat_append_product_factor + S (ff_p_fsat_append_product) = S ((S (ff_i_fsat_append_product)) * e)) /\ exists ff_q_fsat_append_product_factor. d = ff_q_fsat_append_product_factor * S ((S (ff_i_fsat_append_product)) * e) + (ff_p_fsat_append_product))) /\ ((((exists ff_h_fsat_append_product_partial. ff_h_fsat_append_product_partial + S (ff_r_fsat_append_product) = S ((S (ff_i_fsat_append_product)) * ff_v_fsat_append_product)) /\ exists ff_q_fsat_append_product_partial. ff_u_fsat_append_product = ff_q_fsat_append_product_partial * S ((S (ff_i_fsat_append_product)) * ff_v_fsat_append_product) + (ff_r_fsat_append_product))) /\ ((((exists ff_h_fsat_append_product_successor. ff_h_fsat_append_product_successor + S (ff_s_fsat_append_product) = S ((S (S ff_i_fsat_append_product)) * ff_v_fsat_append_product)) /\ exists ff_q_fsat_append_product_successor. ff_u_fsat_append_product = ff_q_fsat_append_product_successor * S ((S (S ff_i_fsat_append_product)) * ff_v_fsat_append_product) + (ff_s_fsat_append_product))) /\ ff_s_fsat_append_product = ff_r_fsat_append_product * ff_p_fsat_append_product)))))))))
  11. 0011specialize beta_factor_prefix_product_append (b)
  12. 0012specialize beta_factor_prefix_product_append (c)
  13. 0013specialize beta_factor_prefix_product_append (l)
  14. 0014specialize beta_factor_prefix_product_append (n)
  15. 0015specialize beta_factor_prefix_product_append (p)
  16. 0016apply beta_factor_prefix_product_append
  17. 0017exact hf_right_left
  18. 0018cases hext
  19. 0019cases hext_witness
  20. 0020cases hext_witness_witness
  21. 0021cases hext_witness_witness_right
  22. 0022exists x
  23. 0023exists x1
  24. 0024split
  25. 0025intro hz
  26. 0026specialize mul_ne_zero (n)
  27. 0027specialize mul_ne_zero (p)
  28. 0028apply mul_ne_zero
  29. 0029exact hf_left
  30. 0030intro hpz
  31. 0031specialize prime_nonzero (p)
  32. 0032apply prime_nonzero
  33. 0033exact hp
  34. 0034exact hpz
  35. 0035exact hz
  36. 0036split
  37. 0037exact hext_witness_witness_right_right
  38. 0038specialize all_prime_succ_intro (x)
  39. 0039specialize all_prime_succ_intro (x1)
  40. 0040specialize all_prime_succ_intro (l)
  41. 0041specialize all_prime_succ_intro (p)
  42. 0042apply all_prime_succ_intro
  43. 0043specialize all_prime_transport (b)
  44. 0044specialize all_prime_transport (c)
  45. 0045specialize all_prime_transport (x)
  46. 0046specialize all_prime_transport (x1)
  47. 0047specialize all_prime_transport (l)
  48. 0048apply all_prime_transport
  49. 0049exact hf_right_right
  50. 0050exact hext_witness_witness_right_left
  51. 0051split
  52. 0052exact hext_witness_witness_left
  53. 0053exact hp