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 qb qc db dc. exists z t. (forall lmd_choose_index_choose_empty. (exists lmd_gap_choose_empty_bound. lmd_gap_choose_empty_bound + S (lmd_choose_index_choose_empty) = (0)) -> exists lmd_choose_upper_choose_empty lmd_choose_lower_choose_empty lmd_choose_value_choose_empty. ((((exists ff_h_lmd_choose_empty_upper. ff_h_lmd_choose_empty_upper + S (lmd_choose_upper_choose_empty) = S ((S (lmd_choose_index_choose_empty)) * qc)) /\ exists ff_q_lmd_choose_empty_upper. qb = ff_q_lmd_choose_empty_upper * S ((S (lmd_choose_index_choose_empty)) * qc) + (lmd_choose_upper_choose_empty))) /\ ((((exists ff_h_lmd_choose_empty_lower. ff_h_lmd_choose_empty_lower + S (lmd_choose_lower_choose_empty) = S ((S (lmd_choose_index_choose_empty)) * dc)) /\ exists ff_q_lmd_choose_empty_lower. db = ff_q_lmd_choose_empty_lower * S ((S (lmd_choose_index_choose_empty)) * dc) + (lmd_choose_lower_choose_empty))) /\ ((((exists ff_h_lmd_choose_empty_result. ff_h_lmd_choose_empty_result + S (lmd_choose_value_choose_empty) = S ((S (lmd_choose_index_choose_empty)) * t)) /\ exists ff_q_lmd_choose_empty_result. z = ff_q_lmd_choose_empty_result * S ((S (lmd_choose_index_choose_empty)) * t) + (lmd_choose_value_choose_empty))) /\ (((exists bcf_lt_gap_lmd_choose_empty_choose_out_of_range. bcf_lt_gap_lmd_choose_empty_choose_out_of_range + S (lmd_choose_upper_choose_empty) = lmd_choose_lower_choose_empty) /\ lmd_choose_value_choose_empty = 0) \/ ((exists bcf_le_gap_lmd_choose_empty_choose_in_range. bcf_le_gap_lmd_choose_empty_choose_in_range + (lmd_choose_lower_choose_empty) = lmd_choose_upper_choose_empty) /\ (exists bcf_row_code_code_lmd_choose_empty_choose bcf_row_code_scale_lmd_choose_empty_choose bcf_row_scale_code_lmd_choose_empty_choose bcf_row_scale_scale_lmd_choose_empty_choose bcf_row_code_lmd_choose_empty_choose bcf_row_scale_lmd_choose_empty_choose. ((forall bcf_row_index_lmd_choose_empty_choose_table. (exists bcf_lt_gap_lmd_choose_empty_choose_table_row_bound. bcf_lt_gap_lmd_choose_empty_choose_table_row_bound + S (bcf_row_index_lmd_choose_empty_choose_table) = S (lmd_choose_upper_choose_empty)) -> exists bcf_row_code_lmd_choose_empty_choose_table bcf_row_scale_lmd_choose_empty_choose_table. ((((exists bcf_height_lmd_choose_empty_choose_table_decoded_row_code. bcf_height_lmd_choose_empty_choose_table_decoded_row_code + S (bcf_row_code_lmd_choose_empty_choose_table) = S ((S (bcf_row_index_lmd_choose_empty_choose_table)) * bcf_row_code_scale_lmd_choose_empty_choose)) /\ exists bcf_quotient_lmd_choose_empty_choose_table_decoded_row_code. bcf_row_code_code_lmd_choose_empty_choose = bcf_quotient_lmd_choose_empty_choose_table_decoded_row_code * S ((S (bcf_row_index_lmd_choose_empty_choose_table)) * bcf_row_code_scale_lmd_choose_empty_choose) + (bcf_row_code_lmd_choose_empty_choose_table))) /\ ((((exists bcf_height_lmd_choose_empty_choose_table_decoded_row_scale. bcf_height_lmd_choose_empty_choose_table_decoded_row_scale + S (bcf_row_scale_lmd_choose_empty_choose_table) = S ((S (bcf_row_index_lmd_choose_empty_choose_table)) * bcf_row_scale_scale_lmd_choose_empty_choose)) /\ exists bcf_quotient_lmd_choose_empty_choose_table_decoded_row_scale. bcf_row_scale_code_lmd_choose_empty_choose = bcf_quotient_lmd_choose_empty_choose_table_decoded_row_scale * S ((S (bcf_row_index_lmd_choose_empty_choose_table)) * bcf_row_scale_scale_lmd_choose_empty_choose) + (bcf_row_scale_lmd_choose_empty_choose_table))) /\ ((bcf_row_index_lmd_choose_empty_choose_table = 0 /\ (forall bcf_index_lmd_choose_empty_choose_table_zero_row. (exists bcf_lt_gap_lmd_choose_empty_choose_table_zero_row_bound. bcf_lt_gap_lmd_choose_empty_choose_table_zero_row_bound + S (bcf_index_lmd_choose_empty_choose_table_zero_row) = S (lmd_choose_upper_choose_empty)) -> exists bcf_value_lmd_choose_empty_choose_table_zero_row. ((((exists bcf_height_lmd_choose_empty_choose_table_zero_row_entry. bcf_height_lmd_choose_empty_choose_table_zero_row_entry + S (bcf_value_lmd_choose_empty_choose_table_zero_row) = S ((S (bcf_index_lmd_choose_empty_choose_table_zero_row)) * bcf_row_scale_lmd_choose_empty_choose_table)) /\ exists bcf_quotient_lmd_choose_empty_choose_table_zero_row_entry. bcf_row_code_lmd_choose_empty_choose_table = bcf_quotient_lmd_choose_empty_choose_table_zero_row_entry * S ((S (bcf_index_lmd_choose_empty_choose_table_zero_row)) * bcf_row_scale_lmd_choose_empty_choose_table) + (bcf_value_lmd_choose_empty_choose_table_zero_row))) /\ ((bcf_index_lmd_choose_empty_choose_table_zero_row = 0 /\ bcf_value_lmd_choose_empty_choose_table_zero_row = 1) \/ exists bcf_predecessor_lmd_choose_empty_choose_table_zero_row. bcf_index_lmd_choose_empty_choose_table_zero_row = S bcf_predecessor_lmd_choose_empty_choose_table_zero_row /\ bcf_value_lmd_choose_empty_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lmd_choose_empty_choose_table bcf_previous_code_lmd_choose_empty_choose_table bcf_previous_scale_lmd_choose_empty_choose_table. bcf_row_index_lmd_choose_empty_choose_table = S bcf_predecessor_lmd_choose_empty_choose_table /\ ((((exists bcf_height_lmd_choose_empty_choose_table_decoded_previous_code. bcf_height_lmd_choose_empty_choose_table_decoded_previous_code + S (bcf_previous_code_lmd_choose_empty_choose_table) = S ((S (bcf_predecessor_lmd_choose_empty_choose_table)) * bcf_row_code_scale_lmd_choose_empty_choose)) /\ exists bcf_quotient_lmd_choose_empty_choose_table_decoded_previous_code. bcf_row_code_code_lmd_choose_empty_choose = bcf_quotient_lmd_choose_empty_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lmd_choose_empty_choose_table)) * bcf_row_code_scale_lmd_choose_empty_choose) + (bcf_previous_code_lmd_choose_empty_choose_table))) /\ ((((exists bcf_height_lmd_choose_empty_choose_table_decoded_previous_scale. bcf_height_lmd_choose_empty_choose_table_decoded_previous_scale + S (bcf_previous_scale_lmd_choose_empty_choose_table) = S ((S (bcf_predecessor_lmd_choose_empty_choose_table)) * bcf_row_scale_scale_lmd_choose_empty_choose)) /\ exists bcf_quotient_lmd_choose_empty_choose_table_decoded_previous_scale. bcf_row_scale_code_lmd_choose_empty_choose = bcf_quotient_lmd_choose_empty_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lmd_choose_empty_choose_table)) * bcf_row_scale_scale_lmd_choose_empty_choose) + (bcf_previous_scale_lmd_choose_empty_choose_table))) /\ (forall bcf_index_lmd_choose_empty_choose_table_row_step. (exists bcf_lt_gap_lmd_choose_empty_choose_table_row_step_bound. bcf_lt_gap_lmd_choose_empty_choose_table_row_step_bound + S (bcf_index_lmd_choose_empty_choose_table_row_step) = S (lmd_choose_upper_choose_empty)) -> exists bcf_value_lmd_choose_empty_choose_table_row_step. ((((exists bcf_height_lmd_choose_empty_choose_table_row_step_entry. bcf_height_lmd_choose_empty_choose_table_row_step_entry + S (bcf_value_lmd_choose_empty_choose_table_row_step) = S ((S (bcf_index_lmd_choose_empty_choose_table_row_step)) * bcf_row_scale_lmd_choose_empty_choose_table)) /\ exists bcf_quotient_lmd_choose_empty_choose_table_row_step_entry. bcf_row_code_lmd_choose_empty_choose_table = bcf_quotient_lmd_choose_empty_choose_table_row_step_entry * S ((S (bcf_index_lmd_choose_empty_choose_table_row_step)) * bcf_row_scale_lmd_choose_empty_choose_table) + (bcf_value_lmd_choose_empty_choose_table_row_step))) /\ ((bcf_index_lmd_choose_empty_choose_table_row_step = 0 /\ bcf_value_lmd_choose_empty_choose_table_row_step = 1) \/ exists bcf_predecessor_lmd_choose_empty_choose_table_row_step bcf_left_lmd_choose_empty_choose_table_row_step bcf_right_lmd_choose_empty_choose_table_row_step. bcf_index_lmd_choose_empty_choose_table_row_step = S bcf_predecessor_lmd_choose_empty_choose_table_row_step /\ ((((exists bcf_height_lmd_choose_empty_choose_table_row_step_previous_left. bcf_height_lmd_choose_empty_choose_table_row_step_previous_left + S (bcf_left_lmd_choose_empty_choose_table_row_step) = S ((S (bcf_predecessor_lmd_choose_empty_choose_table_row_step)) * bcf_previous_scale_lmd_choose_empty_choose_table)) /\ exists bcf_quotient_lmd_choose_empty_choose_table_row_step_previous_left. bcf_previous_code_lmd_choose_empty_choose_table = bcf_quotient_lmd_choose_empty_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lmd_choose_empty_choose_table_row_step)) * bcf_previous_scale_lmd_choose_empty_choose_table) + (bcf_left_lmd_choose_empty_choose_table_row_step))) /\ ((((exists bcf_height_lmd_choose_empty_choose_table_row_step_previous_right. bcf_height_lmd_choose_empty_choose_table_row_step_previous_right + S (bcf_right_lmd_choose_empty_choose_table_row_step) = S ((S (S (bcf_predecessor_lmd_choose_empty_choose_table_row_step))) * bcf_previous_scale_lmd_choose_empty_choose_table)) /\ exists bcf_quotient_lmd_choose_empty_choose_table_row_step_previous_right. bcf_previous_code_lmd_choose_empty_choose_table = bcf_quotient_lmd_choose_empty_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lmd_choose_empty_choose_table_row_step))) * bcf_previous_scale_lmd_choose_empty_choose_table) + (bcf_right_lmd_choose_empty_choose_table_row_step))) /\ bcf_value_lmd_choose_empty_choose_table_row_step = bcf_left_lmd_choose_empty_choose_table_row_step + bcf_right_lmd_choose_empty_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lmd_choose_empty_choose_decoded_row_code. bcf_height_lmd_choose_empty_choose_decoded_row_code + S (bcf_row_code_lmd_choose_empty_choose) = S ((S (lmd_choose_upper_choose_empty)) * bcf_row_code_scale_lmd_choose_empty_choose)) /\ exists bcf_quotient_lmd_choose_empty_choose_decoded_row_code. bcf_row_code_code_lmd_choose_empty_choose = bcf_quotient_lmd_choose_empty_choose_decoded_row_code * S ((S (lmd_choose_upper_choose_empty)) * bcf_row_code_scale_lmd_choose_empty_choose) + (bcf_row_code_lmd_choose_empty_choose))) /\ ((((exists bcf_height_lmd_choose_empty_choose_decoded_row_scale. bcf_height_lmd_choose_empty_choose_decoded_row_scale + S (bcf_row_scale_lmd_choose_empty_choose) = S ((S (lmd_choose_upper_choose_empty)) * bcf_row_scale_scale_lmd_choose_empty_choose)) /\ exists bcf_quotient_lmd_choose_empty_choose_decoded_row_scale. bcf_row_scale_code_lmd_choose_empty_choose = bcf_quotient_lmd_choose_empty_choose_decoded_row_scale * S ((S (lmd_choose_upper_choose_empty)) * bcf_row_scale_scale_lmd_choose_empty_choose) + (bcf_row_scale_lmd_choose_empty_choose))) /\ (((exists bcf_height_lmd_choose_empty_choose_decoded_value. bcf_height_lmd_choose_empty_choose_decoded_value + S (lmd_choose_value_choose_empty) = S ((S (lmd_choose_lower_choose_empty)) * bcf_row_scale_lmd_choose_empty_choose)) /\ exists bcf_quotient_lmd_choose_empty_choose_decoded_value. bcf_row_code_lmd_choose_empty_choose = bcf_quotient_lmd_choose_empty_choose_decoded_value * S ((S (lmd_choose_lower_choose_empty)) * bcf_row_scale_lmd_choose_empty_choose) + (lmd_choose_value_choose_empty)))))))))))))Constructive proof overview
Generated structural guide
Any pair of beta-coded source streams has a constructively empty relational-Choose coefficient prefix.
The unchanged tactic script uses 0 declared prerequisites and contains 13 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
Historical empty-context replay experiment only; that experiment persisted no certificate and granted no release authority. Current checked use follows separately sealed, independently verified proof bundles; there is no Stable promotion.
Proof neighborhood
Direct dependencies
none
Direct 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–4
02Construct an explicit witnessL5–6
03Fix variables and assumptionsL7–8
04Separate the logical casesL9–10
05Calculate and transport equalitiesL11–11
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L11
rewrite PA4 at hi_witness