JT0018

jordan_tuple_equal_extend

Extend equal prefixes using two actual equal last entries.

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. ∀ a. ∀ z. IntegerVectorZero(b,c,d,e,k) → BetaAt(b,c,k,a) → BetaAt(d,e,k,z) → a = z → IntegerVectorZero(b,c,d,e,S k)

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

Definition DAG

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

Actual proof prerequisites

finite_lt_succ_eq_or_lt · checked external prerequisitebeta_at_unique · checked external prerequisite
Original expanded first-order 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)

Complete tactic proof in conservative notation

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 ∨ Lt(i,k)Definitions: Lt(i,k)Original native command in the exact edition
  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 defined 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 ∨ Lt(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