JT0014

jordan_tuple_primitive_bounded_decidable

A finite sweep decides the primitive common-divisor condition up to any natural bound.

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

∀ n. ∀ b. ∀ c. ∀ k. ∀ L. (∀ x. Lt(x,L) → Dvd(x,n) → JordanTupleAllDivisible(x,b,c,k) → x = 1) ∨ ¬(∀ x. Lt(x,L) → Dvd(x,n) → JordanTupleAllDivisible(x,b,c,k) → x = 1)

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

Definition DAG

JordanTupleAllDivisible(d,b,c,k) · 4Lt(a,b) · 3Dvd(d,n) · 4

Actual proof prerequisites

lt_not_le · checked external prerequisitezero_le · checked external prerequisitejordan_tuple_divisor_test_decidablefinite_lt_succ_eq_or_lt · checked external prerequisitele_refl · checked external prerequisitele_succ · checked external prerequisite
Original expanded first-order statement 
forall n b c k L. (forall jt_divisor_bounddec_yes. (exists jt_gap_bounddec_yesbound. jt_gap_bounddec_yesbound+S (jt_divisor_bounddec_yes)=(L)) -> ((exists jt_factor_bounddec_yestestmodulus. (n)=(jt_divisor_bounddec_yes)*jt_factor_bounddec_yestestmodulus) -> (forall jt_index_bounddec_yestestcoordinates jt_value_bounddec_yestestcoordinates. (exists jt_gap_bounddec_yestestcoordinatesindex. jt_gap_bounddec_yestestcoordinatesindex+S (jt_index_bounddec_yestestcoordinates)=(k)) -> (((exists fs_h_jt_bounddec_yestestcoordinatesat. fs_h_jt_bounddec_yestestcoordinatesat + S (jt_value_bounddec_yestestcoordinates) = S ((S (jt_index_bounddec_yestestcoordinates)) * c)) /\ exists fs_q_jt_bounddec_yestestcoordinatesat. b = fs_q_jt_bounddec_yestestcoordinatesat * S ((S (jt_index_bounddec_yestestcoordinates)) * c) + (jt_value_bounddec_yestestcoordinates))) -> (exists jt_factor_bounddec_yestestcoordinatesdivides. (jt_value_bounddec_yestestcoordinates)=(jt_divisor_bounddec_yes)*jt_factor_bounddec_yestestcoordinatesdivides)) -> (jt_divisor_bounddec_yes)=1)) \/ ~(forall jt_divisor_bounddec_no. (exists jt_gap_bounddec_nobound. jt_gap_bounddec_nobound+S (jt_divisor_bounddec_no)=(L)) -> ((exists jt_factor_bounddec_notestmodulus. (n)=(jt_divisor_bounddec_no)*jt_factor_bounddec_notestmodulus) -> (forall jt_index_bounddec_notestcoordinates jt_value_bounddec_notestcoordinates. (exists jt_gap_bounddec_notestcoordinatesindex. jt_gap_bounddec_notestcoordinatesindex+S (jt_index_bounddec_notestcoordinates)=(k)) -> (((exists fs_h_jt_bounddec_notestcoordinatesat. fs_h_jt_bounddec_notestcoordinatesat + S (jt_value_bounddec_notestcoordinates) = S ((S (jt_index_bounddec_notestcoordinates)) * c)) /\ exists fs_q_jt_bounddec_notestcoordinatesat. b = fs_q_jt_bounddec_notestcoordinatesat * S ((S (jt_index_bounddec_notestcoordinates)) * c) + (jt_value_bounddec_notestcoordinates))) -> (exists jt_factor_bounddec_notestcoordinatesdivides. (jt_value_bounddec_notestcoordinates)=(jt_divisor_bounddec_no)*jt_factor_bounddec_notestcoordinatesdivides)) -> (jt_divisor_bounddec_no)=1))

Complete tactic proof in conservative notation

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

87 script commands · 28 reading checkpoints · 3 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 test decidable
01Fix variables and assumptionsL1–4

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

  1. L1
    intro n
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro k
02Induction on LL5–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L5
    induction L
03Separate the logical casesL6–6

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

  1. L6
    left
04Fix variables and assumptionsL7–10

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

  1. L7
    intro d
  2. L8
    intro hd
  3. L9
    intro hdiv
  4. L10
    intro hall
05Separate the logical casesL11–11

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

  1. L11
    exfalso
06Use earlier factsL12–17

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

  1. L12
    specialize lt_not_le (d)
  2. L13
    specialize lt_not_le (0)
  3. L14
    apply lt_not_le
  4. L15
    exact hd
  5. L16
    specialize zero_le (d)
  6. L17
    apply zero_le
07Establish htL18–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply jordan tuple divisor test decidable.

  1. L18
    have ht : (Dvd(L,n) → JordanTupleAllDivisible(L,b,c,k) → L = 1) ∨ ¬(Dvd(L,n) → JordanTupleAllDivisible(L,b,c,k) → L = 1)Definitions: Dvd(L,n)JordanTupleAllDivisible(L,b,c,k)Original native command in the exact edition
  2. L19
    specialize jordan_tuple_divisor_test_decidable (n)
  3. L20
    specialize jordan_tuple_divisor_test_decidable (b)
  4. L21
    specialize jordan_tuple_divisor_test_decidable (c)
  5. L22
    specialize jordan_tuple_divisor_test_decidable (k)
  6. L23
    specialize jordan_tuple_divisor_test_decidable (L)
  7. L24
    apply jordan_tuple_divisor_test_decidable
08Separate the logical casesL25–27

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

  1. L25
    cases IH
  2. L26
    cases ht
  3. L27
    left
09Fix variables and assumptionsL28–29

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

  1. L28
    intro d
  2. L29
    intro hd
10Establish hcL30–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L30
    have hc : d = L ∨ Lt(d,L)Definitions: Lt(d,L)Original native command in the exact edition
  2. L31
    specialize finite_lt_succ_eq_or_lt (L)
  3. L32
    specialize finite_lt_succ_eq_or_lt (d)
  4. L33
    apply finite_lt_succ_eq_or_lt
  5. L34
    exact hd
11Separate the logical casesL35–35

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

  1. L35
    cases hc
12Fix variables and assumptionsL36–37

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

  1. L36
    intro hdiv
  2. L37
    intro hall
13Establish heqL38–47

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

  1. L38
    have heq : L=1
  2. L39
    apply ht_left
  3. L40
    rewrite <- hc_left
  4. L41
    exact hdiv
  5. L42
    intro i
  6. L43
    intro a
  7. L44
    intro hi
  8. L45
    intro ha
  9. L46
    rewrite <- hc_left
  10. L47
    specialize hall (i)
14Use earlier factsL48–51

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

  1. L48
    specialize hall (a)
  2. L49
    apply hall
  3. L50
    exact hi
  4. L51
    exact ha
15Calculate and transport equalitiesL52–52

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

  1. L52
    trans L
16Use earlier factsL53–54

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

  1. L53
    exact hc_left
  2. L54
    exact heq
17Fix variables and assumptionsL55–56

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

  1. L55
    intro hdiv
  2. L56
    intro hall
18Use earlier factsL57–61

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

  1. L57
    specialize IH_left (d)
  2. L58
    apply IH_left
  3. L59
    exact hc_right
  4. L60
    exact hdiv
  5. L61
    exact hall
19Separate the logical casesL62–62

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

  1. L62
    right
20Fix variables and assumptionsL63–63

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

  1. L63
    intro h
21Use earlier factsL64–64

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

  1. L64
    apply ht_right
22Fix variables and assumptionsL65–66

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

  1. L65
    intro hdiv
  2. L66
    intro hall
23Use earlier factsL67–72

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

  1. L67
    specialize h (L)
  2. L68
    apply h
  3. L69
    specialize le_refl (S L)
  4. L70
    apply le_refl
  5. L71
    exact hdiv
  6. L72
    exact hall
24Separate the logical casesL73–73

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

  1. L73
    right
25Fix variables and assumptionsL74–74

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

  1. L74
    intro h
26Use earlier factsL75–75

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

  1. L75
    apply IH_right
27Fix variables and assumptionsL76–79

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

  1. L76
    intro d
  2. L77
    intro hd
  3. L78
    intro hdiv
  4. L79
    intro hall
28Use earlier factsL80–87

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

  1. L80
    specialize h (d)
  2. L81
    apply h
  3. L82
    specialize le_succ (S d)
  4. L83
    specialize le_succ (L)
  5. L84
    apply le_succ
  6. L85
    exact hd
  7. L86
    exact hdiv
  8. L87
    exact hall

Library-wide reading audit

Original defined command ledger · 87 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro k
  5. 0005induction L
  6. 0006left
  7. 0007intro d
  8. 0008intro hd
  9. 0009intro hdiv
  10. 0010intro hall
  11. 0011exfalso
  12. 0012specialize lt_not_le (d)
  13. 0013specialize lt_not_le (0)
  14. 0014apply lt_not_le
  15. 0015exact hd
  16. 0016specialize zero_le (d)
  17. 0017apply zero_le
  18. 0018have ht : (Dvd(L,n) → JordanTupleAllDivisible(L,b,c,k) → L = 1) ∨ ¬(Dvd(L,n) → JordanTupleAllDivisible(L,b,c,k) → L = 1)
  19. 0019specialize jordan_tuple_divisor_test_decidable (n)
  20. 0020specialize jordan_tuple_divisor_test_decidable (b)
  21. 0021specialize jordan_tuple_divisor_test_decidable (c)
  22. 0022specialize jordan_tuple_divisor_test_decidable (k)
  23. 0023specialize jordan_tuple_divisor_test_decidable (L)
  24. 0024apply jordan_tuple_divisor_test_decidable
  25. 0025cases IH
  26. 0026cases ht
  27. 0027left
  28. 0028intro d
  29. 0029intro hd
  30. 0030have hc : d = L ∨ Lt(d,L)
  31. 0031specialize finite_lt_succ_eq_or_lt (L)
  32. 0032specialize finite_lt_succ_eq_or_lt (d)
  33. 0033apply finite_lt_succ_eq_or_lt
  34. 0034exact hd
  35. 0035cases hc
  36. 0036intro hdiv
  37. 0037intro hall
  38. 0038have heq : L=1
  39. 0039apply ht_left
  40. 0040rewrite <- hc_left
  41. 0041exact hdiv
  42. 0042intro i
  43. 0043intro a
  44. 0044intro hi
  45. 0045intro ha
  46. 0046rewrite <- hc_left
  47. 0047specialize hall (i)
  48. 0048specialize hall (a)
  49. 0049apply hall
  50. 0050exact hi
  51. 0051exact ha
  52. 0052trans L
  53. 0053exact hc_left
  54. 0054exact heq
  55. 0055intro hdiv
  56. 0056intro hall
  57. 0057specialize IH_left (d)
  58. 0058apply IH_left
  59. 0059exact hc_right
  60. 0060exact hdiv
  61. 0061exact hall
  62. 0062right
  63. 0063intro h
  64. 0064apply ht_right
  65. 0065intro hdiv
  66. 0066intro hall
  67. 0067specialize h (L)
  68. 0068apply h
  69. 0069specialize le_refl (S L)
  70. 0070apply le_refl
  71. 0071exact hdiv
  72. 0072exact hall
  73. 0073right
  74. 0074intro h
  75. 0075apply IH_right
  76. 0076intro d
  77. 0077intro hd
  78. 0078intro hdiv
  79. 0079intro hall
  80. 0080specialize h (d)
  81. 0081apply h
  82. 0082specialize le_succ (S d)
  83. 0083specialize le_succ (L)
  84. 0084apply le_succ
  85. 0085exact hd
  86. 0086exact hdiv
  87. 0087exact hall