LU000K

lucas_positive_lower_quotient_digit_coefficient_zero

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

A binomial row consisting of one upper digit vanishes at every index with positive lower base quotient.

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 first-order arithmetic statement

forall p r d e C. (exists lbd_gap_digit_zero_bound. lbd_gap_digit_zero_bound + S (d) = (p)) -> ~(r = 0) -> (((exists bcf_lt_gap_lucas_block_digit_digit_zero_choose_out_of_range. bcf_lt_gap_lucas_block_digit_digit_zero_choose_out_of_range + S (d) = p * r + e) /\ C = 0) \/ ((exists bcf_le_gap_lucas_block_digit_digit_zero_choose_in_range. bcf_le_gap_lucas_block_digit_digit_zero_choose_in_range + (p * r + e) = d) /\ (exists bcf_row_code_code_lucas_block_digit_digit_zero_choose bcf_row_code_scale_lucas_block_digit_digit_zero_choose bcf_row_scale_code_lucas_block_digit_digit_zero_choose bcf_row_scale_scale_lucas_block_digit_digit_zero_choose bcf_row_code_lucas_block_digit_digit_zero_choose bcf_row_scale_lucas_block_digit_digit_zero_choose. ((forall bcf_row_index_lucas_block_digit_digit_zero_choose_table. (exists bcf_lt_gap_lucas_block_digit_digit_zero_choose_table_row_bound. bcf_lt_gap_lucas_block_digit_digit_zero_choose_table_row_bound + S (bcf_row_index_lucas_block_digit_digit_zero_choose_table) = S (d)) -> exists bcf_row_code_lucas_block_digit_digit_zero_choose_table bcf_row_scale_lucas_block_digit_digit_zero_choose_table. ((((exists bcf_height_lucas_block_digit_digit_zero_choose_table_decoded_row_code. bcf_height_lucas_block_digit_digit_zero_choose_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_digit_zero_choose_table) = S ((S (bcf_row_index_lucas_block_digit_digit_zero_choose_table)) * bcf_row_code_scale_lucas_block_digit_digit_zero_choose)) /\ exists bcf_quotient_lucas_block_digit_digit_zero_choose_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_digit_zero_choose = bcf_quotient_lucas_block_digit_digit_zero_choose_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_digit_zero_choose_table)) * bcf_row_code_scale_lucas_block_digit_digit_zero_choose) + (bcf_row_code_lucas_block_digit_digit_zero_choose_table))) /\ ((((exists bcf_height_lucas_block_digit_digit_zero_choose_table_decoded_row_scale. bcf_height_lucas_block_digit_digit_zero_choose_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_digit_zero_choose_table) = S ((S (bcf_row_index_lucas_block_digit_digit_zero_choose_table)) * bcf_row_scale_scale_lucas_block_digit_digit_zero_choose)) /\ exists bcf_quotient_lucas_block_digit_digit_zero_choose_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_digit_zero_choose = bcf_quotient_lucas_block_digit_digit_zero_choose_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_digit_zero_choose_table)) * bcf_row_scale_scale_lucas_block_digit_digit_zero_choose) + (bcf_row_scale_lucas_block_digit_digit_zero_choose_table))) /\ ((bcf_row_index_lucas_block_digit_digit_zero_choose_table = 0 /\ (forall bcf_index_lucas_block_digit_digit_zero_choose_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_digit_zero_choose_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_digit_zero_choose_table_zero_row_bound + S (bcf_index_lucas_block_digit_digit_zero_choose_table_zero_row) = S (d)) -> exists bcf_value_lucas_block_digit_digit_zero_choose_table_zero_row. ((((exists bcf_height_lucas_block_digit_digit_zero_choose_table_zero_row_entry. bcf_height_lucas_block_digit_digit_zero_choose_table_zero_row_entry + S (bcf_value_lucas_block_digit_digit_zero_choose_table_zero_row) = S ((S (bcf_index_lucas_block_digit_digit_zero_choose_table_zero_row)) * bcf_row_scale_lucas_block_digit_digit_zero_choose_table)) /\ exists bcf_quotient_lucas_block_digit_digit_zero_choose_table_zero_row_entry. bcf_row_code_lucas_block_digit_digit_zero_choose_table = bcf_quotient_lucas_block_digit_digit_zero_choose_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_digit_zero_choose_table_zero_row)) * bcf_row_scale_lucas_block_digit_digit_zero_choose_table) + (bcf_value_lucas_block_digit_digit_zero_choose_table_zero_row))) /\ ((bcf_index_lucas_block_digit_digit_zero_choose_table_zero_row = 0 /\ bcf_value_lucas_block_digit_digit_zero_choose_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_digit_zero_choose_table_zero_row. bcf_index_lucas_block_digit_digit_zero_choose_table_zero_row = S bcf_predecessor_lucas_block_digit_digit_zero_choose_table_zero_row /\ bcf_value_lucas_block_digit_digit_zero_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_digit_zero_choose_table bcf_previous_code_lucas_block_digit_digit_zero_choose_table bcf_previous_scale_lucas_block_digit_digit_zero_choose_table. bcf_row_index_lucas_block_digit_digit_zero_choose_table = S bcf_predecessor_lucas_block_digit_digit_zero_choose_table /\ ((((exists bcf_height_lucas_block_digit_digit_zero_choose_table_decoded_previous_code. bcf_height_lucas_block_digit_digit_zero_choose_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_digit_zero_choose_table) = S ((S (bcf_predecessor_lucas_block_digit_digit_zero_choose_table)) * bcf_row_code_scale_lucas_block_digit_digit_zero_choose)) /\ exists bcf_quotient_lucas_block_digit_digit_zero_choose_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_digit_zero_choose = bcf_quotient_lucas_block_digit_digit_zero_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_digit_zero_choose_table)) * bcf_row_code_scale_lucas_block_digit_digit_zero_choose) + (bcf_previous_code_lucas_block_digit_digit_zero_choose_table))) /\ ((((exists bcf_height_lucas_block_digit_digit_zero_choose_table_decoded_previous_scale. bcf_height_lucas_block_digit_digit_zero_choose_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_digit_zero_choose_table) = S ((S (bcf_predecessor_lucas_block_digit_digit_zero_choose_table)) * bcf_row_scale_scale_lucas_block_digit_digit_zero_choose)) /\ exists bcf_quotient_lucas_block_digit_digit_zero_choose_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_digit_zero_choose = bcf_quotient_lucas_block_digit_digit_zero_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_digit_zero_choose_table)) * bcf_row_scale_scale_lucas_block_digit_digit_zero_choose) + (bcf_previous_scale_lucas_block_digit_digit_zero_choose_table))) /\ (forall bcf_index_lucas_block_digit_digit_zero_choose_table_row_step. (exists bcf_lt_gap_lucas_block_digit_digit_zero_choose_table_row_step_bound. bcf_lt_gap_lucas_block_digit_digit_zero_choose_table_row_step_bound + S (bcf_index_lucas_block_digit_digit_zero_choose_table_row_step) = S (d)) -> exists bcf_value_lucas_block_digit_digit_zero_choose_table_row_step. ((((exists bcf_height_lucas_block_digit_digit_zero_choose_table_row_step_entry. bcf_height_lucas_block_digit_digit_zero_choose_table_row_step_entry + S (bcf_value_lucas_block_digit_digit_zero_choose_table_row_step) = S ((S (bcf_index_lucas_block_digit_digit_zero_choose_table_row_step)) * bcf_row_scale_lucas_block_digit_digit_zero_choose_table)) /\ exists bcf_quotient_lucas_block_digit_digit_zero_choose_table_row_step_entry. bcf_row_code_lucas_block_digit_digit_zero_choose_table = bcf_quotient_lucas_block_digit_digit_zero_choose_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_digit_zero_choose_table_row_step)) * bcf_row_scale_lucas_block_digit_digit_zero_choose_table) + (bcf_value_lucas_block_digit_digit_zero_choose_table_row_step))) /\ ((bcf_index_lucas_block_digit_digit_zero_choose_table_row_step = 0 /\ bcf_value_lucas_block_digit_digit_zero_choose_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_digit_zero_choose_table_row_step bcf_left_lucas_block_digit_digit_zero_choose_table_row_step bcf_right_lucas_block_digit_digit_zero_choose_table_row_step. bcf_index_lucas_block_digit_digit_zero_choose_table_row_step = S bcf_predecessor_lucas_block_digit_digit_zero_choose_table_row_step /\ ((((exists bcf_height_lucas_block_digit_digit_zero_choose_table_row_step_previous_left. bcf_height_lucas_block_digit_digit_zero_choose_table_row_step_previous_left + S (bcf_left_lucas_block_digit_digit_zero_choose_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_digit_zero_choose_table_row_step)) * bcf_previous_scale_lucas_block_digit_digit_zero_choose_table)) /\ exists bcf_quotient_lucas_block_digit_digit_zero_choose_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_digit_zero_choose_table = bcf_quotient_lucas_block_digit_digit_zero_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_digit_zero_choose_table_row_step)) * bcf_previous_scale_lucas_block_digit_digit_zero_choose_table) + (bcf_left_lucas_block_digit_digit_zero_choose_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_digit_zero_choose_table_row_step_previous_right. bcf_height_lucas_block_digit_digit_zero_choose_table_row_step_previous_right + S (bcf_right_lucas_block_digit_digit_zero_choose_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_digit_zero_choose_table_row_step))) * bcf_previous_scale_lucas_block_digit_digit_zero_choose_table)) /\ exists bcf_quotient_lucas_block_digit_digit_zero_choose_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_digit_zero_choose_table = bcf_quotient_lucas_block_digit_digit_zero_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_digit_zero_choose_table_row_step))) * bcf_previous_scale_lucas_block_digit_digit_zero_choose_table) + (bcf_right_lucas_block_digit_digit_zero_choose_table_row_step))) /\ bcf_value_lucas_block_digit_digit_zero_choose_table_row_step = bcf_left_lucas_block_digit_digit_zero_choose_table_row_step + bcf_right_lucas_block_digit_digit_zero_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_digit_zero_choose_decoded_row_code. bcf_height_lucas_block_digit_digit_zero_choose_decoded_row_code + S (bcf_row_code_lucas_block_digit_digit_zero_choose) = S ((S (d)) * bcf_row_code_scale_lucas_block_digit_digit_zero_choose)) /\ exists bcf_quotient_lucas_block_digit_digit_zero_choose_decoded_row_code. bcf_row_code_code_lucas_block_digit_digit_zero_choose = bcf_quotient_lucas_block_digit_digit_zero_choose_decoded_row_code * S ((S (d)) * bcf_row_code_scale_lucas_block_digit_digit_zero_choose) + (bcf_row_code_lucas_block_digit_digit_zero_choose))) /\ ((((exists bcf_height_lucas_block_digit_digit_zero_choose_decoded_row_scale. bcf_height_lucas_block_digit_digit_zero_choose_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_digit_zero_choose) = S ((S (d)) * bcf_row_scale_scale_lucas_block_digit_digit_zero_choose)) /\ exists bcf_quotient_lucas_block_digit_digit_zero_choose_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_digit_zero_choose = bcf_quotient_lucas_block_digit_digit_zero_choose_decoded_row_scale * S ((S (d)) * bcf_row_scale_scale_lucas_block_digit_digit_zero_choose) + (bcf_row_scale_lucas_block_digit_digit_zero_choose))) /\ (((exists bcf_height_lucas_block_digit_digit_zero_choose_decoded_value. bcf_height_lucas_block_digit_digit_zero_choose_decoded_value + S (C) = S ((S (p * r + e)) * bcf_row_scale_lucas_block_digit_digit_zero_choose)) /\ exists bcf_quotient_lucas_block_digit_digit_zero_choose_decoded_value. bcf_row_code_lucas_block_digit_digit_zero_choose = bcf_quotient_lucas_block_digit_digit_zero_choose_decoded_value * S ((S (p * r + e)) * bcf_row_scale_lucas_block_digit_digit_zero_choose) + (C))))))))) -> C = 0

Constructive proof overview

Generated structural guide

A binomial row consisting of one upper digit vanishes at every index with positive lower base quotient.

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

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Historical empty-context replay experiment only; that experiment persisted no certificate and granted no release authority. Current checked use follows separately sealed, independently verified proof bundles; there is no Stable promotion.

Proof neighborhood

Direct dependencies

LU000J lucas_positive_lower_quotient_exceeds_upper_digit choose_out_of_range_zero Alpha theorem; checked-use authorized

Direct dependents

LU000L lucas_zero_upper_quotient_high_column_vanishes

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

20 script commands · 3 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)
lucas positive lower quotient exceeds upper digit
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro r
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro C
  6. L6
    intro hdigit
  7. L7
    intro hpositive
  8. L8
    intro hchoose
02Use earlier factsL9–18

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

  1. L9
    specialize choose_out_of_range_zero d
  2. L10
    specialize choose_out_of_range_zero (p * r + e)
  3. L11
    specialize choose_out_of_range_zero C
  4. L12
    apply choose_out_of_range_zero
  5. L13
    specialize lucas_positive_lower_quotient_exceeds_upper_digit p
  6. L14
    specialize lucas_positive_lower_quotient_exceeds_upper_digit r
  7. L15
    specialize lucas_positive_lower_quotient_exceeds_upper_digit d
  8. L16
    specialize lucas_positive_lower_quotient_exceeds_upper_digit e
  9. L17
    apply lucas_positive_lower_quotient_exceeds_upper_digit
  10. L18
    exact hdigit
03Use earlier factsL19–20

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

  1. L19
    exact hpositive
  2. L20
    exact hchoose

Library-wide reading audit

Original exact command ledger · 20 lines
  1. 0001intro p
  2. 0002intro r
  3. 0003intro d
  4. 0004intro e
  5. 0005intro C
  6. 0006intro hdigit
  7. 0007intro hpositive
  8. 0008intro hchoose
  9. 0009specialize choose_out_of_range_zero d
  10. 0010specialize choose_out_of_range_zero (p * r + e)
  11. 0011specialize choose_out_of_range_zero C
  12. 0012apply choose_out_of_range_zero
  13. 0013specialize lucas_positive_lower_quotient_exceeds_upper_digit p
  14. 0014specialize lucas_positive_lower_quotient_exceeds_upper_digit r
  15. 0015specialize lucas_positive_lower_quotient_exceeds_upper_digit d
  16. 0016specialize lucas_positive_lower_quotient_exceeds_upper_digit e
  17. 0017apply lucas_positive_lower_quotient_exceeds_upper_digit
  18. 0018exact hdigit
  19. 0019exact hpositive
  20. 0020exact hchoose