JT004E

jordan_enumeration_index_map_empty

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

The zero-length index map is vacuous, independently of target length.

Exact expanded first-order arithmetic statement

forall k A B C D E F G H Z W v. (forall jt_index_empty_map. (exists jt_gap_empty_mapindex. jt_gap_empty_mapindex+S (jt_index_empty_map)=(0)) -> exists jt_image_empty_map. ((((exists fs_h_jt_empty_mapat. fs_h_jt_empty_mapat + S (jt_image_empty_map) = S ((S (jt_index_empty_map)) * W)) /\ exists fs_q_jt_empty_mapat. Z = fs_q_jt_empty_mapat * S ((S (jt_index_empty_map)) * W) + (jt_image_empty_map))) /\ (((exists jt_gap_empty_mapbound. jt_gap_empty_mapbound+S (jt_image_empty_map)=(v)) /\ (forall jt_b_empty_mapmatch jt_c_empty_mapmatch jt_d_empty_mapmatch jt_e_empty_mapmatch. (((((exists fs_h_jt_empty_mapmatchleftcode. fs_h_jt_empty_mapmatchleftcode + S (jt_b_empty_mapmatch) = S ((S (jt_index_empty_map)) * B)) /\ exists fs_q_jt_empty_mapmatchleftcode. A = fs_q_jt_empty_mapmatchleftcode * S ((S (jt_index_empty_map)) * B) + (jt_b_empty_mapmatch))) /\ (((exists fs_h_jt_empty_mapmatchleftscale. fs_h_jt_empty_mapmatchleftscale + S (jt_c_empty_mapmatch) = S ((S (jt_index_empty_map)) * D)) /\ exists fs_q_jt_empty_mapmatchleftscale. C = fs_q_jt_empty_mapmatchleftscale * S ((S (jt_index_empty_map)) * D) + (jt_c_empty_mapmatch))))) -> (((((exists fs_h_jt_empty_mapmatchrightcode. fs_h_jt_empty_mapmatchrightcode + S (jt_d_empty_mapmatch) = S ((S (jt_image_empty_map)) * F)) /\ exists fs_q_jt_empty_mapmatchrightcode. E = fs_q_jt_empty_mapmatchrightcode * S ((S (jt_image_empty_map)) * F) + (jt_d_empty_mapmatch))) /\ (((exists fs_h_jt_empty_mapmatchrightscale. fs_h_jt_empty_mapmatchrightscale + S (jt_e_empty_mapmatch) = S ((S (jt_image_empty_map)) * H)) /\ exists fs_q_jt_empty_mapmatchrightscale. G = fs_q_jt_empty_mapmatchrightscale * S ((S (jt_image_empty_map)) * H) + (jt_e_empty_mapmatch))))) -> (forall jt_index_empty_mapmatchequal jt_left_empty_mapmatchequal jt_right_empty_mapmatchequal. (exists jt_gap_empty_mapmatchequalindex. jt_gap_empty_mapmatchequalindex+S (jt_index_empty_mapmatchequal)=(k)) -> (((exists fs_h_jt_empty_mapmatchequalleft. fs_h_jt_empty_mapmatchequalleft + S (jt_left_empty_mapmatchequal) = S ((S (jt_index_empty_mapmatchequal)) * jt_c_empty_mapmatch)) /\ exists fs_q_jt_empty_mapmatchequalleft. jt_b_empty_mapmatch = fs_q_jt_empty_mapmatchequalleft * S ((S (jt_index_empty_mapmatchequal)) * jt_c_empty_mapmatch) + (jt_left_empty_mapmatchequal))) -> (((exists fs_h_jt_empty_mapmatchequalright. fs_h_jt_empty_mapmatchequalright + S (jt_right_empty_mapmatchequal) = S ((S (jt_index_empty_mapmatchequal)) * jt_e_empty_mapmatch)) /\ exists fs_q_jt_empty_mapmatchequalright. jt_d_empty_mapmatch = fs_q_jt_empty_mapmatchequalright * S ((S (jt_index_empty_mapmatchequal)) * jt_e_empty_mapmatch) + (jt_right_empty_mapmatchequal))) -> jt_left_empty_mapmatchequal=jt_right_empty_mapmatchequal))))))

Constructive proof overview

Generated structural guide

The zero-length index map is vacuous, independently of target length.

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

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

Proof neighborhood

Direct dependencies

lt_not_le Alpha theorem; checked-use authorized zero_le 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

21 script commands · 4 reading checkpoints · 0 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 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–14

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

  1. L11
    intro W
  2. L12
    intro v
  3. L13
    intro i
  4. L14
    intro hi
03Separate the logical casesL15–15

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

  1. L15
    exfalso
04Use earlier factsL16–21

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

  1. L16
    specialize lt_not_le (i)
  2. L17
    specialize lt_not_le (0)
  3. L18
    apply lt_not_le
  4. L19
    exact hi
  5. L20
    specialize zero_le (i)
  6. L21
    apply zero_le

Library-wide reading audit

Original exact command ledger · 21 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 v
  13. 0013intro i
  14. 0014intro hi
  15. 0015exfalso
  16. 0016specialize lt_not_le (i)
  17. 0017specialize lt_not_le (0)
  18. 0018apply lt_not_le
  19. 0019exact hi
  20. 0020specialize zero_le (i)
  21. 0021apply zero_le