JT0018

jordan_tuple_equal_extend

Alpha v35 independently verified · alpha_closed; checked-use authorized; not Stable

Extend equal prefixes using two actual equal last entries.

Exact expanded first-order arithmetic statement

forall b c d e k a z. (forall jt_index_eqextendprefix jt_left_eqextendprefix jt_right_eqextendprefix. (exists jt_gap_eqextendprefixindex. jt_gap_eqextendprefixindex+S (jt_index_eqextendprefix)=(k)) -> (((exists fs_h_jt_eqextendprefixleft. fs_h_jt_eqextendprefixleft + S (jt_left_eqextendprefix) = S ((S (jt_index_eqextendprefix)) * c)) /\ exists fs_q_jt_eqextendprefixleft. b = fs_q_jt_eqextendprefixleft * S ((S (jt_index_eqextendprefix)) * c) + (jt_left_eqextendprefix))) -> (((exists fs_h_jt_eqextendprefixright. fs_h_jt_eqextendprefixright + S (jt_right_eqextendprefix) = S ((S (jt_index_eqextendprefix)) * e)) /\ exists fs_q_jt_eqextendprefixright. d = fs_q_jt_eqextendprefixright * S ((S (jt_index_eqextendprefix)) * e) + (jt_right_eqextendprefix))) -> jt_left_eqextendprefix=jt_right_eqextendprefix) -> (((exists fs_h_jt_eqextendleft. fs_h_jt_eqextendleft + S (a) = S ((S (k)) * c)) /\ exists fs_q_jt_eqextendleft. b = fs_q_jt_eqextendleft * S ((S (k)) * c) + (a))) -> (((exists fs_h_jt_eqextendright. fs_h_jt_eqextendright + S (z) = S ((S (k)) * e)) /\ exists fs_q_jt_eqextendright. d = fs_q_jt_eqextendright * S ((S (k)) * e) + (z))) -> a=z -> (forall jt_index_eqextendtarget jt_left_eqextendtarget jt_right_eqextendtarget. (exists jt_gap_eqextendtargetindex. jt_gap_eqextendtargetindex+S (jt_index_eqextendtarget)=(S k)) -> (((exists fs_h_jt_eqextendtargetleft. fs_h_jt_eqextendtargetleft + S (jt_left_eqextendtarget) = S ((S (jt_index_eqextendtarget)) * c)) /\ exists fs_q_jt_eqextendtargetleft. b = fs_q_jt_eqextendtargetleft * S ((S (jt_index_eqextendtarget)) * c) + (jt_left_eqextendtarget))) -> (((exists fs_h_jt_eqextendtargetright. fs_h_jt_eqextendtargetright + S (jt_right_eqextendtarget) = S ((S (jt_index_eqextendtarget)) * e)) /\ exists fs_q_jt_eqextendtargetright. d = fs_q_jt_eqextendtargetright * S ((S (jt_index_eqextendtarget)) * e) + (jt_right_eqextendtarget))) -> jt_left_eqextendtarget=jt_right_eqextendtarget)

Constructive proof overview

Generated structural guide

Extend equal prefixes using two actual equal last entries.

The unchanged tactic script uses 2 declared prerequisites and contains 55 exact native proof lines.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

finite_lt_succ_eq_or_lt Alpha theorem; checked-use authorized beta_at_unique Alpha theorem; checked-use authorized

Direct dependents

JT0019 jordan_tuple_equal_decidable

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

55 script commands · 10 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.

01Fix variables and assumptionsL1–10

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
  5. L5
    intro k
  6. L6
    intro a
  7. L7
    intro z
  8. L8
    intro hp
  9. L9
    intro ha
  10. L10
    intro hz
02Fix variables and assumptionsL11–17

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

  1. L11
    intro heq
  2. L12
    intro i
  3. L13
    intro r
  4. L14
    intro s
  5. L15
    intro hi
  6. L16
    intro hr
  7. L17
    intro hs
03Establish hcL18–22

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. L18
    have hc : i=k \/ (exists jt_gap_eqextendcases. jt_gap_eqextendcases+S (i)=(k))
  2. L19
    specialize finite_lt_succ_eq_or_lt (k)
  3. L20
    specialize finite_lt_succ_eq_or_lt (i)
  4. L21
    apply finite_lt_succ_eq_or_lt
  5. L22
    exact hi
04Separate the logical casesL23–23

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

  1. L23
    cases hc
05Establish hleftL24–33

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

  1. L24
    have hleft : r=a
  2. L25
    specialize beta_at_unique (b)
  3. L26
    specialize beta_at_unique (c)
  4. L27
    specialize beta_at_unique (k)
  5. L28
    specialize beta_at_unique (r)
  6. L29
    specialize beta_at_unique (a)
  7. L30
    apply beta_at_unique
  8. L31
    rewrite hc_left at hr
  9. L32
    rewrite hc_left at hr
  10. L33
    exact hr
06Use earlier factsL34–34

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

  1. L34
    exact ha
07Establish hrightL35–44

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

  1. L35
    have hright : s=z
  2. L36
    specialize beta_at_unique (d)
  3. L37
    specialize beta_at_unique (e)
  4. L38
    specialize beta_at_unique (k)
  5. L39
    specialize beta_at_unique (s)
  6. L40
    specialize beta_at_unique (z)
  7. L41
    apply beta_at_unique
  8. L42
    rewrite hc_left at hs
  9. L43
    rewrite hc_left at hs
  10. L44
    exact hs
08Use earlier factsL45–45

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

  1. L45
    exact hz
09Calculate and transport equalitiesL46–47

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

  1. L46
    rewrite hleft
  2. L47
    rewrite hright
10Use earlier factsL48–55

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

  1. L48
    exact heq
  2. L49
    specialize hp (i)
  3. L50
    specialize hp (r)
  4. L51
    specialize hp (s)
  5. L52
    apply hp
  6. L53
    exact hc_right
  7. L54
    exact hr
  8. L55
    exact hs

Library-wide reading audit

Original exact command ledger · 55 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro k
  6. 0006intro a
  7. 0007intro z
  8. 0008intro hp
  9. 0009intro ha
  10. 0010intro hz
  11. 0011intro heq
  12. 0012intro i
  13. 0013intro r
  14. 0014intro s
  15. 0015intro hi
  16. 0016intro hr
  17. 0017intro hs
  18. 0018have hc : i=k \/ (exists jt_gap_eqextendcases. jt_gap_eqextendcases+S (i)=(k))
  19. 0019specialize finite_lt_succ_eq_or_lt (k)
  20. 0020specialize finite_lt_succ_eq_or_lt (i)
  21. 0021apply finite_lt_succ_eq_or_lt
  22. 0022exact hi
  23. 0023cases hc
  24. 0024have hleft : r=a
  25. 0025specialize beta_at_unique (b)
  26. 0026specialize beta_at_unique (c)
  27. 0027specialize beta_at_unique (k)
  28. 0028specialize beta_at_unique (r)
  29. 0029specialize beta_at_unique (a)
  30. 0030apply beta_at_unique
  31. 0031rewrite hc_left at hr
  32. 0032rewrite hc_left at hr
  33. 0033exact hr
  34. 0034exact ha
  35. 0035have hright : s=z
  36. 0036specialize beta_at_unique (d)
  37. 0037specialize beta_at_unique (e)
  38. 0038specialize beta_at_unique (k)
  39. 0039specialize beta_at_unique (s)
  40. 0040specialize beta_at_unique (z)
  41. 0041apply beta_at_unique
  42. 0042rewrite hc_left at hs
  43. 0043rewrite hc_left at hs
  44. 0044exact hs
  45. 0045exact hz
  46. 0046rewrite hleft
  47. 0047rewrite hright
  48. 0048exact heq
  49. 0049specialize hp (i)
  50. 0050specialize hp (r)
  51. 0051specialize hp (s)
  52. 0052apply hp
  53. 0053exact hc_right
  54. 0054exact hr
  55. 0055exact hs