JT0051

jordan_enumeration_index_map_entry

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

Every actual decoded map value is bounded and matches the represented source tuple.

Exact expanded first-order arithmetic statement

forall k A B C D E F G H Z W q v i j. (forall jt_index_actual_given_map. (exists jt_gap_actual_given_mapindex. jt_gap_actual_given_mapindex+S (jt_index_actual_given_map)=(q)) -> exists jt_image_actual_given_map. ((((exists fs_h_jt_actual_given_mapat. fs_h_jt_actual_given_mapat + S (jt_image_actual_given_map) = S ((S (jt_index_actual_given_map)) * W)) /\ exists fs_q_jt_actual_given_mapat. Z = fs_q_jt_actual_given_mapat * S ((S (jt_index_actual_given_map)) * W) + (jt_image_actual_given_map))) /\ (((exists jt_gap_actual_given_mapbound. jt_gap_actual_given_mapbound+S (jt_image_actual_given_map)=(v)) /\ (forall jt_b_actual_given_mapmatch jt_c_actual_given_mapmatch jt_d_actual_given_mapmatch jt_e_actual_given_mapmatch. (((((exists fs_h_jt_actual_given_mapmatchleftcode. fs_h_jt_actual_given_mapmatchleftcode + S (jt_b_actual_given_mapmatch) = S ((S (jt_index_actual_given_map)) * B)) /\ exists fs_q_jt_actual_given_mapmatchleftcode. A = fs_q_jt_actual_given_mapmatchleftcode * S ((S (jt_index_actual_given_map)) * B) + (jt_b_actual_given_mapmatch))) /\ (((exists fs_h_jt_actual_given_mapmatchleftscale. fs_h_jt_actual_given_mapmatchleftscale + S (jt_c_actual_given_mapmatch) = S ((S (jt_index_actual_given_map)) * D)) /\ exists fs_q_jt_actual_given_mapmatchleftscale. C = fs_q_jt_actual_given_mapmatchleftscale * S ((S (jt_index_actual_given_map)) * D) + (jt_c_actual_given_mapmatch))))) -> (((((exists fs_h_jt_actual_given_mapmatchrightcode. fs_h_jt_actual_given_mapmatchrightcode + S (jt_d_actual_given_mapmatch) = S ((S (jt_image_actual_given_map)) * F)) /\ exists fs_q_jt_actual_given_mapmatchrightcode. E = fs_q_jt_actual_given_mapmatchrightcode * S ((S (jt_image_actual_given_map)) * F) + (jt_d_actual_given_mapmatch))) /\ (((exists fs_h_jt_actual_given_mapmatchrightscale. fs_h_jt_actual_given_mapmatchrightscale + S (jt_e_actual_given_mapmatch) = S ((S (jt_image_actual_given_map)) * H)) /\ exists fs_q_jt_actual_given_mapmatchrightscale. G = fs_q_jt_actual_given_mapmatchrightscale * S ((S (jt_image_actual_given_map)) * H) + (jt_e_actual_given_mapmatch))))) -> (forall jt_index_actual_given_mapmatchequal jt_left_actual_given_mapmatchequal jt_right_actual_given_mapmatchequal. (exists jt_gap_actual_given_mapmatchequalindex. jt_gap_actual_given_mapmatchequalindex+S (jt_index_actual_given_mapmatchequal)=(k)) -> (((exists fs_h_jt_actual_given_mapmatchequalleft. fs_h_jt_actual_given_mapmatchequalleft + S (jt_left_actual_given_mapmatchequal) = S ((S (jt_index_actual_given_mapmatchequal)) * jt_c_actual_given_mapmatch)) /\ exists fs_q_jt_actual_given_mapmatchequalleft. jt_b_actual_given_mapmatch = fs_q_jt_actual_given_mapmatchequalleft * S ((S (jt_index_actual_given_mapmatchequal)) * jt_c_actual_given_mapmatch) + (jt_left_actual_given_mapmatchequal))) -> (((exists fs_h_jt_actual_given_mapmatchequalright. fs_h_jt_actual_given_mapmatchequalright + S (jt_right_actual_given_mapmatchequal) = S ((S (jt_index_actual_given_mapmatchequal)) * jt_e_actual_given_mapmatch)) /\ exists fs_q_jt_actual_given_mapmatchequalright. jt_d_actual_given_mapmatch = fs_q_jt_actual_given_mapmatchequalright * S ((S (jt_index_actual_given_mapmatchequal)) * jt_e_actual_given_mapmatch) + (jt_right_actual_given_mapmatchequal))) -> jt_left_actual_given_mapmatchequal=jt_right_actual_given_mapmatchequal)))))) -> (exists jt_gap_actual_index. jt_gap_actual_index+S (i)=(q)) -> (((exists fs_h_jt_actual_value. fs_h_jt_actual_value + S (j) = S ((S (i)) * W)) /\ exists fs_q_jt_actual_value. Z = fs_q_jt_actual_value * S ((S (i)) * W) + (j))) -> (((exists jt_gap_actual_result_bound. jt_gap_actual_result_bound+S (j)=(v)) /\ (forall jt_b_actual_result_match jt_c_actual_result_match jt_d_actual_result_match jt_e_actual_result_match. (((((exists fs_h_jt_actual_result_matchleftcode. fs_h_jt_actual_result_matchleftcode + S (jt_b_actual_result_match) = S ((S (i)) * B)) /\ exists fs_q_jt_actual_result_matchleftcode. A = fs_q_jt_actual_result_matchleftcode * S ((S (i)) * B) + (jt_b_actual_result_match))) /\ (((exists fs_h_jt_actual_result_matchleftscale. fs_h_jt_actual_result_matchleftscale + S (jt_c_actual_result_match) = S ((S (i)) * D)) /\ exists fs_q_jt_actual_result_matchleftscale. C = fs_q_jt_actual_result_matchleftscale * S ((S (i)) * D) + (jt_c_actual_result_match))))) -> (((((exists fs_h_jt_actual_result_matchrightcode. fs_h_jt_actual_result_matchrightcode + S (jt_d_actual_result_match) = S ((S (j)) * F)) /\ exists fs_q_jt_actual_result_matchrightcode. E = fs_q_jt_actual_result_matchrightcode * S ((S (j)) * F) + (jt_d_actual_result_match))) /\ (((exists fs_h_jt_actual_result_matchrightscale. fs_h_jt_actual_result_matchrightscale + S (jt_e_actual_result_match) = S ((S (j)) * H)) /\ exists fs_q_jt_actual_result_matchrightscale. G = fs_q_jt_actual_result_matchrightscale * S ((S (j)) * H) + (jt_e_actual_result_match))))) -> (forall jt_index_actual_result_matchequal jt_left_actual_result_matchequal jt_right_actual_result_matchequal. (exists jt_gap_actual_result_matchequalindex. jt_gap_actual_result_matchequalindex+S (jt_index_actual_result_matchequal)=(k)) -> (((exists fs_h_jt_actual_result_matchequalleft. fs_h_jt_actual_result_matchequalleft + S (jt_left_actual_result_matchequal) = S ((S (jt_index_actual_result_matchequal)) * jt_c_actual_result_match)) /\ exists fs_q_jt_actual_result_matchequalleft. jt_b_actual_result_match = fs_q_jt_actual_result_matchequalleft * S ((S (jt_index_actual_result_matchequal)) * jt_c_actual_result_match) + (jt_left_actual_result_matchequal))) -> (((exists fs_h_jt_actual_result_matchequalright. fs_h_jt_actual_result_matchequalright + S (jt_right_actual_result_matchequal) = S ((S (jt_index_actual_result_matchequal)) * jt_e_actual_result_match)) /\ exists fs_q_jt_actual_result_matchequalright. jt_d_actual_result_match = fs_q_jt_actual_result_matchequalright * S ((S (jt_index_actual_result_matchequal)) * jt_e_actual_result_match) + (jt_right_actual_result_matchequal))) -> jt_left_actual_result_matchequal=jt_right_actual_result_matchequal))))

Constructive proof overview

Generated structural guide

Every actual decoded map value is bounded and matches the represented source tuple.

The unchanged tactic script uses 1 declared prerequisite and contains 42 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_unique Alpha theorem; checked-use authorized

Direct dependents

JT0052 jordan_enumeration_index_map_bounded_injective

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

42 script commands · 10 reading checkpoints · 2 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–18

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 i
  5. L15
    intro j
  6. L16
    intro hm
  7. L17
    intro hi
  8. L18
    intro hat
03Establish hvL19–22

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

  1. L19
    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. L20
    specialize hm (i)
  3. L21
    apply hm
  4. L22
    exact hi
04Separate the logical casesL23–25

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

  1. L23
    cases hv
  2. L24
    cases hv_witness
  3. L25
    cases hv_witness_right
05Establish heL26–34

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

  1. L26
    have he : x=j
  2. L27
    specialize beta_at_unique (Z)
  3. L28
    specialize beta_at_unique (W)
  4. L29
    specialize beta_at_unique (i)
  5. L30
    specialize beta_at_unique (x)
  6. L31
    specialize beta_at_unique (j)
  7. L32
    apply beta_at_unique
  8. L33
    exact hv_witness_left
  9. L34
    exact hat
06Separate the logical casesL35–35

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

  1. L35
    split
07Calculate and transport equalitiesL36–36

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

  1. L36
    rewrite he at hv_witness_right_left
08Use earlier factsL37–37

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

  1. L37
    exact hv_witness_right_left
09Calculate and transport equalitiesL38–41

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

  1. L38
    rewrite he at hv_witness_right_right
  2. L39
    rewrite he at hv_witness_right_right
  3. L40
    rewrite he at hv_witness_right_right
  4. L41
    rewrite he at hv_witness_right_right
10Use earlier factsL42–42

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

  1. L42
    exact hv_witness_right_right

Library-wide reading audit

Original exact command ledger · 42 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 i
  15. 0015intro j
  16. 0016intro hm
  17. 0017intro hi
  18. 0018intro hat
  19. 0019have hv : exists r. ((((exists fs_h_jt_actual_mapat. fs_h_jt_actual_mapat + S (r) = S ((S (i)) * W)) /\ exists fs_q_jt_actual_mapat. Z = fs_q_jt_actual_mapat * S ((S (i)) * W) + (r))) /\ (((exists jt_gap_actual_mapbound. jt_gap_actual_mapbound+S (r)=(v)) /\ (forall jt_b_actual_mapmatch jt_c_actual_mapmatch jt_d_actual_mapmatch jt_e_actual_mapmatch. (((((exists fs_h_jt_actual_mapmatchleftcode. fs_h_jt_actual_mapmatchleftcode + S (jt_b_actual_mapmatch) = S ((S (i)) * B)) /\ exists fs_q_jt_actual_mapmatchleftcode. A = fs_q_jt_actual_mapmatchleftcode * S ((S (i)) * B) + (jt_b_actual_mapmatch))) /\ (((exists fs_h_jt_actual_mapmatchleftscale. fs_h_jt_actual_mapmatchleftscale + S (jt_c_actual_mapmatch) = S ((S (i)) * D)) /\ exists fs_q_jt_actual_mapmatchleftscale. C = fs_q_jt_actual_mapmatchleftscale * S ((S (i)) * D) + (jt_c_actual_mapmatch))))) -> (((((exists fs_h_jt_actual_mapmatchrightcode. fs_h_jt_actual_mapmatchrightcode + S (jt_d_actual_mapmatch) = S ((S (r)) * F)) /\ exists fs_q_jt_actual_mapmatchrightcode. E = fs_q_jt_actual_mapmatchrightcode * S ((S (r)) * F) + (jt_d_actual_mapmatch))) /\ (((exists fs_h_jt_actual_mapmatchrightscale. fs_h_jt_actual_mapmatchrightscale + S (jt_e_actual_mapmatch) = S ((S (r)) * H)) /\ exists fs_q_jt_actual_mapmatchrightscale. G = fs_q_jt_actual_mapmatchrightscale * S ((S (r)) * H) + (jt_e_actual_mapmatch))))) -> (forall jt_index_actual_mapmatchequal jt_left_actual_mapmatchequal jt_right_actual_mapmatchequal. (exists jt_gap_actual_mapmatchequalindex. jt_gap_actual_mapmatchequalindex+S (jt_index_actual_mapmatchequal)=(k)) -> (((exists fs_h_jt_actual_mapmatchequalleft. fs_h_jt_actual_mapmatchequalleft + S (jt_left_actual_mapmatchequal) = S ((S (jt_index_actual_mapmatchequal)) * jt_c_actual_mapmatch)) /\ exists fs_q_jt_actual_mapmatchequalleft. jt_b_actual_mapmatch = fs_q_jt_actual_mapmatchequalleft * S ((S (jt_index_actual_mapmatchequal)) * jt_c_actual_mapmatch) + (jt_left_actual_mapmatchequal))) -> (((exists fs_h_jt_actual_mapmatchequalright. fs_h_jt_actual_mapmatchequalright + S (jt_right_actual_mapmatchequal) = S ((S (jt_index_actual_mapmatchequal)) * jt_e_actual_mapmatch)) /\ exists fs_q_jt_actual_mapmatchequalright. jt_d_actual_mapmatch = fs_q_jt_actual_mapmatchequalright * S ((S (jt_index_actual_mapmatchequal)) * jt_e_actual_mapmatch) + (jt_right_actual_mapmatchequal))) -> jt_left_actual_mapmatchequal=jt_right_actual_mapmatchequal)))))
  20. 0020specialize hm (i)
  21. 0021apply hm
  22. 0022exact hi
  23. 0023cases hv
  24. 0024cases hv_witness
  25. 0025cases hv_witness_right
  26. 0026have he : x=j
  27. 0027specialize beta_at_unique (Z)
  28. 0028specialize beta_at_unique (W)
  29. 0029specialize beta_at_unique (i)
  30. 0030specialize beta_at_unique (x)
  31. 0031specialize beta_at_unique (j)
  32. 0032apply beta_at_unique
  33. 0033exact hv_witness_left
  34. 0034exact hat
  35. 0035split
  36. 0036rewrite he at hv_witness_right_left
  37. 0037exact hv_witness_right_left
  38. 0038rewrite he at hv_witness_right_right
  39. 0039rewrite he at hv_witness_right_right
  40. 0040rewrite he at hv_witness_right_right
  41. 0041rewrite he at hv_witness_right_right
  42. 0042exact hv_witness_right_right