LU000K · theorem body

lucas_positive_lower_quotient_digit_coefficient_zero

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

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

historical independently replay-verified empty-context experiment; the experiment itself persisted no certificate and granted no release authority; current checked use follows separately sealed proof bundles; no Stable promotion.

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.

Statement with defined notation

∀ p. ∀ r. ∀ d. ∀ e. ∀ C. Lt(d,p) → ¬r = 0 → Choose(d,p · r + e,C) → C = 0

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0041 Choose

In local proof propositions

none
Exact expanded first-order 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

Proof neighborhood

Direct theorem prerequisites

LU000J lucas_positive_lower_quotient_exceeds_upper_digit choose_out_of_range_zero · Alpha closed

Direct theorem dependents

LU000L lucas_zero_upper_quotient_high_column_vanishes

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 defined 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