JT005F

jordan_prime_power_tuple_primitive_characterization

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

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

Exact expanded first-order arithmetic 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)))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 40 exact native proof lines.

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

Proof neighborhood

Direct dependencies

JT005D jordan_primitive_tuple_avoids_prime_common_divisor pow_positive_exponent_base_divides Alpha theorem; checked-use authorized succ_ne_zero Alpha theorem; checked-use authorized JT005E jordan_prime_power_tuple_primitive_of_not_all_divisible

Direct dependents

none

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

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.

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 exact 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