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 e p q. (exists pa_b_bl_power pa_c_bl_power. ((forall pa_i_bl_power_repeat. (exists pa_lt_bl_power_repeat_bound. pa_lt_bl_power_repeat_bound + S pa_i_bl_power_repeat = e) -> (((exists pa_h_bl_power_repeat_decoded. pa_h_bl_power_repeat_decoded + S (2) = S ((S (pa_i_bl_power_repeat)) * pa_c_bl_power)) /\ exists pa_q_bl_power_repeat_decoded. pa_b_bl_power = pa_q_bl_power_repeat_decoded * S ((S (pa_i_bl_power_repeat)) * pa_c_bl_power) + (2)))) /\ (exists pa_u_bl_power_product pa_v_bl_power_product. ((((exists pa_h_bl_power_product_start. pa_h_bl_power_product_start + S (1) = S ((S (0)) * pa_v_bl_power_product)) /\ exists pa_q_bl_power_product_start. pa_u_bl_power_product = pa_q_bl_power_product_start * S ((S (0)) * pa_v_bl_power_product) + (1))) /\ ((((exists pa_h_bl_power_product_terminal. pa_h_bl_power_product_terminal + S (p) = S ((S (e)) * pa_v_bl_power_product)) /\ exists pa_q_bl_power_product_terminal. pa_u_bl_power_product = pa_q_bl_power_product_terminal * S ((S (e)) * pa_v_bl_power_product) + (p))) /\ forall pa_i_bl_power_product. (exists pa_lt_bl_power_product_bound. pa_lt_bl_power_product_bound + S pa_i_bl_power_product = e) -> exists pa_p_bl_power_product pa_r_bl_power_product pa_s_bl_power_product. ((((exists pa_h_bl_power_product_factor. pa_h_bl_power_product_factor + S (pa_p_bl_power_product) = S ((S (pa_i_bl_power_product)) * pa_c_bl_power)) /\ exists pa_q_bl_power_product_factor. pa_b_bl_power = pa_q_bl_power_product_factor * S ((S (pa_i_bl_power_product)) * pa_c_bl_power) + (pa_p_bl_power_product))) /\ ((((exists pa_h_bl_power_product_partial. pa_h_bl_power_product_partial + S (pa_r_bl_power_product) = S ((S (pa_i_bl_power_product)) * pa_v_bl_power_product)) /\ exists pa_q_bl_power_product_partial. pa_u_bl_power_product = pa_q_bl_power_product_partial * S ((S (pa_i_bl_power_product)) * pa_v_bl_power_product) + (pa_r_bl_power_product))) /\ ((((exists pa_h_bl_power_product_successor. pa_h_bl_power_product_successor + S (pa_s_bl_power_product) = S ((S (S pa_i_bl_power_product)) * pa_v_bl_power_product)) /\ exists pa_q_bl_power_product_successor. pa_u_bl_power_product = pa_q_bl_power_product_successor * S ((S (S pa_i_bl_power_product)) * pa_v_bl_power_product) + (pa_s_bl_power_product))) /\ pa_s_bl_power_product = pa_r_bl_power_product * pa_p_bl_power_product)))))))) -> (exists pa_b_bl_other_power pa_c_bl_other_power. ((forall pa_i_bl_other_power_repeat. (exists pa_lt_bl_other_power_repeat_bound. pa_lt_bl_other_power_repeat_bound + S pa_i_bl_other_power_repeat = e) -> (((exists pa_h_bl_other_power_repeat_decoded. pa_h_bl_other_power_repeat_decoded + S (2) = S ((S (pa_i_bl_other_power_repeat)) * pa_c_bl_other_power)) /\ exists pa_q_bl_other_power_repeat_decoded. pa_b_bl_other_power = pa_q_bl_other_power_repeat_decoded * S ((S (pa_i_bl_other_power_repeat)) * pa_c_bl_other_power) + (2)))) /\ (exists pa_u_bl_other_power_product pa_v_bl_other_power_product. ((((exists pa_h_bl_other_power_product_start. pa_h_bl_other_power_product_start + S (1) = S ((S (0)) * pa_v_bl_other_power_product)) /\ exists pa_q_bl_other_power_product_start. pa_u_bl_other_power_product = pa_q_bl_other_power_product_start * S ((S (0)) * pa_v_bl_other_power_product) + (1))) /\ ((((exists pa_h_bl_other_power_product_terminal. pa_h_bl_other_power_product_terminal + S (q) = S ((S (e)) * pa_v_bl_other_power_product)) /\ exists pa_q_bl_other_power_product_terminal. pa_u_bl_other_power_product = pa_q_bl_other_power_product_terminal * S ((S (e)) * pa_v_bl_other_power_product) + (q))) /\ forall pa_i_bl_other_power_product. (exists pa_lt_bl_other_power_product_bound. pa_lt_bl_other_power_product_bound + S pa_i_bl_other_power_product = e) -> exists pa_p_bl_other_power_product pa_r_bl_other_power_product pa_s_bl_other_power_product. ((((exists pa_h_bl_other_power_product_factor. pa_h_bl_other_power_product_factor + S (pa_p_bl_other_power_product) = S ((S (pa_i_bl_other_power_product)) * pa_c_bl_other_power)) /\ exists pa_q_bl_other_power_product_factor. pa_b_bl_other_power = pa_q_bl_other_power_product_factor * S ((S (pa_i_bl_other_power_product)) * pa_c_bl_other_power) + (pa_p_bl_other_power_product))) /\ ((((exists pa_h_bl_other_power_product_partial. pa_h_bl_other_power_product_partial + S (pa_r_bl_other_power_product) = S ((S (pa_i_bl_other_power_product)) * pa_v_bl_other_power_product)) /\ exists pa_q_bl_other_power_product_partial. pa_u_bl_other_power_product = pa_q_bl_other_power_product_partial * S ((S (pa_i_bl_other_power_product)) * pa_v_bl_other_power_product) + (pa_r_bl_other_power_product))) /\ ((((exists pa_h_bl_other_power_product_successor. pa_h_bl_other_power_product_successor + S (pa_s_bl_other_power_product) = S ((S (S pa_i_bl_other_power_product)) * pa_v_bl_other_power_product)) /\ exists pa_q_bl_other_power_product_successor. pa_u_bl_other_power_product = pa_q_bl_other_power_product_successor * S ((S (S pa_i_bl_other_power_product)) * pa_v_bl_other_power_product) + (pa_s_bl_other_power_product))) /\ pa_s_bl_other_power_product = pa_r_bl_other_power_product * pa_p_bl_other_power_product)))))))) -> p = qConstructive proof overview
Generated structural guide
The relational power of two is functional at every exponent.
The unchanged tactic script uses 1 declared prerequisite and contains 12 exact native proof lines.
Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
pow_functional Stable theorem; checked-use authorizedDirect dependents
none
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.