JT005F

jordan_prime_power_tuple_primitive_characterization

Over every positive power of a prime, a tuple is primitive exactly when p does not divide all its coordinates.

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. ∀ n. ∀ b. ∀ c. ∀ k. Prime(p) → Pow(p,S h,n) → (JordanPrimitiveTuple(n,b,c,k) → ¬JordanTupleAllDivisible(p,b,c,k)) ∧ (¬JordanTupleAllDivisible(p,b,c,k) → JordanPrimitiveTuple(n,b,c,k))

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

Definition DAG

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

Actual proof prerequisites

jordan_primitive_tuple_avoids_prime_common_divisorpow_positive_exponent_base_divides · checked external prerequisitesucc_ne_zero · checked external prerequisitejordan_prime_power_tuple_primitive_of_not_all_divisible
Original expanded first-order statement 
forall p h 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_positive_power pa_c_pvs_jordan_positive_power. ((forall pa_i_pvs_jordan_positive_power_repeat. (exists pa_lt_pvs_jordan_positive_power_repeat_bound. pa_lt_pvs_jordan_positive_power_repeat_bound + S pa_i_pvs_jordan_positive_power_repeat = S h) -> (((exists pa_h_pvs_jordan_positive_power_repeat_decoded. pa_h_pvs_jordan_positive_power_repeat_decoded + S (p) = S ((S (pa_i_pvs_jordan_positive_power_repeat)) * pa_c_pvs_jordan_positive_power)) /\ exists pa_q_pvs_jordan_positive_power_repeat_decoded. pa_b_pvs_jordan_positive_power = pa_q_pvs_jordan_positive_power_repeat_decoded * S ((S (pa_i_pvs_jordan_positive_power_repeat)) * pa_c_pvs_jordan_positive_power) + (p)))) /\ (exists pa_u_pvs_jordan_positive_power_product pa_v_pvs_jordan_positive_power_product. ((((exists pa_h_pvs_jordan_positive_power_product_start. pa_h_pvs_jordan_positive_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_jordan_positive_power_product)) /\ exists pa_q_pvs_jordan_positive_power_product_start. pa_u_pvs_jordan_positive_power_product = pa_q_pvs_jordan_positive_power_product_start * S ((S (0)) * pa_v_pvs_jordan_positive_power_product) + (1))) /\ ((((exists pa_h_pvs_jordan_positive_power_product_terminal. pa_h_pvs_jordan_positive_power_product_terminal + S (n) = S ((S (S h)) * pa_v_pvs_jordan_positive_power_product)) /\ exists pa_q_pvs_jordan_positive_power_product_terminal. pa_u_pvs_jordan_positive_power_product = pa_q_pvs_jordan_positive_power_product_terminal * S ((S (S h)) * pa_v_pvs_jordan_positive_power_product) + (n))) /\ forall pa_i_pvs_jordan_positive_power_product. (exists pa_lt_pvs_jordan_positive_power_product_bound. pa_lt_pvs_jordan_positive_power_product_bound + S pa_i_pvs_jordan_positive_power_product = S h) -> exists pa_p_pvs_jordan_positive_power_product pa_r_pvs_jordan_positive_power_product pa_s_pvs_jordan_positive_power_product. ((((exists pa_h_pvs_jordan_positive_power_product_factor. pa_h_pvs_jordan_positive_power_product_factor + S (pa_p_pvs_jordan_positive_power_product) = S ((S (pa_i_pvs_jordan_positive_power_product)) * pa_c_pvs_jordan_positive_power)) /\ exists pa_q_pvs_jordan_positive_power_product_factor. pa_b_pvs_jordan_positive_power = pa_q_pvs_jordan_positive_power_product_factor * S ((S (pa_i_pvs_jordan_positive_power_product)) * pa_c_pvs_jordan_positive_power) + (pa_p_pvs_jordan_positive_power_product))) /\ ((((exists pa_h_pvs_jordan_positive_power_product_partial. pa_h_pvs_jordan_positive_power_product_partial + S (pa_r_pvs_jordan_positive_power_product) = S ((S (pa_i_pvs_jordan_positive_power_product)) * pa_v_pvs_jordan_positive_power_product)) /\ exists pa_q_pvs_jordan_positive_power_product_partial. pa_u_pvs_jordan_positive_power_product = pa_q_pvs_jordan_positive_power_product_partial * S ((S (pa_i_pvs_jordan_positive_power_product)) * pa_v_pvs_jordan_positive_power_product) + (pa_r_pvs_jordan_positive_power_product))) /\ ((((exists pa_h_pvs_jordan_positive_power_product_successor. pa_h_pvs_jordan_positive_power_product_successor + S (pa_s_pvs_jordan_positive_power_product) = S ((S (S pa_i_pvs_jordan_positive_power_product)) * pa_v_pvs_jordan_positive_power_product)) /\ exists pa_q_pvs_jordan_positive_power_product_successor. pa_u_pvs_jordan_positive_power_product = pa_q_pvs_jordan_positive_power_product_successor * S ((S (S pa_i_pvs_jordan_positive_power_product)) * pa_v_pvs_jordan_positive_power_product) + (pa_s_pvs_jordan_positive_power_product))) /\ pa_s_pvs_jordan_positive_power_product = pa_r_pvs_jordan_positive_power_product * pa_p_pvs_jordan_positive_power_product)))))))) -> (((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) -> (~(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_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)))

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 · 9 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 primitive tuple avoids prime common divisorjordan prime power tuple primitive of not all divisible
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro n
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro k
  7. L7
    intro hp
  8. L8
    intro hpow
02Separate the logical casesL9–9

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

  1. L9
    split
03Fix variables and assumptionsL10–11

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

  1. L10
    intro hprimitive
  2. L11
    intro hall
04Use earlier factsL12–21

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

  1. L12
    specialize jordan_primitive_tuple_avoids_prime_common_divisor (p)
  2. L13
    specialize jordan_primitive_tuple_avoids_prime_common_divisor (n)
  3. L14
    specialize jordan_primitive_tuple_avoids_prime_common_divisor (b)
  4. L15
    specialize jordan_primitive_tuple_avoids_prime_common_divisor (c)
  5. L16
    specialize jordan_primitive_tuple_avoids_prime_common_divisor (k)
  6. L17
    apply jordan_primitive_tuple_avoids_prime_common_divisor
  7. L18
    exact hp
  8. L19
    specialize pow_positive_exponent_base_divides (p)
  9. L20
    specialize pow_positive_exponent_base_divides (S h)
  10. L21
    specialize pow_positive_exponent_base_divides (n)
05Use earlier factsL22–22

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

  1. L22
    apply pow_positive_exponent_base_divides
06Fix variables and assumptionsL23–23

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

  1. L23
    intro hszero
07Use earlier factsL24–29

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

  1. L24
    specialize succ_ne_zero (h)
  2. L25
    apply succ_ne_zero
  3. L26
    exact hszero
  4. L27
    exact hpow
  5. L28
    exact hprimitive
  6. L29
    exact hall
08Fix variables and assumptionsL30–30

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

  1. L30
    intro hnot
09Use earlier factsL31–40

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

  1. L31
    specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (p)
  2. L32
    specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (S h)
  3. L33
    specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (n)
  4. L34
    specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (b)
  5. L35
    specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (c)
  6. L36
    specialize jordan_prime_power_tuple_primitive_of_not_all_divisible (k)
  7. L37
    apply jordan_prime_power_tuple_primitive_of_not_all_divisible
  8. L38
    exact hp
  9. L39
    exact hpow
  10. L40
    exact hnot

Library-wide reading audit

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