BT00TD

choose_out_of_range_zero

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

An out-of-range Choose value is zero.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall n k z. (exists bcf_lt_gap_bcloor_bound. bcf_lt_gap_bcloor_bound + S (n) = k) -> (((exists bcf_lt_gap_bcloor_choose_out_of_range. bcf_lt_gap_bcloor_choose_out_of_range + S (n) = k) /\ z = 0) \/ ((exists bcf_le_gap_bcloor_choose_in_range. bcf_le_gap_bcloor_choose_in_range + (k) = n) /\ (exists bcf_row_code_code_bcloor_choose bcf_row_code_scale_bcloor_choose bcf_row_scale_code_bcloor_choose bcf_row_scale_scale_bcloor_choose bcf_row_code_bcloor_choose bcf_row_scale_bcloor_choose. ((forall bcf_row_index_bcloor_choose_table. (exists bcf_lt_gap_bcloor_choose_table_row_bound. bcf_lt_gap_bcloor_choose_table_row_bound + S (bcf_row_index_bcloor_choose_table) = S (n)) -> exists bcf_row_code_bcloor_choose_table bcf_row_scale_bcloor_choose_table. ((((exists bcf_height_bcloor_choose_table_decoded_row_code. bcf_height_bcloor_choose_table_decoded_row_code + S (bcf_row_code_bcloor_choose_table) = S ((S (bcf_row_index_bcloor_choose_table)) * bcf_row_code_scale_bcloor_choose)) /\ exists bcf_quotient_bcloor_choose_table_decoded_row_code. bcf_row_code_code_bcloor_choose = bcf_quotient_bcloor_choose_table_decoded_row_code * S ((S (bcf_row_index_bcloor_choose_table)) * bcf_row_code_scale_bcloor_choose) + (bcf_row_code_bcloor_choose_table))) /\ ((((exists bcf_height_bcloor_choose_table_decoded_row_scale. bcf_height_bcloor_choose_table_decoded_row_scale + S (bcf_row_scale_bcloor_choose_table) = S ((S (bcf_row_index_bcloor_choose_table)) * bcf_row_scale_scale_bcloor_choose)) /\ exists bcf_quotient_bcloor_choose_table_decoded_row_scale. bcf_row_scale_code_bcloor_choose = bcf_quotient_bcloor_choose_table_decoded_row_scale * S ((S (bcf_row_index_bcloor_choose_table)) * bcf_row_scale_scale_bcloor_choose) + (bcf_row_scale_bcloor_choose_table))) /\ ((bcf_row_index_bcloor_choose_table = 0 /\ (forall bcf_index_bcloor_choose_table_zero_row. (exists bcf_lt_gap_bcloor_choose_table_zero_row_bound. bcf_lt_gap_bcloor_choose_table_zero_row_bound + S (bcf_index_bcloor_choose_table_zero_row) = S (n)) -> exists bcf_value_bcloor_choose_table_zero_row. ((((exists bcf_height_bcloor_choose_table_zero_row_entry. bcf_height_bcloor_choose_table_zero_row_entry + S (bcf_value_bcloor_choose_table_zero_row) = S ((S (bcf_index_bcloor_choose_table_zero_row)) * bcf_row_scale_bcloor_choose_table)) /\ exists bcf_quotient_bcloor_choose_table_zero_row_entry. bcf_row_code_bcloor_choose_table = bcf_quotient_bcloor_choose_table_zero_row_entry * S ((S (bcf_index_bcloor_choose_table_zero_row)) * bcf_row_scale_bcloor_choose_table) + (bcf_value_bcloor_choose_table_zero_row))) /\ ((bcf_index_bcloor_choose_table_zero_row = 0 /\ bcf_value_bcloor_choose_table_zero_row = 1) \/ exists bcf_predecessor_bcloor_choose_table_zero_row. bcf_index_bcloor_choose_table_zero_row = S bcf_predecessor_bcloor_choose_table_zero_row /\ bcf_value_bcloor_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_bcloor_choose_table bcf_previous_code_bcloor_choose_table bcf_previous_scale_bcloor_choose_table. bcf_row_index_bcloor_choose_table = S bcf_predecessor_bcloor_choose_table /\ ((((exists bcf_height_bcloor_choose_table_decoded_previous_code. bcf_height_bcloor_choose_table_decoded_previous_code + S (bcf_previous_code_bcloor_choose_table) = S ((S (bcf_predecessor_bcloor_choose_table)) * bcf_row_code_scale_bcloor_choose)) /\ exists bcf_quotient_bcloor_choose_table_decoded_previous_code. bcf_row_code_code_bcloor_choose = bcf_quotient_bcloor_choose_table_decoded_previous_code * S ((S (bcf_predecessor_bcloor_choose_table)) * bcf_row_code_scale_bcloor_choose) + (bcf_previous_code_bcloor_choose_table))) /\ ((((exists bcf_height_bcloor_choose_table_decoded_previous_scale. bcf_height_bcloor_choose_table_decoded_previous_scale + S (bcf_previous_scale_bcloor_choose_table) = S ((S (bcf_predecessor_bcloor_choose_table)) * bcf_row_scale_scale_bcloor_choose)) /\ exists bcf_quotient_bcloor_choose_table_decoded_previous_scale. bcf_row_scale_code_bcloor_choose = bcf_quotient_bcloor_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_bcloor_choose_table)) * bcf_row_scale_scale_bcloor_choose) + (bcf_previous_scale_bcloor_choose_table))) /\ (forall bcf_index_bcloor_choose_table_row_step. (exists bcf_lt_gap_bcloor_choose_table_row_step_bound. bcf_lt_gap_bcloor_choose_table_row_step_bound + S (bcf_index_bcloor_choose_table_row_step) = S (n)) -> exists bcf_value_bcloor_choose_table_row_step. ((((exists bcf_height_bcloor_choose_table_row_step_entry. bcf_height_bcloor_choose_table_row_step_entry + S (bcf_value_bcloor_choose_table_row_step) = S ((S (bcf_index_bcloor_choose_table_row_step)) * bcf_row_scale_bcloor_choose_table)) /\ exists bcf_quotient_bcloor_choose_table_row_step_entry. bcf_row_code_bcloor_choose_table = bcf_quotient_bcloor_choose_table_row_step_entry * S ((S (bcf_index_bcloor_choose_table_row_step)) * bcf_row_scale_bcloor_choose_table) + (bcf_value_bcloor_choose_table_row_step))) /\ ((bcf_index_bcloor_choose_table_row_step = 0 /\ bcf_value_bcloor_choose_table_row_step = 1) \/ exists bcf_predecessor_bcloor_choose_table_row_step bcf_left_bcloor_choose_table_row_step bcf_right_bcloor_choose_table_row_step. bcf_index_bcloor_choose_table_row_step = S bcf_predecessor_bcloor_choose_table_row_step /\ ((((exists bcf_height_bcloor_choose_table_row_step_previous_left. bcf_height_bcloor_choose_table_row_step_previous_left + S (bcf_left_bcloor_choose_table_row_step) = S ((S (bcf_predecessor_bcloor_choose_table_row_step)) * bcf_previous_scale_bcloor_choose_table)) /\ exists bcf_quotient_bcloor_choose_table_row_step_previous_left. bcf_previous_code_bcloor_choose_table = bcf_quotient_bcloor_choose_table_row_step_previous_left * S ((S (bcf_predecessor_bcloor_choose_table_row_step)) * bcf_previous_scale_bcloor_choose_table) + (bcf_left_bcloor_choose_table_row_step))) /\ ((((exists bcf_height_bcloor_choose_table_row_step_previous_right. bcf_height_bcloor_choose_table_row_step_previous_right + S (bcf_right_bcloor_choose_table_row_step) = S ((S (S (bcf_predecessor_bcloor_choose_table_row_step))) * bcf_previous_scale_bcloor_choose_table)) /\ exists bcf_quotient_bcloor_choose_table_row_step_previous_right. bcf_previous_code_bcloor_choose_table = bcf_quotient_bcloor_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcloor_choose_table_row_step))) * bcf_previous_scale_bcloor_choose_table) + (bcf_right_bcloor_choose_table_row_step))) /\ bcf_value_bcloor_choose_table_row_step = bcf_left_bcloor_choose_table_row_step + bcf_right_bcloor_choose_table_row_step))))))))))) /\ ((((exists bcf_height_bcloor_choose_decoded_row_code. bcf_height_bcloor_choose_decoded_row_code + S (bcf_row_code_bcloor_choose) = S ((S (n)) * bcf_row_code_scale_bcloor_choose)) /\ exists bcf_quotient_bcloor_choose_decoded_row_code. bcf_row_code_code_bcloor_choose = bcf_quotient_bcloor_choose_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcloor_choose) + (bcf_row_code_bcloor_choose))) /\ ((((exists bcf_height_bcloor_choose_decoded_row_scale. bcf_height_bcloor_choose_decoded_row_scale + S (bcf_row_scale_bcloor_choose) = S ((S (n)) * bcf_row_scale_scale_bcloor_choose)) /\ exists bcf_quotient_bcloor_choose_decoded_row_scale. bcf_row_scale_code_bcloor_choose = bcf_quotient_bcloor_choose_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcloor_choose) + (bcf_row_scale_bcloor_choose))) /\ (((exists bcf_height_bcloor_choose_decoded_value. bcf_height_bcloor_choose_decoded_value + S (z) = S ((S (k)) * bcf_row_scale_bcloor_choose)) /\ exists bcf_quotient_bcloor_choose_decoded_value. bcf_row_code_bcloor_choose = bcf_quotient_bcloor_choose_decoded_value * S ((S (k)) * bcf_row_scale_bcloor_choose) + (z))))))))) -> z = 0

Structural proof guide

An out-of-range Choose value is zero.

Direct prerequisites: lt_not_le. The authored body proceeds by case analysis (3).

Proof neighborhood

Direct dependencies

BT001I lt_not_le

Direct dependents

BT00TJ choose_succ_succ

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

15 script commands · 5 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.

Named ingredients (1)
lt not le
01Fix variables and assumptionsL1–5

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

  1. L1
    intro n
  2. L2
    intro k
  3. L3
    intro z
  4. L4
    intro hbound
  5. L5
    intro hchoose
02Separate the logical casesL6–7

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

  1. L6
    cases hchoose
  2. L7
    cases hchoose_left
03Use earlier factsL8–8

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

  1. L8
    exact hchoose_left_right
04Separate the logical casesL9–10

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

  1. L9
    cases hchoose_right
  2. L10
    exfalso
05Use earlier factsL11–15

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

  1. L11
    specialize lt_not_le n
  2. L12
    specialize lt_not_le k
  3. L13
    apply lt_not_le
  4. L14
    exact hbound
  5. L15
    exact hchoose_right_left

Library-wide reading audit

Original exact command ledger · 15 lines
  1. 0001intro n
  2. 0002intro k
  3. 0003intro z
  4. 0004intro hbound
  5. 0005intro hchoose
  6. 0006cases hchoose
  7. 0007cases hchoose_left
  8. 0008exact hchoose_left_right
  9. 0009cases hchoose_right
  10. 0010exfalso
  11. 0011specialize lt_not_le n
  12. 0012specialize lt_not_le k
  13. 0013apply lt_not_le
  14. 0014exact hbound
  15. 0015exact hchoose_right_left