JT0019

jordan_tuple_equal_decidable

Inductively decide decoded coordinate equality, never equality of beta codes.

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. ∀ d. ∀ e. ∀ k. IntegerVectorZero(b,c,d,e,k) ∨ ¬IntegerVectorZero(b,c,d,e,k)

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

Definition DAG

IntegerVectorZero(ab,ac,db,dc,l) · 2BetaAt(b,c,i,x) · 2

Actual proof prerequisites

jordan_tuple_equal_emptybeta_at_exists · checked external prerequisiteeq_decidable · checked external prerequisitejordan_tuple_equal_extendle_refl · checked external prerequisitejordan_tuple_equal_drop_last
Original expanded first-order statement 
forall b c d e k. (forall jt_index_eqyes jt_left_eqyes jt_right_eqyes. (exists jt_gap_eqyesindex. jt_gap_eqyesindex+S (jt_index_eqyes)=(k)) -> (((exists fs_h_jt_eqyesleft. fs_h_jt_eqyesleft + S (jt_left_eqyes) = S ((S (jt_index_eqyes)) * c)) /\ exists fs_q_jt_eqyesleft. b = fs_q_jt_eqyesleft * S ((S (jt_index_eqyes)) * c) + (jt_left_eqyes))) -> (((exists fs_h_jt_eqyesright. fs_h_jt_eqyesright + S (jt_right_eqyes) = S ((S (jt_index_eqyes)) * e)) /\ exists fs_q_jt_eqyesright. d = fs_q_jt_eqyesright * S ((S (jt_index_eqyes)) * e) + (jt_right_eqyes))) -> jt_left_eqyes=jt_right_eqyes) \/ ~(forall jt_index_eqno jt_left_eqno jt_right_eqno. (exists jt_gap_eqnoindex. jt_gap_eqnoindex+S (jt_index_eqno)=(k)) -> (((exists fs_h_jt_eqnoleft. fs_h_jt_eqnoleft + S (jt_left_eqno) = S ((S (jt_index_eqno)) * c)) /\ exists fs_q_jt_eqnoleft. b = fs_q_jt_eqnoleft * S ((S (jt_index_eqno)) * c) + (jt_left_eqno))) -> (((exists fs_h_jt_eqnoright. fs_h_jt_eqnoright + S (jt_right_eqno) = S ((S (jt_index_eqno)) * e)) /\ exists fs_q_jt_eqnoright. d = fs_q_jt_eqnoright * S ((S (jt_index_eqno)) * e) + (jt_right_eqno))) -> jt_left_eqno=jt_right_eqno)

Complete tactic proof in conservative notation

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

63 script commands · 18 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 (3)
jordan tuple equal emptyjordan tuple equal extendjordan tuple equal drop last
01Fix variables and assumptionsL1–4

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
02Induction on kL5–5

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

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

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

  1. L6
    left
04Use earlier factsL7–11

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

  1. L7
    specialize jordan_tuple_equal_empty (b)
  2. L8
    specialize jordan_tuple_equal_empty (c)
  3. L9
    specialize jordan_tuple_equal_empty (d)
  4. L10
    specialize jordan_tuple_equal_empty (e)
  5. L11
    apply jordan_tuple_equal_empty
05Establish haL12–16

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

  1. L12
    have ha : ∃ a. BetaAt(b,c,k,a)Definitions: BetaAt(b,c,k,a)Original native command in the exact edition
  2. L13
    specialize beta_at_exists (b)
  3. L14
    specialize beta_at_exists (c)
  4. L15
    specialize beta_at_exists (k)
  5. L16
    apply beta_at_exists
06Separate the logical casesL17–17

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

  1. L17
    cases ha
07Establish hzL18–22

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

  1. L18
    have hz : ∃ z. BetaAt(d,e,k,z)Definitions: BetaAt(d,e,k,z)Original native command in the exact edition
  2. L19
    specialize beta_at_exists (d)
  3. L20
    specialize beta_at_exists (e)
  4. L21
    specialize beta_at_exists (k)
  5. L22
    apply beta_at_exists
08Separate the logical casesL23–23

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

  1. L23
    cases hz
09Establish heqL24–27

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

  1. L24
    have heq : x=x1 \/ ~(x=x1)
  2. L25
    specialize eq_decidable (x)
  3. L26
    specialize eq_decidable (x1)
  4. L27
    apply eq_decidable
10Separate the logical casesL28–30

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

  1. L28
    cases IH
  2. L29
    cases heq
  3. L30
    left
11Use earlier factsL31–40

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

  1. L31
    specialize jordan_tuple_equal_extend (b)
  2. L32
    specialize jordan_tuple_equal_extend (c)
  3. L33
    specialize jordan_tuple_equal_extend (d)
  4. L34
    specialize jordan_tuple_equal_extend (e)
  5. L35
    specialize jordan_tuple_equal_extend (k)
  6. L36
    specialize jordan_tuple_equal_extend (x)
  7. L37
    specialize jordan_tuple_equal_extend (x1)
  8. L38
    apply jordan_tuple_equal_extend
  9. L39
    exact IH_left
  10. L40
    exact ha_witness
12Use earlier factsL41–42

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

  1. L41
    exact hz_witness
  2. L42
    exact heq_left
13Separate the logical casesL43–43

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

  1. L43
    right
14Fix variables and assumptionsL44–44

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

  1. L44
    intro h
15Use earlier factsL45–53

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

  1. L45
    apply heq_right
  2. L46
    specialize h (k)
  3. L47
    specialize h (x)
  4. L48
    specialize h (x1)
  5. L49
    apply h
  6. L50
    specialize le_refl (S k)
  7. L51
    apply le_refl
  8. L52
    exact ha_witness
  9. L53
    exact hz_witness
16Separate the logical casesL54–54

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

  1. L54
    right
17Fix variables and assumptionsL55–55

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

  1. L55
    intro h
18Use earlier factsL56–63

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

  1. L56
    apply IH_right
  2. L57
    specialize jordan_tuple_equal_drop_last (b)
  3. L58
    specialize jordan_tuple_equal_drop_last (c)
  4. L59
    specialize jordan_tuple_equal_drop_last (d)
  5. L60
    specialize jordan_tuple_equal_drop_last (e)
  6. L61
    specialize jordan_tuple_equal_drop_last (k)
  7. L62
    apply jordan_tuple_equal_drop_last
  8. L63
    exact h

Library-wide reading audit

Original defined command ledger · 63 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005induction k
  6. 0006left
  7. 0007specialize jordan_tuple_equal_empty (b)
  8. 0008specialize jordan_tuple_equal_empty (c)
  9. 0009specialize jordan_tuple_equal_empty (d)
  10. 0010specialize jordan_tuple_equal_empty (e)
  11. 0011apply jordan_tuple_equal_empty
  12. 0012have ha : ∃ a. BetaAt(b,c,k,a)
  13. 0013specialize beta_at_exists (b)
  14. 0014specialize beta_at_exists (c)
  15. 0015specialize beta_at_exists (k)
  16. 0016apply beta_at_exists
  17. 0017cases ha
  18. 0018have hz : ∃ z. BetaAt(d,e,k,z)
  19. 0019specialize beta_at_exists (d)
  20. 0020specialize beta_at_exists (e)
  21. 0021specialize beta_at_exists (k)
  22. 0022apply beta_at_exists
  23. 0023cases hz
  24. 0024have heq : x=x1 \/ ~(x=x1)
  25. 0025specialize eq_decidable (x)
  26. 0026specialize eq_decidable (x1)
  27. 0027apply eq_decidable
  28. 0028cases IH
  29. 0029cases heq
  30. 0030left
  31. 0031specialize jordan_tuple_equal_extend (b)
  32. 0032specialize jordan_tuple_equal_extend (c)
  33. 0033specialize jordan_tuple_equal_extend (d)
  34. 0034specialize jordan_tuple_equal_extend (e)
  35. 0035specialize jordan_tuple_equal_extend (k)
  36. 0036specialize jordan_tuple_equal_extend (x)
  37. 0037specialize jordan_tuple_equal_extend (x1)
  38. 0038apply jordan_tuple_equal_extend
  39. 0039exact IH_left
  40. 0040exact ha_witness
  41. 0041exact hz_witness
  42. 0042exact heq_left
  43. 0043right
  44. 0044intro h
  45. 0045apply heq_right
  46. 0046specialize h (k)
  47. 0047specialize h (x)
  48. 0048specialize h (x1)
  49. 0049apply h
  50. 0050specialize le_refl (S k)
  51. 0051apply le_refl
  52. 0052exact ha_witness
  53. 0053exact hz_witness
  54. 0054right
  55. 0055intro h
  56. 0056apply IH_right
  57. 0057specialize jordan_tuple_equal_drop_last (b)
  58. 0058specialize jordan_tuple_equal_drop_last (c)
  59. 0059specialize jordan_tuple_equal_drop_last (d)
  60. 0060specialize jordan_tuple_equal_drop_last (e)
  61. 0061specialize jordan_tuple_equal_drop_last (k)
  62. 0062apply jordan_tuple_equal_drop_last
  63. 0063exact h