JT0033

jordan_primitive_crt_tuple_exists

The constructed canonical CRT tuple is primitive collectively, by coprime common-divisor decomposition.

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

∀ m. ∀ n. ∀ b. ∀ c. ∀ d. ∀ e. ∀ k. ¬m = 0 → ¬n = 0 → Coprime(m,n) → JordanPrimitiveTuple(m,b,c,k) → JordanPrimitiveTuple(n,d,e,k) → ∃ x. ∃ y. JordanCanonicalTupleCRT(m,n,b,c,d,e,x,y,k) ∧ JordanPrimitiveTuple(m · n,x,y,k)

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

Definition DAG

JordanPrimitiveTuple(n,b,c,k) · 3JordanCanonicalTupleCRT(m,n,b,c,d,e,f,g,k) · 2Coprime(a,b) · 1

Actual proof prerequisites

jordan_canonical_crt_tuple_existsjordan_primitive_tuple_coprime_productjordan_primitive_tuple_congruence_transportjordan_tuple_congruence_symm
Original expanded first-order statement 
forall m n b c d e k. ~(m=0) -> ~(n=0) -> (forall jt_divisor_primitivecrtcoprime. (exists jt_factor_primitivecrtcoprimea. (m)=(jt_divisor_primitivecrtcoprime)*jt_factor_primitivecrtcoprimea) -> (exists jt_factor_primitivecrtcoprimeb. (n)=(jt_divisor_primitivecrtcoprime)*jt_factor_primitivecrtcoprimeb) -> jt_divisor_primitivecrtcoprime=1) -> (forall jt_divisor_primitivecrtleft. (exists jt_factor_primitivecrtleftmodulus. (m)=(jt_divisor_primitivecrtleft)*jt_factor_primitivecrtleftmodulus) -> (forall jt_index_primitivecrtleftcoordinates jt_value_primitivecrtleftcoordinates. (exists jt_gap_primitivecrtleftcoordinatesindex. jt_gap_primitivecrtleftcoordinatesindex+S (jt_index_primitivecrtleftcoordinates)=(k)) -> (((exists fs_h_jt_primitivecrtleftcoordinatesat. fs_h_jt_primitivecrtleftcoordinatesat + S (jt_value_primitivecrtleftcoordinates) = S ((S (jt_index_primitivecrtleftcoordinates)) * c)) /\ exists fs_q_jt_primitivecrtleftcoordinatesat. b = fs_q_jt_primitivecrtleftcoordinatesat * S ((S (jt_index_primitivecrtleftcoordinates)) * c) + (jt_value_primitivecrtleftcoordinates))) -> (exists jt_factor_primitivecrtleftcoordinatesdivides. (jt_value_primitivecrtleftcoordinates)=(jt_divisor_primitivecrtleft)*jt_factor_primitivecrtleftcoordinatesdivides)) -> jt_divisor_primitivecrtleft=1) -> (forall jt_divisor_primitivecrtright. (exists jt_factor_primitivecrtrightmodulus. (n)=(jt_divisor_primitivecrtright)*jt_factor_primitivecrtrightmodulus) -> (forall jt_index_primitivecrtrightcoordinates jt_value_primitivecrtrightcoordinates. (exists jt_gap_primitivecrtrightcoordinatesindex. jt_gap_primitivecrtrightcoordinatesindex+S (jt_index_primitivecrtrightcoordinates)=(k)) -> (((exists fs_h_jt_primitivecrtrightcoordinatesat. fs_h_jt_primitivecrtrightcoordinatesat + S (jt_value_primitivecrtrightcoordinates) = S ((S (jt_index_primitivecrtrightcoordinates)) * e)) /\ exists fs_q_jt_primitivecrtrightcoordinatesat. d = fs_q_jt_primitivecrtrightcoordinatesat * S ((S (jt_index_primitivecrtrightcoordinates)) * e) + (jt_value_primitivecrtrightcoordinates))) -> (exists jt_factor_primitivecrtrightcoordinatesdivides. (jt_value_primitivecrtrightcoordinates)=(jt_divisor_primitivecrtright)*jt_factor_primitivecrtrightcoordinatesdivides)) -> jt_divisor_primitivecrtright=1) -> exists f g. ((((forall jt_index_primitivecrtresultbound. (exists jt_gap_primitivecrtresultboundindex. jt_gap_primitivecrtresultboundindex+S (jt_index_primitivecrtresultbound)=(k)) -> exists jt_value_primitivecrtresultbound. ((((exists fs_h_jt_primitivecrtresultboundat. fs_h_jt_primitivecrtresultboundat + S (jt_value_primitivecrtresultbound) = S ((S (jt_index_primitivecrtresultbound)) * g)) /\ exists fs_q_jt_primitivecrtresultboundat. f = fs_q_jt_primitivecrtresultboundat * S ((S (jt_index_primitivecrtresultbound)) * g) + (jt_value_primitivecrtresultbound))) /\ (exists jt_gap_primitivecrtresultboundvalue. jt_gap_primitivecrtresultboundvalue+S (jt_value_primitivecrtresultbound)=(m*n)))) /\ (((forall jt_index_primitivecrtresultleft jt_left_primitivecrtresultleft jt_right_primitivecrtresultleft. (exists jt_gap_primitivecrtresultleftindex. jt_gap_primitivecrtresultleftindex+S (jt_index_primitivecrtresultleft)=(k)) -> (((exists fs_h_jt_primitivecrtresultleftleft. fs_h_jt_primitivecrtresultleftleft + S (jt_left_primitivecrtresultleft) = S ((S (jt_index_primitivecrtresultleft)) * g)) /\ exists fs_q_jt_primitivecrtresultleftleft. f = fs_q_jt_primitivecrtresultleftleft * S ((S (jt_index_primitivecrtresultleft)) * g) + (jt_left_primitivecrtresultleft))) -> (((exists fs_h_jt_primitivecrtresultleftright. fs_h_jt_primitivecrtresultleftright + S (jt_right_primitivecrtresultleft) = S ((S (jt_index_primitivecrtresultleft)) * c)) /\ exists fs_q_jt_primitivecrtresultleftright. b = fs_q_jt_primitivecrtresultleftright * S ((S (jt_index_primitivecrtresultleft)) * c) + (jt_right_primitivecrtresultleft))) -> (exists jt_left_primitivecrtresultleftmod jt_right_primitivecrtresultleftmod. (jt_left_primitivecrtresultleft)+(m)*jt_left_primitivecrtresultleftmod=(jt_right_primitivecrtresultleft)+(m)*jt_right_primitivecrtresultleftmod)) /\ (forall jt_index_primitivecrtresultright jt_left_primitivecrtresultright jt_right_primitivecrtresultright. (exists jt_gap_primitivecrtresultrightindex. jt_gap_primitivecrtresultrightindex+S (jt_index_primitivecrtresultright)=(k)) -> (((exists fs_h_jt_primitivecrtresultrightleft. fs_h_jt_primitivecrtresultrightleft + S (jt_left_primitivecrtresultright) = S ((S (jt_index_primitivecrtresultright)) * g)) /\ exists fs_q_jt_primitivecrtresultrightleft. f = fs_q_jt_primitivecrtresultrightleft * S ((S (jt_index_primitivecrtresultright)) * g) + (jt_left_primitivecrtresultright))) -> (((exists fs_h_jt_primitivecrtresultrightright. fs_h_jt_primitivecrtresultrightright + S (jt_right_primitivecrtresultright) = S ((S (jt_index_primitivecrtresultright)) * e)) /\ exists fs_q_jt_primitivecrtresultrightright. d = fs_q_jt_primitivecrtresultrightright * S ((S (jt_index_primitivecrtresultright)) * e) + (jt_right_primitivecrtresultright))) -> (exists jt_left_primitivecrtresultrightmod jt_right_primitivecrtresultrightmod. (jt_left_primitivecrtresultright)+(n)*jt_left_primitivecrtresultrightmod=(jt_right_primitivecrtresultright)+(n)*jt_right_primitivecrtresultrightmod)))))) /\ (forall jt_divisor_primitivecrtproduct. (exists jt_factor_primitivecrtproductmodulus. (m*n)=(jt_divisor_primitivecrtproduct)*jt_factor_primitivecrtproductmodulus) -> (forall jt_index_primitivecrtproductcoordinates jt_value_primitivecrtproductcoordinates. (exists jt_gap_primitivecrtproductcoordinatesindex. jt_gap_primitivecrtproductcoordinatesindex+S (jt_index_primitivecrtproductcoordinates)=(k)) -> (((exists fs_h_jt_primitivecrtproductcoordinatesat. fs_h_jt_primitivecrtproductcoordinatesat + S (jt_value_primitivecrtproductcoordinates) = S ((S (jt_index_primitivecrtproductcoordinates)) * g)) /\ exists fs_q_jt_primitivecrtproductcoordinatesat. f = fs_q_jt_primitivecrtproductcoordinatesat * S ((S (jt_index_primitivecrtproductcoordinates)) * g) + (jt_value_primitivecrtproductcoordinates))) -> (exists jt_factor_primitivecrtproductcoordinatesdivides. (jt_value_primitivecrtproductcoordinates)=(jt_divisor_primitivecrtproduct)*jt_factor_primitivecrtproductcoordinatesdivides)) -> jt_divisor_primitivecrtproduct=1))

Complete tactic proof in conservative notation

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

77 script commands · 14 reading checkpoints · 1 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 (4)
jordan canonical crt tuple existsjordan primitive tuple coprime productjordan primitive tuple congruence transportjordan tuple congruence symm
01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    intro hleft
  2. L12
    intro hright
03Establish hcrtL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply jordan canonical crt tuple exists.

  1. L13
    have hcrt : ∃ f. ∃ g. JordanCanonicalTupleCRT(m,n,b,c,d,e,f,g,k)Definitions: JordanCanonicalTupleCRT(m,n,b,c,d,e,f,g,k)Original native command in the exact edition
  2. L14
    specialize jordan_canonical_crt_tuple_exists (m)
  3. L15
    specialize jordan_canonical_crt_tuple_exists (n)
  4. L16
    specialize jordan_canonical_crt_tuple_exists (b)
  5. L17
    specialize jordan_canonical_crt_tuple_exists (c)
  6. L18
    specialize jordan_canonical_crt_tuple_exists (d)
  7. L19
    specialize jordan_canonical_crt_tuple_exists (e)
  8. L20
    specialize jordan_canonical_crt_tuple_exists (k)
  9. L21
    apply jordan_canonical_crt_tuple_exists
  10. L22
    exact hm
04Use earlier factsL23–24

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

  1. L23
    exact hn
  2. L24
    exact hcop
05Separate the logical casesL25–28

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

  1. L25
    cases hcrt
  2. L26
    cases hcrt_witness
  3. L27
    cases hcrt_witness_witness
  4. L28
    cases hcrt_witness_witness_right
06Construct an explicit witnessL29–30

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

  1. L29
    exists x
  2. L30
    exists x1
07Separate the logical casesL31–32

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

  1. L31
    split
  2. L32
    split
08Use earlier factsL33–33

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

  1. L33
    exact hcrt_witness_witness_left
09Separate the logical casesL34–34

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

  1. L34
    split
10Use earlier factsL35–44

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

  1. L35
    exact hcrt_witness_witness_right_left
  2. L36
    exact hcrt_witness_witness_right_right
  3. L37
    specialize jordan_primitive_tuple_coprime_product (m)
  4. L38
    specialize jordan_primitive_tuple_coprime_product (n)
  5. L39
    specialize jordan_primitive_tuple_coprime_product (x)
  6. L40
    specialize jordan_primitive_tuple_coprime_product (x1)
  7. L41
    specialize jordan_primitive_tuple_coprime_product (k)
  8. L42
    apply jordan_primitive_tuple_coprime_product
  9. L43
    exact hm
  10. L44
    exact hn
11Use earlier factsL45–54

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

  1. L45
    exact hcop
  2. L46
    specialize jordan_primitive_tuple_congruence_transport (m)
  3. L47
    specialize jordan_primitive_tuple_congruence_transport (b)
  4. L48
    specialize jordan_primitive_tuple_congruence_transport (c)
  5. L49
    specialize jordan_primitive_tuple_congruence_transport (x)
  6. L50
    specialize jordan_primitive_tuple_congruence_transport (x1)
  7. L51
    specialize jordan_primitive_tuple_congruence_transport (k)
  8. L52
    apply jordan_primitive_tuple_congruence_transport
  9. L53
    specialize jordan_tuple_congruence_symm (m)
  10. L54
    specialize jordan_tuple_congruence_symm (x)
12Use earlier factsL55–64

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

  1. L55
    specialize jordan_tuple_congruence_symm (x1)
  2. L56
    specialize jordan_tuple_congruence_symm (b)
  3. L57
    specialize jordan_tuple_congruence_symm (c)
  4. L58
    specialize jordan_tuple_congruence_symm (k)
  5. L59
    apply jordan_tuple_congruence_symm
  6. L60
    exact hcrt_witness_witness_right_left
  7. L61
    exact hleft
  8. L62
    specialize jordan_primitive_tuple_congruence_transport (n)
  9. L63
    specialize jordan_primitive_tuple_congruence_transport (d)
  10. L64
    specialize jordan_primitive_tuple_congruence_transport (e)
13Use earlier factsL65–74

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

  1. L65
    specialize jordan_primitive_tuple_congruence_transport (x)
  2. L66
    specialize jordan_primitive_tuple_congruence_transport (x1)
  3. L67
    specialize jordan_primitive_tuple_congruence_transport (k)
  4. L68
    apply jordan_primitive_tuple_congruence_transport
  5. L69
    specialize jordan_tuple_congruence_symm (n)
  6. L70
    specialize jordan_tuple_congruence_symm (x)
  7. L71
    specialize jordan_tuple_congruence_symm (x1)
  8. L72
    specialize jordan_tuple_congruence_symm (d)
  9. L73
    specialize jordan_tuple_congruence_symm (e)
  10. L74
    specialize jordan_tuple_congruence_symm (k)
14Use earlier factsL75–77

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

  1. L75
    apply jordan_tuple_congruence_symm
  2. L76
    exact hcrt_witness_witness_right_right
  3. L77
    exact hright

Library-wide reading audit

Original defined command ledger · 77 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro k
  8. 0008intro hm
  9. 0009intro hn
  10. 0010intro hcop
  11. 0011intro hleft
  12. 0012intro hright
  13. 0013have hcrt : ∃ f. ∃ g. JordanCanonicalTupleCRT(m,n,b,c,d,e,f,g,k)
  14. 0014specialize jordan_canonical_crt_tuple_exists (m)
  15. 0015specialize jordan_canonical_crt_tuple_exists (n)
  16. 0016specialize jordan_canonical_crt_tuple_exists (b)
  17. 0017specialize jordan_canonical_crt_tuple_exists (c)
  18. 0018specialize jordan_canonical_crt_tuple_exists (d)
  19. 0019specialize jordan_canonical_crt_tuple_exists (e)
  20. 0020specialize jordan_canonical_crt_tuple_exists (k)
  21. 0021apply jordan_canonical_crt_tuple_exists
  22. 0022exact hm
  23. 0023exact hn
  24. 0024exact hcop
  25. 0025cases hcrt
  26. 0026cases hcrt_witness
  27. 0027cases hcrt_witness_witness
  28. 0028cases hcrt_witness_witness_right
  29. 0029exists x
  30. 0030exists x1
  31. 0031split
  32. 0032split
  33. 0033exact hcrt_witness_witness_left
  34. 0034split
  35. 0035exact hcrt_witness_witness_right_left
  36. 0036exact hcrt_witness_witness_right_right
  37. 0037specialize jordan_primitive_tuple_coprime_product (m)
  38. 0038specialize jordan_primitive_tuple_coprime_product (n)
  39. 0039specialize jordan_primitive_tuple_coprime_product (x)
  40. 0040specialize jordan_primitive_tuple_coprime_product (x1)
  41. 0041specialize jordan_primitive_tuple_coprime_product (k)
  42. 0042apply jordan_primitive_tuple_coprime_product
  43. 0043exact hm
  44. 0044exact hn
  45. 0045exact hcop
  46. 0046specialize jordan_primitive_tuple_congruence_transport (m)
  47. 0047specialize jordan_primitive_tuple_congruence_transport (b)
  48. 0048specialize jordan_primitive_tuple_congruence_transport (c)
  49. 0049specialize jordan_primitive_tuple_congruence_transport (x)
  50. 0050specialize jordan_primitive_tuple_congruence_transport (x1)
  51. 0051specialize jordan_primitive_tuple_congruence_transport (k)
  52. 0052apply jordan_primitive_tuple_congruence_transport
  53. 0053specialize jordan_tuple_congruence_symm (m)
  54. 0054specialize jordan_tuple_congruence_symm (x)
  55. 0055specialize jordan_tuple_congruence_symm (x1)
  56. 0056specialize jordan_tuple_congruence_symm (b)
  57. 0057specialize jordan_tuple_congruence_symm (c)
  58. 0058specialize jordan_tuple_congruence_symm (k)
  59. 0059apply jordan_tuple_congruence_symm
  60. 0060exact hcrt_witness_witness_right_left
  61. 0061exact hleft
  62. 0062specialize jordan_primitive_tuple_congruence_transport (n)
  63. 0063specialize jordan_primitive_tuple_congruence_transport (d)
  64. 0064specialize jordan_primitive_tuple_congruence_transport (e)
  65. 0065specialize jordan_primitive_tuple_congruence_transport (x)
  66. 0066specialize jordan_primitive_tuple_congruence_transport (x1)
  67. 0067specialize jordan_primitive_tuple_congruence_transport (k)
  68. 0068apply jordan_primitive_tuple_congruence_transport
  69. 0069specialize jordan_tuple_congruence_symm (n)
  70. 0070specialize jordan_tuple_congruence_symm (x)
  71. 0071specialize jordan_tuple_congruence_symm (x1)
  72. 0072specialize jordan_tuple_congruence_symm (d)
  73. 0073specialize jordan_tuple_congruence_symm (e)
  74. 0074specialize jordan_tuple_congruence_symm (k)
  75. 0075apply jordan_tuple_congruence_symm
  76. 0076exact hcrt_witness_witness_right_right
  77. 0077exact hright