LU000N · theorem body

lucas_one_step_division_congruence

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

Every actual prime-base division of the upper and lower indices satisfies the complete Lucas quotient-times-digit binomial congruence.

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. ∀ n. ∀ k. ∀ q. ∀ r. ∀ d. ∀ e. ∀ C. ∀ A. ∀ B. Prime(p) → n = p · q + d → k = p · r + e → Lt(d,p) → Lt(e,p) → Choose(n,k,C) → Choose(q,r,A) → Choose(d,e,B) → ModEq(p,C,A · B)

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 PD0004 Prime PD0008 ModEq PD0041 Choose

In local proof propositions

PD0041 Choose
Exact expanded first-order statement
forall p n k q r d e C A B. ((~(p = 1) /\ forall frm_prime_left_lucas_block_digit_prime frm_prime_right_lucas_block_digit_prime. p = frm_prime_left_lucas_block_digit_prime * frm_prime_right_lucas_block_digit_prime -> frm_prime_left_lucas_block_digit_prime = 1 \/ frm_prime_right_lucas_block_digit_prime = 1)) -> n = p * q + d -> k = p * r + e -> (exists lbd_gap_division_upper_bound. lbd_gap_division_upper_bound + S (d) = (p)) -> (exists lbd_gap_division_lower_bound. lbd_gap_division_lower_bound + S (e) = (p)) -> (((exists bcf_lt_gap_lucas_block_digit_division_whole_out_of_range. bcf_lt_gap_lucas_block_digit_division_whole_out_of_range + S (n) = k) /\ C = 0) \/ ((exists bcf_le_gap_lucas_block_digit_division_whole_in_range. bcf_le_gap_lucas_block_digit_division_whole_in_range + (k) = n) /\ (exists bcf_row_code_code_lucas_block_digit_division_whole bcf_row_code_scale_lucas_block_digit_division_whole bcf_row_scale_code_lucas_block_digit_division_whole bcf_row_scale_scale_lucas_block_digit_division_whole bcf_row_code_lucas_block_digit_division_whole bcf_row_scale_lucas_block_digit_division_whole. ((forall bcf_row_index_lucas_block_digit_division_whole_table. (exists bcf_lt_gap_lucas_block_digit_division_whole_table_row_bound. bcf_lt_gap_lucas_block_digit_division_whole_table_row_bound + S (bcf_row_index_lucas_block_digit_division_whole_table) = S (n)) -> exists bcf_row_code_lucas_block_digit_division_whole_table bcf_row_scale_lucas_block_digit_division_whole_table. ((((exists bcf_height_lucas_block_digit_division_whole_table_decoded_row_code. bcf_height_lucas_block_digit_division_whole_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_division_whole_table) = S ((S (bcf_row_index_lucas_block_digit_division_whole_table)) * bcf_row_code_scale_lucas_block_digit_division_whole)) /\ exists bcf_quotient_lucas_block_digit_division_whole_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_division_whole = bcf_quotient_lucas_block_digit_division_whole_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_division_whole_table)) * bcf_row_code_scale_lucas_block_digit_division_whole) + (bcf_row_code_lucas_block_digit_division_whole_table))) /\ ((((exists bcf_height_lucas_block_digit_division_whole_table_decoded_row_scale. bcf_height_lucas_block_digit_division_whole_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_division_whole_table) = S ((S (bcf_row_index_lucas_block_digit_division_whole_table)) * bcf_row_scale_scale_lucas_block_digit_division_whole)) /\ exists bcf_quotient_lucas_block_digit_division_whole_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_division_whole = bcf_quotient_lucas_block_digit_division_whole_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_division_whole_table)) * bcf_row_scale_scale_lucas_block_digit_division_whole) + (bcf_row_scale_lucas_block_digit_division_whole_table))) /\ ((bcf_row_index_lucas_block_digit_division_whole_table = 0 /\ (forall bcf_index_lucas_block_digit_division_whole_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_division_whole_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_division_whole_table_zero_row_bound + S (bcf_index_lucas_block_digit_division_whole_table_zero_row) = S (n)) -> exists bcf_value_lucas_block_digit_division_whole_table_zero_row. ((((exists bcf_height_lucas_block_digit_division_whole_table_zero_row_entry. bcf_height_lucas_block_digit_division_whole_table_zero_row_entry + S (bcf_value_lucas_block_digit_division_whole_table_zero_row) = S ((S (bcf_index_lucas_block_digit_division_whole_table_zero_row)) * bcf_row_scale_lucas_block_digit_division_whole_table)) /\ exists bcf_quotient_lucas_block_digit_division_whole_table_zero_row_entry. bcf_row_code_lucas_block_digit_division_whole_table = bcf_quotient_lucas_block_digit_division_whole_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_division_whole_table_zero_row)) * bcf_row_scale_lucas_block_digit_division_whole_table) + (bcf_value_lucas_block_digit_division_whole_table_zero_row))) /\ ((bcf_index_lucas_block_digit_division_whole_table_zero_row = 0 /\ bcf_value_lucas_block_digit_division_whole_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_division_whole_table_zero_row. bcf_index_lucas_block_digit_division_whole_table_zero_row = S bcf_predecessor_lucas_block_digit_division_whole_table_zero_row /\ bcf_value_lucas_block_digit_division_whole_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_division_whole_table bcf_previous_code_lucas_block_digit_division_whole_table bcf_previous_scale_lucas_block_digit_division_whole_table. bcf_row_index_lucas_block_digit_division_whole_table = S bcf_predecessor_lucas_block_digit_division_whole_table /\ ((((exists bcf_height_lucas_block_digit_division_whole_table_decoded_previous_code. bcf_height_lucas_block_digit_division_whole_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_division_whole_table) = S ((S (bcf_predecessor_lucas_block_digit_division_whole_table)) * bcf_row_code_scale_lucas_block_digit_division_whole)) /\ exists bcf_quotient_lucas_block_digit_division_whole_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_division_whole = bcf_quotient_lucas_block_digit_division_whole_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_division_whole_table)) * bcf_row_code_scale_lucas_block_digit_division_whole) + (bcf_previous_code_lucas_block_digit_division_whole_table))) /\ ((((exists bcf_height_lucas_block_digit_division_whole_table_decoded_previous_scale. bcf_height_lucas_block_digit_division_whole_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_division_whole_table) = S ((S (bcf_predecessor_lucas_block_digit_division_whole_table)) * bcf_row_scale_scale_lucas_block_digit_division_whole)) /\ exists bcf_quotient_lucas_block_digit_division_whole_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_division_whole = bcf_quotient_lucas_block_digit_division_whole_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_division_whole_table)) * bcf_row_scale_scale_lucas_block_digit_division_whole) + (bcf_previous_scale_lucas_block_digit_division_whole_table))) /\ (forall bcf_index_lucas_block_digit_division_whole_table_row_step. (exists bcf_lt_gap_lucas_block_digit_division_whole_table_row_step_bound. bcf_lt_gap_lucas_block_digit_division_whole_table_row_step_bound + S (bcf_index_lucas_block_digit_division_whole_table_row_step) = S (n)) -> exists bcf_value_lucas_block_digit_division_whole_table_row_step. ((((exists bcf_height_lucas_block_digit_division_whole_table_row_step_entry. bcf_height_lucas_block_digit_division_whole_table_row_step_entry + S (bcf_value_lucas_block_digit_division_whole_table_row_step) = S ((S (bcf_index_lucas_block_digit_division_whole_table_row_step)) * bcf_row_scale_lucas_block_digit_division_whole_table)) /\ exists bcf_quotient_lucas_block_digit_division_whole_table_row_step_entry. bcf_row_code_lucas_block_digit_division_whole_table = bcf_quotient_lucas_block_digit_division_whole_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_division_whole_table_row_step)) * bcf_row_scale_lucas_block_digit_division_whole_table) + (bcf_value_lucas_block_digit_division_whole_table_row_step))) /\ ((bcf_index_lucas_block_digit_division_whole_table_row_step = 0 /\ bcf_value_lucas_block_digit_division_whole_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_division_whole_table_row_step bcf_left_lucas_block_digit_division_whole_table_row_step bcf_right_lucas_block_digit_division_whole_table_row_step. bcf_index_lucas_block_digit_division_whole_table_row_step = S bcf_predecessor_lucas_block_digit_division_whole_table_row_step /\ ((((exists bcf_height_lucas_block_digit_division_whole_table_row_step_previous_left. bcf_height_lucas_block_digit_division_whole_table_row_step_previous_left + S (bcf_left_lucas_block_digit_division_whole_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_division_whole_table_row_step)) * bcf_previous_scale_lucas_block_digit_division_whole_table)) /\ exists bcf_quotient_lucas_block_digit_division_whole_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_division_whole_table = bcf_quotient_lucas_block_digit_division_whole_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_division_whole_table_row_step)) * bcf_previous_scale_lucas_block_digit_division_whole_table) + (bcf_left_lucas_block_digit_division_whole_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_division_whole_table_row_step_previous_right. bcf_height_lucas_block_digit_division_whole_table_row_step_previous_right + S (bcf_right_lucas_block_digit_division_whole_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_division_whole_table_row_step))) * bcf_previous_scale_lucas_block_digit_division_whole_table)) /\ exists bcf_quotient_lucas_block_digit_division_whole_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_division_whole_table = bcf_quotient_lucas_block_digit_division_whole_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_division_whole_table_row_step))) * bcf_previous_scale_lucas_block_digit_division_whole_table) + (bcf_right_lucas_block_digit_division_whole_table_row_step))) /\ bcf_value_lucas_block_digit_division_whole_table_row_step = bcf_left_lucas_block_digit_division_whole_table_row_step + bcf_right_lucas_block_digit_division_whole_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_division_whole_decoded_row_code. bcf_height_lucas_block_digit_division_whole_decoded_row_code + S (bcf_row_code_lucas_block_digit_division_whole) = S ((S (n)) * bcf_row_code_scale_lucas_block_digit_division_whole)) /\ exists bcf_quotient_lucas_block_digit_division_whole_decoded_row_code. bcf_row_code_code_lucas_block_digit_division_whole = bcf_quotient_lucas_block_digit_division_whole_decoded_row_code * S ((S (n)) * bcf_row_code_scale_lucas_block_digit_division_whole) + (bcf_row_code_lucas_block_digit_division_whole))) /\ ((((exists bcf_height_lucas_block_digit_division_whole_decoded_row_scale. bcf_height_lucas_block_digit_division_whole_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_division_whole) = S ((S (n)) * bcf_row_scale_scale_lucas_block_digit_division_whole)) /\ exists bcf_quotient_lucas_block_digit_division_whole_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_division_whole = bcf_quotient_lucas_block_digit_division_whole_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_lucas_block_digit_division_whole) + (bcf_row_scale_lucas_block_digit_division_whole))) /\ (((exists bcf_height_lucas_block_digit_division_whole_decoded_value. bcf_height_lucas_block_digit_division_whole_decoded_value + S (C) = S ((S (k)) * bcf_row_scale_lucas_block_digit_division_whole)) /\ exists bcf_quotient_lucas_block_digit_division_whole_decoded_value. bcf_row_code_lucas_block_digit_division_whole = bcf_quotient_lucas_block_digit_division_whole_decoded_value * S ((S (k)) * bcf_row_scale_lucas_block_digit_division_whole) + (C))))))))) -> (((exists bcf_lt_gap_lucas_block_digit_division_quotient_out_of_range. bcf_lt_gap_lucas_block_digit_division_quotient_out_of_range + S (q) = r) /\ A = 0) \/ ((exists bcf_le_gap_lucas_block_digit_division_quotient_in_range. bcf_le_gap_lucas_block_digit_division_quotient_in_range + (r) = q) /\ (exists bcf_row_code_code_lucas_block_digit_division_quotient bcf_row_code_scale_lucas_block_digit_division_quotient bcf_row_scale_code_lucas_block_digit_division_quotient bcf_row_scale_scale_lucas_block_digit_division_quotient bcf_row_code_lucas_block_digit_division_quotient bcf_row_scale_lucas_block_digit_division_quotient. ((forall bcf_row_index_lucas_block_digit_division_quotient_table. (exists bcf_lt_gap_lucas_block_digit_division_quotient_table_row_bound. bcf_lt_gap_lucas_block_digit_division_quotient_table_row_bound + S (bcf_row_index_lucas_block_digit_division_quotient_table) = S (q)) -> exists bcf_row_code_lucas_block_digit_division_quotient_table bcf_row_scale_lucas_block_digit_division_quotient_table. ((((exists bcf_height_lucas_block_digit_division_quotient_table_decoded_row_code. bcf_height_lucas_block_digit_division_quotient_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_division_quotient_table) = S ((S (bcf_row_index_lucas_block_digit_division_quotient_table)) * bcf_row_code_scale_lucas_block_digit_division_quotient)) /\ exists bcf_quotient_lucas_block_digit_division_quotient_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_division_quotient = bcf_quotient_lucas_block_digit_division_quotient_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_division_quotient_table)) * bcf_row_code_scale_lucas_block_digit_division_quotient) + (bcf_row_code_lucas_block_digit_division_quotient_table))) /\ ((((exists bcf_height_lucas_block_digit_division_quotient_table_decoded_row_scale. bcf_height_lucas_block_digit_division_quotient_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_division_quotient_table) = S ((S (bcf_row_index_lucas_block_digit_division_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_division_quotient)) /\ exists bcf_quotient_lucas_block_digit_division_quotient_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_division_quotient = bcf_quotient_lucas_block_digit_division_quotient_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_division_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_division_quotient) + (bcf_row_scale_lucas_block_digit_division_quotient_table))) /\ ((bcf_row_index_lucas_block_digit_division_quotient_table = 0 /\ (forall bcf_index_lucas_block_digit_division_quotient_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_division_quotient_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_division_quotient_table_zero_row_bound + S (bcf_index_lucas_block_digit_division_quotient_table_zero_row) = S (q)) -> exists bcf_value_lucas_block_digit_division_quotient_table_zero_row. ((((exists bcf_height_lucas_block_digit_division_quotient_table_zero_row_entry. bcf_height_lucas_block_digit_division_quotient_table_zero_row_entry + S (bcf_value_lucas_block_digit_division_quotient_table_zero_row) = S ((S (bcf_index_lucas_block_digit_division_quotient_table_zero_row)) * bcf_row_scale_lucas_block_digit_division_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_division_quotient_table_zero_row_entry. bcf_row_code_lucas_block_digit_division_quotient_table = bcf_quotient_lucas_block_digit_division_quotient_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_division_quotient_table_zero_row)) * bcf_row_scale_lucas_block_digit_division_quotient_table) + (bcf_value_lucas_block_digit_division_quotient_table_zero_row))) /\ ((bcf_index_lucas_block_digit_division_quotient_table_zero_row = 0 /\ bcf_value_lucas_block_digit_division_quotient_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_division_quotient_table_zero_row. bcf_index_lucas_block_digit_division_quotient_table_zero_row = S bcf_predecessor_lucas_block_digit_division_quotient_table_zero_row /\ bcf_value_lucas_block_digit_division_quotient_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_division_quotient_table bcf_previous_code_lucas_block_digit_division_quotient_table bcf_previous_scale_lucas_block_digit_division_quotient_table. bcf_row_index_lucas_block_digit_division_quotient_table = S bcf_predecessor_lucas_block_digit_division_quotient_table /\ ((((exists bcf_height_lucas_block_digit_division_quotient_table_decoded_previous_code. bcf_height_lucas_block_digit_division_quotient_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_division_quotient_table) = S ((S (bcf_predecessor_lucas_block_digit_division_quotient_table)) * bcf_row_code_scale_lucas_block_digit_division_quotient)) /\ exists bcf_quotient_lucas_block_digit_division_quotient_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_division_quotient = bcf_quotient_lucas_block_digit_division_quotient_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_division_quotient_table)) * bcf_row_code_scale_lucas_block_digit_division_quotient) + (bcf_previous_code_lucas_block_digit_division_quotient_table))) /\ ((((exists bcf_height_lucas_block_digit_division_quotient_table_decoded_previous_scale. bcf_height_lucas_block_digit_division_quotient_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_division_quotient_table) = S ((S (bcf_predecessor_lucas_block_digit_division_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_division_quotient)) /\ exists bcf_quotient_lucas_block_digit_division_quotient_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_division_quotient = bcf_quotient_lucas_block_digit_division_quotient_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_division_quotient_table)) * bcf_row_scale_scale_lucas_block_digit_division_quotient) + (bcf_previous_scale_lucas_block_digit_division_quotient_table))) /\ (forall bcf_index_lucas_block_digit_division_quotient_table_row_step. (exists bcf_lt_gap_lucas_block_digit_division_quotient_table_row_step_bound. bcf_lt_gap_lucas_block_digit_division_quotient_table_row_step_bound + S (bcf_index_lucas_block_digit_division_quotient_table_row_step) = S (q)) -> exists bcf_value_lucas_block_digit_division_quotient_table_row_step. ((((exists bcf_height_lucas_block_digit_division_quotient_table_row_step_entry. bcf_height_lucas_block_digit_division_quotient_table_row_step_entry + S (bcf_value_lucas_block_digit_division_quotient_table_row_step) = S ((S (bcf_index_lucas_block_digit_division_quotient_table_row_step)) * bcf_row_scale_lucas_block_digit_division_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_division_quotient_table_row_step_entry. bcf_row_code_lucas_block_digit_division_quotient_table = bcf_quotient_lucas_block_digit_division_quotient_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_division_quotient_table_row_step)) * bcf_row_scale_lucas_block_digit_division_quotient_table) + (bcf_value_lucas_block_digit_division_quotient_table_row_step))) /\ ((bcf_index_lucas_block_digit_division_quotient_table_row_step = 0 /\ bcf_value_lucas_block_digit_division_quotient_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_division_quotient_table_row_step bcf_left_lucas_block_digit_division_quotient_table_row_step bcf_right_lucas_block_digit_division_quotient_table_row_step. bcf_index_lucas_block_digit_division_quotient_table_row_step = S bcf_predecessor_lucas_block_digit_division_quotient_table_row_step /\ ((((exists bcf_height_lucas_block_digit_division_quotient_table_row_step_previous_left. bcf_height_lucas_block_digit_division_quotient_table_row_step_previous_left + S (bcf_left_lucas_block_digit_division_quotient_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_division_quotient_table_row_step)) * bcf_previous_scale_lucas_block_digit_division_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_division_quotient_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_division_quotient_table = bcf_quotient_lucas_block_digit_division_quotient_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_division_quotient_table_row_step)) * bcf_previous_scale_lucas_block_digit_division_quotient_table) + (bcf_left_lucas_block_digit_division_quotient_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_division_quotient_table_row_step_previous_right. bcf_height_lucas_block_digit_division_quotient_table_row_step_previous_right + S (bcf_right_lucas_block_digit_division_quotient_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_division_quotient_table_row_step))) * bcf_previous_scale_lucas_block_digit_division_quotient_table)) /\ exists bcf_quotient_lucas_block_digit_division_quotient_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_division_quotient_table = bcf_quotient_lucas_block_digit_division_quotient_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_division_quotient_table_row_step))) * bcf_previous_scale_lucas_block_digit_division_quotient_table) + (bcf_right_lucas_block_digit_division_quotient_table_row_step))) /\ bcf_value_lucas_block_digit_division_quotient_table_row_step = bcf_left_lucas_block_digit_division_quotient_table_row_step + bcf_right_lucas_block_digit_division_quotient_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_division_quotient_decoded_row_code. bcf_height_lucas_block_digit_division_quotient_decoded_row_code + S (bcf_row_code_lucas_block_digit_division_quotient) = S ((S (q)) * bcf_row_code_scale_lucas_block_digit_division_quotient)) /\ exists bcf_quotient_lucas_block_digit_division_quotient_decoded_row_code. bcf_row_code_code_lucas_block_digit_division_quotient = bcf_quotient_lucas_block_digit_division_quotient_decoded_row_code * S ((S (q)) * bcf_row_code_scale_lucas_block_digit_division_quotient) + (bcf_row_code_lucas_block_digit_division_quotient))) /\ ((((exists bcf_height_lucas_block_digit_division_quotient_decoded_row_scale. bcf_height_lucas_block_digit_division_quotient_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_division_quotient) = S ((S (q)) * bcf_row_scale_scale_lucas_block_digit_division_quotient)) /\ exists bcf_quotient_lucas_block_digit_division_quotient_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_division_quotient = bcf_quotient_lucas_block_digit_division_quotient_decoded_row_scale * S ((S (q)) * bcf_row_scale_scale_lucas_block_digit_division_quotient) + (bcf_row_scale_lucas_block_digit_division_quotient))) /\ (((exists bcf_height_lucas_block_digit_division_quotient_decoded_value. bcf_height_lucas_block_digit_division_quotient_decoded_value + S (A) = S ((S (r)) * bcf_row_scale_lucas_block_digit_division_quotient)) /\ exists bcf_quotient_lucas_block_digit_division_quotient_decoded_value. bcf_row_code_lucas_block_digit_division_quotient = bcf_quotient_lucas_block_digit_division_quotient_decoded_value * S ((S (r)) * bcf_row_scale_lucas_block_digit_division_quotient) + (A))))))))) -> (((exists bcf_lt_gap_lucas_block_digit_division_digit_out_of_range. bcf_lt_gap_lucas_block_digit_division_digit_out_of_range + S (d) = e) /\ B = 0) \/ ((exists bcf_le_gap_lucas_block_digit_division_digit_in_range. bcf_le_gap_lucas_block_digit_division_digit_in_range + (e) = d) /\ (exists bcf_row_code_code_lucas_block_digit_division_digit bcf_row_code_scale_lucas_block_digit_division_digit bcf_row_scale_code_lucas_block_digit_division_digit bcf_row_scale_scale_lucas_block_digit_division_digit bcf_row_code_lucas_block_digit_division_digit bcf_row_scale_lucas_block_digit_division_digit. ((forall bcf_row_index_lucas_block_digit_division_digit_table. (exists bcf_lt_gap_lucas_block_digit_division_digit_table_row_bound. bcf_lt_gap_lucas_block_digit_division_digit_table_row_bound + S (bcf_row_index_lucas_block_digit_division_digit_table) = S (d)) -> exists bcf_row_code_lucas_block_digit_division_digit_table bcf_row_scale_lucas_block_digit_division_digit_table. ((((exists bcf_height_lucas_block_digit_division_digit_table_decoded_row_code. bcf_height_lucas_block_digit_division_digit_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_division_digit_table) = S ((S (bcf_row_index_lucas_block_digit_division_digit_table)) * bcf_row_code_scale_lucas_block_digit_division_digit)) /\ exists bcf_quotient_lucas_block_digit_division_digit_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_division_digit = bcf_quotient_lucas_block_digit_division_digit_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_division_digit_table)) * bcf_row_code_scale_lucas_block_digit_division_digit) + (bcf_row_code_lucas_block_digit_division_digit_table))) /\ ((((exists bcf_height_lucas_block_digit_division_digit_table_decoded_row_scale. bcf_height_lucas_block_digit_division_digit_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_division_digit_table) = S ((S (bcf_row_index_lucas_block_digit_division_digit_table)) * bcf_row_scale_scale_lucas_block_digit_division_digit)) /\ exists bcf_quotient_lucas_block_digit_division_digit_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_division_digit = bcf_quotient_lucas_block_digit_division_digit_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_division_digit_table)) * bcf_row_scale_scale_lucas_block_digit_division_digit) + (bcf_row_scale_lucas_block_digit_division_digit_table))) /\ ((bcf_row_index_lucas_block_digit_division_digit_table = 0 /\ (forall bcf_index_lucas_block_digit_division_digit_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_division_digit_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_division_digit_table_zero_row_bound + S (bcf_index_lucas_block_digit_division_digit_table_zero_row) = S (d)) -> exists bcf_value_lucas_block_digit_division_digit_table_zero_row. ((((exists bcf_height_lucas_block_digit_division_digit_table_zero_row_entry. bcf_height_lucas_block_digit_division_digit_table_zero_row_entry + S (bcf_value_lucas_block_digit_division_digit_table_zero_row) = S ((S (bcf_index_lucas_block_digit_division_digit_table_zero_row)) * bcf_row_scale_lucas_block_digit_division_digit_table)) /\ exists bcf_quotient_lucas_block_digit_division_digit_table_zero_row_entry. bcf_row_code_lucas_block_digit_division_digit_table = bcf_quotient_lucas_block_digit_division_digit_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_division_digit_table_zero_row)) * bcf_row_scale_lucas_block_digit_division_digit_table) + (bcf_value_lucas_block_digit_division_digit_table_zero_row))) /\ ((bcf_index_lucas_block_digit_division_digit_table_zero_row = 0 /\ bcf_value_lucas_block_digit_division_digit_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_division_digit_table_zero_row. bcf_index_lucas_block_digit_division_digit_table_zero_row = S bcf_predecessor_lucas_block_digit_division_digit_table_zero_row /\ bcf_value_lucas_block_digit_division_digit_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_division_digit_table bcf_previous_code_lucas_block_digit_division_digit_table bcf_previous_scale_lucas_block_digit_division_digit_table. bcf_row_index_lucas_block_digit_division_digit_table = S bcf_predecessor_lucas_block_digit_division_digit_table /\ ((((exists bcf_height_lucas_block_digit_division_digit_table_decoded_previous_code. bcf_height_lucas_block_digit_division_digit_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_division_digit_table) = S ((S (bcf_predecessor_lucas_block_digit_division_digit_table)) * bcf_row_code_scale_lucas_block_digit_division_digit)) /\ exists bcf_quotient_lucas_block_digit_division_digit_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_division_digit = bcf_quotient_lucas_block_digit_division_digit_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_division_digit_table)) * bcf_row_code_scale_lucas_block_digit_division_digit) + (bcf_previous_code_lucas_block_digit_division_digit_table))) /\ ((((exists bcf_height_lucas_block_digit_division_digit_table_decoded_previous_scale. bcf_height_lucas_block_digit_division_digit_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_division_digit_table) = S ((S (bcf_predecessor_lucas_block_digit_division_digit_table)) * bcf_row_scale_scale_lucas_block_digit_division_digit)) /\ exists bcf_quotient_lucas_block_digit_division_digit_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_division_digit = bcf_quotient_lucas_block_digit_division_digit_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_division_digit_table)) * bcf_row_scale_scale_lucas_block_digit_division_digit) + (bcf_previous_scale_lucas_block_digit_division_digit_table))) /\ (forall bcf_index_lucas_block_digit_division_digit_table_row_step. (exists bcf_lt_gap_lucas_block_digit_division_digit_table_row_step_bound. bcf_lt_gap_lucas_block_digit_division_digit_table_row_step_bound + S (bcf_index_lucas_block_digit_division_digit_table_row_step) = S (d)) -> exists bcf_value_lucas_block_digit_division_digit_table_row_step. ((((exists bcf_height_lucas_block_digit_division_digit_table_row_step_entry. bcf_height_lucas_block_digit_division_digit_table_row_step_entry + S (bcf_value_lucas_block_digit_division_digit_table_row_step) = S ((S (bcf_index_lucas_block_digit_division_digit_table_row_step)) * bcf_row_scale_lucas_block_digit_division_digit_table)) /\ exists bcf_quotient_lucas_block_digit_division_digit_table_row_step_entry. bcf_row_code_lucas_block_digit_division_digit_table = bcf_quotient_lucas_block_digit_division_digit_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_division_digit_table_row_step)) * bcf_row_scale_lucas_block_digit_division_digit_table) + (bcf_value_lucas_block_digit_division_digit_table_row_step))) /\ ((bcf_index_lucas_block_digit_division_digit_table_row_step = 0 /\ bcf_value_lucas_block_digit_division_digit_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_division_digit_table_row_step bcf_left_lucas_block_digit_division_digit_table_row_step bcf_right_lucas_block_digit_division_digit_table_row_step. bcf_index_lucas_block_digit_division_digit_table_row_step = S bcf_predecessor_lucas_block_digit_division_digit_table_row_step /\ ((((exists bcf_height_lucas_block_digit_division_digit_table_row_step_previous_left. bcf_height_lucas_block_digit_division_digit_table_row_step_previous_left + S (bcf_left_lucas_block_digit_division_digit_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_division_digit_table_row_step)) * bcf_previous_scale_lucas_block_digit_division_digit_table)) /\ exists bcf_quotient_lucas_block_digit_division_digit_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_division_digit_table = bcf_quotient_lucas_block_digit_division_digit_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_division_digit_table_row_step)) * bcf_previous_scale_lucas_block_digit_division_digit_table) + (bcf_left_lucas_block_digit_division_digit_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_division_digit_table_row_step_previous_right. bcf_height_lucas_block_digit_division_digit_table_row_step_previous_right + S (bcf_right_lucas_block_digit_division_digit_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_division_digit_table_row_step))) * bcf_previous_scale_lucas_block_digit_division_digit_table)) /\ exists bcf_quotient_lucas_block_digit_division_digit_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_division_digit_table = bcf_quotient_lucas_block_digit_division_digit_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_division_digit_table_row_step))) * bcf_previous_scale_lucas_block_digit_division_digit_table) + (bcf_right_lucas_block_digit_division_digit_table_row_step))) /\ bcf_value_lucas_block_digit_division_digit_table_row_step = bcf_left_lucas_block_digit_division_digit_table_row_step + bcf_right_lucas_block_digit_division_digit_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_division_digit_decoded_row_code. bcf_height_lucas_block_digit_division_digit_decoded_row_code + S (bcf_row_code_lucas_block_digit_division_digit) = S ((S (d)) * bcf_row_code_scale_lucas_block_digit_division_digit)) /\ exists bcf_quotient_lucas_block_digit_division_digit_decoded_row_code. bcf_row_code_code_lucas_block_digit_division_digit = bcf_quotient_lucas_block_digit_division_digit_decoded_row_code * S ((S (d)) * bcf_row_code_scale_lucas_block_digit_division_digit) + (bcf_row_code_lucas_block_digit_division_digit))) /\ ((((exists bcf_height_lucas_block_digit_division_digit_decoded_row_scale. bcf_height_lucas_block_digit_division_digit_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_division_digit) = S ((S (d)) * bcf_row_scale_scale_lucas_block_digit_division_digit)) /\ exists bcf_quotient_lucas_block_digit_division_digit_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_division_digit = bcf_quotient_lucas_block_digit_division_digit_decoded_row_scale * S ((S (d)) * bcf_row_scale_scale_lucas_block_digit_division_digit) + (bcf_row_scale_lucas_block_digit_division_digit))) /\ (((exists bcf_height_lucas_block_digit_division_digit_decoded_value. bcf_height_lucas_block_digit_division_digit_decoded_value + S (B) = S ((S (e)) * bcf_row_scale_lucas_block_digit_division_digit)) /\ exists bcf_quotient_lucas_block_digit_division_digit_decoded_value. bcf_row_code_lucas_block_digit_division_digit = bcf_quotient_lucas_block_digit_division_digit_decoded_value * S ((S (e)) * bcf_row_scale_lucas_block_digit_division_digit) + (B))))))))) -> (exists lbd_left_division_result lbd_right_division_result. (C) + (p) * lbd_left_division_result = (A * B) + (p) * lbd_right_division_result)

Proof neighborhood

Direct theorem prerequisites

choose_upper_eq_transport · Alpha closed LU000O lucas_choose_lower_eq_transport LU000M lucas_prime_block_digit_congruence

Direct theorem dependents

LU001O lucas_multidigit_congruence LU001P lucas_terminating_multidigit_theorem

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

49 script commands · 6 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.

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 (2)
lucas choose lower eq transportlucas prime block digit congruence
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro k
  4. L4
    intro q
  5. L5
    intro r
  6. L6
    intro d
  7. L7
    intro e
  8. L8
    intro C
  9. L9
    intro A
  10. L10
    intro B
02Fix variables and assumptionsL11–18

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

  1. L11
    intro hprime
  2. L12
    intro hn
  3. L13
    intro hk
  4. L14
    intro hdigit
  5. L15
    intro he_digit
  6. L16
    intro hwhole
  7. L17
    intro hquotient
  8. L18
    intro hfactor
03Establish hupperL19–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose upper eq transport.

  1. L19
    have hupper : Choose(p · q + d,k,C)Definitions: Choose(p · q + d,k,C)Original native command in the exact edition
  2. L20
    specialize choose_upper_eq_transport n
  3. L21
    specialize choose_upper_eq_transport (p * q + d)
  4. L22
    specialize choose_upper_eq_transport k
  5. L23
    specialize choose_upper_eq_transport C
  6. L24
    apply choose_upper_eq_transport
  7. L25
    exact hn
  8. L26
    exact hwhole
04Establish hcanonicalL27–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas choose lower eq transport.

  1. L27
    have hcanonical : Choose(p · q + d,p · r + e,C)Definitions: Choose(p · q + d,p · r + e,C)Original native command in the exact edition
  2. L28
    specialize lucas_choose_lower_eq_transport (p * q + d)
  3. L29
    specialize lucas_choose_lower_eq_transport k
  4. L30
    specialize lucas_choose_lower_eq_transport (p * r + e)
  5. L31
    specialize lucas_choose_lower_eq_transport C
  6. L32
    apply lucas_choose_lower_eq_transport
  7. L33
    exact hk
  8. L34
    exact hupper
  9. L35
    specialize lucas_prime_block_digit_congruence p
  10. L36
    specialize lucas_prime_block_digit_congruence q
05Use earlier factsL37–46

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

  1. L37
    specialize lucas_prime_block_digit_congruence r
  2. L38
    specialize lucas_prime_block_digit_congruence d
  3. L39
    specialize lucas_prime_block_digit_congruence e
  4. L40
    specialize lucas_prime_block_digit_congruence C
  5. L41
    specialize lucas_prime_block_digit_congruence A
  6. L42
    specialize lucas_prime_block_digit_congruence B
  7. L43
    apply lucas_prime_block_digit_congruence
  8. L44
    exact hprime
  9. L45
    exact hdigit
  10. L46
    exact he_digit
06Use earlier factsL47–49

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

  1. L47
    exact hcanonical
  2. L48
    exact hquotient
  3. L49
    exact hfactor

Library-wide reading audit

Original defined command ledger · 49 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro k
  4. 0004intro q
  5. 0005intro r
  6. 0006intro d
  7. 0007intro e
  8. 0008intro C
  9. 0009intro A
  10. 0010intro B
  11. 0011intro hprime
  12. 0012intro hn
  13. 0013intro hk
  14. 0014intro hdigit
  15. 0015intro he_digit
  16. 0016intro hwhole
  17. 0017intro hquotient
  18. 0018intro hfactor
  19. 0019have hupper : Choose(p · q + d,k,C)
    Exact native replay linehave hupper : ((exists bcf_lt_gap_lucas_block_digit_division_upper_normal_out_of_range. bcf_lt_gap_lucas_block_digit_division_upper_normal_out_of_range + S (p * q + d) = k) /\ C = 0) \/ ((exists bcf_le_gap_lucas_block_digit_division_upper_normal_in_range. bcf_le_gap_lucas_block_digit_division_upper_normal_in_range + (k) = p * q + d) /\ (exists bcf_row_code_code_lucas_block_digit_division_upper_normal bcf_row_code_scale_lucas_block_digit_division_upper_normal bcf_row_scale_code_lucas_block_digit_division_upper_normal bcf_row_scale_scale_lucas_block_digit_division_upper_normal bcf_row_code_lucas_block_digit_division_upper_normal bcf_row_scale_lucas_block_digit_division_upper_normal. ((forall bcf_row_index_lucas_block_digit_division_upper_normal_table. (exists bcf_lt_gap_lucas_block_digit_division_upper_normal_table_row_bound. bcf_lt_gap_lucas_block_digit_division_upper_normal_table_row_bound + S (bcf_row_index_lucas_block_digit_division_upper_normal_table) = S (p * q + d)) -> exists bcf_row_code_lucas_block_digit_division_upper_normal_table bcf_row_scale_lucas_block_digit_division_upper_normal_table. ((((exists bcf_height_lucas_block_digit_division_upper_normal_table_decoded_row_code. bcf_height_lucas_block_digit_division_upper_normal_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_division_upper_normal_table) = S ((S (bcf_row_index_lucas_block_digit_division_upper_normal_table)) * bcf_row_code_scale_lucas_block_digit_division_upper_normal)) /\ exists bcf_quotient_lucas_block_digit_division_upper_normal_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_division_upper_normal = bcf_quotient_lucas_block_digit_division_upper_normal_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_division_upper_normal_table)) * bcf_row_code_scale_lucas_block_digit_division_upper_normal) + (bcf_row_code_lucas_block_digit_division_upper_normal_table))) /\ ((((exists bcf_height_lucas_block_digit_division_upper_normal_table_decoded_row_scale. bcf_height_lucas_block_digit_division_upper_normal_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_division_upper_normal_table) = S ((S (bcf_row_index_lucas_block_digit_division_upper_normal_table)) * bcf_row_scale_scale_lucas_block_digit_division_upper_normal)) /\ exists bcf_quotient_lucas_block_digit_division_upper_normal_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_division_upper_normal = bcf_quotient_lucas_block_digit_division_upper_normal_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_division_upper_normal_table)) * bcf_row_scale_scale_lucas_block_digit_division_upper_normal) + (bcf_row_scale_lucas_block_digit_division_upper_normal_table))) /\ ((bcf_row_index_lucas_block_digit_division_upper_normal_table = 0 /\ (forall bcf_index_lucas_block_digit_division_upper_normal_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_division_upper_normal_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_division_upper_normal_table_zero_row_bound + S (bcf_index_lucas_block_digit_division_upper_normal_table_zero_row) = S (p * q + d)) -> exists bcf_value_lucas_block_digit_division_upper_normal_table_zero_row. ((((exists bcf_height_lucas_block_digit_division_upper_normal_table_zero_row_entry. bcf_height_lucas_block_digit_division_upper_normal_table_zero_row_entry + S (bcf_value_lucas_block_digit_division_upper_normal_table_zero_row) = S ((S (bcf_index_lucas_block_digit_division_upper_normal_table_zero_row)) * bcf_row_scale_lucas_block_digit_division_upper_normal_table)) /\ exists bcf_quotient_lucas_block_digit_division_upper_normal_table_zero_row_entry. bcf_row_code_lucas_block_digit_division_upper_normal_table = bcf_quotient_lucas_block_digit_division_upper_normal_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_division_upper_normal_table_zero_row)) * bcf_row_scale_lucas_block_digit_division_upper_normal_table) + (bcf_value_lucas_block_digit_division_upper_normal_table_zero_row))) /\ ((bcf_index_lucas_block_digit_division_upper_normal_table_zero_row = 0 /\ bcf_value_lucas_block_digit_division_upper_normal_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_division_upper_normal_table_zero_row. bcf_index_lucas_block_digit_division_upper_normal_table_zero_row = S bcf_predecessor_lucas_block_digit_division_upper_normal_table_zero_row /\ bcf_value_lucas_block_digit_division_upper_normal_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_division_upper_normal_table bcf_previous_code_lucas_block_digit_division_upper_normal_table bcf_previous_scale_lucas_block_digit_division_upper_normal_table. bcf_row_index_lucas_block_digit_division_upper_normal_table = S bcf_predecessor_lucas_block_digit_division_upper_normal_table /\ ((((exists bcf_height_lucas_block_digit_division_upper_normal_table_decoded_previous_code. bcf_height_lucas_block_digit_division_upper_normal_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_division_upper_normal_table) = S ((S (bcf_predecessor_lucas_block_digit_division_upper_normal_table)) * bcf_row_code_scale_lucas_block_digit_division_upper_normal)) /\ exists bcf_quotient_lucas_block_digit_division_upper_normal_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_division_upper_normal = bcf_quotient_lucas_block_digit_division_upper_normal_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_division_upper_normal_table)) * bcf_row_code_scale_lucas_block_digit_division_upper_normal) + (bcf_previous_code_lucas_block_digit_division_upper_normal_table))) /\ ((((exists bcf_height_lucas_block_digit_division_upper_normal_table_decoded_previous_scale. bcf_height_lucas_block_digit_division_upper_normal_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_division_upper_normal_table) = S ((S (bcf_predecessor_lucas_block_digit_division_upper_normal_table)) * bcf_row_scale_scale_lucas_block_digit_division_upper_normal)) /\ exists bcf_quotient_lucas_block_digit_division_upper_normal_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_division_upper_normal = bcf_quotient_lucas_block_digit_division_upper_normal_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_division_upper_normal_table)) * bcf_row_scale_scale_lucas_block_digit_division_upper_normal) + (bcf_previous_scale_lucas_block_digit_division_upper_normal_table))) /\ (forall bcf_index_lucas_block_digit_division_upper_normal_table_row_step. (exists bcf_lt_gap_lucas_block_digit_division_upper_normal_table_row_step_bound. bcf_lt_gap_lucas_block_digit_division_upper_normal_table_row_step_bound + S (bcf_index_lucas_block_digit_division_upper_normal_table_row_step) = S (p * q + d)) -> exists bcf_value_lucas_block_digit_division_upper_normal_table_row_step. ((((exists bcf_height_lucas_block_digit_division_upper_normal_table_row_step_entry. bcf_height_lucas_block_digit_division_upper_normal_table_row_step_entry + S (bcf_value_lucas_block_digit_division_upper_normal_table_row_step) = S ((S (bcf_index_lucas_block_digit_division_upper_normal_table_row_step)) * bcf_row_scale_lucas_block_digit_division_upper_normal_table)) /\ exists bcf_quotient_lucas_block_digit_division_upper_normal_table_row_step_entry. bcf_row_code_lucas_block_digit_division_upper_normal_table = bcf_quotient_lucas_block_digit_division_upper_normal_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_division_upper_normal_table_row_step)) * bcf_row_scale_lucas_block_digit_division_upper_normal_table) + (bcf_value_lucas_block_digit_division_upper_normal_table_row_step))) /\ ((bcf_index_lucas_block_digit_division_upper_normal_table_row_step = 0 /\ bcf_value_lucas_block_digit_division_upper_normal_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_division_upper_normal_table_row_step bcf_left_lucas_block_digit_division_upper_normal_table_row_step bcf_right_lucas_block_digit_division_upper_normal_table_row_step. bcf_index_lucas_block_digit_division_upper_normal_table_row_step = S bcf_predecessor_lucas_block_digit_division_upper_normal_table_row_step /\ ((((exists bcf_height_lucas_block_digit_division_upper_normal_table_row_step_previous_left. bcf_height_lucas_block_digit_division_upper_normal_table_row_step_previous_left + S (bcf_left_lucas_block_digit_division_upper_normal_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_division_upper_normal_table_row_step)) * bcf_previous_scale_lucas_block_digit_division_upper_normal_table)) /\ exists bcf_quotient_lucas_block_digit_division_upper_normal_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_division_upper_normal_table = bcf_quotient_lucas_block_digit_division_upper_normal_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_division_upper_normal_table_row_step)) * bcf_previous_scale_lucas_block_digit_division_upper_normal_table) + (bcf_left_lucas_block_digit_division_upper_normal_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_division_upper_normal_table_row_step_previous_right. bcf_height_lucas_block_digit_division_upper_normal_table_row_step_previous_right + S (bcf_right_lucas_block_digit_division_upper_normal_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_division_upper_normal_table_row_step))) * bcf_previous_scale_lucas_block_digit_division_upper_normal_table)) /\ exists bcf_quotient_lucas_block_digit_division_upper_normal_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_division_upper_normal_table = bcf_quotient_lucas_block_digit_division_upper_normal_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_division_upper_normal_table_row_step))) * bcf_previous_scale_lucas_block_digit_division_upper_normal_table) + (bcf_right_lucas_block_digit_division_upper_normal_table_row_step))) /\ bcf_value_lucas_block_digit_division_upper_normal_table_row_step = bcf_left_lucas_block_digit_division_upper_normal_table_row_step + bcf_right_lucas_block_digit_division_upper_normal_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_division_upper_normal_decoded_row_code. bcf_height_lucas_block_digit_division_upper_normal_decoded_row_code + S (bcf_row_code_lucas_block_digit_division_upper_normal) = S ((S (p * q + d)) * bcf_row_code_scale_lucas_block_digit_division_upper_normal)) /\ exists bcf_quotient_lucas_block_digit_division_upper_normal_decoded_row_code. bcf_row_code_code_lucas_block_digit_division_upper_normal = bcf_quotient_lucas_block_digit_division_upper_normal_decoded_row_code * S ((S (p * q + d)) * bcf_row_code_scale_lucas_block_digit_division_upper_normal) + (bcf_row_code_lucas_block_digit_division_upper_normal))) /\ ((((exists bcf_height_lucas_block_digit_division_upper_normal_decoded_row_scale. bcf_height_lucas_block_digit_division_upper_normal_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_division_upper_normal) = S ((S (p * q + d)) * bcf_row_scale_scale_lucas_block_digit_division_upper_normal)) /\ exists bcf_quotient_lucas_block_digit_division_upper_normal_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_division_upper_normal = bcf_quotient_lucas_block_digit_division_upper_normal_decoded_row_scale * S ((S (p * q + d)) * bcf_row_scale_scale_lucas_block_digit_division_upper_normal) + (bcf_row_scale_lucas_block_digit_division_upper_normal))) /\ (((exists bcf_height_lucas_block_digit_division_upper_normal_decoded_value. bcf_height_lucas_block_digit_division_upper_normal_decoded_value + S (C) = S ((S (k)) * bcf_row_scale_lucas_block_digit_division_upper_normal)) /\ exists bcf_quotient_lucas_block_digit_division_upper_normal_decoded_value. bcf_row_code_lucas_block_digit_division_upper_normal = bcf_quotient_lucas_block_digit_division_upper_normal_decoded_value * S ((S (k)) * bcf_row_scale_lucas_block_digit_division_upper_normal) + (C))))))))
  20. 0020specialize choose_upper_eq_transport n
  21. 0021specialize choose_upper_eq_transport (p * q + d)
  22. 0022specialize choose_upper_eq_transport k
  23. 0023specialize choose_upper_eq_transport C
  24. 0024apply choose_upper_eq_transport
  25. 0025exact hn
  26. 0026exact hwhole
  27. 0027have hcanonical : Choose(p · q + d,p · r + e,C)
    Exact native replay linehave hcanonical : ((exists bcf_lt_gap_lucas_block_digit_division_canonical_out_of_range. bcf_lt_gap_lucas_block_digit_division_canonical_out_of_range + S (p * q + d) = p * r + e) /\ C = 0) \/ ((exists bcf_le_gap_lucas_block_digit_division_canonical_in_range. bcf_le_gap_lucas_block_digit_division_canonical_in_range + (p * r + e) = p * q + d) /\ (exists bcf_row_code_code_lucas_block_digit_division_canonical bcf_row_code_scale_lucas_block_digit_division_canonical bcf_row_scale_code_lucas_block_digit_division_canonical bcf_row_scale_scale_lucas_block_digit_division_canonical bcf_row_code_lucas_block_digit_division_canonical bcf_row_scale_lucas_block_digit_division_canonical. ((forall bcf_row_index_lucas_block_digit_division_canonical_table. (exists bcf_lt_gap_lucas_block_digit_division_canonical_table_row_bound. bcf_lt_gap_lucas_block_digit_division_canonical_table_row_bound + S (bcf_row_index_lucas_block_digit_division_canonical_table) = S (p * q + d)) -> exists bcf_row_code_lucas_block_digit_division_canonical_table bcf_row_scale_lucas_block_digit_division_canonical_table. ((((exists bcf_height_lucas_block_digit_division_canonical_table_decoded_row_code. bcf_height_lucas_block_digit_division_canonical_table_decoded_row_code + S (bcf_row_code_lucas_block_digit_division_canonical_table) = S ((S (bcf_row_index_lucas_block_digit_division_canonical_table)) * bcf_row_code_scale_lucas_block_digit_division_canonical)) /\ exists bcf_quotient_lucas_block_digit_division_canonical_table_decoded_row_code. bcf_row_code_code_lucas_block_digit_division_canonical = bcf_quotient_lucas_block_digit_division_canonical_table_decoded_row_code * S ((S (bcf_row_index_lucas_block_digit_division_canonical_table)) * bcf_row_code_scale_lucas_block_digit_division_canonical) + (bcf_row_code_lucas_block_digit_division_canonical_table))) /\ ((((exists bcf_height_lucas_block_digit_division_canonical_table_decoded_row_scale. bcf_height_lucas_block_digit_division_canonical_table_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_division_canonical_table) = S ((S (bcf_row_index_lucas_block_digit_division_canonical_table)) * bcf_row_scale_scale_lucas_block_digit_division_canonical)) /\ exists bcf_quotient_lucas_block_digit_division_canonical_table_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_division_canonical = bcf_quotient_lucas_block_digit_division_canonical_table_decoded_row_scale * S ((S (bcf_row_index_lucas_block_digit_division_canonical_table)) * bcf_row_scale_scale_lucas_block_digit_division_canonical) + (bcf_row_scale_lucas_block_digit_division_canonical_table))) /\ ((bcf_row_index_lucas_block_digit_division_canonical_table = 0 /\ (forall bcf_index_lucas_block_digit_division_canonical_table_zero_row. (exists bcf_lt_gap_lucas_block_digit_division_canonical_table_zero_row_bound. bcf_lt_gap_lucas_block_digit_division_canonical_table_zero_row_bound + S (bcf_index_lucas_block_digit_division_canonical_table_zero_row) = S (p * q + d)) -> exists bcf_value_lucas_block_digit_division_canonical_table_zero_row. ((((exists bcf_height_lucas_block_digit_division_canonical_table_zero_row_entry. bcf_height_lucas_block_digit_division_canonical_table_zero_row_entry + S (bcf_value_lucas_block_digit_division_canonical_table_zero_row) = S ((S (bcf_index_lucas_block_digit_division_canonical_table_zero_row)) * bcf_row_scale_lucas_block_digit_division_canonical_table)) /\ exists bcf_quotient_lucas_block_digit_division_canonical_table_zero_row_entry. bcf_row_code_lucas_block_digit_division_canonical_table = bcf_quotient_lucas_block_digit_division_canonical_table_zero_row_entry * S ((S (bcf_index_lucas_block_digit_division_canonical_table_zero_row)) * bcf_row_scale_lucas_block_digit_division_canonical_table) + (bcf_value_lucas_block_digit_division_canonical_table_zero_row))) /\ ((bcf_index_lucas_block_digit_division_canonical_table_zero_row = 0 /\ bcf_value_lucas_block_digit_division_canonical_table_zero_row = 1) \/ exists bcf_predecessor_lucas_block_digit_division_canonical_table_zero_row. bcf_index_lucas_block_digit_division_canonical_table_zero_row = S bcf_predecessor_lucas_block_digit_division_canonical_table_zero_row /\ bcf_value_lucas_block_digit_division_canonical_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_block_digit_division_canonical_table bcf_previous_code_lucas_block_digit_division_canonical_table bcf_previous_scale_lucas_block_digit_division_canonical_table. bcf_row_index_lucas_block_digit_division_canonical_table = S bcf_predecessor_lucas_block_digit_division_canonical_table /\ ((((exists bcf_height_lucas_block_digit_division_canonical_table_decoded_previous_code. bcf_height_lucas_block_digit_division_canonical_table_decoded_previous_code + S (bcf_previous_code_lucas_block_digit_division_canonical_table) = S ((S (bcf_predecessor_lucas_block_digit_division_canonical_table)) * bcf_row_code_scale_lucas_block_digit_division_canonical)) /\ exists bcf_quotient_lucas_block_digit_division_canonical_table_decoded_previous_code. bcf_row_code_code_lucas_block_digit_division_canonical = bcf_quotient_lucas_block_digit_division_canonical_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_block_digit_division_canonical_table)) * bcf_row_code_scale_lucas_block_digit_division_canonical) + (bcf_previous_code_lucas_block_digit_division_canonical_table))) /\ ((((exists bcf_height_lucas_block_digit_division_canonical_table_decoded_previous_scale. bcf_height_lucas_block_digit_division_canonical_table_decoded_previous_scale + S (bcf_previous_scale_lucas_block_digit_division_canonical_table) = S ((S (bcf_predecessor_lucas_block_digit_division_canonical_table)) * bcf_row_scale_scale_lucas_block_digit_division_canonical)) /\ exists bcf_quotient_lucas_block_digit_division_canonical_table_decoded_previous_scale. bcf_row_scale_code_lucas_block_digit_division_canonical = bcf_quotient_lucas_block_digit_division_canonical_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_block_digit_division_canonical_table)) * bcf_row_scale_scale_lucas_block_digit_division_canonical) + (bcf_previous_scale_lucas_block_digit_division_canonical_table))) /\ (forall bcf_index_lucas_block_digit_division_canonical_table_row_step. (exists bcf_lt_gap_lucas_block_digit_division_canonical_table_row_step_bound. bcf_lt_gap_lucas_block_digit_division_canonical_table_row_step_bound + S (bcf_index_lucas_block_digit_division_canonical_table_row_step) = S (p * q + d)) -> exists bcf_value_lucas_block_digit_division_canonical_table_row_step. ((((exists bcf_height_lucas_block_digit_division_canonical_table_row_step_entry. bcf_height_lucas_block_digit_division_canonical_table_row_step_entry + S (bcf_value_lucas_block_digit_division_canonical_table_row_step) = S ((S (bcf_index_lucas_block_digit_division_canonical_table_row_step)) * bcf_row_scale_lucas_block_digit_division_canonical_table)) /\ exists bcf_quotient_lucas_block_digit_division_canonical_table_row_step_entry. bcf_row_code_lucas_block_digit_division_canonical_table = bcf_quotient_lucas_block_digit_division_canonical_table_row_step_entry * S ((S (bcf_index_lucas_block_digit_division_canonical_table_row_step)) * bcf_row_scale_lucas_block_digit_division_canonical_table) + (bcf_value_lucas_block_digit_division_canonical_table_row_step))) /\ ((bcf_index_lucas_block_digit_division_canonical_table_row_step = 0 /\ bcf_value_lucas_block_digit_division_canonical_table_row_step = 1) \/ exists bcf_predecessor_lucas_block_digit_division_canonical_table_row_step bcf_left_lucas_block_digit_division_canonical_table_row_step bcf_right_lucas_block_digit_division_canonical_table_row_step. bcf_index_lucas_block_digit_division_canonical_table_row_step = S bcf_predecessor_lucas_block_digit_division_canonical_table_row_step /\ ((((exists bcf_height_lucas_block_digit_division_canonical_table_row_step_previous_left. bcf_height_lucas_block_digit_division_canonical_table_row_step_previous_left + S (bcf_left_lucas_block_digit_division_canonical_table_row_step) = S ((S (bcf_predecessor_lucas_block_digit_division_canonical_table_row_step)) * bcf_previous_scale_lucas_block_digit_division_canonical_table)) /\ exists bcf_quotient_lucas_block_digit_division_canonical_table_row_step_previous_left. bcf_previous_code_lucas_block_digit_division_canonical_table = bcf_quotient_lucas_block_digit_division_canonical_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_block_digit_division_canonical_table_row_step)) * bcf_previous_scale_lucas_block_digit_division_canonical_table) + (bcf_left_lucas_block_digit_division_canonical_table_row_step))) /\ ((((exists bcf_height_lucas_block_digit_division_canonical_table_row_step_previous_right. bcf_height_lucas_block_digit_division_canonical_table_row_step_previous_right + S (bcf_right_lucas_block_digit_division_canonical_table_row_step) = S ((S (S (bcf_predecessor_lucas_block_digit_division_canonical_table_row_step))) * bcf_previous_scale_lucas_block_digit_division_canonical_table)) /\ exists bcf_quotient_lucas_block_digit_division_canonical_table_row_step_previous_right. bcf_previous_code_lucas_block_digit_division_canonical_table = bcf_quotient_lucas_block_digit_division_canonical_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_block_digit_division_canonical_table_row_step))) * bcf_previous_scale_lucas_block_digit_division_canonical_table) + (bcf_right_lucas_block_digit_division_canonical_table_row_step))) /\ bcf_value_lucas_block_digit_division_canonical_table_row_step = bcf_left_lucas_block_digit_division_canonical_table_row_step + bcf_right_lucas_block_digit_division_canonical_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_block_digit_division_canonical_decoded_row_code. bcf_height_lucas_block_digit_division_canonical_decoded_row_code + S (bcf_row_code_lucas_block_digit_division_canonical) = S ((S (p * q + d)) * bcf_row_code_scale_lucas_block_digit_division_canonical)) /\ exists bcf_quotient_lucas_block_digit_division_canonical_decoded_row_code. bcf_row_code_code_lucas_block_digit_division_canonical = bcf_quotient_lucas_block_digit_division_canonical_decoded_row_code * S ((S (p * q + d)) * bcf_row_code_scale_lucas_block_digit_division_canonical) + (bcf_row_code_lucas_block_digit_division_canonical))) /\ ((((exists bcf_height_lucas_block_digit_division_canonical_decoded_row_scale. bcf_height_lucas_block_digit_division_canonical_decoded_row_scale + S (bcf_row_scale_lucas_block_digit_division_canonical) = S ((S (p * q + d)) * bcf_row_scale_scale_lucas_block_digit_division_canonical)) /\ exists bcf_quotient_lucas_block_digit_division_canonical_decoded_row_scale. bcf_row_scale_code_lucas_block_digit_division_canonical = bcf_quotient_lucas_block_digit_division_canonical_decoded_row_scale * S ((S (p * q + d)) * bcf_row_scale_scale_lucas_block_digit_division_canonical) + (bcf_row_scale_lucas_block_digit_division_canonical))) /\ (((exists bcf_height_lucas_block_digit_division_canonical_decoded_value. bcf_height_lucas_block_digit_division_canonical_decoded_value + S (C) = S ((S (p * r + e)) * bcf_row_scale_lucas_block_digit_division_canonical)) /\ exists bcf_quotient_lucas_block_digit_division_canonical_decoded_value. bcf_row_code_lucas_block_digit_division_canonical = bcf_quotient_lucas_block_digit_division_canonical_decoded_value * S ((S (p * r + e)) * bcf_row_scale_lucas_block_digit_division_canonical) + (C))))))))
  28. 0028specialize lucas_choose_lower_eq_transport (p * q + d)
  29. 0029specialize lucas_choose_lower_eq_transport k
  30. 0030specialize lucas_choose_lower_eq_transport (p * r + e)
  31. 0031specialize lucas_choose_lower_eq_transport C
  32. 0032apply lucas_choose_lower_eq_transport
  33. 0033exact hk
  34. 0034exact hupper
  35. 0035specialize lucas_prime_block_digit_congruence p
  36. 0036specialize lucas_prime_block_digit_congruence q
  37. 0037specialize lucas_prime_block_digit_congruence r
  38. 0038specialize lucas_prime_block_digit_congruence d
  39. 0039specialize lucas_prime_block_digit_congruence e
  40. 0040specialize lucas_prime_block_digit_congruence C
  41. 0041specialize lucas_prime_block_digit_congruence A
  42. 0042specialize lucas_prime_block_digit_congruence B
  43. 0043apply lucas_prime_block_digit_congruence
  44. 0044exact hprime
  45. 0045exact hdigit
  46. 0046exact he_digit
  47. 0047exact hcanonical
  48. 0048exact hquotient
  49. 0049exact hfactor