JT005E

jordan_prime_power_tuple_primitive_of_not_all_divisible

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

Every nonunit common divisor has an actual prime divisor; prime-power support then forces a forbidden common factor p.

Exact expanded first-order arithmetic statement

forall p e n b c k. (~((p) = 1) /\ forall pvs_left_jordan_base pvs_right_jordan_base. (p) = pvs_left_jordan_base * pvs_right_jordan_base -> pvs_left_jordan_base = 1 \/ pvs_right_jordan_base = 1) -> (exists pa_b_pvs_jordan_power pa_c_pvs_jordan_power. ((forall pa_i_pvs_jordan_power_repeat. (exists pa_lt_pvs_jordan_power_repeat_bound. pa_lt_pvs_jordan_power_repeat_bound + S pa_i_pvs_jordan_power_repeat = e) -> (((exists pa_h_pvs_jordan_power_repeat_decoded. pa_h_pvs_jordan_power_repeat_decoded + S (p) = S ((S (pa_i_pvs_jordan_power_repeat)) * pa_c_pvs_jordan_power)) /\ exists pa_q_pvs_jordan_power_repeat_decoded. pa_b_pvs_jordan_power = pa_q_pvs_jordan_power_repeat_decoded * S ((S (pa_i_pvs_jordan_power_repeat)) * pa_c_pvs_jordan_power) + (p)))) /\ (exists pa_u_pvs_jordan_power_product pa_v_pvs_jordan_power_product. ((((exists pa_h_pvs_jordan_power_product_start. pa_h_pvs_jordan_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_jordan_power_product)) /\ exists pa_q_pvs_jordan_power_product_start. pa_u_pvs_jordan_power_product = pa_q_pvs_jordan_power_product_start * S ((S (0)) * pa_v_pvs_jordan_power_product) + (1))) /\ ((((exists pa_h_pvs_jordan_power_product_terminal. pa_h_pvs_jordan_power_product_terminal + S (n) = S ((S (e)) * pa_v_pvs_jordan_power_product)) /\ exists pa_q_pvs_jordan_power_product_terminal. pa_u_pvs_jordan_power_product = pa_q_pvs_jordan_power_product_terminal * S ((S (e)) * pa_v_pvs_jordan_power_product) + (n))) /\ forall pa_i_pvs_jordan_power_product. (exists pa_lt_pvs_jordan_power_product_bound. pa_lt_pvs_jordan_power_product_bound + S pa_i_pvs_jordan_power_product = e) -> exists pa_p_pvs_jordan_power_product pa_r_pvs_jordan_power_product pa_s_pvs_jordan_power_product. ((((exists pa_h_pvs_jordan_power_product_factor. pa_h_pvs_jordan_power_product_factor + S (pa_p_pvs_jordan_power_product) = S ((S (pa_i_pvs_jordan_power_product)) * pa_c_pvs_jordan_power)) /\ exists pa_q_pvs_jordan_power_product_factor. pa_b_pvs_jordan_power = pa_q_pvs_jordan_power_product_factor * S ((S (pa_i_pvs_jordan_power_product)) * pa_c_pvs_jordan_power) + (pa_p_pvs_jordan_power_product))) /\ ((((exists pa_h_pvs_jordan_power_product_partial. pa_h_pvs_jordan_power_product_partial + S (pa_r_pvs_jordan_power_product) = S ((S (pa_i_pvs_jordan_power_product)) * pa_v_pvs_jordan_power_product)) /\ exists pa_q_pvs_jordan_power_product_partial. pa_u_pvs_jordan_power_product = pa_q_pvs_jordan_power_product_partial * S ((S (pa_i_pvs_jordan_power_product)) * pa_v_pvs_jordan_power_product) + (pa_r_pvs_jordan_power_product))) /\ ((((exists pa_h_pvs_jordan_power_product_successor. pa_h_pvs_jordan_power_product_successor + S (pa_s_pvs_jordan_power_product) = S ((S (S pa_i_pvs_jordan_power_product)) * pa_v_pvs_jordan_power_product)) /\ exists pa_q_pvs_jordan_power_product_successor. pa_u_pvs_jordan_power_product = pa_q_pvs_jordan_power_product_successor * S ((S (S pa_i_pvs_jordan_power_product)) * pa_v_pvs_jordan_power_product) + (pa_s_pvs_jordan_power_product))) /\ pa_s_pvs_jordan_power_product = pa_r_pvs_jordan_power_product * pa_p_pvs_jordan_power_product)))))))) -> (~(forall jt_index_power_all_divisible jt_value_power_all_divisible. (exists jt_gap_power_all_divisibleindex. jt_gap_power_all_divisibleindex+S (jt_index_power_all_divisible)=(k)) -> (((exists fs_h_jt_power_all_divisibleat. fs_h_jt_power_all_divisibleat + S (jt_value_power_all_divisible) = S ((S (jt_index_power_all_divisible)) * c)) /\ exists fs_q_jt_power_all_divisibleat. b = fs_q_jt_power_all_divisibleat * S ((S (jt_index_power_all_divisible)) * c) + (jt_value_power_all_divisible))) -> (exists jt_factor_power_all_divisibledivides. (jt_value_power_all_divisible)=(p)*jt_factor_power_all_divisibledivides))) -> forall jt_divisor_power_primitive. (exists jt_factor_power_primitivemodulus. (n)=(jt_divisor_power_primitive)*jt_factor_power_primitivemodulus) -> (forall jt_index_power_primitivecoordinates jt_value_power_primitivecoordinates. (exists jt_gap_power_primitivecoordinatesindex. jt_gap_power_primitivecoordinatesindex+S (jt_index_power_primitivecoordinates)=(k)) -> (((exists fs_h_jt_power_primitivecoordinatesat. fs_h_jt_power_primitivecoordinatesat + S (jt_value_power_primitivecoordinates) = S ((S (jt_index_power_primitivecoordinates)) * c)) /\ exists fs_q_jt_power_primitivecoordinatesat. b = fs_q_jt_power_primitivecoordinatesat * S ((S (jt_index_power_primitivecoordinates)) * c) + (jt_value_power_primitivecoordinates))) -> (exists jt_factor_power_primitivecoordinatesdivides. (jt_value_power_primitivecoordinates)=(jt_divisor_power_primitive)*jt_factor_power_primitivecoordinatesdivides)) -> jt_divisor_power_primitive=1

Constructive proof overview

Generated structural guide

Every nonunit common divisor has an actual prime divisor; prime-power support then forces a forbidden common factor p.

The unchanged tactic script uses 9 declared prerequisites and contains 75 exact native proof lines.

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

Proof neighborhood

Direct dependencies

pow_nonzero_of_one_le Alpha theorem; checked-use authorized one_le_of_ne_zero Alpha theorem; checked-use authorized prime_nonzero Alpha theorem; checked-use authorized eq_decidable Alpha theorem; checked-use authorized mul_zero_left Alpha theorem; checked-use authorized prime_divisor_exists Alpha theorem; checked-use authorized multiple_trans Alpha theorem; checked-use authorized prime_divisor_of_prime_power Alpha theorem; checked-use authorized JT0007 jordan_tuple_divisor_downward

Direct dependents

JT005F jordan_prime_power_tuple_primitive_characterization JT0060 jordan_prime_power_tuple_primitivity_invariant

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

75 script commands · 21 reading checkpoints · 5 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.

Named ingredients (1)
jordan tuple divisor downward
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro e
  3. L3
    intro n
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro k
  7. L7
    intro hp
  8. L8
    intro hpow
  9. L9
    intro hnot
02Establish hnL10–19

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

  1. L10
    have hn : ~(n=0)
  2. L11
    intro hz
  3. L12
    specialize pow_nonzero_of_one_le (p)
  4. L13
    specialize pow_nonzero_of_one_le (e)
  5. L14
    specialize pow_nonzero_of_one_le (n)
  6. L15
    apply pow_nonzero_of_one_le
  7. L16
    specialize one_le_of_ne_zero (p)
  8. L17
    apply one_le_of_ne_zero
  9. L18
    intro hpzero
  10. L19
    specialize prime_nonzero (p)
03Use earlier factsL20–24

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

  1. L20
    apply prime_nonzero
  2. L21
    exact hp
  3. L22
    exact hpzero
  4. L23
    exact hpow
  5. L24
    exact hz
04Fix variables and assumptionsL25–27

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

  1. L25
    intro d
  2. L26
    intro hd
  3. L27
    intro hall
05Use earlier factsL28–29

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

  1. L28
    specialize eq_decidable d
  2. L29
    specialize eq_decidable 1
06Separate the logical casesL30–30

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

  1. L30
    cases eq_decidable
07Use earlier factsL31–31

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

  1. L31
    exact eq_decidable_left
08Separate the logical casesL32–32

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

  1. L32
    exfalso
09Use earlier factsL33–33

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

  1. L33
    apply hnot
10Establish hdnonzeroL34–36

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

  1. L34
    have hdnonzero : ~(d=0)
  2. L35
    intro hz
  3. L36
    apply hn
11Separate the logical casesL37–37

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

  1. L37
    cases hd
12Calculate and transport equalitiesL38–38

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

  1. L38
    trans d*x
13Use earlier factsL39–39

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

  1. L39
    exact hd_witness
14Calculate and transport equalitiesL40–40

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

  1. L40
    rewrite hz
15Use earlier factsL41–42

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

  1. L41
    specialize mul_zero_left (x)
  2. L42
    apply mul_zero_left
16Establish hprimeL43–47

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

  1. L43
    have hprime : exists q. ((~((q) = 1) /\ forall pvs_left_jordan_common_prime pvs_right_jordan_common_prime. (q) = pvs_left_jordan_common_prime * pvs_right_jordan_common_prime -> pvs_left_jordan_common_prime = 1 \/ pvs_right_jordan_common_prime = 1) /\ (exists jt_factor_jordan_common_divisor. (d)=(q)*jt_factor_jordan_common_divisor))
  2. L44
    specialize prime_divisor_exists (d)
  3. L45
    apply prime_divisor_exists
  4. L46
    exact hdnonzero
  5. L47
    exact eq_decidable_right
17Separate the logical casesL48–49

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

  1. L48
    cases hprime
  2. L49
    cases hprime_witness
18Establish hqnL50–56

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

  1. L50
    have hqn : exists jt_factor_jordan_modulus_prime. (n)=(x)*jt_factor_jordan_modulus_prime
  2. L51
    specialize multiple_trans (d)
  3. L52
    specialize multiple_trans (x)
  4. L53
    specialize multiple_trans (n)
  5. L54
    apply multiple_trans
  6. L55
    exact hd
  7. L56
    exact hprime_witness_right
19Establish hqpL57–66

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

  1. L57
    have hqp : x=p
  2. L58
    specialize prime_divisor_of_prime_power (p)
  3. L59
    specialize prime_divisor_of_prime_power (x)
  4. L60
    specialize prime_divisor_of_prime_power (e)
  5. L61
    specialize prime_divisor_of_prime_power (n)
  6. L62
    apply prime_divisor_of_prime_power
  7. L63
    exact hp
  8. L64
    exact hprime_witness_left
  9. L65
    exact hpow
  10. L66
    exact hqn
20Calculate and transport equalitiesL67–67

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

  1. L67
    rewrite <- hqp
21Use earlier factsL68–75

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

  1. L68
    specialize jordan_tuple_divisor_downward (x)
  2. L69
    specialize jordan_tuple_divisor_downward (d)
  3. L70
    specialize jordan_tuple_divisor_downward (b)
  4. L71
    specialize jordan_tuple_divisor_downward (c)
  5. L72
    specialize jordan_tuple_divisor_downward (k)
  6. L73
    apply jordan_tuple_divisor_downward
  7. L74
    exact hprime_witness_right
  8. L75
    exact hall

Library-wide reading audit

Original exact command ledger · 75 lines
  1. 0001intro p
  2. 0002intro e
  3. 0003intro n
  4. 0004intro b
  5. 0005intro c
  6. 0006intro k
  7. 0007intro hp
  8. 0008intro hpow
  9. 0009intro hnot
  10. 0010have hn : ~(n=0)
  11. 0011intro hz
  12. 0012specialize pow_nonzero_of_one_le (p)
  13. 0013specialize pow_nonzero_of_one_le (e)
  14. 0014specialize pow_nonzero_of_one_le (n)
  15. 0015apply pow_nonzero_of_one_le
  16. 0016specialize one_le_of_ne_zero (p)
  17. 0017apply one_le_of_ne_zero
  18. 0018intro hpzero
  19. 0019specialize prime_nonzero (p)
  20. 0020apply prime_nonzero
  21. 0021exact hp
  22. 0022exact hpzero
  23. 0023exact hpow
  24. 0024exact hz
  25. 0025intro d
  26. 0026intro hd
  27. 0027intro hall
  28. 0028specialize eq_decidable d
  29. 0029specialize eq_decidable 1
  30. 0030cases eq_decidable
  31. 0031exact eq_decidable_left
  32. 0032exfalso
  33. 0033apply hnot
  34. 0034have hdnonzero : ~(d=0)
  35. 0035intro hz
  36. 0036apply hn
  37. 0037cases hd
  38. 0038trans d*x
  39. 0039exact hd_witness
  40. 0040rewrite hz
  41. 0041specialize mul_zero_left (x)
  42. 0042apply mul_zero_left
  43. 0043have hprime : exists q. ((~((q) = 1) /\ forall pvs_left_jordan_common_prime pvs_right_jordan_common_prime. (q) = pvs_left_jordan_common_prime * pvs_right_jordan_common_prime -> pvs_left_jordan_common_prime = 1 \/ pvs_right_jordan_common_prime = 1) /\ (exists jt_factor_jordan_common_divisor. (d)=(q)*jt_factor_jordan_common_divisor))
  44. 0044specialize prime_divisor_exists (d)
  45. 0045apply prime_divisor_exists
  46. 0046exact hdnonzero
  47. 0047exact eq_decidable_right
  48. 0048cases hprime
  49. 0049cases hprime_witness
  50. 0050have hqn : exists jt_factor_jordan_modulus_prime. (n)=(x)*jt_factor_jordan_modulus_prime
  51. 0051specialize multiple_trans (d)
  52. 0052specialize multiple_trans (x)
  53. 0053specialize multiple_trans (n)
  54. 0054apply multiple_trans
  55. 0055exact hd
  56. 0056exact hprime_witness_right
  57. 0057have hqp : x=p
  58. 0058specialize prime_divisor_of_prime_power (p)
  59. 0059specialize prime_divisor_of_prime_power (x)
  60. 0060specialize prime_divisor_of_prime_power (e)
  61. 0061specialize prime_divisor_of_prime_power (n)
  62. 0062apply prime_divisor_of_prime_power
  63. 0063exact hp
  64. 0064exact hprime_witness_left
  65. 0065exact hpow
  66. 0066exact hqn
  67. 0067rewrite <- hqp
  68. 0068specialize jordan_tuple_divisor_downward (x)
  69. 0069specialize jordan_tuple_divisor_downward (d)
  70. 0070specialize jordan_tuple_divisor_downward (b)
  71. 0071specialize jordan_tuple_divisor_downward (c)
  72. 0072specialize jordan_tuple_divisor_downward (k)
  73. 0073apply jordan_tuple_divisor_downward
  74. 0074exact hprime_witness_right
  75. 0075exact hall