JT001C

jordan_tuple_listed_decidable

Finite list membership is decided by actual outer entries and coordinate equality.

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

∀ b. ∀ c. ∀ k. ∀ B. ∀ C. ∀ D. ∀ E. ∀ j. JordanTupleListed(b,c,k,B,C,D,E,j) ∨ ¬JordanTupleListed(b,c,k,B,C,D,E,j)

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

Definition DAG

IntegerVectorZero(ab,ac,db,dc,l) · 2JordanTupleListed(b,c,k,B,C,D,E,j) · 2Lt(a,b) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

jordan_tuple_listed_emptyjordan_tuple_listed_liftbeta_at_exists · checked external prerequisitejordan_tuple_equal_decidablele_refl · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisitebeta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall b c k B C D E j. (exists jt_index_listedyes jt_code_listedyes jt_scale_listedyes. ((exists jt_gap_listedyesindex. jt_gap_listedyesindex+S (jt_index_listedyes)=(j)) /\ (((((((exists fs_h_jt_listedyescode. fs_h_jt_listedyescode + S (jt_code_listedyes) = S ((S (jt_index_listedyes)) * C)) /\ exists fs_q_jt_listedyescode. B = fs_q_jt_listedyescode * S ((S (jt_index_listedyes)) * C) + (jt_code_listedyes))) /\ (((exists fs_h_jt_listedyesscale. fs_h_jt_listedyesscale + S (jt_scale_listedyes) = S ((S (jt_index_listedyes)) * E)) /\ exists fs_q_jt_listedyesscale. D = fs_q_jt_listedyesscale * S ((S (jt_index_listedyes)) * E) + (jt_scale_listedyes))))) /\ (forall jt_index_listedyesequal jt_left_listedyesequal jt_right_listedyesequal. (exists jt_gap_listedyesequalindex. jt_gap_listedyesequalindex+S (jt_index_listedyesequal)=(k)) -> (((exists fs_h_jt_listedyesequalleft. fs_h_jt_listedyesequalleft + S (jt_left_listedyesequal) = S ((S (jt_index_listedyesequal)) * c)) /\ exists fs_q_jt_listedyesequalleft. b = fs_q_jt_listedyesequalleft * S ((S (jt_index_listedyesequal)) * c) + (jt_left_listedyesequal))) -> (((exists fs_h_jt_listedyesequalright. fs_h_jt_listedyesequalright + S (jt_right_listedyesequal) = S ((S (jt_index_listedyesequal)) * jt_scale_listedyes)) /\ exists fs_q_jt_listedyesequalright. jt_code_listedyes = fs_q_jt_listedyesequalright * S ((S (jt_index_listedyesequal)) * jt_scale_listedyes) + (jt_right_listedyesequal))) -> jt_left_listedyesequal=jt_right_listedyesequal))))) \/ ~(exists jt_index_listedno jt_code_listedno jt_scale_listedno. ((exists jt_gap_listednoindex. jt_gap_listednoindex+S (jt_index_listedno)=(j)) /\ (((((((exists fs_h_jt_listednocode. fs_h_jt_listednocode + S (jt_code_listedno) = S ((S (jt_index_listedno)) * C)) /\ exists fs_q_jt_listednocode. B = fs_q_jt_listednocode * S ((S (jt_index_listedno)) * C) + (jt_code_listedno))) /\ (((exists fs_h_jt_listednoscale. fs_h_jt_listednoscale + S (jt_scale_listedno) = S ((S (jt_index_listedno)) * E)) /\ exists fs_q_jt_listednoscale. D = fs_q_jt_listednoscale * S ((S (jt_index_listedno)) * E) + (jt_scale_listedno))))) /\ (forall jt_index_listednoequal jt_left_listednoequal jt_right_listednoequal. (exists jt_gap_listednoequalindex. jt_gap_listednoequalindex+S (jt_index_listednoequal)=(k)) -> (((exists fs_h_jt_listednoequalleft. fs_h_jt_listednoequalleft + S (jt_left_listednoequal) = S ((S (jt_index_listednoequal)) * c)) /\ exists fs_q_jt_listednoequalleft. b = fs_q_jt_listednoequalleft * S ((S (jt_index_listednoequal)) * c) + (jt_left_listednoequal))) -> (((exists fs_h_jt_listednoequalright. fs_h_jt_listednoequalright + S (jt_right_listednoequal) = S ((S (jt_index_listednoequal)) * jt_scale_listedno)) /\ exists fs_q_jt_listednoequalright. jt_code_listedno = fs_q_jt_listednoequalright * S ((S (jt_index_listednoequal)) * jt_scale_listedno) + (jt_right_listednoequal))) -> jt_left_listednoequal=jt_right_listednoequal)))))

Complete tactic proof in conservative notation

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

113 script commands · 34 reading checkpoints · 6 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 (3)
jordan tuple listed emptyjordan tuple listed liftjordan tuple equal decidable
01Fix variables and assumptionsL1–7

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro k
  4. L4
    intro B
  5. L5
    intro C
  6. L6
    intro D
  7. L7
    intro E
02Induction on jL8–8

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

  1. L8
    induction j
03Separate the logical casesL9–9

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

  1. L9
    right
04Fix variables and assumptionsL10–10

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

  1. L10
    intro hempty
05Use earlier factsL11–19

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

  1. L11
    specialize jordan_tuple_listed_empty (b)
  2. L12
    specialize jordan_tuple_listed_empty (c)
  3. L13
    specialize jordan_tuple_listed_empty (k)
  4. L14
    specialize jordan_tuple_listed_empty (B)
  5. L15
    specialize jordan_tuple_listed_empty (C)
  6. L16
    specialize jordan_tuple_listed_empty (D)
  7. L17
    specialize jordan_tuple_listed_empty (E)
  8. L18
    apply jordan_tuple_listed_empty
  9. L19
    exact hempty
06Separate the logical casesL20–21

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

  1. L20
    cases IH
  2. L21
    left
07Use earlier factsL22–31

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

  1. L22
    specialize jordan_tuple_listed_lift (b)
  2. L23
    specialize jordan_tuple_listed_lift (c)
  3. L24
    specialize jordan_tuple_listed_lift (k)
  4. L25
    specialize jordan_tuple_listed_lift (B)
  5. L26
    specialize jordan_tuple_listed_lift (C)
  6. L27
    specialize jordan_tuple_listed_lift (D)
  7. L28
    specialize jordan_tuple_listed_lift (E)
  8. L29
    specialize jordan_tuple_listed_lift (j)
  9. L30
    apply jordan_tuple_listed_lift
  10. L31
    exact IH_left
08Establish hdL32–36

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

  1. L32
    have hd : ∃ d. BetaAt(B,C,j,d)Definitions: BetaAt(B,C,j,d)Original native command in the exact edition
  2. L33
    specialize beta_at_exists (B)
  3. L34
    specialize beta_at_exists (C)
  4. L35
    specialize beta_at_exists (j)
  5. L36
    apply beta_at_exists
09Separate the logical casesL37–37

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

  1. L37
    cases hd
10Establish heL38–42

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

  1. L38
    have he : ∃ e. BetaAt(D,E,j,e)Definitions: BetaAt(D,E,j,e)Original native command in the exact edition
  2. L39
    specialize beta_at_exists (D)
  3. L40
    specialize beta_at_exists (E)
  4. L41
    specialize beta_at_exists (j)
  5. L42
    apply beta_at_exists
11Separate the logical casesL43–43

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

  1. L43
    cases he
12Establish heqL44–50

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

  1. L44
    have heq : IntegerVectorZero(b,c,x,x1,k) ∨ ¬IntegerVectorZero(b,c,x,x1,k)Definitions: IntegerVectorZero(b,c,x,x1,k)Original native command in the exact edition
  2. L45
    specialize jordan_tuple_equal_decidable (b)
  3. L46
    specialize jordan_tuple_equal_decidable (c)
  4. L47
    specialize jordan_tuple_equal_decidable (x)
  5. L48
    specialize jordan_tuple_equal_decidable (x1)
  6. L49
    specialize jordan_tuple_equal_decidable (k)
  7. L50
    apply jordan_tuple_equal_decidable
13Separate the logical casesL51–52

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

  1. L51
    cases heq
  2. L52
    left
14Construct an explicit witnessL53–55

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

  1. L53
    exists j
  2. L54
    exists x
  3. L55
    exists x1
15Separate the logical casesL56–56

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

  1. L56
    split
16Use earlier factsL57–58

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

  1. L57
    specialize le_refl (S j)
  2. L58
    apply le_refl
17Separate the logical casesL59–60

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

  1. L59
    split
  2. L60
    split
18Use earlier factsL61–63

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

  1. L61
    exact hd_witness
  2. L62
    exact he_witness
  3. L63
    exact heq_left
19Separate the logical casesL64–64

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

  1. L64
    right
20Fix variables and assumptionsL65–65

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

  1. L65
    intro h
21Separate the logical casesL66–70

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

  1. L66
    cases h
  2. L67
    cases h_witness
  3. L68
    cases h_witness_witness
  4. L69
    cases h_witness_witness_witness
  5. L70
    cases h_witness_witness_witness_right
22Establish hcL71–75

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. L71
    have hc : x2 = j ∨ Lt(x2,j)Definitions: Lt(x2,j)Original native command in the exact edition
  2. L72
    specialize finite_lt_succ_eq_or_lt (j)
  3. L73
    specialize finite_lt_succ_eq_or_lt (x2)
  4. L74
    apply finite_lt_succ_eq_or_lt
  5. L75
    exact h_witness_witness_witness_left
23Separate the logical casesL76–77

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

  1. L76
    cases hc
  2. L77
    cases h_witness_witness_witness_right_left
24Establish hdvalL78–87

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

  1. L78
    have hdval : x3=x
  2. L79
    specialize beta_at_unique (B)
  3. L80
    specialize beta_at_unique (C)
  4. L81
    specialize beta_at_unique (j)
  5. L82
    specialize beta_at_unique (x3)
  6. L83
    specialize beta_at_unique (x)
  7. L84
    apply beta_at_unique
  8. L85
    rewrite hc_left at h_witness_witness_witness_right_left_left
  9. L86
    rewrite hc_left at h_witness_witness_witness_right_left_left
  10. L87
    exact h_witness_witness_witness_right_left_left
25Use earlier factsL88–88

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

  1. L88
    exact hd_witness
26Establish hevalL89–98

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

  1. L89
    have heval : x4=x1
  2. L90
    specialize beta_at_unique (D)
  3. L91
    specialize beta_at_unique (E)
  4. L92
    specialize beta_at_unique (j)
  5. L93
    specialize beta_at_unique (x4)
  6. L94
    specialize beta_at_unique (x1)
  7. L95
    apply beta_at_unique
  8. L96
    rewrite hc_left at h_witness_witness_witness_right_left_right
  9. L97
    rewrite hc_left at h_witness_witness_witness_right_left_right
  10. L98
    exact h_witness_witness_witness_right_left_right
27Use earlier factsL99–100

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

  1. L99
    exact he_witness
  2. L100
    apply heq_right
28Calculate and transport equalitiesL101–103

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

  1. L101
    rewrite hdval at h_witness_witness_witness_right_right
  2. L102
    rewrite heval at h_witness_witness_witness_right_right
  3. L103
    rewrite heval at h_witness_witness_witness_right_right
29Use earlier factsL104–105

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

  1. L104
    exact h_witness_witness_witness_right_right
  2. L105
    apply IH_right
30Construct an explicit witnessL106–108

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

  1. L106
    exists x2
  2. L107
    exists x3
  3. L108
    exists x4
31Separate the logical casesL109–109

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

  1. L109
    split
32Use earlier factsL110–110

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

  1. L110
    exact hc_right
33Separate the logical casesL111–111

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

  1. L111
    split
34Use earlier factsL112–113

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

  1. L112
    exact h_witness_witness_witness_right_left
  2. L113
    exact h_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 113 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro k
  4. 0004intro B
  5. 0005intro C
  6. 0006intro D
  7. 0007intro E
  8. 0008induction j
  9. 0009right
  10. 0010intro hempty
  11. 0011specialize jordan_tuple_listed_empty (b)
  12. 0012specialize jordan_tuple_listed_empty (c)
  13. 0013specialize jordan_tuple_listed_empty (k)
  14. 0014specialize jordan_tuple_listed_empty (B)
  15. 0015specialize jordan_tuple_listed_empty (C)
  16. 0016specialize jordan_tuple_listed_empty (D)
  17. 0017specialize jordan_tuple_listed_empty (E)
  18. 0018apply jordan_tuple_listed_empty
  19. 0019exact hempty
  20. 0020cases IH
  21. 0021left
  22. 0022specialize jordan_tuple_listed_lift (b)
  23. 0023specialize jordan_tuple_listed_lift (c)
  24. 0024specialize jordan_tuple_listed_lift (k)
  25. 0025specialize jordan_tuple_listed_lift (B)
  26. 0026specialize jordan_tuple_listed_lift (C)
  27. 0027specialize jordan_tuple_listed_lift (D)
  28. 0028specialize jordan_tuple_listed_lift (E)
  29. 0029specialize jordan_tuple_listed_lift (j)
  30. 0030apply jordan_tuple_listed_lift
  31. 0031exact IH_left
  32. 0032have hd : ∃ d. BetaAt(B,C,j,d)
  33. 0033specialize beta_at_exists (B)
  34. 0034specialize beta_at_exists (C)
  35. 0035specialize beta_at_exists (j)
  36. 0036apply beta_at_exists
  37. 0037cases hd
  38. 0038have he : ∃ e. BetaAt(D,E,j,e)
  39. 0039specialize beta_at_exists (D)
  40. 0040specialize beta_at_exists (E)
  41. 0041specialize beta_at_exists (j)
  42. 0042apply beta_at_exists
  43. 0043cases he
  44. 0044have heq : IntegerVectorZero(b,c,x,x1,k) ∨ ¬IntegerVectorZero(b,c,x,x1,k)
  45. 0045specialize jordan_tuple_equal_decidable (b)
  46. 0046specialize jordan_tuple_equal_decidable (c)
  47. 0047specialize jordan_tuple_equal_decidable (x)
  48. 0048specialize jordan_tuple_equal_decidable (x1)
  49. 0049specialize jordan_tuple_equal_decidable (k)
  50. 0050apply jordan_tuple_equal_decidable
  51. 0051cases heq
  52. 0052left
  53. 0053exists j
  54. 0054exists x
  55. 0055exists x1
  56. 0056split
  57. 0057specialize le_refl (S j)
  58. 0058apply le_refl
  59. 0059split
  60. 0060split
  61. 0061exact hd_witness
  62. 0062exact he_witness
  63. 0063exact heq_left
  64. 0064right
  65. 0065intro h
  66. 0066cases h
  67. 0067cases h_witness
  68. 0068cases h_witness_witness
  69. 0069cases h_witness_witness_witness
  70. 0070cases h_witness_witness_witness_right
  71. 0071have hc : x2 = j ∨ Lt(x2,j)
  72. 0072specialize finite_lt_succ_eq_or_lt (j)
  73. 0073specialize finite_lt_succ_eq_or_lt (x2)
  74. 0074apply finite_lt_succ_eq_or_lt
  75. 0075exact h_witness_witness_witness_left
  76. 0076cases hc
  77. 0077cases h_witness_witness_witness_right_left
  78. 0078have hdval : x3=x
  79. 0079specialize beta_at_unique (B)
  80. 0080specialize beta_at_unique (C)
  81. 0081specialize beta_at_unique (j)
  82. 0082specialize beta_at_unique (x3)
  83. 0083specialize beta_at_unique (x)
  84. 0084apply beta_at_unique
  85. 0085rewrite hc_left at h_witness_witness_witness_right_left_left
  86. 0086rewrite hc_left at h_witness_witness_witness_right_left_left
  87. 0087exact h_witness_witness_witness_right_left_left
  88. 0088exact hd_witness
  89. 0089have heval : x4=x1
  90. 0090specialize beta_at_unique (D)
  91. 0091specialize beta_at_unique (E)
  92. 0092specialize beta_at_unique (j)
  93. 0093specialize beta_at_unique (x4)
  94. 0094specialize beta_at_unique (x1)
  95. 0095apply beta_at_unique
  96. 0096rewrite hc_left at h_witness_witness_witness_right_left_right
  97. 0097rewrite hc_left at h_witness_witness_witness_right_left_right
  98. 0098exact h_witness_witness_witness_right_left_right
  99. 0099exact he_witness
  100. 0100apply heq_right
  101. 0101rewrite hdval at h_witness_witness_witness_right_right
  102. 0102rewrite heval at h_witness_witness_witness_right_right
  103. 0103rewrite heval at h_witness_witness_witness_right_right
  104. 0104exact h_witness_witness_witness_right_right
  105. 0105apply IH_right
  106. 0106exists x2
  107. 0107exists x3
  108. 0108exists x4
  109. 0109split
  110. 0110exact hc_right
  111. 0111split
  112. 0112exact h_witness_witness_witness_right_left
  113. 0113exact h_witness_witness_witness_right_right