LU0012

lucas_repeated_prime_shift_below_base

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

Every below-base binomial column is invariant modulo a prime under an arbitrary number of prime-row shifts.

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 q a b C D. ((~(p = 1) /\ forall frm_prime_left_lucas_low_digit_prime frm_prime_right_lucas_low_digit_prime. p = frm_prime_left_lucas_low_digit_prime * frm_prime_right_lucas_low_digit_prime -> frm_prime_left_lucas_low_digit_prime = 1 \/ frm_prime_right_lucas_low_digit_prime = 1)) -> (exists lld_gap_repeat_bound. lld_gap_repeat_bound + S (b) = (p)) -> (((exists bcf_lt_gap_lucas_low_digit_repeat_upper_out_of_range. bcf_lt_gap_lucas_low_digit_repeat_upper_out_of_range + S (p * q + a) = b) /\ C = 0) \/ ((exists bcf_le_gap_lucas_low_digit_repeat_upper_in_range. bcf_le_gap_lucas_low_digit_repeat_upper_in_range + (b) = p * q + a) /\ (exists bcf_row_code_code_lucas_low_digit_repeat_upper bcf_row_code_scale_lucas_low_digit_repeat_upper bcf_row_scale_code_lucas_low_digit_repeat_upper bcf_row_scale_scale_lucas_low_digit_repeat_upper bcf_row_code_lucas_low_digit_repeat_upper bcf_row_scale_lucas_low_digit_repeat_upper. ((forall bcf_row_index_lucas_low_digit_repeat_upper_table. (exists bcf_lt_gap_lucas_low_digit_repeat_upper_table_row_bound. bcf_lt_gap_lucas_low_digit_repeat_upper_table_row_bound + S (bcf_row_index_lucas_low_digit_repeat_upper_table) = S (p * q + a)) -> exists bcf_row_code_lucas_low_digit_repeat_upper_table bcf_row_scale_lucas_low_digit_repeat_upper_table. ((((exists bcf_height_lucas_low_digit_repeat_upper_table_decoded_row_code. bcf_height_lucas_low_digit_repeat_upper_table_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_upper_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_upper_table)) * bcf_row_code_scale_lucas_low_digit_repeat_upper)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_upper = bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_row_code * S ((S (bcf_row_index_lucas_low_digit_repeat_upper_table)) * bcf_row_code_scale_lucas_low_digit_repeat_upper) + (bcf_row_code_lucas_low_digit_repeat_upper_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_upper_table_decoded_row_scale. bcf_height_lucas_low_digit_repeat_upper_table_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_upper_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_upper_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_upper)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_upper = bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_row_scale * S ((S (bcf_row_index_lucas_low_digit_repeat_upper_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_upper) + (bcf_row_scale_lucas_low_digit_repeat_upper_table))) /\ ((bcf_row_index_lucas_low_digit_repeat_upper_table = 0 /\ (forall bcf_index_lucas_low_digit_repeat_upper_table_zero_row. (exists bcf_lt_gap_lucas_low_digit_repeat_upper_table_zero_row_bound. bcf_lt_gap_lucas_low_digit_repeat_upper_table_zero_row_bound + S (bcf_index_lucas_low_digit_repeat_upper_table_zero_row) = S (p * q + a)) -> exists bcf_value_lucas_low_digit_repeat_upper_table_zero_row. ((((exists bcf_height_lucas_low_digit_repeat_upper_table_zero_row_entry. bcf_height_lucas_low_digit_repeat_upper_table_zero_row_entry + S (bcf_value_lucas_low_digit_repeat_upper_table_zero_row) = S ((S (bcf_index_lucas_low_digit_repeat_upper_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_upper_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_zero_row_entry. bcf_row_code_lucas_low_digit_repeat_upper_table = bcf_quotient_lucas_low_digit_repeat_upper_table_zero_row_entry * S ((S (bcf_index_lucas_low_digit_repeat_upper_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_upper_table) + (bcf_value_lucas_low_digit_repeat_upper_table_zero_row))) /\ ((bcf_index_lucas_low_digit_repeat_upper_table_zero_row = 0 /\ bcf_value_lucas_low_digit_repeat_upper_table_zero_row = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_upper_table_zero_row. bcf_index_lucas_low_digit_repeat_upper_table_zero_row = S bcf_predecessor_lucas_low_digit_repeat_upper_table_zero_row /\ bcf_value_lucas_low_digit_repeat_upper_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_low_digit_repeat_upper_table bcf_previous_code_lucas_low_digit_repeat_upper_table bcf_previous_scale_lucas_low_digit_repeat_upper_table. bcf_row_index_lucas_low_digit_repeat_upper_table = S bcf_predecessor_lucas_low_digit_repeat_upper_table /\ ((((exists bcf_height_lucas_low_digit_repeat_upper_table_decoded_previous_code. bcf_height_lucas_low_digit_repeat_upper_table_decoded_previous_code + S (bcf_previous_code_lucas_low_digit_repeat_upper_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_upper_table)) * bcf_row_code_scale_lucas_low_digit_repeat_upper)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_previous_code. bcf_row_code_code_lucas_low_digit_repeat_upper = bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_low_digit_repeat_upper_table)) * bcf_row_code_scale_lucas_low_digit_repeat_upper) + (bcf_previous_code_lucas_low_digit_repeat_upper_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_upper_table_decoded_previous_scale. bcf_height_lucas_low_digit_repeat_upper_table_decoded_previous_scale + S (bcf_previous_scale_lucas_low_digit_repeat_upper_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_upper_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_upper)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_previous_scale. bcf_row_scale_code_lucas_low_digit_repeat_upper = bcf_quotient_lucas_low_digit_repeat_upper_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_low_digit_repeat_upper_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_upper) + (bcf_previous_scale_lucas_low_digit_repeat_upper_table))) /\ (forall bcf_index_lucas_low_digit_repeat_upper_table_row_step. (exists bcf_lt_gap_lucas_low_digit_repeat_upper_table_row_step_bound. bcf_lt_gap_lucas_low_digit_repeat_upper_table_row_step_bound + S (bcf_index_lucas_low_digit_repeat_upper_table_row_step) = S (p * q + a)) -> exists bcf_value_lucas_low_digit_repeat_upper_table_row_step. ((((exists bcf_height_lucas_low_digit_repeat_upper_table_row_step_entry. bcf_height_lucas_low_digit_repeat_upper_table_row_step_entry + S (bcf_value_lucas_low_digit_repeat_upper_table_row_step) = S ((S (bcf_index_lucas_low_digit_repeat_upper_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_upper_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_row_step_entry. bcf_row_code_lucas_low_digit_repeat_upper_table = bcf_quotient_lucas_low_digit_repeat_upper_table_row_step_entry * S ((S (bcf_index_lucas_low_digit_repeat_upper_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_upper_table) + (bcf_value_lucas_low_digit_repeat_upper_table_row_step))) /\ ((bcf_index_lucas_low_digit_repeat_upper_table_row_step = 0 /\ bcf_value_lucas_low_digit_repeat_upper_table_row_step = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_upper_table_row_step bcf_left_lucas_low_digit_repeat_upper_table_row_step bcf_right_lucas_low_digit_repeat_upper_table_row_step. bcf_index_lucas_low_digit_repeat_upper_table_row_step = S bcf_predecessor_lucas_low_digit_repeat_upper_table_row_step /\ ((((exists bcf_height_lucas_low_digit_repeat_upper_table_row_step_previous_left. bcf_height_lucas_low_digit_repeat_upper_table_row_step_previous_left + S (bcf_left_lucas_low_digit_repeat_upper_table_row_step) = S ((S (bcf_predecessor_lucas_low_digit_repeat_upper_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_upper_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_row_step_previous_left. bcf_previous_code_lucas_low_digit_repeat_upper_table = bcf_quotient_lucas_low_digit_repeat_upper_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_low_digit_repeat_upper_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_upper_table) + (bcf_left_lucas_low_digit_repeat_upper_table_row_step))) /\ ((((exists bcf_height_lucas_low_digit_repeat_upper_table_row_step_previous_right. bcf_height_lucas_low_digit_repeat_upper_table_row_step_previous_right + S (bcf_right_lucas_low_digit_repeat_upper_table_row_step) = S ((S (S (bcf_predecessor_lucas_low_digit_repeat_upper_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_upper_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_table_row_step_previous_right. bcf_previous_code_lucas_low_digit_repeat_upper_table = bcf_quotient_lucas_low_digit_repeat_upper_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_low_digit_repeat_upper_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_upper_table) + (bcf_right_lucas_low_digit_repeat_upper_table_row_step))) /\ bcf_value_lucas_low_digit_repeat_upper_table_row_step = bcf_left_lucas_low_digit_repeat_upper_table_row_step + bcf_right_lucas_low_digit_repeat_upper_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_low_digit_repeat_upper_decoded_row_code. bcf_height_lucas_low_digit_repeat_upper_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_upper) = S ((S (p * q + a)) * bcf_row_code_scale_lucas_low_digit_repeat_upper)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_upper = bcf_quotient_lucas_low_digit_repeat_upper_decoded_row_code * S ((S (p * q + a)) * bcf_row_code_scale_lucas_low_digit_repeat_upper) + (bcf_row_code_lucas_low_digit_repeat_upper))) /\ ((((exists bcf_height_lucas_low_digit_repeat_upper_decoded_row_scale. bcf_height_lucas_low_digit_repeat_upper_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_upper) = S ((S (p * q + a)) * bcf_row_scale_scale_lucas_low_digit_repeat_upper)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_upper = bcf_quotient_lucas_low_digit_repeat_upper_decoded_row_scale * S ((S (p * q + a)) * bcf_row_scale_scale_lucas_low_digit_repeat_upper) + (bcf_row_scale_lucas_low_digit_repeat_upper))) /\ (((exists bcf_height_lucas_low_digit_repeat_upper_decoded_value. bcf_height_lucas_low_digit_repeat_upper_decoded_value + S (C) = S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_upper)) /\ exists bcf_quotient_lucas_low_digit_repeat_upper_decoded_value. bcf_row_code_lucas_low_digit_repeat_upper = bcf_quotient_lucas_low_digit_repeat_upper_decoded_value * S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_upper) + (C))))))))) -> (((exists bcf_lt_gap_lucas_low_digit_repeat_lower_out_of_range. bcf_lt_gap_lucas_low_digit_repeat_lower_out_of_range + S (a) = b) /\ D = 0) \/ ((exists bcf_le_gap_lucas_low_digit_repeat_lower_in_range. bcf_le_gap_lucas_low_digit_repeat_lower_in_range + (b) = a) /\ (exists bcf_row_code_code_lucas_low_digit_repeat_lower bcf_row_code_scale_lucas_low_digit_repeat_lower bcf_row_scale_code_lucas_low_digit_repeat_lower bcf_row_scale_scale_lucas_low_digit_repeat_lower bcf_row_code_lucas_low_digit_repeat_lower bcf_row_scale_lucas_low_digit_repeat_lower. ((forall bcf_row_index_lucas_low_digit_repeat_lower_table. (exists bcf_lt_gap_lucas_low_digit_repeat_lower_table_row_bound. bcf_lt_gap_lucas_low_digit_repeat_lower_table_row_bound + S (bcf_row_index_lucas_low_digit_repeat_lower_table) = S (a)) -> exists bcf_row_code_lucas_low_digit_repeat_lower_table bcf_row_scale_lucas_low_digit_repeat_lower_table. ((((exists bcf_height_lucas_low_digit_repeat_lower_table_decoded_row_code. bcf_height_lucas_low_digit_repeat_lower_table_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_lower_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_lower_table)) * bcf_row_code_scale_lucas_low_digit_repeat_lower)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_lower = bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_row_code * S ((S (bcf_row_index_lucas_low_digit_repeat_lower_table)) * bcf_row_code_scale_lucas_low_digit_repeat_lower) + (bcf_row_code_lucas_low_digit_repeat_lower_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_lower_table_decoded_row_scale. bcf_height_lucas_low_digit_repeat_lower_table_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_lower_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_lower_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_lower)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_lower = bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_row_scale * S ((S (bcf_row_index_lucas_low_digit_repeat_lower_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_lower) + (bcf_row_scale_lucas_low_digit_repeat_lower_table))) /\ ((bcf_row_index_lucas_low_digit_repeat_lower_table = 0 /\ (forall bcf_index_lucas_low_digit_repeat_lower_table_zero_row. (exists bcf_lt_gap_lucas_low_digit_repeat_lower_table_zero_row_bound. bcf_lt_gap_lucas_low_digit_repeat_lower_table_zero_row_bound + S (bcf_index_lucas_low_digit_repeat_lower_table_zero_row) = S (a)) -> exists bcf_value_lucas_low_digit_repeat_lower_table_zero_row. ((((exists bcf_height_lucas_low_digit_repeat_lower_table_zero_row_entry. bcf_height_lucas_low_digit_repeat_lower_table_zero_row_entry + S (bcf_value_lucas_low_digit_repeat_lower_table_zero_row) = S ((S (bcf_index_lucas_low_digit_repeat_lower_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_lower_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_zero_row_entry. bcf_row_code_lucas_low_digit_repeat_lower_table = bcf_quotient_lucas_low_digit_repeat_lower_table_zero_row_entry * S ((S (bcf_index_lucas_low_digit_repeat_lower_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_lower_table) + (bcf_value_lucas_low_digit_repeat_lower_table_zero_row))) /\ ((bcf_index_lucas_low_digit_repeat_lower_table_zero_row = 0 /\ bcf_value_lucas_low_digit_repeat_lower_table_zero_row = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_lower_table_zero_row. bcf_index_lucas_low_digit_repeat_lower_table_zero_row = S bcf_predecessor_lucas_low_digit_repeat_lower_table_zero_row /\ bcf_value_lucas_low_digit_repeat_lower_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_low_digit_repeat_lower_table bcf_previous_code_lucas_low_digit_repeat_lower_table bcf_previous_scale_lucas_low_digit_repeat_lower_table. bcf_row_index_lucas_low_digit_repeat_lower_table = S bcf_predecessor_lucas_low_digit_repeat_lower_table /\ ((((exists bcf_height_lucas_low_digit_repeat_lower_table_decoded_previous_code. bcf_height_lucas_low_digit_repeat_lower_table_decoded_previous_code + S (bcf_previous_code_lucas_low_digit_repeat_lower_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_lower_table)) * bcf_row_code_scale_lucas_low_digit_repeat_lower)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_previous_code. bcf_row_code_code_lucas_low_digit_repeat_lower = bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_low_digit_repeat_lower_table)) * bcf_row_code_scale_lucas_low_digit_repeat_lower) + (bcf_previous_code_lucas_low_digit_repeat_lower_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_lower_table_decoded_previous_scale. bcf_height_lucas_low_digit_repeat_lower_table_decoded_previous_scale + S (bcf_previous_scale_lucas_low_digit_repeat_lower_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_lower_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_lower)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_previous_scale. bcf_row_scale_code_lucas_low_digit_repeat_lower = bcf_quotient_lucas_low_digit_repeat_lower_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_low_digit_repeat_lower_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_lower) + (bcf_previous_scale_lucas_low_digit_repeat_lower_table))) /\ (forall bcf_index_lucas_low_digit_repeat_lower_table_row_step. (exists bcf_lt_gap_lucas_low_digit_repeat_lower_table_row_step_bound. bcf_lt_gap_lucas_low_digit_repeat_lower_table_row_step_bound + S (bcf_index_lucas_low_digit_repeat_lower_table_row_step) = S (a)) -> exists bcf_value_lucas_low_digit_repeat_lower_table_row_step. ((((exists bcf_height_lucas_low_digit_repeat_lower_table_row_step_entry. bcf_height_lucas_low_digit_repeat_lower_table_row_step_entry + S (bcf_value_lucas_low_digit_repeat_lower_table_row_step) = S ((S (bcf_index_lucas_low_digit_repeat_lower_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_lower_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_row_step_entry. bcf_row_code_lucas_low_digit_repeat_lower_table = bcf_quotient_lucas_low_digit_repeat_lower_table_row_step_entry * S ((S (bcf_index_lucas_low_digit_repeat_lower_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_lower_table) + (bcf_value_lucas_low_digit_repeat_lower_table_row_step))) /\ ((bcf_index_lucas_low_digit_repeat_lower_table_row_step = 0 /\ bcf_value_lucas_low_digit_repeat_lower_table_row_step = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_lower_table_row_step bcf_left_lucas_low_digit_repeat_lower_table_row_step bcf_right_lucas_low_digit_repeat_lower_table_row_step. bcf_index_lucas_low_digit_repeat_lower_table_row_step = S bcf_predecessor_lucas_low_digit_repeat_lower_table_row_step /\ ((((exists bcf_height_lucas_low_digit_repeat_lower_table_row_step_previous_left. bcf_height_lucas_low_digit_repeat_lower_table_row_step_previous_left + S (bcf_left_lucas_low_digit_repeat_lower_table_row_step) = S ((S (bcf_predecessor_lucas_low_digit_repeat_lower_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_lower_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_row_step_previous_left. bcf_previous_code_lucas_low_digit_repeat_lower_table = bcf_quotient_lucas_low_digit_repeat_lower_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_low_digit_repeat_lower_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_lower_table) + (bcf_left_lucas_low_digit_repeat_lower_table_row_step))) /\ ((((exists bcf_height_lucas_low_digit_repeat_lower_table_row_step_previous_right. bcf_height_lucas_low_digit_repeat_lower_table_row_step_previous_right + S (bcf_right_lucas_low_digit_repeat_lower_table_row_step) = S ((S (S (bcf_predecessor_lucas_low_digit_repeat_lower_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_lower_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_table_row_step_previous_right. bcf_previous_code_lucas_low_digit_repeat_lower_table = bcf_quotient_lucas_low_digit_repeat_lower_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_low_digit_repeat_lower_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_lower_table) + (bcf_right_lucas_low_digit_repeat_lower_table_row_step))) /\ bcf_value_lucas_low_digit_repeat_lower_table_row_step = bcf_left_lucas_low_digit_repeat_lower_table_row_step + bcf_right_lucas_low_digit_repeat_lower_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_low_digit_repeat_lower_decoded_row_code. bcf_height_lucas_low_digit_repeat_lower_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_lower) = S ((S (a)) * bcf_row_code_scale_lucas_low_digit_repeat_lower)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_lower = bcf_quotient_lucas_low_digit_repeat_lower_decoded_row_code * S ((S (a)) * bcf_row_code_scale_lucas_low_digit_repeat_lower) + (bcf_row_code_lucas_low_digit_repeat_lower))) /\ ((((exists bcf_height_lucas_low_digit_repeat_lower_decoded_row_scale. bcf_height_lucas_low_digit_repeat_lower_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_lower) = S ((S (a)) * bcf_row_scale_scale_lucas_low_digit_repeat_lower)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_lower = bcf_quotient_lucas_low_digit_repeat_lower_decoded_row_scale * S ((S (a)) * bcf_row_scale_scale_lucas_low_digit_repeat_lower) + (bcf_row_scale_lucas_low_digit_repeat_lower))) /\ (((exists bcf_height_lucas_low_digit_repeat_lower_decoded_value. bcf_height_lucas_low_digit_repeat_lower_decoded_value + S (D) = S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_lower)) /\ exists bcf_quotient_lucas_low_digit_repeat_lower_decoded_value. bcf_row_code_lucas_low_digit_repeat_lower = bcf_quotient_lucas_low_digit_repeat_lower_decoded_value * S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_lower) + (D))))))))) -> (exists lld_left_repeat_result lld_right_repeat_result. (C) + (p) * lld_left_repeat_result = (D) + (p) * lld_right_repeat_result)

Constructive proof overview

Generated structural guide

Every below-base binomial column is invariant modulo a prime under an arbitrary number of prime-row shifts.

The unchanged tactic script uses 8 declared prerequisites and contains 75 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

Proof neighborhood

Direct dependencies

LU0010 lucas_prime_block_zero_reassociation LU0011 lucas_prime_block_successor_reassociation choose_upper_eq_transport Alpha theorem; checked-use authorized choose_functional Alpha theorem; checked-use authorized mod_eq_refl Stable theorem; checked-use authorized choose_exists Alpha theorem; checked-use authorized LU000W lucas_prime_shift_below_base mod_eq_trans Stable theorem; checked-use authorized

Direct dependents

LU0013 lucas_low_digit_congruence

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

75 script commands · 12 reading checkpoints · 6 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 (3)
lucas prime block zero reassociationlucas prime block successor reassociationlucas prime shift below base

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–1

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

  1. L1
    intro p
02Induction on qL2–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction q
  2. L3
    intro a
  3. L4
    intro b
  4. L5
    intro C
  5. L6
    intro D
  6. L7
    intro hprime
  7. L8
    intro hbound
  8. L9
    intro hupper
  9. L10
    intro hlower
03Establish hnormalizedL11–18

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

  1. L11
    have hnormalized : Choose(a,b,C)Definitions: Choose
  2. L12
    specialize choose_upper_eq_transport (p * 0 + a)
  3. L13
    specialize choose_upper_eq_transport a
  4. L14
    specialize choose_upper_eq_transport b
  5. L15
    specialize choose_upper_eq_transport C
  6. L16
    apply choose_upper_eq_transport
  7. L17
    apply lucas_prime_block_zero_reassociation
  8. L18
    exact hupper
04Establish hequalL19–28

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

  1. L19
    have hequal : C = D
  2. L20
    specialize choose_functional a
  3. L21
    specialize choose_functional b
  4. L22
    specialize choose_functional C
  5. L23
    specialize choose_functional D
  6. L24
    apply choose_functional
  7. L25
    exact hnormalized
  8. L26
    exact hlower
  9. L27
    rewrite hequal
  10. L28
    apply mod_eq_refl
05Fix variables and assumptionsL29–36

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

  1. L29
    intro a
  2. L30
    intro b
  3. L31
    intro C
  4. L32
    intro D
  5. L33
    intro hprime
  6. L34
    intro hbound
  7. L35
    intro hupper
  8. L36
    intro hlower
06Establish hnormalizedL37–44

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

  1. L37
    have hnormalized : Choose(p + (p · q + a),b,C)Definitions: Choose
  2. L38
    specialize choose_upper_eq_transport (p * S q + a)
  3. L39
    specialize choose_upper_eq_transport (p + (p * q + a))
  4. L40
    specialize choose_upper_eq_transport b
  5. L41
    specialize choose_upper_eq_transport C
  6. L42
    apply choose_upper_eq_transport
  7. L43
    apply lucas_prime_block_successor_reassociation
  8. L44
    exact hupper
07Establish hmiddleL45–46

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

  1. L45
    have hmiddle : ∃ D. Choose(p · q + a,b,D)Definitions: Choose
  2. L46
    apply choose_exists
08Separate the logical casesL47–47

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

  1. L47
    cases hmiddle
09Establish hshiftL48–57

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lucas prime shift below base.

  1. L48
    have hshift : exists lld_left_repeat_shift lld_right_repeat_shift. (C) + (p) * lld_left_repeat_shift = (x) + (p) * lld_right_repeat_shift
  2. L49
    specialize lucas_prime_shift_below_base p
  3. L50
    specialize lucas_prime_shift_below_base (p * q + a)
  4. L51
    specialize lucas_prime_shift_below_base b
  5. L52
    specialize lucas_prime_shift_below_base C
  6. L53
    specialize lucas_prime_shift_below_base x
  7. L54
    apply lucas_prime_shift_below_base
  8. L55
    exact hprime
  9. L56
    exact hbound
  10. L57
    exact hnormalized
10Use earlier factsL58–58

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

  1. L58
    exact hmiddle_witness
11Establish hremainingL59–68

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L59
    have hremaining : exists lld_left_repeat_remaining lld_right_repeat_remaining. (x) + (p) * lld_left_repeat_remaining = (D) + (p) * lld_right_repeat_remaining
  2. L60
    specialize IH a
  3. L61
    specialize IH b
  4. L62
    specialize IH x
  5. L63
    specialize IH D
  6. L64
    apply IH
  7. L65
    exact hprime
  8. L66
    exact hbound
  9. L67
    exact hmiddle_witness
  10. L68
    exact hlower
12Use earlier factsL69–75

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

  1. L69
    specialize mod_eq_trans p
  2. L70
    specialize mod_eq_trans C
  3. L71
    specialize mod_eq_trans x
  4. L72
    specialize mod_eq_trans D
  5. L73
    apply mod_eq_trans
  6. L74
    exact hshift
  7. L75
    exact hremaining

Library-wide reading audit

Original exact command ledger · 75 lines
  1. 0001intro p
  2. 0002induction q
  3. 0003intro a
  4. 0004intro b
  5. 0005intro C
  6. 0006intro D
  7. 0007intro hprime
  8. 0008intro hbound
  9. 0009intro hupper
  10. 0010intro hlower
  11. 0011have hnormalized : ((exists bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_out_of_range. bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_out_of_range + S (a) = b) /\ C = 0) \/ ((exists bcf_le_gap_lucas_low_digit_repeat_zero_normalized_in_range. bcf_le_gap_lucas_low_digit_repeat_zero_normalized_in_range + (b) = a) /\ (exists bcf_row_code_code_lucas_low_digit_repeat_zero_normalized bcf_row_code_scale_lucas_low_digit_repeat_zero_normalized bcf_row_scale_code_lucas_low_digit_repeat_zero_normalized bcf_row_scale_scale_lucas_low_digit_repeat_zero_normalized bcf_row_code_lucas_low_digit_repeat_zero_normalized bcf_row_scale_lucas_low_digit_repeat_zero_normalized. ((forall bcf_row_index_lucas_low_digit_repeat_zero_normalized_table. (exists bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_table_row_bound. bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_table_row_bound + S (bcf_row_index_lucas_low_digit_repeat_zero_normalized_table) = S (a)) -> exists bcf_row_code_lucas_low_digit_repeat_zero_normalized_table bcf_row_scale_lucas_low_digit_repeat_zero_normalized_table. ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_row_code. bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_zero_normalized_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_zero_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_zero_normalized = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_row_code * S ((S (bcf_row_index_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_zero_normalized) + (bcf_row_code_lucas_low_digit_repeat_zero_normalized_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_row_scale. bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_zero_normalized_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_zero_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_zero_normalized = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_row_scale * S ((S (bcf_row_index_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_zero_normalized) + (bcf_row_scale_lucas_low_digit_repeat_zero_normalized_table))) /\ ((bcf_row_index_lucas_low_digit_repeat_zero_normalized_table = 0 /\ (forall bcf_index_lucas_low_digit_repeat_zero_normalized_table_zero_row. (exists bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_table_zero_row_bound. bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_table_zero_row_bound + S (bcf_index_lucas_low_digit_repeat_zero_normalized_table_zero_row) = S (a)) -> exists bcf_value_lucas_low_digit_repeat_zero_normalized_table_zero_row. ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_zero_row_entry. bcf_height_lucas_low_digit_repeat_zero_normalized_table_zero_row_entry + S (bcf_value_lucas_low_digit_repeat_zero_normalized_table_zero_row) = S ((S (bcf_index_lucas_low_digit_repeat_zero_normalized_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_zero_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_zero_row_entry. bcf_row_code_lucas_low_digit_repeat_zero_normalized_table = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_zero_row_entry * S ((S (bcf_index_lucas_low_digit_repeat_zero_normalized_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_zero_normalized_table) + (bcf_value_lucas_low_digit_repeat_zero_normalized_table_zero_row))) /\ ((bcf_index_lucas_low_digit_repeat_zero_normalized_table_zero_row = 0 /\ bcf_value_lucas_low_digit_repeat_zero_normalized_table_zero_row = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_zero_row. bcf_index_lucas_low_digit_repeat_zero_normalized_table_zero_row = S bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_zero_row /\ bcf_value_lucas_low_digit_repeat_zero_normalized_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table bcf_previous_code_lucas_low_digit_repeat_zero_normalized_table bcf_previous_scale_lucas_low_digit_repeat_zero_normalized_table. bcf_row_index_lucas_low_digit_repeat_zero_normalized_table = S bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table /\ ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_code. bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_code + S (bcf_previous_code_lucas_low_digit_repeat_zero_normalized_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_zero_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_code. bcf_row_code_code_lucas_low_digit_repeat_zero_normalized = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_zero_normalized) + (bcf_previous_code_lucas_low_digit_repeat_zero_normalized_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_scale. bcf_height_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_scale + S (bcf_previous_scale_lucas_low_digit_repeat_zero_normalized_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_zero_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_scale. bcf_row_scale_code_lucas_low_digit_repeat_zero_normalized = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_zero_normalized) + (bcf_previous_scale_lucas_low_digit_repeat_zero_normalized_table))) /\ (forall bcf_index_lucas_low_digit_repeat_zero_normalized_table_row_step. (exists bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_table_row_step_bound. bcf_lt_gap_lucas_low_digit_repeat_zero_normalized_table_row_step_bound + S (bcf_index_lucas_low_digit_repeat_zero_normalized_table_row_step) = S (a)) -> exists bcf_value_lucas_low_digit_repeat_zero_normalized_table_row_step. ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_row_step_entry. bcf_height_lucas_low_digit_repeat_zero_normalized_table_row_step_entry + S (bcf_value_lucas_low_digit_repeat_zero_normalized_table_row_step) = S ((S (bcf_index_lucas_low_digit_repeat_zero_normalized_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_zero_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_row_step_entry. bcf_row_code_lucas_low_digit_repeat_zero_normalized_table = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_row_step_entry * S ((S (bcf_index_lucas_low_digit_repeat_zero_normalized_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_zero_normalized_table) + (bcf_value_lucas_low_digit_repeat_zero_normalized_table_row_step))) /\ ((bcf_index_lucas_low_digit_repeat_zero_normalized_table_row_step = 0 /\ bcf_value_lucas_low_digit_repeat_zero_normalized_table_row_step = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_row_step bcf_left_lucas_low_digit_repeat_zero_normalized_table_row_step bcf_right_lucas_low_digit_repeat_zero_normalized_table_row_step. bcf_index_lucas_low_digit_repeat_zero_normalized_table_row_step = S bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_row_step /\ ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_left. bcf_height_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_left + S (bcf_left_lucas_low_digit_repeat_zero_normalized_table_row_step) = S ((S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_zero_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_left. bcf_previous_code_lucas_low_digit_repeat_zero_normalized_table = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_zero_normalized_table) + (bcf_left_lucas_low_digit_repeat_zero_normalized_table_row_step))) /\ ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_right. bcf_height_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_right + S (bcf_right_lucas_low_digit_repeat_zero_normalized_table_row_step) = S ((S (S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_zero_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_right. bcf_previous_code_lucas_low_digit_repeat_zero_normalized_table = bcf_quotient_lucas_low_digit_repeat_zero_normalized_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_low_digit_repeat_zero_normalized_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_zero_normalized_table) + (bcf_right_lucas_low_digit_repeat_zero_normalized_table_row_step))) /\ bcf_value_lucas_low_digit_repeat_zero_normalized_table_row_step = bcf_left_lucas_low_digit_repeat_zero_normalized_table_row_step + bcf_right_lucas_low_digit_repeat_zero_normalized_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_decoded_row_code. bcf_height_lucas_low_digit_repeat_zero_normalized_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_zero_normalized) = S ((S (a)) * bcf_row_code_scale_lucas_low_digit_repeat_zero_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_zero_normalized = bcf_quotient_lucas_low_digit_repeat_zero_normalized_decoded_row_code * S ((S (a)) * bcf_row_code_scale_lucas_low_digit_repeat_zero_normalized) + (bcf_row_code_lucas_low_digit_repeat_zero_normalized))) /\ ((((exists bcf_height_lucas_low_digit_repeat_zero_normalized_decoded_row_scale. bcf_height_lucas_low_digit_repeat_zero_normalized_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_zero_normalized) = S ((S (a)) * bcf_row_scale_scale_lucas_low_digit_repeat_zero_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_zero_normalized = bcf_quotient_lucas_low_digit_repeat_zero_normalized_decoded_row_scale * S ((S (a)) * bcf_row_scale_scale_lucas_low_digit_repeat_zero_normalized) + (bcf_row_scale_lucas_low_digit_repeat_zero_normalized))) /\ (((exists bcf_height_lucas_low_digit_repeat_zero_normalized_decoded_value. bcf_height_lucas_low_digit_repeat_zero_normalized_decoded_value + S (C) = S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_zero_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_zero_normalized_decoded_value. bcf_row_code_lucas_low_digit_repeat_zero_normalized = bcf_quotient_lucas_low_digit_repeat_zero_normalized_decoded_value * S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_zero_normalized) + (C))))))))
  12. 0012specialize choose_upper_eq_transport (p * 0 + a)
  13. 0013specialize choose_upper_eq_transport a
  14. 0014specialize choose_upper_eq_transport b
  15. 0015specialize choose_upper_eq_transport C
  16. 0016apply choose_upper_eq_transport
  17. 0017apply lucas_prime_block_zero_reassociation
  18. 0018exact hupper
  19. 0019have hequal : C = D
  20. 0020specialize choose_functional a
  21. 0021specialize choose_functional b
  22. 0022specialize choose_functional C
  23. 0023specialize choose_functional D
  24. 0024apply choose_functional
  25. 0025exact hnormalized
  26. 0026exact hlower
  27. 0027rewrite hequal
  28. 0028apply mod_eq_refl
  29. 0029intro a
  30. 0030intro b
  31. 0031intro C
  32. 0032intro D
  33. 0033intro hprime
  34. 0034intro hbound
  35. 0035intro hupper
  36. 0036intro hlower
  37. 0037have hnormalized : ((exists bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_out_of_range. bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_out_of_range + S (p + (p * q + a)) = b) /\ C = 0) \/ ((exists bcf_le_gap_lucas_low_digit_repeat_successor_normalized_in_range. bcf_le_gap_lucas_low_digit_repeat_successor_normalized_in_range + (b) = p + (p * q + a)) /\ (exists bcf_row_code_code_lucas_low_digit_repeat_successor_normalized bcf_row_code_scale_lucas_low_digit_repeat_successor_normalized bcf_row_scale_code_lucas_low_digit_repeat_successor_normalized bcf_row_scale_scale_lucas_low_digit_repeat_successor_normalized bcf_row_code_lucas_low_digit_repeat_successor_normalized bcf_row_scale_lucas_low_digit_repeat_successor_normalized. ((forall bcf_row_index_lucas_low_digit_repeat_successor_normalized_table. (exists bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_table_row_bound. bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_table_row_bound + S (bcf_row_index_lucas_low_digit_repeat_successor_normalized_table) = S (p + (p * q + a))) -> exists bcf_row_code_lucas_low_digit_repeat_successor_normalized_table bcf_row_scale_lucas_low_digit_repeat_successor_normalized_table. ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_row_code. bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_successor_normalized_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_successor_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_successor_normalized = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_row_code * S ((S (bcf_row_index_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_successor_normalized) + (bcf_row_code_lucas_low_digit_repeat_successor_normalized_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_row_scale. bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_successor_normalized_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_successor_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_successor_normalized = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_row_scale * S ((S (bcf_row_index_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_successor_normalized) + (bcf_row_scale_lucas_low_digit_repeat_successor_normalized_table))) /\ ((bcf_row_index_lucas_low_digit_repeat_successor_normalized_table = 0 /\ (forall bcf_index_lucas_low_digit_repeat_successor_normalized_table_zero_row. (exists bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_table_zero_row_bound. bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_table_zero_row_bound + S (bcf_index_lucas_low_digit_repeat_successor_normalized_table_zero_row) = S (p + (p * q + a))) -> exists bcf_value_lucas_low_digit_repeat_successor_normalized_table_zero_row. ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_zero_row_entry. bcf_height_lucas_low_digit_repeat_successor_normalized_table_zero_row_entry + S (bcf_value_lucas_low_digit_repeat_successor_normalized_table_zero_row) = S ((S (bcf_index_lucas_low_digit_repeat_successor_normalized_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_successor_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_zero_row_entry. bcf_row_code_lucas_low_digit_repeat_successor_normalized_table = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_zero_row_entry * S ((S (bcf_index_lucas_low_digit_repeat_successor_normalized_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_successor_normalized_table) + (bcf_value_lucas_low_digit_repeat_successor_normalized_table_zero_row))) /\ ((bcf_index_lucas_low_digit_repeat_successor_normalized_table_zero_row = 0 /\ bcf_value_lucas_low_digit_repeat_successor_normalized_table_zero_row = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_zero_row. bcf_index_lucas_low_digit_repeat_successor_normalized_table_zero_row = S bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_zero_row /\ bcf_value_lucas_low_digit_repeat_successor_normalized_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table bcf_previous_code_lucas_low_digit_repeat_successor_normalized_table bcf_previous_scale_lucas_low_digit_repeat_successor_normalized_table. bcf_row_index_lucas_low_digit_repeat_successor_normalized_table = S bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table /\ ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_code. bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_code + S (bcf_previous_code_lucas_low_digit_repeat_successor_normalized_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_successor_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_code. bcf_row_code_code_lucas_low_digit_repeat_successor_normalized = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_code_scale_lucas_low_digit_repeat_successor_normalized) + (bcf_previous_code_lucas_low_digit_repeat_successor_normalized_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_scale. bcf_height_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_scale + S (bcf_previous_scale_lucas_low_digit_repeat_successor_normalized_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_successor_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_scale. bcf_row_scale_code_lucas_low_digit_repeat_successor_normalized = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_successor_normalized) + (bcf_previous_scale_lucas_low_digit_repeat_successor_normalized_table))) /\ (forall bcf_index_lucas_low_digit_repeat_successor_normalized_table_row_step. (exists bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_table_row_step_bound. bcf_lt_gap_lucas_low_digit_repeat_successor_normalized_table_row_step_bound + S (bcf_index_lucas_low_digit_repeat_successor_normalized_table_row_step) = S (p + (p * q + a))) -> exists bcf_value_lucas_low_digit_repeat_successor_normalized_table_row_step. ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_row_step_entry. bcf_height_lucas_low_digit_repeat_successor_normalized_table_row_step_entry + S (bcf_value_lucas_low_digit_repeat_successor_normalized_table_row_step) = S ((S (bcf_index_lucas_low_digit_repeat_successor_normalized_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_successor_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_row_step_entry. bcf_row_code_lucas_low_digit_repeat_successor_normalized_table = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_row_step_entry * S ((S (bcf_index_lucas_low_digit_repeat_successor_normalized_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_successor_normalized_table) + (bcf_value_lucas_low_digit_repeat_successor_normalized_table_row_step))) /\ ((bcf_index_lucas_low_digit_repeat_successor_normalized_table_row_step = 0 /\ bcf_value_lucas_low_digit_repeat_successor_normalized_table_row_step = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_row_step bcf_left_lucas_low_digit_repeat_successor_normalized_table_row_step bcf_right_lucas_low_digit_repeat_successor_normalized_table_row_step. bcf_index_lucas_low_digit_repeat_successor_normalized_table_row_step = S bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_row_step /\ ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_left. bcf_height_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_left + S (bcf_left_lucas_low_digit_repeat_successor_normalized_table_row_step) = S ((S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_successor_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_left. bcf_previous_code_lucas_low_digit_repeat_successor_normalized_table = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_successor_normalized_table) + (bcf_left_lucas_low_digit_repeat_successor_normalized_table_row_step))) /\ ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_right. bcf_height_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_right + S (bcf_right_lucas_low_digit_repeat_successor_normalized_table_row_step) = S ((S (S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_successor_normalized_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_right. bcf_previous_code_lucas_low_digit_repeat_successor_normalized_table = bcf_quotient_lucas_low_digit_repeat_successor_normalized_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_low_digit_repeat_successor_normalized_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_successor_normalized_table) + (bcf_right_lucas_low_digit_repeat_successor_normalized_table_row_step))) /\ bcf_value_lucas_low_digit_repeat_successor_normalized_table_row_step = bcf_left_lucas_low_digit_repeat_successor_normalized_table_row_step + bcf_right_lucas_low_digit_repeat_successor_normalized_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_decoded_row_code. bcf_height_lucas_low_digit_repeat_successor_normalized_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_successor_normalized) = S ((S (p + (p * q + a))) * bcf_row_code_scale_lucas_low_digit_repeat_successor_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_successor_normalized = bcf_quotient_lucas_low_digit_repeat_successor_normalized_decoded_row_code * S ((S (p + (p * q + a))) * bcf_row_code_scale_lucas_low_digit_repeat_successor_normalized) + (bcf_row_code_lucas_low_digit_repeat_successor_normalized))) /\ ((((exists bcf_height_lucas_low_digit_repeat_successor_normalized_decoded_row_scale. bcf_height_lucas_low_digit_repeat_successor_normalized_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_successor_normalized) = S ((S (p + (p * q + a))) * bcf_row_scale_scale_lucas_low_digit_repeat_successor_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_successor_normalized = bcf_quotient_lucas_low_digit_repeat_successor_normalized_decoded_row_scale * S ((S (p + (p * q + a))) * bcf_row_scale_scale_lucas_low_digit_repeat_successor_normalized) + (bcf_row_scale_lucas_low_digit_repeat_successor_normalized))) /\ (((exists bcf_height_lucas_low_digit_repeat_successor_normalized_decoded_value. bcf_height_lucas_low_digit_repeat_successor_normalized_decoded_value + S (C) = S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_successor_normalized)) /\ exists bcf_quotient_lucas_low_digit_repeat_successor_normalized_decoded_value. bcf_row_code_lucas_low_digit_repeat_successor_normalized = bcf_quotient_lucas_low_digit_repeat_successor_normalized_decoded_value * S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_successor_normalized) + (C))))))))
  38. 0038specialize choose_upper_eq_transport (p * S q + a)
  39. 0039specialize choose_upper_eq_transport (p + (p * q + a))
  40. 0040specialize choose_upper_eq_transport b
  41. 0041specialize choose_upper_eq_transport C
  42. 0042apply choose_upper_eq_transport
  43. 0043apply lucas_prime_block_successor_reassociation
  44. 0044exact hupper
  45. 0045have hmiddle : exists D. ((exists bcf_lt_gap_lucas_low_digit_repeat_middle_out_of_range. bcf_lt_gap_lucas_low_digit_repeat_middle_out_of_range + S (p * q + a) = b) /\ D = 0) \/ ((exists bcf_le_gap_lucas_low_digit_repeat_middle_in_range. bcf_le_gap_lucas_low_digit_repeat_middle_in_range + (b) = p * q + a) /\ (exists bcf_row_code_code_lucas_low_digit_repeat_middle bcf_row_code_scale_lucas_low_digit_repeat_middle bcf_row_scale_code_lucas_low_digit_repeat_middle bcf_row_scale_scale_lucas_low_digit_repeat_middle bcf_row_code_lucas_low_digit_repeat_middle bcf_row_scale_lucas_low_digit_repeat_middle. ((forall bcf_row_index_lucas_low_digit_repeat_middle_table. (exists bcf_lt_gap_lucas_low_digit_repeat_middle_table_row_bound. bcf_lt_gap_lucas_low_digit_repeat_middle_table_row_bound + S (bcf_row_index_lucas_low_digit_repeat_middle_table) = S (p * q + a)) -> exists bcf_row_code_lucas_low_digit_repeat_middle_table bcf_row_scale_lucas_low_digit_repeat_middle_table. ((((exists bcf_height_lucas_low_digit_repeat_middle_table_decoded_row_code. bcf_height_lucas_low_digit_repeat_middle_table_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_middle_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_middle_table)) * bcf_row_code_scale_lucas_low_digit_repeat_middle)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_middle = bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_row_code * S ((S (bcf_row_index_lucas_low_digit_repeat_middle_table)) * bcf_row_code_scale_lucas_low_digit_repeat_middle) + (bcf_row_code_lucas_low_digit_repeat_middle_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_middle_table_decoded_row_scale. bcf_height_lucas_low_digit_repeat_middle_table_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_middle_table) = S ((S (bcf_row_index_lucas_low_digit_repeat_middle_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_middle)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_middle = bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_row_scale * S ((S (bcf_row_index_lucas_low_digit_repeat_middle_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_middle) + (bcf_row_scale_lucas_low_digit_repeat_middle_table))) /\ ((bcf_row_index_lucas_low_digit_repeat_middle_table = 0 /\ (forall bcf_index_lucas_low_digit_repeat_middle_table_zero_row. (exists bcf_lt_gap_lucas_low_digit_repeat_middle_table_zero_row_bound. bcf_lt_gap_lucas_low_digit_repeat_middle_table_zero_row_bound + S (bcf_index_lucas_low_digit_repeat_middle_table_zero_row) = S (p * q + a)) -> exists bcf_value_lucas_low_digit_repeat_middle_table_zero_row. ((((exists bcf_height_lucas_low_digit_repeat_middle_table_zero_row_entry. bcf_height_lucas_low_digit_repeat_middle_table_zero_row_entry + S (bcf_value_lucas_low_digit_repeat_middle_table_zero_row) = S ((S (bcf_index_lucas_low_digit_repeat_middle_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_middle_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_zero_row_entry. bcf_row_code_lucas_low_digit_repeat_middle_table = bcf_quotient_lucas_low_digit_repeat_middle_table_zero_row_entry * S ((S (bcf_index_lucas_low_digit_repeat_middle_table_zero_row)) * bcf_row_scale_lucas_low_digit_repeat_middle_table) + (bcf_value_lucas_low_digit_repeat_middle_table_zero_row))) /\ ((bcf_index_lucas_low_digit_repeat_middle_table_zero_row = 0 /\ bcf_value_lucas_low_digit_repeat_middle_table_zero_row = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_middle_table_zero_row. bcf_index_lucas_low_digit_repeat_middle_table_zero_row = S bcf_predecessor_lucas_low_digit_repeat_middle_table_zero_row /\ bcf_value_lucas_low_digit_repeat_middle_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_low_digit_repeat_middle_table bcf_previous_code_lucas_low_digit_repeat_middle_table bcf_previous_scale_lucas_low_digit_repeat_middle_table. bcf_row_index_lucas_low_digit_repeat_middle_table = S bcf_predecessor_lucas_low_digit_repeat_middle_table /\ ((((exists bcf_height_lucas_low_digit_repeat_middle_table_decoded_previous_code. bcf_height_lucas_low_digit_repeat_middle_table_decoded_previous_code + S (bcf_previous_code_lucas_low_digit_repeat_middle_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_middle_table)) * bcf_row_code_scale_lucas_low_digit_repeat_middle)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_previous_code. bcf_row_code_code_lucas_low_digit_repeat_middle = bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_low_digit_repeat_middle_table)) * bcf_row_code_scale_lucas_low_digit_repeat_middle) + (bcf_previous_code_lucas_low_digit_repeat_middle_table))) /\ ((((exists bcf_height_lucas_low_digit_repeat_middle_table_decoded_previous_scale. bcf_height_lucas_low_digit_repeat_middle_table_decoded_previous_scale + S (bcf_previous_scale_lucas_low_digit_repeat_middle_table) = S ((S (bcf_predecessor_lucas_low_digit_repeat_middle_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_middle)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_previous_scale. bcf_row_scale_code_lucas_low_digit_repeat_middle = bcf_quotient_lucas_low_digit_repeat_middle_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_low_digit_repeat_middle_table)) * bcf_row_scale_scale_lucas_low_digit_repeat_middle) + (bcf_previous_scale_lucas_low_digit_repeat_middle_table))) /\ (forall bcf_index_lucas_low_digit_repeat_middle_table_row_step. (exists bcf_lt_gap_lucas_low_digit_repeat_middle_table_row_step_bound. bcf_lt_gap_lucas_low_digit_repeat_middle_table_row_step_bound + S (bcf_index_lucas_low_digit_repeat_middle_table_row_step) = S (p * q + a)) -> exists bcf_value_lucas_low_digit_repeat_middle_table_row_step. ((((exists bcf_height_lucas_low_digit_repeat_middle_table_row_step_entry. bcf_height_lucas_low_digit_repeat_middle_table_row_step_entry + S (bcf_value_lucas_low_digit_repeat_middle_table_row_step) = S ((S (bcf_index_lucas_low_digit_repeat_middle_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_middle_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_row_step_entry. bcf_row_code_lucas_low_digit_repeat_middle_table = bcf_quotient_lucas_low_digit_repeat_middle_table_row_step_entry * S ((S (bcf_index_lucas_low_digit_repeat_middle_table_row_step)) * bcf_row_scale_lucas_low_digit_repeat_middle_table) + (bcf_value_lucas_low_digit_repeat_middle_table_row_step))) /\ ((bcf_index_lucas_low_digit_repeat_middle_table_row_step = 0 /\ bcf_value_lucas_low_digit_repeat_middle_table_row_step = 1) \/ exists bcf_predecessor_lucas_low_digit_repeat_middle_table_row_step bcf_left_lucas_low_digit_repeat_middle_table_row_step bcf_right_lucas_low_digit_repeat_middle_table_row_step. bcf_index_lucas_low_digit_repeat_middle_table_row_step = S bcf_predecessor_lucas_low_digit_repeat_middle_table_row_step /\ ((((exists bcf_height_lucas_low_digit_repeat_middle_table_row_step_previous_left. bcf_height_lucas_low_digit_repeat_middle_table_row_step_previous_left + S (bcf_left_lucas_low_digit_repeat_middle_table_row_step) = S ((S (bcf_predecessor_lucas_low_digit_repeat_middle_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_middle_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_row_step_previous_left. bcf_previous_code_lucas_low_digit_repeat_middle_table = bcf_quotient_lucas_low_digit_repeat_middle_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_low_digit_repeat_middle_table_row_step)) * bcf_previous_scale_lucas_low_digit_repeat_middle_table) + (bcf_left_lucas_low_digit_repeat_middle_table_row_step))) /\ ((((exists bcf_height_lucas_low_digit_repeat_middle_table_row_step_previous_right. bcf_height_lucas_low_digit_repeat_middle_table_row_step_previous_right + S (bcf_right_lucas_low_digit_repeat_middle_table_row_step) = S ((S (S (bcf_predecessor_lucas_low_digit_repeat_middle_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_middle_table)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_table_row_step_previous_right. bcf_previous_code_lucas_low_digit_repeat_middle_table = bcf_quotient_lucas_low_digit_repeat_middle_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_low_digit_repeat_middle_table_row_step))) * bcf_previous_scale_lucas_low_digit_repeat_middle_table) + (bcf_right_lucas_low_digit_repeat_middle_table_row_step))) /\ bcf_value_lucas_low_digit_repeat_middle_table_row_step = bcf_left_lucas_low_digit_repeat_middle_table_row_step + bcf_right_lucas_low_digit_repeat_middle_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_low_digit_repeat_middle_decoded_row_code. bcf_height_lucas_low_digit_repeat_middle_decoded_row_code + S (bcf_row_code_lucas_low_digit_repeat_middle) = S ((S (p * q + a)) * bcf_row_code_scale_lucas_low_digit_repeat_middle)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_decoded_row_code. bcf_row_code_code_lucas_low_digit_repeat_middle = bcf_quotient_lucas_low_digit_repeat_middle_decoded_row_code * S ((S (p * q + a)) * bcf_row_code_scale_lucas_low_digit_repeat_middle) + (bcf_row_code_lucas_low_digit_repeat_middle))) /\ ((((exists bcf_height_lucas_low_digit_repeat_middle_decoded_row_scale. bcf_height_lucas_low_digit_repeat_middle_decoded_row_scale + S (bcf_row_scale_lucas_low_digit_repeat_middle) = S ((S (p * q + a)) * bcf_row_scale_scale_lucas_low_digit_repeat_middle)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_decoded_row_scale. bcf_row_scale_code_lucas_low_digit_repeat_middle = bcf_quotient_lucas_low_digit_repeat_middle_decoded_row_scale * S ((S (p * q + a)) * bcf_row_scale_scale_lucas_low_digit_repeat_middle) + (bcf_row_scale_lucas_low_digit_repeat_middle))) /\ (((exists bcf_height_lucas_low_digit_repeat_middle_decoded_value. bcf_height_lucas_low_digit_repeat_middle_decoded_value + S (D) = S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_middle)) /\ exists bcf_quotient_lucas_low_digit_repeat_middle_decoded_value. bcf_row_code_lucas_low_digit_repeat_middle = bcf_quotient_lucas_low_digit_repeat_middle_decoded_value * S ((S (b)) * bcf_row_scale_lucas_low_digit_repeat_middle) + (D))))))))
  46. 0046apply choose_exists
  47. 0047cases hmiddle
  48. 0048have hshift : exists lld_left_repeat_shift lld_right_repeat_shift. (C) + (p) * lld_left_repeat_shift = (x) + (p) * lld_right_repeat_shift
  49. 0049specialize lucas_prime_shift_below_base p
  50. 0050specialize lucas_prime_shift_below_base (p * q + a)
  51. 0051specialize lucas_prime_shift_below_base b
  52. 0052specialize lucas_prime_shift_below_base C
  53. 0053specialize lucas_prime_shift_below_base x
  54. 0054apply lucas_prime_shift_below_base
  55. 0055exact hprime
  56. 0056exact hbound
  57. 0057exact hnormalized
  58. 0058exact hmiddle_witness
  59. 0059have hremaining : exists lld_left_repeat_remaining lld_right_repeat_remaining. (x) + (p) * lld_left_repeat_remaining = (D) + (p) * lld_right_repeat_remaining
  60. 0060specialize IH a
  61. 0061specialize IH b
  62. 0062specialize IH x
  63. 0063specialize IH D
  64. 0064apply IH
  65. 0065exact hprime
  66. 0066exact hbound
  67. 0067exact hmiddle_witness
  68. 0068exact hlower
  69. 0069specialize mod_eq_trans p
  70. 0070specialize mod_eq_trans C
  71. 0071specialize mod_eq_trans x
  72. 0072specialize mod_eq_trans D
  73. 0073apply mod_eq_trans
  74. 0074exact hshift
  75. 0075exact hremaining