MV0011

mobius_prime_factor_list_append

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.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Mobius(n,z) is positive-domain only, independently defined from squarefreeness and actual prime-factor parity. Signed codes 0, 2 and 1 represent zero, +1 and -1. This family proves values and prime-adjunction laws; the separate Möbius-inversion family supplies the complete G007 endpoint.

Exact theorem in conservative defined notation

∀ n. ∀ b. ∀ c. ∀ l. ∀ p. PrimeFactorList(n,b,c,l) → Prime(p) → ∃ x. ∃ y. PrimeFactorList(n · p,x,y,S l)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

PrimeFactorList(n,b,c,l) · 2Lt(a,b) · 1Prime(p) · 1BetaAt(b,c,i,x) · 3Product(b,c,l,z) · 1

Actual proof prerequisites

beta_factor_prefix_product_append · checked external prerequisitemul_ne_zero · checked external prerequisiteprime_nonzero · checked external prerequisiteall_prime_transport · checked external prerequisiteall_prime_succ_intro · checked external prerequisite
Original expanded first-order 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)))))))

Complete tactic proof in conservative notation

All 53 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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: BetaAt(d,e,l,p)Lt(x,l)BetaAt(b,c,x,y)BetaAt(d,e,x,y)Product(d,e,S l,n · p)Original native command in the exact edition
  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 defined 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 : ∃ 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))
  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