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 b c sb sc cb cc. forall mkm_index_binempty. (exists mkm_lt_binempty_bound. mkm_lt_binempty_bound + S (mkm_index_binempty) = (0)) -> (exists mkm_value_binempty_point mkm_partial_binempty_point mkm_factor_binempty_point. (((exists fs_h_mkm_binempty_point_source. fs_h_mkm_binempty_point_source + S (mkm_value_binempty_point) = S ((S (mkm_index_binempty)) * c)) /\ exists fs_q_mkm_binempty_point_source. b = fs_q_mkm_binempty_point_source * S ((S (mkm_index_binempty)) * c) + (mkm_value_binempty_point))) /\ ((((exists fs_h_mkm_binempty_point_partial. fs_h_mkm_binempty_point_partial + S (mkm_partial_binempty_point) = S ((S (mkm_index_binempty)) * sc)) /\ exists fs_q_mkm_binempty_point_partial. sb = fs_q_mkm_binempty_point_partial * S ((S (mkm_index_binempty)) * sc) + (mkm_partial_binempty_point))) /\ ((((exists bcf_lt_gap_mkm_binempty_point_choose_out_of_range. bcf_lt_gap_mkm_binempty_point_choose_out_of_range + S (mkm_partial_binempty_point + mkm_value_binempty_point) = mkm_partial_binempty_point) /\ mkm_factor_binempty_point = 0) \/ ((exists bcf_le_gap_mkm_binempty_point_choose_in_range. bcf_le_gap_mkm_binempty_point_choose_in_range + (mkm_partial_binempty_point) = mkm_partial_binempty_point + mkm_value_binempty_point) /\ (exists bcf_row_code_code_mkm_binempty_point_choose bcf_row_code_scale_mkm_binempty_point_choose bcf_row_scale_code_mkm_binempty_point_choose bcf_row_scale_scale_mkm_binempty_point_choose bcf_row_code_mkm_binempty_point_choose bcf_row_scale_mkm_binempty_point_choose. ((forall bcf_row_index_mkm_binempty_point_choose_table. (exists bcf_lt_gap_mkm_binempty_point_choose_table_row_bound. bcf_lt_gap_mkm_binempty_point_choose_table_row_bound + S (bcf_row_index_mkm_binempty_point_choose_table) = S (mkm_partial_binempty_point + mkm_value_binempty_point)) -> exists bcf_row_code_mkm_binempty_point_choose_table bcf_row_scale_mkm_binempty_point_choose_table. ((((exists bcf_height_mkm_binempty_point_choose_table_decoded_row_code. bcf_height_mkm_binempty_point_choose_table_decoded_row_code + S (bcf_row_code_mkm_binempty_point_choose_table) = S ((S (bcf_row_index_mkm_binempty_point_choose_table)) * bcf_row_code_scale_mkm_binempty_point_choose)) /\ exists bcf_quotient_mkm_binempty_point_choose_table_decoded_row_code. bcf_row_code_code_mkm_binempty_point_choose = bcf_quotient_mkm_binempty_point_choose_table_decoded_row_code * S ((S (bcf_row_index_mkm_binempty_point_choose_table)) * bcf_row_code_scale_mkm_binempty_point_choose) + (bcf_row_code_mkm_binempty_point_choose_table))) /\ ((((exists bcf_height_mkm_binempty_point_choose_table_decoded_row_scale. bcf_height_mkm_binempty_point_choose_table_decoded_row_scale + S (bcf_row_scale_mkm_binempty_point_choose_table) = S ((S (bcf_row_index_mkm_binempty_point_choose_table)) * bcf_row_scale_scale_mkm_binempty_point_choose)) /\ exists bcf_quotient_mkm_binempty_point_choose_table_decoded_row_scale. bcf_row_scale_code_mkm_binempty_point_choose = bcf_quotient_mkm_binempty_point_choose_table_decoded_row_scale * S ((S (bcf_row_index_mkm_binempty_point_choose_table)) * bcf_row_scale_scale_mkm_binempty_point_choose) + (bcf_row_scale_mkm_binempty_point_choose_table))) /\ ((bcf_row_index_mkm_binempty_point_choose_table = 0 /\ (forall bcf_index_mkm_binempty_point_choose_table_zero_row. (exists bcf_lt_gap_mkm_binempty_point_choose_table_zero_row_bound. bcf_lt_gap_mkm_binempty_point_choose_table_zero_row_bound + S (bcf_index_mkm_binempty_point_choose_table_zero_row) = S (mkm_partial_binempty_point + mkm_value_binempty_point)) -> exists bcf_value_mkm_binempty_point_choose_table_zero_row. ((((exists bcf_height_mkm_binempty_point_choose_table_zero_row_entry. bcf_height_mkm_binempty_point_choose_table_zero_row_entry + S (bcf_value_mkm_binempty_point_choose_table_zero_row) = S ((S (bcf_index_mkm_binempty_point_choose_table_zero_row)) * bcf_row_scale_mkm_binempty_point_choose_table)) /\ exists bcf_quotient_mkm_binempty_point_choose_table_zero_row_entry. bcf_row_code_mkm_binempty_point_choose_table = bcf_quotient_mkm_binempty_point_choose_table_zero_row_entry * S ((S (bcf_index_mkm_binempty_point_choose_table_zero_row)) * bcf_row_scale_mkm_binempty_point_choose_table) + (bcf_value_mkm_binempty_point_choose_table_zero_row))) /\ ((bcf_index_mkm_binempty_point_choose_table_zero_row = 0 /\ bcf_value_mkm_binempty_point_choose_table_zero_row = 1) \/ exists bcf_predecessor_mkm_binempty_point_choose_table_zero_row. bcf_index_mkm_binempty_point_choose_table_zero_row = S bcf_predecessor_mkm_binempty_point_choose_table_zero_row /\ bcf_value_mkm_binempty_point_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_mkm_binempty_point_choose_table bcf_previous_code_mkm_binempty_point_choose_table bcf_previous_scale_mkm_binempty_point_choose_table. bcf_row_index_mkm_binempty_point_choose_table = S bcf_predecessor_mkm_binempty_point_choose_table /\ ((((exists bcf_height_mkm_binempty_point_choose_table_decoded_previous_code. bcf_height_mkm_binempty_point_choose_table_decoded_previous_code + S (bcf_previous_code_mkm_binempty_point_choose_table) = S ((S (bcf_predecessor_mkm_binempty_point_choose_table)) * bcf_row_code_scale_mkm_binempty_point_choose)) /\ exists bcf_quotient_mkm_binempty_point_choose_table_decoded_previous_code. bcf_row_code_code_mkm_binempty_point_choose = bcf_quotient_mkm_binempty_point_choose_table_decoded_previous_code * S ((S (bcf_predecessor_mkm_binempty_point_choose_table)) * bcf_row_code_scale_mkm_binempty_point_choose) + (bcf_previous_code_mkm_binempty_point_choose_table))) /\ ((((exists bcf_height_mkm_binempty_point_choose_table_decoded_previous_scale. bcf_height_mkm_binempty_point_choose_table_decoded_previous_scale + S (bcf_previous_scale_mkm_binempty_point_choose_table) = S ((S (bcf_predecessor_mkm_binempty_point_choose_table)) * bcf_row_scale_scale_mkm_binempty_point_choose)) /\ exists bcf_quotient_mkm_binempty_point_choose_table_decoded_previous_scale. bcf_row_scale_code_mkm_binempty_point_choose = bcf_quotient_mkm_binempty_point_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_mkm_binempty_point_choose_table)) * bcf_row_scale_scale_mkm_binempty_point_choose) + (bcf_previous_scale_mkm_binempty_point_choose_table))) /\ (forall bcf_index_mkm_binempty_point_choose_table_row_step. (exists bcf_lt_gap_mkm_binempty_point_choose_table_row_step_bound. bcf_lt_gap_mkm_binempty_point_choose_table_row_step_bound + S (bcf_index_mkm_binempty_point_choose_table_row_step) = S (mkm_partial_binempty_point + mkm_value_binempty_point)) -> exists bcf_value_mkm_binempty_point_choose_table_row_step. ((((exists bcf_height_mkm_binempty_point_choose_table_row_step_entry. bcf_height_mkm_binempty_point_choose_table_row_step_entry + S (bcf_value_mkm_binempty_point_choose_table_row_step) = S ((S (bcf_index_mkm_binempty_point_choose_table_row_step)) * bcf_row_scale_mkm_binempty_point_choose_table)) /\ exists bcf_quotient_mkm_binempty_point_choose_table_row_step_entry. bcf_row_code_mkm_binempty_point_choose_table = bcf_quotient_mkm_binempty_point_choose_table_row_step_entry * S ((S (bcf_index_mkm_binempty_point_choose_table_row_step)) * bcf_row_scale_mkm_binempty_point_choose_table) + (bcf_value_mkm_binempty_point_choose_table_row_step))) /\ ((bcf_index_mkm_binempty_point_choose_table_row_step = 0 /\ bcf_value_mkm_binempty_point_choose_table_row_step = 1) \/ exists bcf_predecessor_mkm_binempty_point_choose_table_row_step bcf_left_mkm_binempty_point_choose_table_row_step bcf_right_mkm_binempty_point_choose_table_row_step. bcf_index_mkm_binempty_point_choose_table_row_step = S bcf_predecessor_mkm_binempty_point_choose_table_row_step /\ ((((exists bcf_height_mkm_binempty_point_choose_table_row_step_previous_left. bcf_height_mkm_binempty_point_choose_table_row_step_previous_left + S (bcf_left_mkm_binempty_point_choose_table_row_step) = S ((S (bcf_predecessor_mkm_binempty_point_choose_table_row_step)) * bcf_previous_scale_mkm_binempty_point_choose_table)) /\ exists bcf_quotient_mkm_binempty_point_choose_table_row_step_previous_left. bcf_previous_code_mkm_binempty_point_choose_table = bcf_quotient_mkm_binempty_point_choose_table_row_step_previous_left * S ((S (bcf_predecessor_mkm_binempty_point_choose_table_row_step)) * bcf_previous_scale_mkm_binempty_point_choose_table) + (bcf_left_mkm_binempty_point_choose_table_row_step))) /\ ((((exists bcf_height_mkm_binempty_point_choose_table_row_step_previous_right. bcf_height_mkm_binempty_point_choose_table_row_step_previous_right + S (bcf_right_mkm_binempty_point_choose_table_row_step) = S ((S (S (bcf_predecessor_mkm_binempty_point_choose_table_row_step))) * bcf_previous_scale_mkm_binempty_point_choose_table)) /\ exists bcf_quotient_mkm_binempty_point_choose_table_row_step_previous_right. bcf_previous_code_mkm_binempty_point_choose_table = bcf_quotient_mkm_binempty_point_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_mkm_binempty_point_choose_table_row_step))) * bcf_previous_scale_mkm_binempty_point_choose_table) + (bcf_right_mkm_binempty_point_choose_table_row_step))) /\ bcf_value_mkm_binempty_point_choose_table_row_step = bcf_left_mkm_binempty_point_choose_table_row_step + bcf_right_mkm_binempty_point_choose_table_row_step))))))))))) /\ ((((exists bcf_height_mkm_binempty_point_choose_decoded_row_code. bcf_height_mkm_binempty_point_choose_decoded_row_code + S (bcf_row_code_mkm_binempty_point_choose) = S ((S (mkm_partial_binempty_point + mkm_value_binempty_point)) * bcf_row_code_scale_mkm_binempty_point_choose)) /\ exists bcf_quotient_mkm_binempty_point_choose_decoded_row_code. bcf_row_code_code_mkm_binempty_point_choose = bcf_quotient_mkm_binempty_point_choose_decoded_row_code * S ((S (mkm_partial_binempty_point + mkm_value_binempty_point)) * bcf_row_code_scale_mkm_binempty_point_choose) + (bcf_row_code_mkm_binempty_point_choose))) /\ ((((exists bcf_height_mkm_binempty_point_choose_decoded_row_scale. bcf_height_mkm_binempty_point_choose_decoded_row_scale + S (bcf_row_scale_mkm_binempty_point_choose) = S ((S (mkm_partial_binempty_point + mkm_value_binempty_point)) * bcf_row_scale_scale_mkm_binempty_point_choose)) /\ exists bcf_quotient_mkm_binempty_point_choose_decoded_row_scale. bcf_row_scale_code_mkm_binempty_point_choose = bcf_quotient_mkm_binempty_point_choose_decoded_row_scale * S ((S (mkm_partial_binempty_point + mkm_value_binempty_point)) * bcf_row_scale_scale_mkm_binempty_point_choose) + (bcf_row_scale_mkm_binempty_point_choose))) /\ (((exists bcf_height_mkm_binempty_point_choose_decoded_value. bcf_height_mkm_binempty_point_choose_decoded_value + S (mkm_factor_binempty_point) = S ((S (mkm_partial_binempty_point)) * bcf_row_scale_mkm_binempty_point_choose)) /\ exists bcf_quotient_mkm_binempty_point_choose_decoded_value. bcf_row_code_mkm_binempty_point_choose = bcf_quotient_mkm_binempty_point_choose_decoded_value * S ((S (mkm_partial_binempty_point)) * bcf_row_scale_mkm_binempty_point_choose) + (mkm_factor_binempty_point))))))))) /\ (((exists fs_h_mkm_binempty_point_factor. fs_h_mkm_binempty_point_factor + S (mkm_factor_binempty_point) = S ((S (mkm_index_binempty)) * cc)) /\ exists fs_q_mkm_binempty_point_factor. cb = fs_q_mkm_binempty_point_factor * S ((S (mkm_index_binempty)) * cc) + (mkm_factor_binempty_point))))))Constructive proof overview
Generated structural guide
The empty multinomial factor prefix requires no binomial entries.
The unchanged tactic script uses 2 declared prerequisites and contains 15 exact native proof lines.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
lt_not_le Stable theorem; checked-use authorized zero_le Stable theorem; checked-use authorizedDirect dependents
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
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.
01Fix variables and assumptionsL1–8
02Separate the logical casesL9–9
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L9
exfalso