JT0060

jordan_prime_power_tuple_primitivity_invariant

Primitivity of an actual beta tuple is invariant under changing the positive exponent of its prime-power modulus.

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

95 new Alpha admissions come from 96 source lemmas: tuple equality reflexivity reuses an already-admitted theorem and is not counted twice. All counts use actual finite beta-coded enumerations. G008 multiplicativity is proved; the general prime-power count and distinct-prime product formula are further goals. General prime-power fields (G091) remain open. Stable is unchanged.

Exact theorem in conservative defined notation

∀ p. ∀ h. ∀ j. ∀ m. ∀ n. ∀ b. ∀ c. ∀ k. Prime(p) → Pow(p,S h,m) → Pow(p,S j,n) → JordanPrimitiveTuple(m,b,c,k) → JordanPrimitiveTuple(n,b,c,k)

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

Definition DAG

JordanPrimitiveTuple(n,b,c,k) · 2Prime(p) · 1Pow(a,e,z) · 2

Actual proof prerequisites

jordan_prime_power_tuple_primitive_of_not_all_divisiblejordan_primitive_tuple_avoids_prime_common_divisorpow_positive_exponent_base_divides · checked external prerequisitesucc_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall p h j m 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_first_power pa_c_pvs_jordan_first_power. ((forall pa_i_pvs_jordan_first_power_repeat. (exists pa_lt_pvs_jordan_first_power_repeat_bound. pa_lt_pvs_jordan_first_power_repeat_bound + S pa_i_pvs_jordan_first_power_repeat = S h) -> (((exists pa_h_pvs_jordan_first_power_repeat_decoded. pa_h_pvs_jordan_first_power_repeat_decoded + S (p) = S ((S (pa_i_pvs_jordan_first_power_repeat)) * pa_c_pvs_jordan_first_power)) /\ exists pa_q_pvs_jordan_first_power_repeat_decoded. pa_b_pvs_jordan_first_power = pa_q_pvs_jordan_first_power_repeat_decoded * S ((S (pa_i_pvs_jordan_first_power_repeat)) * pa_c_pvs_jordan_first_power) + (p)))) /\ (exists pa_u_pvs_jordan_first_power_product pa_v_pvs_jordan_first_power_product. ((((exists pa_h_pvs_jordan_first_power_product_start. pa_h_pvs_jordan_first_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_jordan_first_power_product)) /\ exists pa_q_pvs_jordan_first_power_product_start. pa_u_pvs_jordan_first_power_product = pa_q_pvs_jordan_first_power_product_start * S ((S (0)) * pa_v_pvs_jordan_first_power_product) + (1))) /\ ((((exists pa_h_pvs_jordan_first_power_product_terminal. pa_h_pvs_jordan_first_power_product_terminal + S (m) = S ((S (S h)) * pa_v_pvs_jordan_first_power_product)) /\ exists pa_q_pvs_jordan_first_power_product_terminal. pa_u_pvs_jordan_first_power_product = pa_q_pvs_jordan_first_power_product_terminal * S ((S (S h)) * pa_v_pvs_jordan_first_power_product) + (m))) /\ forall pa_i_pvs_jordan_first_power_product. (exists pa_lt_pvs_jordan_first_power_product_bound. pa_lt_pvs_jordan_first_power_product_bound + S pa_i_pvs_jordan_first_power_product = S h) -> exists pa_p_pvs_jordan_first_power_product pa_r_pvs_jordan_first_power_product pa_s_pvs_jordan_first_power_product. ((((exists pa_h_pvs_jordan_first_power_product_factor. pa_h_pvs_jordan_first_power_product_factor + S (pa_p_pvs_jordan_first_power_product) = S ((S (pa_i_pvs_jordan_first_power_product)) * pa_c_pvs_jordan_first_power)) /\ exists pa_q_pvs_jordan_first_power_product_factor. pa_b_pvs_jordan_first_power = pa_q_pvs_jordan_first_power_product_factor * S ((S (pa_i_pvs_jordan_first_power_product)) * pa_c_pvs_jordan_first_power) + (pa_p_pvs_jordan_first_power_product))) /\ ((((exists pa_h_pvs_jordan_first_power_product_partial. pa_h_pvs_jordan_first_power_product_partial + S (pa_r_pvs_jordan_first_power_product) = S ((S (pa_i_pvs_jordan_first_power_product)) * pa_v_pvs_jordan_first_power_product)) /\ exists pa_q_pvs_jordan_first_power_product_partial. pa_u_pvs_jordan_first_power_product = pa_q_pvs_jordan_first_power_product_partial * S ((S (pa_i_pvs_jordan_first_power_product)) * pa_v_pvs_jordan_first_power_product) + (pa_r_pvs_jordan_first_power_product))) /\ ((((exists pa_h_pvs_jordan_first_power_product_successor. pa_h_pvs_jordan_first_power_product_successor + S (pa_s_pvs_jordan_first_power_product) = S ((S (S pa_i_pvs_jordan_first_power_product)) * pa_v_pvs_jordan_first_power_product)) /\ exists pa_q_pvs_jordan_first_power_product_successor. pa_u_pvs_jordan_first_power_product = pa_q_pvs_jordan_first_power_product_successor * S ((S (S pa_i_pvs_jordan_first_power_product)) * pa_v_pvs_jordan_first_power_product) + (pa_s_pvs_jordan_first_power_product))) /\ pa_s_pvs_jordan_first_power_product = pa_r_pvs_jordan_first_power_product * pa_p_pvs_jordan_first_power_product)))))))) -> (exists pa_b_pvs_jordan_second_power pa_c_pvs_jordan_second_power. ((forall pa_i_pvs_jordan_second_power_repeat. (exists pa_lt_pvs_jordan_second_power_repeat_bound. pa_lt_pvs_jordan_second_power_repeat_bound + S pa_i_pvs_jordan_second_power_repeat = S j) -> (((exists pa_h_pvs_jordan_second_power_repeat_decoded. pa_h_pvs_jordan_second_power_repeat_decoded + S (p) = S ((S (pa_i_pvs_jordan_second_power_repeat)) * pa_c_pvs_jordan_second_power)) /\ exists pa_q_pvs_jordan_second_power_repeat_decoded. pa_b_pvs_jordan_second_power = pa_q_pvs_jordan_second_power_repeat_decoded * S ((S (pa_i_pvs_jordan_second_power_repeat)) * pa_c_pvs_jordan_second_power) + (p)))) /\ (exists pa_u_pvs_jordan_second_power_product pa_v_pvs_jordan_second_power_product. ((((exists pa_h_pvs_jordan_second_power_product_start. pa_h_pvs_jordan_second_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_jordan_second_power_product)) /\ exists pa_q_pvs_jordan_second_power_product_start. pa_u_pvs_jordan_second_power_product = pa_q_pvs_jordan_second_power_product_start * S ((S (0)) * pa_v_pvs_jordan_second_power_product) + (1))) /\ ((((exists pa_h_pvs_jordan_second_power_product_terminal. pa_h_pvs_jordan_second_power_product_terminal + S (n) = S ((S (S j)) * pa_v_pvs_jordan_second_power_product)) /\ exists pa_q_pvs_jordan_second_power_product_terminal. pa_u_pvs_jordan_second_power_product = pa_q_pvs_jordan_second_power_product_terminal * S ((S (S j)) * pa_v_pvs_jordan_second_power_product) + (n))) /\ forall pa_i_pvs_jordan_second_power_product. (exists pa_lt_pvs_jordan_second_power_product_bound. pa_lt_pvs_jordan_second_power_product_bound + S pa_i_pvs_jordan_second_power_product = S j) -> exists pa_p_pvs_jordan_second_power_product pa_r_pvs_jordan_second_power_product pa_s_pvs_jordan_second_power_product. ((((exists pa_h_pvs_jordan_second_power_product_factor. pa_h_pvs_jordan_second_power_product_factor + S (pa_p_pvs_jordan_second_power_product) = S ((S (pa_i_pvs_jordan_second_power_product)) * pa_c_pvs_jordan_second_power)) /\ exists pa_q_pvs_jordan_second_power_product_factor. pa_b_pvs_jordan_second_power = pa_q_pvs_jordan_second_power_product_factor * S ((S (pa_i_pvs_jordan_second_power_product)) * pa_c_pvs_jordan_second_power) + (pa_p_pvs_jordan_second_power_product))) /\ ((((exists pa_h_pvs_jordan_second_power_product_partial. pa_h_pvs_jordan_second_power_product_partial + S (pa_r_pvs_jordan_second_power_product) = S ((S (pa_i_pvs_jordan_second_power_product)) * pa_v_pvs_jordan_second_power_product)) /\ exists pa_q_pvs_jordan_second_power_product_partial. pa_u_pvs_jordan_second_power_product = pa_q_pvs_jordan_second_power_product_partial * S ((S (pa_i_pvs_jordan_second_power_product)) * pa_v_pvs_jordan_second_power_product) + (pa_r_pvs_jordan_second_power_product))) /\ ((((exists pa_h_pvs_jordan_second_power_product_successor. pa_h_pvs_jordan_second_power_product_successor + S (pa_s_pvs_jordan_second_power_product) = S ((S (S pa_i_pvs_jordan_second_power_product)) * pa_v_pvs_jordan_second_power_product)) /\ exists pa_q_pvs_jordan_second_power_product_successor. pa_u_pvs_jordan_second_power_product = pa_q_pvs_jordan_second_power_product_successor * S ((S (S pa_i_pvs_jordan_second_power_product)) * pa_v_pvs_jordan_second_power_product) + (pa_s_pvs_jordan_second_power_product))) /\ pa_s_pvs_jordan_second_power_product = pa_r_pvs_jordan_second_power_product * pa_p_pvs_jordan_second_power_product)))))))) -> (forall jt_divisor_jordan_first_primitive. (exists jt_factor_jordan_first_primitivemodulus. (m)=(jt_divisor_jordan_first_primitive)*jt_factor_jordan_first_primitivemodulus) -> (forall jt_index_jordan_first_primitivecoordinates jt_value_jordan_first_primitivecoordinates. (exists jt_gap_jordan_first_primitivecoordinatesindex. jt_gap_jordan_first_primitivecoordinatesindex+S (jt_index_jordan_first_primitivecoordinates)=(k)) -> (((exists fs_h_jt_jordan_first_primitivecoordinatesat. fs_h_jt_jordan_first_primitivecoordinatesat + S (jt_value_jordan_first_primitivecoordinates) = S ((S (jt_index_jordan_first_primitivecoordinates)) * c)) /\ exists fs_q_jt_jordan_first_primitivecoordinatesat. b = fs_q_jt_jordan_first_primitivecoordinatesat * S ((S (jt_index_jordan_first_primitivecoordinates)) * c) + (jt_value_jordan_first_primitivecoordinates))) -> (exists jt_factor_jordan_first_primitivecoordinatesdivides. (jt_value_jordan_first_primitivecoordinates)=(jt_divisor_jordan_first_primitive)*jt_factor_jordan_first_primitivecoordinatesdivides)) -> jt_divisor_jordan_first_primitive=1) -> 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

Complete tactic proof in conservative notation

All 40 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

40 script commands · 8 reading checkpoints · 0 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.

Named ingredients (2)
jordan prime power tuple primitive of not all divisiblejordan primitive tuple avoids prime common divisor
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro j
  4. L4
    intro m
  5. L5
    intro n
  6. L6
    intro b
  7. L7
    intro c
  8. L8
    intro k
  9. L9
    intro hp
  10. L10
    intro hm
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hn
  2. L12
    intro hprimitive
03Use earlier factsL13–21

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

  1. L13
    specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (p)
  2. L14
    specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (S j)
  3. L15
    specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (n)
  4. L16
    specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (b)
  5. L17
    specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (c)
  6. L18
    specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (k)
  7. L19
    apply jordan_prime_power_tuple_primitive_of_not_all_divisible
  8. L20
    exact hp
  9. L21
    exact hn
04Fix variables and assumptionsL22–22

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

  1. L22
    intro hall
05Use earlier factsL23–32

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

  1. L23
    specialize jordan_primitive_tuple_avoids_prime_common_divisor (p)
  2. L24
    specialize jordan_primitive_tuple_avoids_prime_common_divisor (m)
  3. L25
    specialize jordan_primitive_tuple_avoids_prime_common_divisor (b)
  4. L26
    specialize jordan_primitive_tuple_avoids_prime_common_divisor (c)
  5. L27
    specialize jordan_primitive_tuple_avoids_prime_common_divisor (k)
  6. L28
    apply jordan_primitive_tuple_avoids_prime_common_divisor
  7. L29
    exact hp
  8. L30
    specialize pow_positive_exponent_base_divides (p)
  9. L31
    specialize pow_positive_exponent_base_divides (S h)
  10. L32
    specialize pow_positive_exponent_base_divides (m)
06Use earlier factsL33–33

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

  1. L33
    apply pow_positive_exponent_base_divides
07Fix variables and assumptionsL34–34

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

  1. L34
    intro hszero
08Use earlier factsL35–40

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

  1. L35
    specialize succ_ne_zero (h)
  2. L36
    apply succ_ne_zero
  3. L37
    exact hszero
  4. L38
    exact hm
  5. L39
    exact hprimitive
  6. L40
    exact hall

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro j
  4. 0004intro m
  5. 0005intro n
  6. 0006intro b
  7. 0007intro c
  8. 0008intro k
  9. 0009intro hp
  10. 0010intro hm
  11. 0011intro hn
  12. 0012intro hprimitive
  13. 0013specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (p)
  14. 0014specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (S j)
  15. 0015specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (n)
  16. 0016specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (b)
  17. 0017specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (c)
  18. 0018specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (k)
  19. 0019apply jordan_prime_power_tuple_primitive_of_not_all_divisible
  20. 0020exact hp
  21. 0021exact hn
  22. 0022intro hall
  23. 0023specialize jordan_primitive_tuple_avoids_prime_common_divisor (p)
  24. 0024specialize jordan_primitive_tuple_avoids_prime_common_divisor (m)
  25. 0025specialize jordan_primitive_tuple_avoids_prime_common_divisor (b)
  26. 0026specialize jordan_primitive_tuple_avoids_prime_common_divisor (c)
  27. 0027specialize jordan_primitive_tuple_avoids_prime_common_divisor (k)
  28. 0028apply jordan_primitive_tuple_avoids_prime_common_divisor
  29. 0029exact hp
  30. 0030specialize pow_positive_exponent_base_divides (p)
  31. 0031specialize pow_positive_exponent_base_divides (S h)
  32. 0032specialize pow_positive_exponent_base_divides (m)
  33. 0033apply pow_positive_exponent_base_divides
  34. 0034intro hszero
  35. 0035specialize succ_ne_zero (h)
  36. 0036apply succ_ne_zero
  37. 0037exact hszero
  38. 0038exact hm
  39. 0039exact hprimitive
  40. 0040exact hall