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 a l n d p. (exists ff_u_hd_pth_inverse_pair ff_v_hd_pth_inverse_pair ff_d_hd_pth_inverse_pair ff_e_hd_pth_inverse_pair. ((((((exists fs_h_ph_hd_pth_inverse_pair_body_value_start. fs_h_ph_hd_pth_inverse_pair_body_value_start + S (0) = S ((S (0)) * ff_v_hd_pth_inverse_pair)) /\ exists fs_q_ph_hd_pth_inverse_pair_body_value_start. ff_u_hd_pth_inverse_pair = fs_q_ph_hd_pth_inverse_pair_body_value_start * S ((S (0)) * ff_v_hd_pth_inverse_pair) + (0))) /\ ((((exists fs_h_ph_hd_pth_inverse_pair_body_value_terminal. fs_h_ph_hd_pth_inverse_pair_body_value_terminal + S (n) = S ((S (l)) * ff_v_hd_pth_inverse_pair)) /\ exists fs_q_ph_hd_pth_inverse_pair_body_value_terminal. ff_u_hd_pth_inverse_pair = fs_q_ph_hd_pth_inverse_pair_body_value_terminal * S ((S (l)) * ff_v_hd_pth_inverse_pair) + (n))) /\ forall ff_i_ph_hd_pth_inverse_pair_body_value_steps. (exists ph_bound_hd_pth_inverse_pair_body_value_steps. ph_bound_hd_pth_inverse_pair_body_value_steps + S ff_i_ph_hd_pth_inverse_pair_body_value_steps = l) -> exists ff_coefficient_ph_hd_pth_inverse_pair_body_value_steps ff_previous_ph_hd_pth_inverse_pair_body_value_steps ff_current_ph_hd_pth_inverse_pair_body_value_steps. ((((exists fs_h_ph_hd_pth_inverse_pair_body_value_steps_coefficient. fs_h_ph_hd_pth_inverse_pair_body_value_steps_coefficient + S (ff_coefficient_ph_hd_pth_inverse_pair_body_value_steps) = S ((S (ff_i_ph_hd_pth_inverse_pair_body_value_steps)) * c)) /\ exists fs_q_ph_hd_pth_inverse_pair_body_value_steps_coefficient. b = fs_q_ph_hd_pth_inverse_pair_body_value_steps_coefficient * S ((S (ff_i_ph_hd_pth_inverse_pair_body_value_steps)) * c) + (ff_coefficient_ph_hd_pth_inverse_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_inverse_pair_body_value_steps_before. fs_h_ph_hd_pth_inverse_pair_body_value_steps_before + S (ff_previous_ph_hd_pth_inverse_pair_body_value_steps) = S ((S (ff_i_ph_hd_pth_inverse_pair_body_value_steps)) * ff_v_hd_pth_inverse_pair)) /\ exists fs_q_ph_hd_pth_inverse_pair_body_value_steps_before. ff_u_hd_pth_inverse_pair = fs_q_ph_hd_pth_inverse_pair_body_value_steps_before * S ((S (ff_i_ph_hd_pth_inverse_pair_body_value_steps)) * ff_v_hd_pth_inverse_pair) + (ff_previous_ph_hd_pth_inverse_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_inverse_pair_body_value_steps_after. fs_h_ph_hd_pth_inverse_pair_body_value_steps_after + S (ff_current_ph_hd_pth_inverse_pair_body_value_steps) = S ((S (S ff_i_ph_hd_pth_inverse_pair_body_value_steps)) * ff_v_hd_pth_inverse_pair)) /\ exists fs_q_ph_hd_pth_inverse_pair_body_value_steps_after. ff_u_hd_pth_inverse_pair = fs_q_ph_hd_pth_inverse_pair_body_value_steps_after * S ((S (S ff_i_ph_hd_pth_inverse_pair_body_value_steps)) * ff_v_hd_pth_inverse_pair) + (ff_current_ph_hd_pth_inverse_pair_body_value_steps))) /\ ff_current_ph_hd_pth_inverse_pair_body_value_steps = ff_previous_ph_hd_pth_inverse_pair_body_value_steps * a + ff_coefficient_ph_hd_pth_inverse_pair_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_pth_inverse_pair_body_derivative_start. fs_h_ph_hd_pth_inverse_pair_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_pth_inverse_pair)) /\ exists fs_q_ph_hd_pth_inverse_pair_body_derivative_start. ff_d_hd_pth_inverse_pair = fs_q_ph_hd_pth_inverse_pair_body_derivative_start * S ((S (0)) * ff_e_hd_pth_inverse_pair) + (0))) /\ ((((exists fs_h_ph_hd_pth_inverse_pair_body_derivative_terminal. fs_h_ph_hd_pth_inverse_pair_body_derivative_terminal + S (d) = S ((S (l)) * ff_e_hd_pth_inverse_pair)) /\ exists fs_q_ph_hd_pth_inverse_pair_body_derivative_terminal. ff_d_hd_pth_inverse_pair = fs_q_ph_hd_pth_inverse_pair_body_derivative_terminal * S ((S (l)) * ff_e_hd_pth_inverse_pair) + (d))) /\ forall ff_i_ph_hd_pth_inverse_pair_body_derivative_steps. (exists ph_bound_hd_pth_inverse_pair_body_derivative_steps. ph_bound_hd_pth_inverse_pair_body_derivative_steps + S ff_i_ph_hd_pth_inverse_pair_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_pth_inverse_pair_body_derivative_steps ff_previous_ph_hd_pth_inverse_pair_body_derivative_steps ff_current_ph_hd_pth_inverse_pair_body_derivative_steps. ((((exists fs_h_ph_hd_pth_inverse_pair_body_derivative_steps_coefficient. fs_h_ph_hd_pth_inverse_pair_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_pth_inverse_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_inverse_pair_body_derivative_steps)) * ff_v_hd_pth_inverse_pair)) /\ exists fs_q_ph_hd_pth_inverse_pair_body_derivative_steps_coefficient. ff_u_hd_pth_inverse_pair = fs_q_ph_hd_pth_inverse_pair_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_pth_inverse_pair_body_derivative_steps)) * ff_v_hd_pth_inverse_pair) + (ff_coefficient_ph_hd_pth_inverse_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_inverse_pair_body_derivative_steps_before. fs_h_ph_hd_pth_inverse_pair_body_derivative_steps_before + S (ff_previous_ph_hd_pth_inverse_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_inverse_pair_body_derivative_steps)) * ff_e_hd_pth_inverse_pair)) /\ exists fs_q_ph_hd_pth_inverse_pair_body_derivative_steps_before. ff_d_hd_pth_inverse_pair = fs_q_ph_hd_pth_inverse_pair_body_derivative_steps_before * S ((S (ff_i_ph_hd_pth_inverse_pair_body_derivative_steps)) * ff_e_hd_pth_inverse_pair) + (ff_previous_ph_hd_pth_inverse_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_inverse_pair_body_derivative_steps_after. fs_h_ph_hd_pth_inverse_pair_body_derivative_steps_after + S (ff_current_ph_hd_pth_inverse_pair_body_derivative_steps) = S ((S (S ff_i_ph_hd_pth_inverse_pair_body_derivative_steps)) * ff_e_hd_pth_inverse_pair)) /\ exists fs_q_ph_hd_pth_inverse_pair_body_derivative_steps_after. ff_d_hd_pth_inverse_pair = fs_q_ph_hd_pth_inverse_pair_body_derivative_steps_after * S ((S (S ff_i_ph_hd_pth_inverse_pair_body_derivative_steps)) * ff_e_hd_pth_inverse_pair) + (ff_current_ph_hd_pth_inverse_pair_body_derivative_steps))) /\ ff_current_ph_hd_pth_inverse_pair_body_derivative_steps = ff_previous_ph_hd_pth_inverse_pair_body_derivative_steps * a + ff_coefficient_ph_hd_pth_inverse_pair_body_derivative_steps)))))))) -> ~(p = 0) -> (forall hmi_divisor_pth_correction. (exists hmi_left_factor_pth_correction. d = hmi_divisor_pth_correction * hmi_left_factor_pth_correction) -> (exists hmi_right_factor_pth_correction. p = hmi_divisor_pth_correction * hmi_right_factor_pth_correction) -> hmi_divisor_pth_correction = 1) -> exists u. (((exists hmi_gap_pth_root_inverse_bound. hmi_gap_pth_root_inverse_bound + S u = p) /\ (exists hmi_left_offset_pth_root_inverse_inverse hmi_right_offset_pth_root_inverse_inverse. d * u + p * hmi_left_offset_pth_root_inverse_inverse = 1 + p * hmi_right_offset_pth_root_inverse_inverse)))Constructive proof overview
Generated structural guide
An actual evaluated coprime formal derivative has a strictly bounded constructive modular inverse.
The unchanged tactic script uses 1 declared prerequisite and contains 15 exact native proof lines.
Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
coprime_bounded_mod_inverse 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.
01Fix variables and assumptionsL1–10
Original exact command ledger · 15 lines
Separate complete second-wave branches: Full G095 proof · Alpha v27.