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 lb lc rb rc tb tc cb cc l. (forall kmc_index_kmcpr_source. (exists bcf_lt_gap_kmcpr_source_bound. bcf_lt_gap_kmcpr_source_bound + S (kmc_index_kmcpr_source) = S l) -> exists kmc_left_kmcpr_source kmc_right_kmcpr_source kmc_total_kmcpr_source kmc_bit_kmcpr_source. (((exists fs_h_kmcpr_source_left. fs_h_kmcpr_source_left + S (kmc_left_kmcpr_source) = S ((S (kmc_index_kmcpr_source)) * lc)) /\ exists fs_q_kmcpr_source_left. lb = fs_q_kmcpr_source_left * S ((S (kmc_index_kmcpr_source)) * lc) + (kmc_left_kmcpr_source))) /\ ((((exists fs_h_kmcpr_source_right. fs_h_kmcpr_source_right + S (kmc_right_kmcpr_source) = S ((S (kmc_index_kmcpr_source)) * rc)) /\ exists fs_q_kmcpr_source_right. rb = fs_q_kmcpr_source_right * S ((S (kmc_index_kmcpr_source)) * rc) + (kmc_right_kmcpr_source))) /\ ((((exists fs_h_kmcpr_source_total. fs_h_kmcpr_source_total + S (kmc_total_kmcpr_source) = S ((S (kmc_index_kmcpr_source)) * tc)) /\ exists fs_q_kmcpr_source_total. tb = fs_q_kmcpr_source_total * S ((S (kmc_index_kmcpr_source)) * tc) + (kmc_total_kmcpr_source))) /\ ((((exists fs_h_kmcpr_source_bit. fs_h_kmcpr_source_bit + S (kmc_bit_kmcpr_source) = S ((S (kmc_index_kmcpr_source)) * cc)) /\ exists fs_q_kmcpr_source_bit. cb = fs_q_kmcpr_source_bit * S ((S (kmc_index_kmcpr_source)) * cc) + (kmc_bit_kmcpr_source))) /\ (((kmc_bit_kmcpr_source = 0 /\ kmc_total_kmcpr_source = kmc_left_kmcpr_source + kmc_right_kmcpr_source) \/ (kmc_bit_kmcpr_source = 1 /\ kmc_total_kmcpr_source = S (kmc_left_kmcpr_source + kmc_right_kmcpr_source)))))))) -> (forall kmc_index_kmcpr_result. (exists bcf_lt_gap_kmcpr_result_bound. bcf_lt_gap_kmcpr_result_bound + S (kmc_index_kmcpr_result) = l) -> exists kmc_left_kmcpr_result kmc_right_kmcpr_result kmc_total_kmcpr_result kmc_bit_kmcpr_result. (((exists fs_h_kmcpr_result_left. fs_h_kmcpr_result_left + S (kmc_left_kmcpr_result) = S ((S (kmc_index_kmcpr_result)) * lc)) /\ exists fs_q_kmcpr_result_left. lb = fs_q_kmcpr_result_left * S ((S (kmc_index_kmcpr_result)) * lc) + (kmc_left_kmcpr_result))) /\ ((((exists fs_h_kmcpr_result_right. fs_h_kmcpr_result_right + S (kmc_right_kmcpr_result) = S ((S (kmc_index_kmcpr_result)) * rc)) /\ exists fs_q_kmcpr_result_right. rb = fs_q_kmcpr_result_right * S ((S (kmc_index_kmcpr_result)) * rc) + (kmc_right_kmcpr_result))) /\ ((((exists fs_h_kmcpr_result_total. fs_h_kmcpr_result_total + S (kmc_total_kmcpr_result) = S ((S (kmc_index_kmcpr_result)) * tc)) /\ exists fs_q_kmcpr_result_total. tb = fs_q_kmcpr_result_total * S ((S (kmc_index_kmcpr_result)) * tc) + (kmc_total_kmcpr_result))) /\ ((((exists fs_h_kmcpr_result_bit. fs_h_kmcpr_result_bit + S (kmc_bit_kmcpr_result) = S ((S (kmc_index_kmcpr_result)) * cc)) /\ exists fs_q_kmcpr_result_bit. cb = fs_q_kmcpr_result_bit * S ((S (kmc_index_kmcpr_result)) * cc) + (kmc_bit_kmcpr_result))) /\ (((kmc_bit_kmcpr_result = 0 /\ kmc_total_kmcpr_result = kmc_left_kmcpr_result + kmc_right_kmcpr_result) \/ (kmc_bit_kmcpr_result = 1 /\ kmc_total_kmcpr_result = S (kmc_left_kmcpr_result + kmc_right_kmcpr_result))))))))Constructive proof overview
Generated structural guide
Dropping the terminal position preserves a three-prefix additive carry code.
The unchanged tactic script uses 1 declared prerequisite and contains 18 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
le_succ 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.