LU001H · theorem body

lucas_choose_prefix_point

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

Every independently supplied decoded upper index, lower index, and coefficient satisfies the exact relational binomial theorem at that prefix position.

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

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

Statement with defined notation

∀ qb. ∀ qc. ∀ db. ∀ dc. ∀ z. ∀ t. ∀ l. ∀ i. ∀ a. ∀ b. ∀ C. (∀ x. Lt(x,l) → ∃ y. ∃ n. ∃ m. BetaAt(qb,qc,x,y) ∧ (BetaAt(db,dc,x,n) ∧ (BetaAt(z,t,x,m) ∧ Choose(y,n,m)))) → Lt(i,l) → BetaAt(qb,qc,i,a) → BetaAt(db,dc,i,b) → BetaAt(z,t,i,C) → Choose(a,b,C)

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 PD0013 BetaAt PD0041 Choose

In local proof propositions

PD0013 BetaAt PD0041 Choose
Exact expanded first-order statement
forall qb qc db dc z t l i a b C. (forall lmd_choose_index_choose_total. (exists lmd_gap_choose_total_bound. lmd_gap_choose_total_bound + S (lmd_choose_index_choose_total) = (l)) -> exists lmd_choose_upper_choose_total lmd_choose_lower_choose_total lmd_choose_value_choose_total. ((((exists ff_h_lmd_choose_total_upper. ff_h_lmd_choose_total_upper + S (lmd_choose_upper_choose_total) = S ((S (lmd_choose_index_choose_total)) * qc)) /\ exists ff_q_lmd_choose_total_upper. qb = ff_q_lmd_choose_total_upper * S ((S (lmd_choose_index_choose_total)) * qc) + (lmd_choose_upper_choose_total))) /\ ((((exists ff_h_lmd_choose_total_lower. ff_h_lmd_choose_total_lower + S (lmd_choose_lower_choose_total) = S ((S (lmd_choose_index_choose_total)) * dc)) /\ exists ff_q_lmd_choose_total_lower. db = ff_q_lmd_choose_total_lower * S ((S (lmd_choose_index_choose_total)) * dc) + (lmd_choose_lower_choose_total))) /\ ((((exists ff_h_lmd_choose_total_result. ff_h_lmd_choose_total_result + S (lmd_choose_value_choose_total) = S ((S (lmd_choose_index_choose_total)) * t)) /\ exists ff_q_lmd_choose_total_result. z = ff_q_lmd_choose_total_result * S ((S (lmd_choose_index_choose_total)) * t) + (lmd_choose_value_choose_total))) /\ (((exists bcf_lt_gap_lmd_choose_total_choose_out_of_range. bcf_lt_gap_lmd_choose_total_choose_out_of_range + S (lmd_choose_upper_choose_total) = lmd_choose_lower_choose_total) /\ lmd_choose_value_choose_total = 0) \/ ((exists bcf_le_gap_lmd_choose_total_choose_in_range. bcf_le_gap_lmd_choose_total_choose_in_range + (lmd_choose_lower_choose_total) = lmd_choose_upper_choose_total) /\ (exists bcf_row_code_code_lmd_choose_total_choose bcf_row_code_scale_lmd_choose_total_choose bcf_row_scale_code_lmd_choose_total_choose bcf_row_scale_scale_lmd_choose_total_choose bcf_row_code_lmd_choose_total_choose bcf_row_scale_lmd_choose_total_choose. ((forall bcf_row_index_lmd_choose_total_choose_table. (exists bcf_lt_gap_lmd_choose_total_choose_table_row_bound. bcf_lt_gap_lmd_choose_total_choose_table_row_bound + S (bcf_row_index_lmd_choose_total_choose_table) = S (lmd_choose_upper_choose_total)) -> exists bcf_row_code_lmd_choose_total_choose_table bcf_row_scale_lmd_choose_total_choose_table. ((((exists bcf_height_lmd_choose_total_choose_table_decoded_row_code. bcf_height_lmd_choose_total_choose_table_decoded_row_code + S (bcf_row_code_lmd_choose_total_choose_table) = S ((S (bcf_row_index_lmd_choose_total_choose_table)) * bcf_row_code_scale_lmd_choose_total_choose)) /\ exists bcf_quotient_lmd_choose_total_choose_table_decoded_row_code. bcf_row_code_code_lmd_choose_total_choose = bcf_quotient_lmd_choose_total_choose_table_decoded_row_code * S ((S (bcf_row_index_lmd_choose_total_choose_table)) * bcf_row_code_scale_lmd_choose_total_choose) + (bcf_row_code_lmd_choose_total_choose_table))) /\ ((((exists bcf_height_lmd_choose_total_choose_table_decoded_row_scale. bcf_height_lmd_choose_total_choose_table_decoded_row_scale + S (bcf_row_scale_lmd_choose_total_choose_table) = S ((S (bcf_row_index_lmd_choose_total_choose_table)) * bcf_row_scale_scale_lmd_choose_total_choose)) /\ exists bcf_quotient_lmd_choose_total_choose_table_decoded_row_scale. bcf_row_scale_code_lmd_choose_total_choose = bcf_quotient_lmd_choose_total_choose_table_decoded_row_scale * S ((S (bcf_row_index_lmd_choose_total_choose_table)) * bcf_row_scale_scale_lmd_choose_total_choose) + (bcf_row_scale_lmd_choose_total_choose_table))) /\ ((bcf_row_index_lmd_choose_total_choose_table = 0 /\ (forall bcf_index_lmd_choose_total_choose_table_zero_row. (exists bcf_lt_gap_lmd_choose_total_choose_table_zero_row_bound. bcf_lt_gap_lmd_choose_total_choose_table_zero_row_bound + S (bcf_index_lmd_choose_total_choose_table_zero_row) = S (lmd_choose_upper_choose_total)) -> exists bcf_value_lmd_choose_total_choose_table_zero_row. ((((exists bcf_height_lmd_choose_total_choose_table_zero_row_entry. bcf_height_lmd_choose_total_choose_table_zero_row_entry + S (bcf_value_lmd_choose_total_choose_table_zero_row) = S ((S (bcf_index_lmd_choose_total_choose_table_zero_row)) * bcf_row_scale_lmd_choose_total_choose_table)) /\ exists bcf_quotient_lmd_choose_total_choose_table_zero_row_entry. bcf_row_code_lmd_choose_total_choose_table = bcf_quotient_lmd_choose_total_choose_table_zero_row_entry * S ((S (bcf_index_lmd_choose_total_choose_table_zero_row)) * bcf_row_scale_lmd_choose_total_choose_table) + (bcf_value_lmd_choose_total_choose_table_zero_row))) /\ ((bcf_index_lmd_choose_total_choose_table_zero_row = 0 /\ bcf_value_lmd_choose_total_choose_table_zero_row = 1) \/ exists bcf_predecessor_lmd_choose_total_choose_table_zero_row. bcf_index_lmd_choose_total_choose_table_zero_row = S bcf_predecessor_lmd_choose_total_choose_table_zero_row /\ bcf_value_lmd_choose_total_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lmd_choose_total_choose_table bcf_previous_code_lmd_choose_total_choose_table bcf_previous_scale_lmd_choose_total_choose_table. bcf_row_index_lmd_choose_total_choose_table = S bcf_predecessor_lmd_choose_total_choose_table /\ ((((exists bcf_height_lmd_choose_total_choose_table_decoded_previous_code. bcf_height_lmd_choose_total_choose_table_decoded_previous_code + S (bcf_previous_code_lmd_choose_total_choose_table) = S ((S (bcf_predecessor_lmd_choose_total_choose_table)) * bcf_row_code_scale_lmd_choose_total_choose)) /\ exists bcf_quotient_lmd_choose_total_choose_table_decoded_previous_code. bcf_row_code_code_lmd_choose_total_choose = bcf_quotient_lmd_choose_total_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lmd_choose_total_choose_table)) * bcf_row_code_scale_lmd_choose_total_choose) + (bcf_previous_code_lmd_choose_total_choose_table))) /\ ((((exists bcf_height_lmd_choose_total_choose_table_decoded_previous_scale. bcf_height_lmd_choose_total_choose_table_decoded_previous_scale + S (bcf_previous_scale_lmd_choose_total_choose_table) = S ((S (bcf_predecessor_lmd_choose_total_choose_table)) * bcf_row_scale_scale_lmd_choose_total_choose)) /\ exists bcf_quotient_lmd_choose_total_choose_table_decoded_previous_scale. bcf_row_scale_code_lmd_choose_total_choose = bcf_quotient_lmd_choose_total_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lmd_choose_total_choose_table)) * bcf_row_scale_scale_lmd_choose_total_choose) + (bcf_previous_scale_lmd_choose_total_choose_table))) /\ (forall bcf_index_lmd_choose_total_choose_table_row_step. (exists bcf_lt_gap_lmd_choose_total_choose_table_row_step_bound. bcf_lt_gap_lmd_choose_total_choose_table_row_step_bound + S (bcf_index_lmd_choose_total_choose_table_row_step) = S (lmd_choose_upper_choose_total)) -> exists bcf_value_lmd_choose_total_choose_table_row_step. ((((exists bcf_height_lmd_choose_total_choose_table_row_step_entry. bcf_height_lmd_choose_total_choose_table_row_step_entry + S (bcf_value_lmd_choose_total_choose_table_row_step) = S ((S (bcf_index_lmd_choose_total_choose_table_row_step)) * bcf_row_scale_lmd_choose_total_choose_table)) /\ exists bcf_quotient_lmd_choose_total_choose_table_row_step_entry. bcf_row_code_lmd_choose_total_choose_table = bcf_quotient_lmd_choose_total_choose_table_row_step_entry * S ((S (bcf_index_lmd_choose_total_choose_table_row_step)) * bcf_row_scale_lmd_choose_total_choose_table) + (bcf_value_lmd_choose_total_choose_table_row_step))) /\ ((bcf_index_lmd_choose_total_choose_table_row_step = 0 /\ bcf_value_lmd_choose_total_choose_table_row_step = 1) \/ exists bcf_predecessor_lmd_choose_total_choose_table_row_step bcf_left_lmd_choose_total_choose_table_row_step bcf_right_lmd_choose_total_choose_table_row_step. bcf_index_lmd_choose_total_choose_table_row_step = S bcf_predecessor_lmd_choose_total_choose_table_row_step /\ ((((exists bcf_height_lmd_choose_total_choose_table_row_step_previous_left. bcf_height_lmd_choose_total_choose_table_row_step_previous_left + S (bcf_left_lmd_choose_total_choose_table_row_step) = S ((S (bcf_predecessor_lmd_choose_total_choose_table_row_step)) * bcf_previous_scale_lmd_choose_total_choose_table)) /\ exists bcf_quotient_lmd_choose_total_choose_table_row_step_previous_left. bcf_previous_code_lmd_choose_total_choose_table = bcf_quotient_lmd_choose_total_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lmd_choose_total_choose_table_row_step)) * bcf_previous_scale_lmd_choose_total_choose_table) + (bcf_left_lmd_choose_total_choose_table_row_step))) /\ ((((exists bcf_height_lmd_choose_total_choose_table_row_step_previous_right. bcf_height_lmd_choose_total_choose_table_row_step_previous_right + S (bcf_right_lmd_choose_total_choose_table_row_step) = S ((S (S (bcf_predecessor_lmd_choose_total_choose_table_row_step))) * bcf_previous_scale_lmd_choose_total_choose_table)) /\ exists bcf_quotient_lmd_choose_total_choose_table_row_step_previous_right. bcf_previous_code_lmd_choose_total_choose_table = bcf_quotient_lmd_choose_total_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lmd_choose_total_choose_table_row_step))) * bcf_previous_scale_lmd_choose_total_choose_table) + (bcf_right_lmd_choose_total_choose_table_row_step))) /\ bcf_value_lmd_choose_total_choose_table_row_step = bcf_left_lmd_choose_total_choose_table_row_step + bcf_right_lmd_choose_total_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lmd_choose_total_choose_decoded_row_code. bcf_height_lmd_choose_total_choose_decoded_row_code + S (bcf_row_code_lmd_choose_total_choose) = S ((S (lmd_choose_upper_choose_total)) * bcf_row_code_scale_lmd_choose_total_choose)) /\ exists bcf_quotient_lmd_choose_total_choose_decoded_row_code. bcf_row_code_code_lmd_choose_total_choose = bcf_quotient_lmd_choose_total_choose_decoded_row_code * S ((S (lmd_choose_upper_choose_total)) * bcf_row_code_scale_lmd_choose_total_choose) + (bcf_row_code_lmd_choose_total_choose))) /\ ((((exists bcf_height_lmd_choose_total_choose_decoded_row_scale. bcf_height_lmd_choose_total_choose_decoded_row_scale + S (bcf_row_scale_lmd_choose_total_choose) = S ((S (lmd_choose_upper_choose_total)) * bcf_row_scale_scale_lmd_choose_total_choose)) /\ exists bcf_quotient_lmd_choose_total_choose_decoded_row_scale. bcf_row_scale_code_lmd_choose_total_choose = bcf_quotient_lmd_choose_total_choose_decoded_row_scale * S ((S (lmd_choose_upper_choose_total)) * bcf_row_scale_scale_lmd_choose_total_choose) + (bcf_row_scale_lmd_choose_total_choose))) /\ (((exists bcf_height_lmd_choose_total_choose_decoded_value. bcf_height_lmd_choose_total_choose_decoded_value + S (lmd_choose_value_choose_total) = S ((S (lmd_choose_lower_choose_total)) * bcf_row_scale_lmd_choose_total_choose)) /\ exists bcf_quotient_lmd_choose_total_choose_decoded_value. bcf_row_code_lmd_choose_total_choose = bcf_quotient_lmd_choose_total_choose_decoded_value * S ((S (lmd_choose_lower_choose_total)) * bcf_row_scale_lmd_choose_total_choose) + (lmd_choose_value_choose_total))))))))))))) -> (exists lmd_gap_choose_point_bound. lmd_gap_choose_point_bound + S (i) = (l)) -> (((exists ff_h_lmd_choose_point_upper. ff_h_lmd_choose_point_upper + S (a) = S ((S (i)) * qc)) /\ exists ff_q_lmd_choose_point_upper. qb = ff_q_lmd_choose_point_upper * S ((S (i)) * qc) + (a))) -> (((exists ff_h_lmd_choose_point_lower. ff_h_lmd_choose_point_lower + S (b) = S ((S (i)) * dc)) /\ exists ff_q_lmd_choose_point_lower. db = ff_q_lmd_choose_point_lower * S ((S (i)) * dc) + (b))) -> (((exists ff_h_lmd_choose_point_value. ff_h_lmd_choose_point_value + S (C) = S ((S (i)) * t)) /\ exists ff_q_lmd_choose_point_value. z = ff_q_lmd_choose_point_value * S ((S (i)) * t) + (C))) -> (((exists bcf_lt_gap_lmd_choose_point_out_of_range. bcf_lt_gap_lmd_choose_point_out_of_range + S (a) = b) /\ C = 0) \/ ((exists bcf_le_gap_lmd_choose_point_in_range. bcf_le_gap_lmd_choose_point_in_range + (b) = a) /\ (exists bcf_row_code_code_lmd_choose_point bcf_row_code_scale_lmd_choose_point bcf_row_scale_code_lmd_choose_point bcf_row_scale_scale_lmd_choose_point bcf_row_code_lmd_choose_point bcf_row_scale_lmd_choose_point. ((forall bcf_row_index_lmd_choose_point_table. (exists bcf_lt_gap_lmd_choose_point_table_row_bound. bcf_lt_gap_lmd_choose_point_table_row_bound + S (bcf_row_index_lmd_choose_point_table) = S (a)) -> exists bcf_row_code_lmd_choose_point_table bcf_row_scale_lmd_choose_point_table. ((((exists bcf_height_lmd_choose_point_table_decoded_row_code. bcf_height_lmd_choose_point_table_decoded_row_code + S (bcf_row_code_lmd_choose_point_table) = S ((S (bcf_row_index_lmd_choose_point_table)) * bcf_row_code_scale_lmd_choose_point)) /\ exists bcf_quotient_lmd_choose_point_table_decoded_row_code. bcf_row_code_code_lmd_choose_point = bcf_quotient_lmd_choose_point_table_decoded_row_code * S ((S (bcf_row_index_lmd_choose_point_table)) * bcf_row_code_scale_lmd_choose_point) + (bcf_row_code_lmd_choose_point_table))) /\ ((((exists bcf_height_lmd_choose_point_table_decoded_row_scale. bcf_height_lmd_choose_point_table_decoded_row_scale + S (bcf_row_scale_lmd_choose_point_table) = S ((S (bcf_row_index_lmd_choose_point_table)) * bcf_row_scale_scale_lmd_choose_point)) /\ exists bcf_quotient_lmd_choose_point_table_decoded_row_scale. bcf_row_scale_code_lmd_choose_point = bcf_quotient_lmd_choose_point_table_decoded_row_scale * S ((S (bcf_row_index_lmd_choose_point_table)) * bcf_row_scale_scale_lmd_choose_point) + (bcf_row_scale_lmd_choose_point_table))) /\ ((bcf_row_index_lmd_choose_point_table = 0 /\ (forall bcf_index_lmd_choose_point_table_zero_row. (exists bcf_lt_gap_lmd_choose_point_table_zero_row_bound. bcf_lt_gap_lmd_choose_point_table_zero_row_bound + S (bcf_index_lmd_choose_point_table_zero_row) = S (a)) -> exists bcf_value_lmd_choose_point_table_zero_row. ((((exists bcf_height_lmd_choose_point_table_zero_row_entry. bcf_height_lmd_choose_point_table_zero_row_entry + S (bcf_value_lmd_choose_point_table_zero_row) = S ((S (bcf_index_lmd_choose_point_table_zero_row)) * bcf_row_scale_lmd_choose_point_table)) /\ exists bcf_quotient_lmd_choose_point_table_zero_row_entry. bcf_row_code_lmd_choose_point_table = bcf_quotient_lmd_choose_point_table_zero_row_entry * S ((S (bcf_index_lmd_choose_point_table_zero_row)) * bcf_row_scale_lmd_choose_point_table) + (bcf_value_lmd_choose_point_table_zero_row))) /\ ((bcf_index_lmd_choose_point_table_zero_row = 0 /\ bcf_value_lmd_choose_point_table_zero_row = 1) \/ exists bcf_predecessor_lmd_choose_point_table_zero_row. bcf_index_lmd_choose_point_table_zero_row = S bcf_predecessor_lmd_choose_point_table_zero_row /\ bcf_value_lmd_choose_point_table_zero_row = 0)))) \/ exists bcf_predecessor_lmd_choose_point_table bcf_previous_code_lmd_choose_point_table bcf_previous_scale_lmd_choose_point_table. bcf_row_index_lmd_choose_point_table = S bcf_predecessor_lmd_choose_point_table /\ ((((exists bcf_height_lmd_choose_point_table_decoded_previous_code. bcf_height_lmd_choose_point_table_decoded_previous_code + S (bcf_previous_code_lmd_choose_point_table) = S ((S (bcf_predecessor_lmd_choose_point_table)) * bcf_row_code_scale_lmd_choose_point)) /\ exists bcf_quotient_lmd_choose_point_table_decoded_previous_code. bcf_row_code_code_lmd_choose_point = bcf_quotient_lmd_choose_point_table_decoded_previous_code * S ((S (bcf_predecessor_lmd_choose_point_table)) * bcf_row_code_scale_lmd_choose_point) + (bcf_previous_code_lmd_choose_point_table))) /\ ((((exists bcf_height_lmd_choose_point_table_decoded_previous_scale. bcf_height_lmd_choose_point_table_decoded_previous_scale + S (bcf_previous_scale_lmd_choose_point_table) = S ((S (bcf_predecessor_lmd_choose_point_table)) * bcf_row_scale_scale_lmd_choose_point)) /\ exists bcf_quotient_lmd_choose_point_table_decoded_previous_scale. bcf_row_scale_code_lmd_choose_point = bcf_quotient_lmd_choose_point_table_decoded_previous_scale * S ((S (bcf_predecessor_lmd_choose_point_table)) * bcf_row_scale_scale_lmd_choose_point) + (bcf_previous_scale_lmd_choose_point_table))) /\ (forall bcf_index_lmd_choose_point_table_row_step. (exists bcf_lt_gap_lmd_choose_point_table_row_step_bound. bcf_lt_gap_lmd_choose_point_table_row_step_bound + S (bcf_index_lmd_choose_point_table_row_step) = S (a)) -> exists bcf_value_lmd_choose_point_table_row_step. ((((exists bcf_height_lmd_choose_point_table_row_step_entry. bcf_height_lmd_choose_point_table_row_step_entry + S (bcf_value_lmd_choose_point_table_row_step) = S ((S (bcf_index_lmd_choose_point_table_row_step)) * bcf_row_scale_lmd_choose_point_table)) /\ exists bcf_quotient_lmd_choose_point_table_row_step_entry. bcf_row_code_lmd_choose_point_table = bcf_quotient_lmd_choose_point_table_row_step_entry * S ((S (bcf_index_lmd_choose_point_table_row_step)) * bcf_row_scale_lmd_choose_point_table) + (bcf_value_lmd_choose_point_table_row_step))) /\ ((bcf_index_lmd_choose_point_table_row_step = 0 /\ bcf_value_lmd_choose_point_table_row_step = 1) \/ exists bcf_predecessor_lmd_choose_point_table_row_step bcf_left_lmd_choose_point_table_row_step bcf_right_lmd_choose_point_table_row_step. bcf_index_lmd_choose_point_table_row_step = S bcf_predecessor_lmd_choose_point_table_row_step /\ ((((exists bcf_height_lmd_choose_point_table_row_step_previous_left. bcf_height_lmd_choose_point_table_row_step_previous_left + S (bcf_left_lmd_choose_point_table_row_step) = S ((S (bcf_predecessor_lmd_choose_point_table_row_step)) * bcf_previous_scale_lmd_choose_point_table)) /\ exists bcf_quotient_lmd_choose_point_table_row_step_previous_left. bcf_previous_code_lmd_choose_point_table = bcf_quotient_lmd_choose_point_table_row_step_previous_left * S ((S (bcf_predecessor_lmd_choose_point_table_row_step)) * bcf_previous_scale_lmd_choose_point_table) + (bcf_left_lmd_choose_point_table_row_step))) /\ ((((exists bcf_height_lmd_choose_point_table_row_step_previous_right. bcf_height_lmd_choose_point_table_row_step_previous_right + S (bcf_right_lmd_choose_point_table_row_step) = S ((S (S (bcf_predecessor_lmd_choose_point_table_row_step))) * bcf_previous_scale_lmd_choose_point_table)) /\ exists bcf_quotient_lmd_choose_point_table_row_step_previous_right. bcf_previous_code_lmd_choose_point_table = bcf_quotient_lmd_choose_point_table_row_step_previous_right * S ((S (S (bcf_predecessor_lmd_choose_point_table_row_step))) * bcf_previous_scale_lmd_choose_point_table) + (bcf_right_lmd_choose_point_table_row_step))) /\ bcf_value_lmd_choose_point_table_row_step = bcf_left_lmd_choose_point_table_row_step + bcf_right_lmd_choose_point_table_row_step))))))))))) /\ ((((exists bcf_height_lmd_choose_point_decoded_row_code. bcf_height_lmd_choose_point_decoded_row_code + S (bcf_row_code_lmd_choose_point) = S ((S (a)) * bcf_row_code_scale_lmd_choose_point)) /\ exists bcf_quotient_lmd_choose_point_decoded_row_code. bcf_row_code_code_lmd_choose_point = bcf_quotient_lmd_choose_point_decoded_row_code * S ((S (a)) * bcf_row_code_scale_lmd_choose_point) + (bcf_row_code_lmd_choose_point))) /\ ((((exists bcf_height_lmd_choose_point_decoded_row_scale. bcf_height_lmd_choose_point_decoded_row_scale + S (bcf_row_scale_lmd_choose_point) = S ((S (a)) * bcf_row_scale_scale_lmd_choose_point)) /\ exists bcf_quotient_lmd_choose_point_decoded_row_scale. bcf_row_scale_code_lmd_choose_point = bcf_quotient_lmd_choose_point_decoded_row_scale * S ((S (a)) * bcf_row_scale_scale_lmd_choose_point) + (bcf_row_scale_lmd_choose_point))) /\ (((exists bcf_height_lmd_choose_point_decoded_value. bcf_height_lmd_choose_point_decoded_value + S (C) = S ((S (b)) * bcf_row_scale_lmd_choose_point)) /\ exists bcf_quotient_lmd_choose_point_decoded_value. bcf_row_code_lmd_choose_point = bcf_quotient_lmd_choose_point_decoded_value * S ((S (b)) * bcf_row_scale_lmd_choose_point) + (C)))))))))

Proof neighborhood

Direct theorem prerequisites

beta_at_unique · Stable closed

Direct theorem dependents

LU001I lucas_multidigit_congruence_from_one_step LU001J lucas_terminating_multidigit_theorem_from_one_step LU001Q lucas_theorem_for_length

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

70 script commands · 10 reading checkpoints · 4 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro qb
  2. L2
    intro qc
  3. L3
    intro db
  4. L4
    intro dc
  5. L5
    intro z
  6. L6
    intro t
  7. L7
    intro l
  8. L8
    intro i
  9. L9
    intro a
  10. L10
    intro b
02Fix variables and assumptionsL11–16

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

  1. L11
    intro C
  2. L12
    intro hprefix
  3. L13
    intro hi
  4. L14
    intro ha
  5. L15
    intro hb
  6. L16
    intro hC
03Establish hchoiceL17–20

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

  1. L17
    have hchoice : ∃ a. ∃ b. ∃ C. BetaAt(qb,qc,i,a) ∧ (BetaAt(db,dc,i,b) ∧ (BetaAt(z,t,i,C) ∧ Choose(a,b,C)))Definitions: BetaAt(qb,qc,i,a)BetaAt(db,dc,i,b)BetaAt(z,t,i,C)Choose(a,b,C)Original native command in the exact edition
  2. L18
    specialize hprefix i
  3. L19
    apply hprefix
  4. L20
    exact hi
04Separate the logical casesL21–26

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

  1. L21
    cases hchoice
  2. L22
    cases hchoice_witness
  3. L23
    cases hchoice_witness_witness
  4. L24
    cases hchoice_witness_witness_witness
  5. L25
    cases hchoice_witness_witness_witness_right
  6. L26
    cases hchoice_witness_witness_witness_right_right
05Establish hupperL27–35

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

  1. L27
    have hupper : x = a
  2. L28
    specialize beta_at_unique qb
  3. L29
    specialize beta_at_unique qc
  4. L30
    specialize beta_at_unique i
  5. L31
    specialize beta_at_unique x
  6. L32
    specialize beta_at_unique a
  7. L33
    apply beta_at_unique
  8. L34
    exact hchoice_witness_witness_witness_left
  9. L35
    exact ha
06Establish hlowerL36–44

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

  1. L36
    have hlower : x1 = b
  2. L37
    specialize beta_at_unique db
  3. L38
    specialize beta_at_unique dc
  4. L39
    specialize beta_at_unique i
  5. L40
    specialize beta_at_unique x1
  6. L41
    specialize beta_at_unique b
  7. L42
    apply beta_at_unique
  8. L43
    exact hchoice_witness_witness_witness_right_left
  9. L44
    exact hb
07Establish hvalueL45–54

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

  1. L45
    have hvalue : x2 = C
  2. L46
    specialize beta_at_unique z
  3. L47
    specialize beta_at_unique t
  4. L48
    specialize beta_at_unique i
  5. L49
    specialize beta_at_unique x2
  6. L50
    specialize beta_at_unique C
  7. L51
    apply beta_at_unique
  8. L52
    exact hchoice_witness_witness_witness_right_right_left
  9. L53
    exact hC
  10. L54
    rewrite hupper at hchoice_witness_witness_witness_right_right_right
08Calculate and transport equalitiesL55–64

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L55
    rewrite hupper at hchoice_witness_witness_witness_right_right_right
  2. L56
    rewrite hupper at hchoice_witness_witness_witness_right_right_right
  3. L57
    rewrite hupper at hchoice_witness_witness_witness_right_right_right
  4. L58
    rewrite hupper at hchoice_witness_witness_witness_right_right_right
  5. L59
    rewrite hupper at hchoice_witness_witness_witness_right_right_right
  6. L60
    rewrite hupper at hchoice_witness_witness_witness_right_right_right
  7. L61
    rewrite hupper at hchoice_witness_witness_witness_right_right_right
  8. L62
    rewrite hupper at hchoice_witness_witness_witness_right_right_right
  9. L63
    rewrite hlower at hchoice_witness_witness_witness_right_right_right
  10. L64
    rewrite hlower at hchoice_witness_witness_witness_right_right_right
09Calculate and transport equalitiesL65–69

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L65
    rewrite hlower at hchoice_witness_witness_witness_right_right_right
  2. L66
    rewrite hlower at hchoice_witness_witness_witness_right_right_right
  3. L67
    rewrite hvalue at hchoice_witness_witness_witness_right_right_right
  4. L68
    rewrite hvalue at hchoice_witness_witness_witness_right_right_right
  5. L69
    rewrite hvalue at hchoice_witness_witness_witness_right_right_right
10Use earlier factsL70–70

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

  1. L70
    exact hchoice_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 70 lines
  1. 0001intro qb
  2. 0002intro qc
  3. 0003intro db
  4. 0004intro dc
  5. 0005intro z
  6. 0006intro t
  7. 0007intro l
  8. 0008intro i
  9. 0009intro a
  10. 0010intro b
  11. 0011intro C
  12. 0012intro hprefix
  13. 0013intro hi
  14. 0014intro ha
  15. 0015intro hb
  16. 0016intro hC
  17. 0017have hchoice : ∃ a. ∃ b. ∃ C. BetaAt(qb,qc,i,a) ∧ (BetaAt(db,dc,i,b) ∧ (BetaAt(z,t,i,C) ∧ Choose(a,b,C)))
    Exact native replay linehave hchoice : exists a b C. ((((exists ff_h_lmd_choose_old_upper. ff_h_lmd_choose_old_upper + S (a) = S ((S (i)) * qc)) /\ exists ff_q_lmd_choose_old_upper. qb = ff_q_lmd_choose_old_upper * S ((S (i)) * qc) + (a))) /\ ((((exists ff_h_lmd_choose_old_lower. ff_h_lmd_choose_old_lower + S (b) = S ((S (i)) * dc)) /\ exists ff_q_lmd_choose_old_lower. db = ff_q_lmd_choose_old_lower * S ((S (i)) * dc) + (b))) /\ ((((exists ff_h_lmd_choose_old_value. ff_h_lmd_choose_old_value + S (C) = S ((S (i)) * t)) /\ exists ff_q_lmd_choose_old_value. z = ff_q_lmd_choose_old_value * S ((S (i)) * t) + (C))) /\ (((exists bcf_lt_gap_lmd_old_choose_out_of_range. bcf_lt_gap_lmd_old_choose_out_of_range + S (a) = b) /\ C = 0) \/ ((exists bcf_le_gap_lmd_old_choose_in_range. bcf_le_gap_lmd_old_choose_in_range + (b) = a) /\ (exists bcf_row_code_code_lmd_old_choose bcf_row_code_scale_lmd_old_choose bcf_row_scale_code_lmd_old_choose bcf_row_scale_scale_lmd_old_choose bcf_row_code_lmd_old_choose bcf_row_scale_lmd_old_choose. ((forall bcf_row_index_lmd_old_choose_table. (exists bcf_lt_gap_lmd_old_choose_table_row_bound. bcf_lt_gap_lmd_old_choose_table_row_bound + S (bcf_row_index_lmd_old_choose_table) = S (a)) -> exists bcf_row_code_lmd_old_choose_table bcf_row_scale_lmd_old_choose_table. ((((exists bcf_height_lmd_old_choose_table_decoded_row_code. bcf_height_lmd_old_choose_table_decoded_row_code + S (bcf_row_code_lmd_old_choose_table) = S ((S (bcf_row_index_lmd_old_choose_table)) * bcf_row_code_scale_lmd_old_choose)) /\ exists bcf_quotient_lmd_old_choose_table_decoded_row_code. bcf_row_code_code_lmd_old_choose = bcf_quotient_lmd_old_choose_table_decoded_row_code * S ((S (bcf_row_index_lmd_old_choose_table)) * bcf_row_code_scale_lmd_old_choose) + (bcf_row_code_lmd_old_choose_table))) /\ ((((exists bcf_height_lmd_old_choose_table_decoded_row_scale. bcf_height_lmd_old_choose_table_decoded_row_scale + S (bcf_row_scale_lmd_old_choose_table) = S ((S (bcf_row_index_lmd_old_choose_table)) * bcf_row_scale_scale_lmd_old_choose)) /\ exists bcf_quotient_lmd_old_choose_table_decoded_row_scale. bcf_row_scale_code_lmd_old_choose = bcf_quotient_lmd_old_choose_table_decoded_row_scale * S ((S (bcf_row_index_lmd_old_choose_table)) * bcf_row_scale_scale_lmd_old_choose) + (bcf_row_scale_lmd_old_choose_table))) /\ ((bcf_row_index_lmd_old_choose_table = 0 /\ (forall bcf_index_lmd_old_choose_table_zero_row. (exists bcf_lt_gap_lmd_old_choose_table_zero_row_bound. bcf_lt_gap_lmd_old_choose_table_zero_row_bound + S (bcf_index_lmd_old_choose_table_zero_row) = S (a)) -> exists bcf_value_lmd_old_choose_table_zero_row. ((((exists bcf_height_lmd_old_choose_table_zero_row_entry. bcf_height_lmd_old_choose_table_zero_row_entry + S (bcf_value_lmd_old_choose_table_zero_row) = S ((S (bcf_index_lmd_old_choose_table_zero_row)) * bcf_row_scale_lmd_old_choose_table)) /\ exists bcf_quotient_lmd_old_choose_table_zero_row_entry. bcf_row_code_lmd_old_choose_table = bcf_quotient_lmd_old_choose_table_zero_row_entry * S ((S (bcf_index_lmd_old_choose_table_zero_row)) * bcf_row_scale_lmd_old_choose_table) + (bcf_value_lmd_old_choose_table_zero_row))) /\ ((bcf_index_lmd_old_choose_table_zero_row = 0 /\ bcf_value_lmd_old_choose_table_zero_row = 1) \/ exists bcf_predecessor_lmd_old_choose_table_zero_row. bcf_index_lmd_old_choose_table_zero_row = S bcf_predecessor_lmd_old_choose_table_zero_row /\ bcf_value_lmd_old_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lmd_old_choose_table bcf_previous_code_lmd_old_choose_table bcf_previous_scale_lmd_old_choose_table. bcf_row_index_lmd_old_choose_table = S bcf_predecessor_lmd_old_choose_table /\ ((((exists bcf_height_lmd_old_choose_table_decoded_previous_code. bcf_height_lmd_old_choose_table_decoded_previous_code + S (bcf_previous_code_lmd_old_choose_table) = S ((S (bcf_predecessor_lmd_old_choose_table)) * bcf_row_code_scale_lmd_old_choose)) /\ exists bcf_quotient_lmd_old_choose_table_decoded_previous_code. bcf_row_code_code_lmd_old_choose = bcf_quotient_lmd_old_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lmd_old_choose_table)) * bcf_row_code_scale_lmd_old_choose) + (bcf_previous_code_lmd_old_choose_table))) /\ ((((exists bcf_height_lmd_old_choose_table_decoded_previous_scale. bcf_height_lmd_old_choose_table_decoded_previous_scale + S (bcf_previous_scale_lmd_old_choose_table) = S ((S (bcf_predecessor_lmd_old_choose_table)) * bcf_row_scale_scale_lmd_old_choose)) /\ exists bcf_quotient_lmd_old_choose_table_decoded_previous_scale. bcf_row_scale_code_lmd_old_choose = bcf_quotient_lmd_old_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lmd_old_choose_table)) * bcf_row_scale_scale_lmd_old_choose) + (bcf_previous_scale_lmd_old_choose_table))) /\ (forall bcf_index_lmd_old_choose_table_row_step. (exists bcf_lt_gap_lmd_old_choose_table_row_step_bound. bcf_lt_gap_lmd_old_choose_table_row_step_bound + S (bcf_index_lmd_old_choose_table_row_step) = S (a)) -> exists bcf_value_lmd_old_choose_table_row_step. ((((exists bcf_height_lmd_old_choose_table_row_step_entry. bcf_height_lmd_old_choose_table_row_step_entry + S (bcf_value_lmd_old_choose_table_row_step) = S ((S (bcf_index_lmd_old_choose_table_row_step)) * bcf_row_scale_lmd_old_choose_table)) /\ exists bcf_quotient_lmd_old_choose_table_row_step_entry. bcf_row_code_lmd_old_choose_table = bcf_quotient_lmd_old_choose_table_row_step_entry * S ((S (bcf_index_lmd_old_choose_table_row_step)) * bcf_row_scale_lmd_old_choose_table) + (bcf_value_lmd_old_choose_table_row_step))) /\ ((bcf_index_lmd_old_choose_table_row_step = 0 /\ bcf_value_lmd_old_choose_table_row_step = 1) \/ exists bcf_predecessor_lmd_old_choose_table_row_step bcf_left_lmd_old_choose_table_row_step bcf_right_lmd_old_choose_table_row_step. bcf_index_lmd_old_choose_table_row_step = S bcf_predecessor_lmd_old_choose_table_row_step /\ ((((exists bcf_height_lmd_old_choose_table_row_step_previous_left. bcf_height_lmd_old_choose_table_row_step_previous_left + S (bcf_left_lmd_old_choose_table_row_step) = S ((S (bcf_predecessor_lmd_old_choose_table_row_step)) * bcf_previous_scale_lmd_old_choose_table)) /\ exists bcf_quotient_lmd_old_choose_table_row_step_previous_left. bcf_previous_code_lmd_old_choose_table = bcf_quotient_lmd_old_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lmd_old_choose_table_row_step)) * bcf_previous_scale_lmd_old_choose_table) + (bcf_left_lmd_old_choose_table_row_step))) /\ ((((exists bcf_height_lmd_old_choose_table_row_step_previous_right. bcf_height_lmd_old_choose_table_row_step_previous_right + S (bcf_right_lmd_old_choose_table_row_step) = S ((S (S (bcf_predecessor_lmd_old_choose_table_row_step))) * bcf_previous_scale_lmd_old_choose_table)) /\ exists bcf_quotient_lmd_old_choose_table_row_step_previous_right. bcf_previous_code_lmd_old_choose_table = bcf_quotient_lmd_old_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lmd_old_choose_table_row_step))) * bcf_previous_scale_lmd_old_choose_table) + (bcf_right_lmd_old_choose_table_row_step))) /\ bcf_value_lmd_old_choose_table_row_step = bcf_left_lmd_old_choose_table_row_step + bcf_right_lmd_old_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lmd_old_choose_decoded_row_code. bcf_height_lmd_old_choose_decoded_row_code + S (bcf_row_code_lmd_old_choose) = S ((S (a)) * bcf_row_code_scale_lmd_old_choose)) /\ exists bcf_quotient_lmd_old_choose_decoded_row_code. bcf_row_code_code_lmd_old_choose = bcf_quotient_lmd_old_choose_decoded_row_code * S ((S (a)) * bcf_row_code_scale_lmd_old_choose) + (bcf_row_code_lmd_old_choose))) /\ ((((exists bcf_height_lmd_old_choose_decoded_row_scale. bcf_height_lmd_old_choose_decoded_row_scale + S (bcf_row_scale_lmd_old_choose) = S ((S (a)) * bcf_row_scale_scale_lmd_old_choose)) /\ exists bcf_quotient_lmd_old_choose_decoded_row_scale. bcf_row_scale_code_lmd_old_choose = bcf_quotient_lmd_old_choose_decoded_row_scale * S ((S (a)) * bcf_row_scale_scale_lmd_old_choose) + (bcf_row_scale_lmd_old_choose))) /\ (((exists bcf_height_lmd_old_choose_decoded_value. bcf_height_lmd_old_choose_decoded_value + S (C) = S ((S (b)) * bcf_row_scale_lmd_old_choose)) /\ exists bcf_quotient_lmd_old_choose_decoded_value. bcf_row_code_lmd_old_choose = bcf_quotient_lmd_old_choose_decoded_value * S ((S (b)) * bcf_row_scale_lmd_old_choose) + (C))))))))))))
  18. 0018specialize hprefix i
  19. 0019apply hprefix
  20. 0020exact hi
  21. 0021cases hchoice
  22. 0022cases hchoice_witness
  23. 0023cases hchoice_witness_witness
  24. 0024cases hchoice_witness_witness_witness
  25. 0025cases hchoice_witness_witness_witness_right
  26. 0026cases hchoice_witness_witness_witness_right_right
  27. 0027have hupper : x = a
  28. 0028specialize beta_at_unique qb
  29. 0029specialize beta_at_unique qc
  30. 0030specialize beta_at_unique i
  31. 0031specialize beta_at_unique x
  32. 0032specialize beta_at_unique a
  33. 0033apply beta_at_unique
  34. 0034exact hchoice_witness_witness_witness_left
  35. 0035exact ha
  36. 0036have hlower : x1 = b
  37. 0037specialize beta_at_unique db
  38. 0038specialize beta_at_unique dc
  39. 0039specialize beta_at_unique i
  40. 0040specialize beta_at_unique x1
  41. 0041specialize beta_at_unique b
  42. 0042apply beta_at_unique
  43. 0043exact hchoice_witness_witness_witness_right_left
  44. 0044exact hb
  45. 0045have hvalue : x2 = C
  46. 0046specialize beta_at_unique z
  47. 0047specialize beta_at_unique t
  48. 0048specialize beta_at_unique i
  49. 0049specialize beta_at_unique x2
  50. 0050specialize beta_at_unique C
  51. 0051apply beta_at_unique
  52. 0052exact hchoice_witness_witness_witness_right_right_left
  53. 0053exact hC
  54. 0054rewrite hupper at hchoice_witness_witness_witness_right_right_right
  55. 0055rewrite hupper at hchoice_witness_witness_witness_right_right_right
  56. 0056rewrite hupper at hchoice_witness_witness_witness_right_right_right
  57. 0057rewrite hupper at hchoice_witness_witness_witness_right_right_right
  58. 0058rewrite hupper at hchoice_witness_witness_witness_right_right_right
  59. 0059rewrite hupper at hchoice_witness_witness_witness_right_right_right
  60. 0060rewrite hupper at hchoice_witness_witness_witness_right_right_right
  61. 0061rewrite hupper at hchoice_witness_witness_witness_right_right_right
  62. 0062rewrite hupper at hchoice_witness_witness_witness_right_right_right
  63. 0063rewrite hlower at hchoice_witness_witness_witness_right_right_right
  64. 0064rewrite hlower at hchoice_witness_witness_witness_right_right_right
  65. 0065rewrite hlower at hchoice_witness_witness_witness_right_right_right
  66. 0066rewrite hlower at hchoice_witness_witness_witness_right_right_right
  67. 0067rewrite hvalue at hchoice_witness_witness_witness_right_right_right
  68. 0068rewrite hvalue at hchoice_witness_witness_witness_right_right_right
  69. 0069rewrite hvalue at hchoice_witness_witness_witness_right_right_right
  70. 0070exact hchoice_witness_witness_witness_right_right_right