JT004F

jordan_enumeration_index_map_append

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

Append one genuine matched target index and preserve all previous mapped positions by beta extension.

Exact expanded first-order arithmetic statement

forall k A B C D E F G H Z W q v j. (forall jt_index_append_old. (exists jt_gap_append_oldindex. jt_gap_append_oldindex+S (jt_index_append_old)=(q)) -> exists jt_image_append_old. ((((exists fs_h_jt_append_oldat. fs_h_jt_append_oldat + S (jt_image_append_old) = S ((S (jt_index_append_old)) * W)) /\ exists fs_q_jt_append_oldat. Z = fs_q_jt_append_oldat * S ((S (jt_index_append_old)) * W) + (jt_image_append_old))) /\ (((exists jt_gap_append_oldbound. jt_gap_append_oldbound+S (jt_image_append_old)=(v)) /\ (forall jt_b_append_oldmatch jt_c_append_oldmatch jt_d_append_oldmatch jt_e_append_oldmatch. (((((exists fs_h_jt_append_oldmatchleftcode. fs_h_jt_append_oldmatchleftcode + S (jt_b_append_oldmatch) = S ((S (jt_index_append_old)) * B)) /\ exists fs_q_jt_append_oldmatchleftcode. A = fs_q_jt_append_oldmatchleftcode * S ((S (jt_index_append_old)) * B) + (jt_b_append_oldmatch))) /\ (((exists fs_h_jt_append_oldmatchleftscale. fs_h_jt_append_oldmatchleftscale + S (jt_c_append_oldmatch) = S ((S (jt_index_append_old)) * D)) /\ exists fs_q_jt_append_oldmatchleftscale. C = fs_q_jt_append_oldmatchleftscale * S ((S (jt_index_append_old)) * D) + (jt_c_append_oldmatch))))) -> (((((exists fs_h_jt_append_oldmatchrightcode. fs_h_jt_append_oldmatchrightcode + S (jt_d_append_oldmatch) = S ((S (jt_image_append_old)) * F)) /\ exists fs_q_jt_append_oldmatchrightcode. E = fs_q_jt_append_oldmatchrightcode * S ((S (jt_image_append_old)) * F) + (jt_d_append_oldmatch))) /\ (((exists fs_h_jt_append_oldmatchrightscale. fs_h_jt_append_oldmatchrightscale + S (jt_e_append_oldmatch) = S ((S (jt_image_append_old)) * H)) /\ exists fs_q_jt_append_oldmatchrightscale. G = fs_q_jt_append_oldmatchrightscale * S ((S (jt_image_append_old)) * H) + (jt_e_append_oldmatch))))) -> (forall jt_index_append_oldmatchequal jt_left_append_oldmatchequal jt_right_append_oldmatchequal. (exists jt_gap_append_oldmatchequalindex. jt_gap_append_oldmatchequalindex+S (jt_index_append_oldmatchequal)=(k)) -> (((exists fs_h_jt_append_oldmatchequalleft. fs_h_jt_append_oldmatchequalleft + S (jt_left_append_oldmatchequal) = S ((S (jt_index_append_oldmatchequal)) * jt_c_append_oldmatch)) /\ exists fs_q_jt_append_oldmatchequalleft. jt_b_append_oldmatch = fs_q_jt_append_oldmatchequalleft * S ((S (jt_index_append_oldmatchequal)) * jt_c_append_oldmatch) + (jt_left_append_oldmatchequal))) -> (((exists fs_h_jt_append_oldmatchequalright. fs_h_jt_append_oldmatchequalright + S (jt_right_append_oldmatchequal) = S ((S (jt_index_append_oldmatchequal)) * jt_e_append_oldmatch)) /\ exists fs_q_jt_append_oldmatchequalright. jt_d_append_oldmatch = fs_q_jt_append_oldmatchequalright * S ((S (jt_index_append_oldmatchequal)) * jt_e_append_oldmatch) + (jt_right_append_oldmatchequal))) -> jt_left_append_oldmatchequal=jt_right_append_oldmatchequal)))))) -> (exists jt_gap_append_bound. jt_gap_append_bound+S (j)=(v)) -> (forall jt_b_append_match jt_c_append_match jt_d_append_match jt_e_append_match. (((((exists fs_h_jt_append_matchleftcode. fs_h_jt_append_matchleftcode + S (jt_b_append_match) = S ((S (q)) * B)) /\ exists fs_q_jt_append_matchleftcode. A = fs_q_jt_append_matchleftcode * S ((S (q)) * B) + (jt_b_append_match))) /\ (((exists fs_h_jt_append_matchleftscale. fs_h_jt_append_matchleftscale + S (jt_c_append_match) = S ((S (q)) * D)) /\ exists fs_q_jt_append_matchleftscale. C = fs_q_jt_append_matchleftscale * S ((S (q)) * D) + (jt_c_append_match))))) -> (((((exists fs_h_jt_append_matchrightcode. fs_h_jt_append_matchrightcode + S (jt_d_append_match) = S ((S (j)) * F)) /\ exists fs_q_jt_append_matchrightcode. E = fs_q_jt_append_matchrightcode * S ((S (j)) * F) + (jt_d_append_match))) /\ (((exists fs_h_jt_append_matchrightscale. fs_h_jt_append_matchrightscale + S (jt_e_append_match) = S ((S (j)) * H)) /\ exists fs_q_jt_append_matchrightscale. G = fs_q_jt_append_matchrightscale * S ((S (j)) * H) + (jt_e_append_match))))) -> (forall jt_index_append_matchequal jt_left_append_matchequal jt_right_append_matchequal. (exists jt_gap_append_matchequalindex. jt_gap_append_matchequalindex+S (jt_index_append_matchequal)=(k)) -> (((exists fs_h_jt_append_matchequalleft. fs_h_jt_append_matchequalleft + S (jt_left_append_matchequal) = S ((S (jt_index_append_matchequal)) * jt_c_append_match)) /\ exists fs_q_jt_append_matchequalleft. jt_b_append_match = fs_q_jt_append_matchequalleft * S ((S (jt_index_append_matchequal)) * jt_c_append_match) + (jt_left_append_matchequal))) -> (((exists fs_h_jt_append_matchequalright. fs_h_jt_append_matchequalright + S (jt_right_append_matchequal) = S ((S (jt_index_append_matchequal)) * jt_e_append_match)) /\ exists fs_q_jt_append_matchequalright. jt_d_append_match = fs_q_jt_append_matchequalright * S ((S (jt_index_append_matchequal)) * jt_e_append_match) + (jt_right_append_matchequal))) -> jt_left_append_matchequal=jt_right_append_matchequal)) -> (exists P Q. forall jt_index_append_result. (exists jt_gap_append_resultindex. jt_gap_append_resultindex+S (jt_index_append_result)=(S q)) -> exists jt_image_append_result. ((((exists fs_h_jt_append_resultat. fs_h_jt_append_resultat + S (jt_image_append_result) = S ((S (jt_index_append_result)) * Q)) /\ exists fs_q_jt_append_resultat. P = fs_q_jt_append_resultat * S ((S (jt_index_append_result)) * Q) + (jt_image_append_result))) /\ (((exists jt_gap_append_resultbound. jt_gap_append_resultbound+S (jt_image_append_result)=(v)) /\ (forall jt_b_append_resultmatch jt_c_append_resultmatch jt_d_append_resultmatch jt_e_append_resultmatch. (((((exists fs_h_jt_append_resultmatchleftcode. fs_h_jt_append_resultmatchleftcode + S (jt_b_append_resultmatch) = S ((S (jt_index_append_result)) * B)) /\ exists fs_q_jt_append_resultmatchleftcode. A = fs_q_jt_append_resultmatchleftcode * S ((S (jt_index_append_result)) * B) + (jt_b_append_resultmatch))) /\ (((exists fs_h_jt_append_resultmatchleftscale. fs_h_jt_append_resultmatchleftscale + S (jt_c_append_resultmatch) = S ((S (jt_index_append_result)) * D)) /\ exists fs_q_jt_append_resultmatchleftscale. C = fs_q_jt_append_resultmatchleftscale * S ((S (jt_index_append_result)) * D) + (jt_c_append_resultmatch))))) -> (((((exists fs_h_jt_append_resultmatchrightcode. fs_h_jt_append_resultmatchrightcode + S (jt_d_append_resultmatch) = S ((S (jt_image_append_result)) * F)) /\ exists fs_q_jt_append_resultmatchrightcode. E = fs_q_jt_append_resultmatchrightcode * S ((S (jt_image_append_result)) * F) + (jt_d_append_resultmatch))) /\ (((exists fs_h_jt_append_resultmatchrightscale. fs_h_jt_append_resultmatchrightscale + S (jt_e_append_resultmatch) = S ((S (jt_image_append_result)) * H)) /\ exists fs_q_jt_append_resultmatchrightscale. G = fs_q_jt_append_resultmatchrightscale * S ((S (jt_image_append_result)) * H) + (jt_e_append_resultmatch))))) -> (forall jt_index_append_resultmatchequal jt_left_append_resultmatchequal jt_right_append_resultmatchequal. (exists jt_gap_append_resultmatchequalindex. jt_gap_append_resultmatchequalindex+S (jt_index_append_resultmatchequal)=(k)) -> (((exists fs_h_jt_append_resultmatchequalleft. fs_h_jt_append_resultmatchequalleft + S (jt_left_append_resultmatchequal) = S ((S (jt_index_append_resultmatchequal)) * jt_c_append_resultmatch)) /\ exists fs_q_jt_append_resultmatchequalleft. jt_b_append_resultmatch = fs_q_jt_append_resultmatchequalleft * S ((S (jt_index_append_resultmatchequal)) * jt_c_append_resultmatch) + (jt_left_append_resultmatchequal))) -> (((exists fs_h_jt_append_resultmatchequalright. fs_h_jt_append_resultmatchequalright + S (jt_right_append_resultmatchequal) = S ((S (jt_index_append_resultmatchequal)) * jt_e_append_resultmatch)) /\ exists fs_q_jt_append_resultmatchequalright. jt_d_append_resultmatch = fs_q_jt_append_resultmatchequalright * S ((S (jt_index_append_resultmatchequal)) * jt_e_append_resultmatch) + (jt_right_append_resultmatchequal))) -> jt_left_append_resultmatchequal=jt_right_append_resultmatchequal))))))

Constructive proof overview

Generated structural guide

Append one genuine matched target index and preserve all previous mapped positions by beta extension.

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

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

Proof neighborhood

Direct dependencies

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

Direct dependents

JT0050 jordan_enumeration_index_map_exists

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

65 script commands · 23 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro k
  2. L2
    intro A
  3. L3
    intro B
  4. L4
    intro C
  5. L5
    intro D
  6. L6
    intro E
  7. L7
    intro F
  8. L8
    intro G
  9. L9
    intro H
  10. L10
    intro Z
02Fix variables and assumptionsL11–17

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

  1. L11
    intro W
  2. L12
    intro q
  3. L13
    intro v
  4. L14
    intro j
  5. L15
    intro hm
  6. L16
    intro hj
  7. L17
    intro hmatch
03Establish hextL18–23

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

  1. L18
    have hext : ∃ P. ∃ Q. BetaAt(P,Q,q,j) ∧ BetaPrefixEqual(Z,W,P,Q,q)Definitions: BetaPrefixEqualBetaAt
  2. L19
    specialize beta_prefix_extend (q)
  3. L20
    specialize beta_prefix_extend (Z)
  4. L21
    specialize beta_prefix_extend (W)
  5. L22
    specialize beta_prefix_extend (j)
  6. L23
    apply beta_prefix_extend
04Separate the logical casesL24–26

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

  1. L24
    cases hext
  2. L25
    cases hext_witness
  3. L26
    cases hext_witness_witness
05Construct an explicit witnessL27–28

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

  1. L27
    exists x
  2. L28
    exists x1
06Fix variables and assumptionsL29–30

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

  1. L29
    intro i
  2. L30
    intro hi
07Establish hcL31–35

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. L31
    have hc : i=q \/ (exists jt_gap_append_old_index. jt_gap_append_old_index+S (i)=(q))
  2. L32
    specialize finite_lt_succ_eq_or_lt (q)
  3. L33
    specialize finite_lt_succ_eq_or_lt (i)
  4. L34
    apply finite_lt_succ_eq_or_lt
  5. L35
    exact hi
08Separate the logical casesL36–36

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

  1. L36
    cases hc
09Construct an explicit witnessL37–37

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

  1. L37
    exists j
10Separate the logical casesL38–38

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

  1. L38
    split
11Calculate and transport equalitiesL39–40

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

  1. L39
    rewrite hc_left
  2. L40
    rewrite hc_left
12Use earlier factsL41–41

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

  1. L41
    exact hext_witness_witness_left
13Separate the logical casesL42–42

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

  1. L42
    split
14Use earlier factsL43–43

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

  1. L43
    exact hj
15Calculate and transport equalitiesL44–47

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

  1. L44
    rewrite hc_left
  2. L45
    rewrite hc_left
  3. L46
    rewrite hc_left
  4. L47
    rewrite hc_left
16Use earlier factsL48–48

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

  1. L48
    exact hmatch
17Establish hvL49–52

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

  1. L49
    have hv : ∃ r. BetaAt(Z,W,i,r) ∧ (Lt(r,v) ∧ (∀ x. ∀ y. ∀ z. ∀ n. BetaAt(A,B,i,x) ∧ BetaAt(C,D,i,y) → BetaAt(E,F,r,z) ∧ BetaAt(G,H,r,n) → IntegerVectorZero(x,y,z,n,k)))Definitions: IntegerVectorZeroLtBetaAt
  2. L50
    specialize hm (i)
  3. L51
    apply hm
  4. L52
    exact hc_right
18Separate the logical casesL53–55

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

  1. L53
    cases hv
  2. L54
    cases hv_witness
  3. L55
    cases hv_witness_right
19Construct an explicit witnessL56–56

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

  1. L56
    exists x2
20Separate the logical casesL57–57

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

  1. L57
    split
21Use earlier factsL58–62

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

  1. L58
    specialize hext_witness_witness_right (i)
  2. L59
    specialize hext_witness_witness_right (x2)
  3. L60
    apply hext_witness_witness_right
  4. L61
    exact hc_right
  5. L62
    exact hv_witness_left
22Separate the logical casesL63–63

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

  1. L63
    split
23Use earlier factsL64–65

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

  1. L64
    exact hv_witness_right_left
  2. L65
    exact hv_witness_right_right

Library-wide reading audit

Original exact command ledger · 65 lines
  1. 0001intro k
  2. 0002intro A
  3. 0003intro B
  4. 0004intro C
  5. 0005intro D
  6. 0006intro E
  7. 0007intro F
  8. 0008intro G
  9. 0009intro H
  10. 0010intro Z
  11. 0011intro W
  12. 0012intro q
  13. 0013intro v
  14. 0014intro j
  15. 0015intro hm
  16. 0016intro hj
  17. 0017intro hmatch
  18. 0018have hext : exists P Q. ((((exists fs_h_jt_append_image. fs_h_jt_append_image + S (j) = S ((S (q)) * Q)) /\ exists fs_q_jt_append_image. P = fs_q_jt_append_image * S ((S (q)) * Q) + (j))) /\ (forall jt_index_append_preserves jt_value_append_preserves. (exists jt_gap_append_preservesindex. jt_gap_append_preservesindex+S (jt_index_append_preserves)=(q)) -> (((exists fs_h_jt_append_preservesold. fs_h_jt_append_preservesold + S (jt_value_append_preserves) = S ((S (jt_index_append_preserves)) * W)) /\ exists fs_q_jt_append_preservesold. Z = fs_q_jt_append_preservesold * S ((S (jt_index_append_preserves)) * W) + (jt_value_append_preserves))) -> (((exists fs_h_jt_append_preservesnew. fs_h_jt_append_preservesnew + S (jt_value_append_preserves) = S ((S (jt_index_append_preserves)) * Q)) /\ exists fs_q_jt_append_preservesnew. P = fs_q_jt_append_preservesnew * S ((S (jt_index_append_preserves)) * Q) + (jt_value_append_preserves)))))
  19. 0019specialize beta_prefix_extend (q)
  20. 0020specialize beta_prefix_extend (Z)
  21. 0021specialize beta_prefix_extend (W)
  22. 0022specialize beta_prefix_extend (j)
  23. 0023apply beta_prefix_extend
  24. 0024cases hext
  25. 0025cases hext_witness
  26. 0026cases hext_witness_witness
  27. 0027exists x
  28. 0028exists x1
  29. 0029intro i
  30. 0030intro hi
  31. 0031have hc : i=q \/ (exists jt_gap_append_old_index. jt_gap_append_old_index+S (i)=(q))
  32. 0032specialize finite_lt_succ_eq_or_lt (q)
  33. 0033specialize finite_lt_succ_eq_or_lt (i)
  34. 0034apply finite_lt_succ_eq_or_lt
  35. 0035exact hi
  36. 0036cases hc
  37. 0037exists j
  38. 0038split
  39. 0039rewrite hc_left
  40. 0040rewrite hc_left
  41. 0041exact hext_witness_witness_left
  42. 0042split
  43. 0043exact hj
  44. 0044rewrite hc_left
  45. 0045rewrite hc_left
  46. 0046rewrite hc_left
  47. 0047rewrite hc_left
  48. 0048exact hmatch
  49. 0049have hv : exists r. ((((exists fs_h_jt_append_previousat. fs_h_jt_append_previousat + S (r) = S ((S (i)) * W)) /\ exists fs_q_jt_append_previousat. Z = fs_q_jt_append_previousat * S ((S (i)) * W) + (r))) /\ (((exists jt_gap_append_previousbound. jt_gap_append_previousbound+S (r)=(v)) /\ (forall jt_b_append_previousmatch jt_c_append_previousmatch jt_d_append_previousmatch jt_e_append_previousmatch. (((((exists fs_h_jt_append_previousmatchleftcode. fs_h_jt_append_previousmatchleftcode + S (jt_b_append_previousmatch) = S ((S (i)) * B)) /\ exists fs_q_jt_append_previousmatchleftcode. A = fs_q_jt_append_previousmatchleftcode * S ((S (i)) * B) + (jt_b_append_previousmatch))) /\ (((exists fs_h_jt_append_previousmatchleftscale. fs_h_jt_append_previousmatchleftscale + S (jt_c_append_previousmatch) = S ((S (i)) * D)) /\ exists fs_q_jt_append_previousmatchleftscale. C = fs_q_jt_append_previousmatchleftscale * S ((S (i)) * D) + (jt_c_append_previousmatch))))) -> (((((exists fs_h_jt_append_previousmatchrightcode. fs_h_jt_append_previousmatchrightcode + S (jt_d_append_previousmatch) = S ((S (r)) * F)) /\ exists fs_q_jt_append_previousmatchrightcode. E = fs_q_jt_append_previousmatchrightcode * S ((S (r)) * F) + (jt_d_append_previousmatch))) /\ (((exists fs_h_jt_append_previousmatchrightscale. fs_h_jt_append_previousmatchrightscale + S (jt_e_append_previousmatch) = S ((S (r)) * H)) /\ exists fs_q_jt_append_previousmatchrightscale. G = fs_q_jt_append_previousmatchrightscale * S ((S (r)) * H) + (jt_e_append_previousmatch))))) -> (forall jt_index_append_previousmatchequal jt_left_append_previousmatchequal jt_right_append_previousmatchequal. (exists jt_gap_append_previousmatchequalindex. jt_gap_append_previousmatchequalindex+S (jt_index_append_previousmatchequal)=(k)) -> (((exists fs_h_jt_append_previousmatchequalleft. fs_h_jt_append_previousmatchequalleft + S (jt_left_append_previousmatchequal) = S ((S (jt_index_append_previousmatchequal)) * jt_c_append_previousmatch)) /\ exists fs_q_jt_append_previousmatchequalleft. jt_b_append_previousmatch = fs_q_jt_append_previousmatchequalleft * S ((S (jt_index_append_previousmatchequal)) * jt_c_append_previousmatch) + (jt_left_append_previousmatchequal))) -> (((exists fs_h_jt_append_previousmatchequalright. fs_h_jt_append_previousmatchequalright + S (jt_right_append_previousmatchequal) = S ((S (jt_index_append_previousmatchequal)) * jt_e_append_previousmatch)) /\ exists fs_q_jt_append_previousmatchequalright. jt_d_append_previousmatch = fs_q_jt_append_previousmatchequalright * S ((S (jt_index_append_previousmatchequal)) * jt_e_append_previousmatch) + (jt_right_append_previousmatchequal))) -> jt_left_append_previousmatchequal=jt_right_append_previousmatchequal)))))
  50. 0050specialize hm (i)
  51. 0051apply hm
  52. 0052exact hc_right
  53. 0053cases hv
  54. 0054cases hv_witness
  55. 0055cases hv_witness_right
  56. 0056exists x2
  57. 0057split
  58. 0058specialize hext_witness_witness_right (i)
  59. 0059specialize hext_witness_witness_right (x2)
  60. 0060apply hext_witness_witness_right
  61. 0061exact hc_right
  62. 0062exact hv_witness_left
  63. 0063split
  64. 0064exact hv_witness_right_left
  65. 0065exact hv_witness_right_right