JT000B

jordan_primitive_tuple_coprime_product

Actual coprime divisor decomposition proves primitivity for the product 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

∀ a. ∀ b. ∀ B. ∀ C. ∀ k. ¬a = 0 → ¬b = 0 → Coprime(a,b) → JordanPrimitiveTuple(a,B,C,k) → JordanPrimitiveTuple(b,B,C,k) → JordanPrimitiveTuple(a · b,B,C,k)

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

Definition DAG

DivisorFactorPair(m,n,d,a,b) · 1JordanPrimitiveTuple(n,b,c,k) · 3Coprime(a,b) · 1

Actual proof prerequisites

mul_ne_zero · checked external prerequisitemul_zero_left · checked external prerequisitecoprime_divisor_factor_pair_exists · checked external prerequisitejordan_tuple_divisor_downwardmul_comm · checked external prerequisiteone_mul · checked external prerequisite
Original expanded first-order statement 
forall a b B C k. ~(a=0) -> ~(b=0) -> (forall jt_divisor_productcop. (exists jt_factor_productcopa. (a)=(jt_divisor_productcop)*jt_factor_productcopa) -> (exists jt_factor_productcopb. (b)=(jt_divisor_productcop)*jt_factor_productcopb) -> jt_divisor_productcop=1) -> (forall jt_divisor_producta. (exists jt_factor_productamodulus. (a)=(jt_divisor_producta)*jt_factor_productamodulus) -> (forall jt_index_productacoordinates jt_value_productacoordinates. (exists jt_gap_productacoordinatesindex. jt_gap_productacoordinatesindex+S (jt_index_productacoordinates)=(k)) -> (((exists fs_h_jt_productacoordinatesat. fs_h_jt_productacoordinatesat + S (jt_value_productacoordinates) = S ((S (jt_index_productacoordinates)) * C)) /\ exists fs_q_jt_productacoordinatesat. B = fs_q_jt_productacoordinatesat * S ((S (jt_index_productacoordinates)) * C) + (jt_value_productacoordinates))) -> (exists jt_factor_productacoordinatesdivides. (jt_value_productacoordinates)=(jt_divisor_producta)*jt_factor_productacoordinatesdivides)) -> jt_divisor_producta=1) -> (forall jt_divisor_productb. (exists jt_factor_productbmodulus. (b)=(jt_divisor_productb)*jt_factor_productbmodulus) -> (forall jt_index_productbcoordinates jt_value_productbcoordinates. (exists jt_gap_productbcoordinatesindex. jt_gap_productbcoordinatesindex+S (jt_index_productbcoordinates)=(k)) -> (((exists fs_h_jt_productbcoordinatesat. fs_h_jt_productbcoordinatesat + S (jt_value_productbcoordinates) = S ((S (jt_index_productbcoordinates)) * C)) /\ exists fs_q_jt_productbcoordinatesat. B = fs_q_jt_productbcoordinatesat * S ((S (jt_index_productbcoordinates)) * C) + (jt_value_productbcoordinates))) -> (exists jt_factor_productbcoordinatesdivides. (jt_value_productbcoordinates)=(jt_divisor_productb)*jt_factor_productbcoordinatesdivides)) -> jt_divisor_productb=1) -> (forall jt_divisor_productab. (exists jt_factor_productabmodulus. (a*b)=(jt_divisor_productab)*jt_factor_productabmodulus) -> (forall jt_index_productabcoordinates jt_value_productabcoordinates. (exists jt_gap_productabcoordinatesindex. jt_gap_productabcoordinatesindex+S (jt_index_productabcoordinates)=(k)) -> (((exists fs_h_jt_productabcoordinatesat. fs_h_jt_productabcoordinatesat + S (jt_value_productabcoordinates) = S ((S (jt_index_productabcoordinates)) * C)) /\ exists fs_q_jt_productabcoordinatesat. B = fs_q_jt_productabcoordinatesat * S ((S (jt_index_productabcoordinates)) * C) + (jt_value_productabcoordinates))) -> (exists jt_factor_productabcoordinatesdivides. (jt_value_productabcoordinates)=(jt_divisor_productab)*jt_factor_productabcoordinatesdivides)) -> jt_divisor_productab=1)

Complete tactic proof in conservative notation

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

84 script commands · 16 reading checkpoints · 7 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 (1)
jordan tuple divisor downward
01Fix variables and assumptionsL1–10

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro B
  4. L4
    intro C
  5. L5
    intro k
  6. L6
    intro ha
  7. L7
    intro hb
  8. L8
    intro hc
  9. L9
    intro hpa
  10. L10
    intro hpb
02Fix variables and assumptionsL11–13

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

  1. L11
    intro d
  2. L12
    intro hd
  3. L13
    intro hall
03Establish hnL14–21

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

  1. L14
    have hn : ~(a*b=0)
  2. L15
    intro hproductzero
  3. L16
    specialize mul_ne_zero (a)
  4. L17
    specialize mul_ne_zero (b)
  5. L18
    apply mul_ne_zero
  6. L19
    exact ha
  7. L20
    exact hb
  8. L21
    exact hproductzero
04Establish hdposL22–24

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

  1. L22
    have hdpos : ~(d=0)
  2. L23
    intro hz
  3. L24
    apply hn
05Separate the logical casesL25–25

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

  1. L25
    cases hd
06Establish hzeroL26–32

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

  1. L26
    have hzero : d*x=0
  2. L27
    rewrite hz
  3. L28
    specialize mul_zero_left (x)
  4. L29
    apply mul_zero_left
  5. L30
    trans d*x
  6. L31
    exact hd_witness
  7. L32
    exact hzero
07Establish hpL33–40

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

  1. L33
    have hp : ∃ r. ∃ s. DivisorFactorPair(a,b,d,r,s)Definitions: DivisorFactorPair(a,b,d,r,s)Original native command in the exact edition
  2. L34
    specialize coprime_divisor_factor_pair_exists (a)
  3. L35
    specialize coprime_divisor_factor_pair_exists (b)
  4. L36
    specialize coprime_divisor_factor_pair_exists (d)
  5. L37
    apply coprime_divisor_factor_pair_exists
  6. L38
    exact hdpos
  7. L39
    exact hc
  8. L40
    exact hd
08Separate the logical casesL41–46

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

  1. L41
    cases hp
  2. L42
    cases hp_witness
  3. L43
    cases hp_witness_witness
  4. L44
    cases hp_witness_witness_right
  5. L45
    cases hp_witness_witness_right_right
  6. L46
    cases hp_witness_witness_right_right_right
09Establish hrL47–56

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

  1. L47
    have hr : x=1
  2. L48
    specialize hpa (x)
  3. L49
    apply hpa
  4. L50
    exact hp_witness_witness_right_right_left
  5. L51
    specialize jordan_tuple_divisor_downward (x)
  6. L52
    specialize jordan_tuple_divisor_downward (d)
  7. L53
    specialize jordan_tuple_divisor_downward (B)
  8. L54
    specialize jordan_tuple_divisor_downward (C)
  9. L55
    specialize jordan_tuple_divisor_downward (k)
  10. L56
    apply jordan_tuple_divisor_downward
10Construct an explicit witnessL57–57

Supply the displayed value, then prove that it has the required property.

  1. L57
    exists x1
11Use earlier factsL58–59

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

  1. L58
    exact hp_witness_witness_right_right_right_right
  2. L59
    exact hall
12Establish hsL60–69

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

  1. L60
    have hs : x1=1
  2. L61
    specialize hpb (x1)
  3. L62
    apply hpb
  4. L63
    exact hp_witness_witness_right_right_right_left
  5. L64
    specialize jordan_tuple_divisor_downward (x1)
  6. L65
    specialize jordan_tuple_divisor_downward (d)
  7. L66
    specialize jordan_tuple_divisor_downward (B)
  8. L67
    specialize jordan_tuple_divisor_downward (C)
  9. L68
    specialize jordan_tuple_divisor_downward (k)
  10. L69
    apply jordan_tuple_divisor_downward
13Construct an explicit witnessL70–70

Supply the displayed value, then prove that it has the required property.

  1. L70
    exists x
14Establish hcommL71–80

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

  1. L71
    have hcomm : x*x1=x1*x
  2. L72
    specialize mul_comm (x)
  3. L73
    specialize mul_comm (x1)
  4. L74
    apply mul_comm
  5. L75
    trans x*x1
  6. L76
    exact hp_witness_witness_right_right_right_right
  7. L77
    exact hcomm
  8. L78
    exact hall
  9. L79
    trans x*x1
  10. L80
    exact hp_witness_witness_right_right_right_right
15Calculate and transport equalitiesL81–82

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

  1. L81
    rewrite hr
  2. L82
    rewrite hs
16Use earlier factsL83–84

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

  1. L83
    specialize one_mul (1)
  2. L84
    apply one_mul

Library-wide reading audit

Original defined command ledger · 84 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro B
  4. 0004intro C
  5. 0005intro k
  6. 0006intro ha
  7. 0007intro hb
  8. 0008intro hc
  9. 0009intro hpa
  10. 0010intro hpb
  11. 0011intro d
  12. 0012intro hd
  13. 0013intro hall
  14. 0014have hn : ~(a*b=0)
  15. 0015intro hproductzero
  16. 0016specialize mul_ne_zero (a)
  17. 0017specialize mul_ne_zero (b)
  18. 0018apply mul_ne_zero
  19. 0019exact ha
  20. 0020exact hb
  21. 0021exact hproductzero
  22. 0022have hdpos : ~(d=0)
  23. 0023intro hz
  24. 0024apply hn
  25. 0025cases hd
  26. 0026have hzero : d*x=0
  27. 0027rewrite hz
  28. 0028specialize mul_zero_left (x)
  29. 0029apply mul_zero_left
  30. 0030trans d*x
  31. 0031exact hd_witness
  32. 0032exact hzero
  33. 0033have hp : ∃ r. ∃ s. DivisorFactorPair(a,b,d,r,s)
  34. 0034specialize coprime_divisor_factor_pair_exists (a)
  35. 0035specialize coprime_divisor_factor_pair_exists (b)
  36. 0036specialize coprime_divisor_factor_pair_exists (d)
  37. 0037apply coprime_divisor_factor_pair_exists
  38. 0038exact hdpos
  39. 0039exact hc
  40. 0040exact hd
  41. 0041cases hp
  42. 0042cases hp_witness
  43. 0043cases hp_witness_witness
  44. 0044cases hp_witness_witness_right
  45. 0045cases hp_witness_witness_right_right
  46. 0046cases hp_witness_witness_right_right_right
  47. 0047have hr : x=1
  48. 0048specialize hpa (x)
  49. 0049apply hpa
  50. 0050exact hp_witness_witness_right_right_left
  51. 0051specialize jordan_tuple_divisor_downward (x)
  52. 0052specialize jordan_tuple_divisor_downward (d)
  53. 0053specialize jordan_tuple_divisor_downward (B)
  54. 0054specialize jordan_tuple_divisor_downward (C)
  55. 0055specialize jordan_tuple_divisor_downward (k)
  56. 0056apply jordan_tuple_divisor_downward
  57. 0057exists x1
  58. 0058exact hp_witness_witness_right_right_right_right
  59. 0059exact hall
  60. 0060have hs : x1=1
  61. 0061specialize hpb (x1)
  62. 0062apply hpb
  63. 0063exact hp_witness_witness_right_right_right_left
  64. 0064specialize jordan_tuple_divisor_downward (x1)
  65. 0065specialize jordan_tuple_divisor_downward (d)
  66. 0066specialize jordan_tuple_divisor_downward (B)
  67. 0067specialize jordan_tuple_divisor_downward (C)
  68. 0068specialize jordan_tuple_divisor_downward (k)
  69. 0069apply jordan_tuple_divisor_downward
  70. 0070exists x
  71. 0071have hcomm : x*x1=x1*x
  72. 0072specialize mul_comm (x)
  73. 0073specialize mul_comm (x1)
  74. 0074apply mul_comm
  75. 0075trans x*x1
  76. 0076exact hp_witness_witness_right_right_right_right
  77. 0077exact hcomm
  78. 0078exact hall
  79. 0079trans x*x1
  80. 0080exact hp_witness_witness_right_right_right_right
  81. 0081rewrite hr
  82. 0082rewrite hs
  83. 0083specialize one_mul (1)
  84. 0084apply one_mul