HL001E

beta_signed_horner_lift_preserves_simplicity

Every canonical integer-polynomial lift retains an actual invertible formal derivative, with explicit coupled traces for both signed components.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

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.

The derivative-nonzero criterion supplies no inverse or power witness: both are constructed. Roots may be arbitrary natural representatives of signed integer polynomials. Singular-root classification and p-adic completion are separate milestones.

Exact theorem in conservative defined notation

∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ a. ∀ l. ∀ vp. ∀ dp. ∀ vn. ∀ dn. ∀ m. ∀ p. ∀ s. ∀ M. ∀ r. SignedHornerValueDerivative(pb,pc,nb,nc,a,l,vp,dp,vn,dn) → SignedDerivativeUnit(p,dp,dn) → m = p · s → CanonicalSignedHornerLift(pb,pc,nb,nc,l,m,a,M,r) → SignedSimpleHornerRoot(pb,pc,nb,nc,r,l,M,p)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedHornerValueDerivative(pb,pc,nb,nc,a,l,vp,dp,vn,dn) · 2SignedDerivativeUnit(p,dp,dn) · 1SignedSimpleHornerRoot(pb,pc,nb,nc,a,l,m,p) · 1CanonicalSignedHornerLift(pb,pc,nb,nc,l,m,a,M,r) · 1ModEq(m,a,b) · 6

Actual proof prerequisites

beta_signed_horner_root_value_derivative_existsbeta_horner_derivative_mod_congruence · checked external prerequisitemod_eq_of_mod_eq_multiple · checked external prerequisitemod_eq_symm · checked external prerequisitehensel_signed_derivative_unit_mod_transport
Original expanded first-order statement 
forall pb pc nb nc a l vp dp vn dn m p s M r. (((exists ff_u_hd_hpl_sph_pair_positive ff_v_hd_hpl_sph_pair_positive ff_d_hd_hpl_sph_pair_positive ff_e_hd_hpl_sph_pair_positive. ((((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_value_start. fs_h_ph_hd_hpl_sph_pair_positive_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_value_start. ff_u_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_value_start * S ((S (0)) * ff_v_hd_hpl_sph_pair_positive) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_value_terminal. fs_h_ph_hd_hpl_sph_pair_positive_body_value_terminal + S (vp) = S ((S (l)) * ff_v_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_value_terminal. ff_u_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_sph_pair_positive) + (vp))) /\ forall ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps. (exists ph_bound_hd_hpl_sph_pair_positive_body_value_steps. ph_bound_hd_hpl_sph_pair_positive_body_value_steps + S ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_pair_positive_body_value_steps ff_previous_ph_hd_hpl_sph_pair_positive_body_value_steps ff_current_ph_hd_hpl_sph_pair_positive_body_value_steps. ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_value_steps_coefficient. fs_h_ph_hd_hpl_sph_pair_positive_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_pair_positive_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps)) * pc)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_value_steps_coefficient. pb = fs_q_ph_hd_hpl_sph_pair_positive_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps)) * pc) + (ff_coefficient_ph_hd_hpl_sph_pair_positive_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_value_steps_before. fs_h_ph_hd_hpl_sph_pair_positive_body_value_steps_before + S (ff_previous_ph_hd_hpl_sph_pair_positive_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps)) * ff_v_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_value_steps_before. ff_u_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps)) * ff_v_hd_hpl_sph_pair_positive) + (ff_previous_ph_hd_hpl_sph_pair_positive_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_value_steps_after. fs_h_ph_hd_hpl_sph_pair_positive_body_value_steps_after + S (ff_current_ph_hd_hpl_sph_pair_positive_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps)) * ff_v_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_value_steps_after. ff_u_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_pair_positive_body_value_steps)) * ff_v_hd_hpl_sph_pair_positive) + (ff_current_ph_hd_hpl_sph_pair_positive_body_value_steps))) /\ ff_current_ph_hd_hpl_sph_pair_positive_body_value_steps = ff_previous_ph_hd_hpl_sph_pair_positive_body_value_steps * a + ff_coefficient_ph_hd_hpl_sph_pair_positive_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_start. fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_start. ff_d_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_sph_pair_positive) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_terminal. fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_terminal + S (dp) = S ((S (l)) * ff_e_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_terminal. ff_d_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_sph_pair_positive) + (dp))) /\ forall ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps. (exists ph_bound_hd_hpl_sph_pair_positive_body_derivative_steps. ph_bound_hd_hpl_sph_pair_positive_body_derivative_steps + S ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_pair_positive_body_derivative_steps ff_previous_ph_hd_hpl_sph_pair_positive_body_derivative_steps ff_current_ph_hd_hpl_sph_pair_positive_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_pair_positive_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps)) * ff_v_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_steps_coefficient. ff_u_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps)) * ff_v_hd_hpl_sph_pair_positive) + (ff_coefficient_ph_hd_hpl_sph_pair_positive_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_steps_before. fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_sph_pair_positive_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_steps_before. ff_d_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_positive) + (ff_previous_ph_hd_hpl_sph_pair_positive_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_steps_after. fs_h_ph_hd_hpl_sph_pair_positive_body_derivative_steps_after + S (ff_current_ph_hd_hpl_sph_pair_positive_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_positive)) /\ exists fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_steps_after. ff_d_hd_hpl_sph_pair_positive = fs_q_ph_hd_hpl_sph_pair_positive_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_pair_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_positive) + (ff_current_ph_hd_hpl_sph_pair_positive_body_derivative_steps))) /\ ff_current_ph_hd_hpl_sph_pair_positive_body_derivative_steps = ff_previous_ph_hd_hpl_sph_pair_positive_body_derivative_steps * a + ff_coefficient_ph_hd_hpl_sph_pair_positive_body_derivative_steps)))))))) /\ (exists ff_u_hd_hpl_sph_pair_negative ff_v_hd_hpl_sph_pair_negative ff_d_hd_hpl_sph_pair_negative ff_e_hd_hpl_sph_pair_negative. ((((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_value_start. fs_h_ph_hd_hpl_sph_pair_negative_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_value_start. ff_u_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_value_start * S ((S (0)) * ff_v_hd_hpl_sph_pair_negative) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_value_terminal. fs_h_ph_hd_hpl_sph_pair_negative_body_value_terminal + S (vn) = S ((S (l)) * ff_v_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_value_terminal. ff_u_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_sph_pair_negative) + (vn))) /\ forall ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps. (exists ph_bound_hd_hpl_sph_pair_negative_body_value_steps. ph_bound_hd_hpl_sph_pair_negative_body_value_steps + S ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_pair_negative_body_value_steps ff_previous_ph_hd_hpl_sph_pair_negative_body_value_steps ff_current_ph_hd_hpl_sph_pair_negative_body_value_steps. ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_value_steps_coefficient. fs_h_ph_hd_hpl_sph_pair_negative_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_pair_negative_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps)) * nc)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_value_steps_coefficient. nb = fs_q_ph_hd_hpl_sph_pair_negative_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps)) * nc) + (ff_coefficient_ph_hd_hpl_sph_pair_negative_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_value_steps_before. fs_h_ph_hd_hpl_sph_pair_negative_body_value_steps_before + S (ff_previous_ph_hd_hpl_sph_pair_negative_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps)) * ff_v_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_value_steps_before. ff_u_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps)) * ff_v_hd_hpl_sph_pair_negative) + (ff_previous_ph_hd_hpl_sph_pair_negative_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_value_steps_after. fs_h_ph_hd_hpl_sph_pair_negative_body_value_steps_after + S (ff_current_ph_hd_hpl_sph_pair_negative_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps)) * ff_v_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_value_steps_after. ff_u_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_pair_negative_body_value_steps)) * ff_v_hd_hpl_sph_pair_negative) + (ff_current_ph_hd_hpl_sph_pair_negative_body_value_steps))) /\ ff_current_ph_hd_hpl_sph_pair_negative_body_value_steps = ff_previous_ph_hd_hpl_sph_pair_negative_body_value_steps * a + ff_coefficient_ph_hd_hpl_sph_pair_negative_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_start. fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_start. ff_d_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_sph_pair_negative) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_terminal. fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_terminal + S (dn) = S ((S (l)) * ff_e_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_terminal. ff_d_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_sph_pair_negative) + (dn))) /\ forall ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps. (exists ph_bound_hd_hpl_sph_pair_negative_body_derivative_steps. ph_bound_hd_hpl_sph_pair_negative_body_derivative_steps + S ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_pair_negative_body_derivative_steps ff_previous_ph_hd_hpl_sph_pair_negative_body_derivative_steps ff_current_ph_hd_hpl_sph_pair_negative_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_pair_negative_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps)) * ff_v_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_steps_coefficient. ff_u_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps)) * ff_v_hd_hpl_sph_pair_negative) + (ff_coefficient_ph_hd_hpl_sph_pair_negative_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_steps_before. fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_sph_pair_negative_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_steps_before. ff_d_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_negative) + (ff_previous_ph_hd_hpl_sph_pair_negative_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_steps_after. fs_h_ph_hd_hpl_sph_pair_negative_body_derivative_steps_after + S (ff_current_ph_hd_hpl_sph_pair_negative_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_negative)) /\ exists fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_steps_after. ff_d_hd_hpl_sph_pair_negative = fs_q_ph_hd_hpl_sph_pair_negative_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_pair_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_pair_negative) + (ff_current_ph_hd_hpl_sph_pair_negative_body_derivative_steps))) /\ ff_current_ph_hd_hpl_sph_pair_negative_body_derivative_steps = ff_previous_ph_hd_hpl_sph_pair_negative_body_derivative_steps * a + ff_coefficient_ph_hd_hpl_sph_pair_negative_body_derivative_steps)))))))))) -> (exists sph_inverse_unit. ((exists hpl_gap_unit. hpl_gap_unit + S (sph_inverse_unit) = (p)) /\ (exists hgcrt_mod_left_hpl_unit hgcrt_mod_right_hpl_unit. (dp * sph_inverse_unit) + p * hgcrt_mod_left_hpl_unit = (1 + dn * sph_inverse_unit) + p * hgcrt_mod_right_hpl_unit))) -> m = p * s -> (((exists hpl_gap_lift. hpl_gap_lift + S (r) = (M)) /\ ((exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. r + m * hgcrt_mod_left_hpl_lift = a + m * hgcrt_mod_right_hpl_lift) /\ (exists sph_positive_lift sph_negative_lift. ((exists ff_u_ph_hpl_sph_lift_positive ff_v_ph_hpl_sph_lift_positive. ((((exists fs_h_ph_hpl_sph_lift_positive_body_start. fs_h_ph_hpl_sph_lift_positive_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_sph_lift_positive)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_start. ff_u_ph_hpl_sph_lift_positive = fs_q_ph_hpl_sph_lift_positive_body_start * S ((S (0)) * ff_v_ph_hpl_sph_lift_positive) + (0))) /\ ((((exists fs_h_ph_hpl_sph_lift_positive_body_terminal. fs_h_ph_hpl_sph_lift_positive_body_terminal + S (sph_positive_lift) = S ((S (l)) * ff_v_ph_hpl_sph_lift_positive)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_terminal. ff_u_ph_hpl_sph_lift_positive = fs_q_ph_hpl_sph_lift_positive_body_terminal * S ((S (l)) * ff_v_ph_hpl_sph_lift_positive) + (sph_positive_lift))) /\ forall ff_i_ph_hpl_sph_lift_positive_body_steps. (exists ph_bound_hpl_sph_lift_positive_body_steps. ph_bound_hpl_sph_lift_positive_body_steps + S ff_i_ph_hpl_sph_lift_positive_body_steps = l) -> exists ff_coefficient_ph_hpl_sph_lift_positive_body_steps ff_previous_ph_hpl_sph_lift_positive_body_steps ff_current_ph_hpl_sph_lift_positive_body_steps. ((((exists fs_h_ph_hpl_sph_lift_positive_body_steps_coefficient. fs_h_ph_hpl_sph_lift_positive_body_steps_coefficient + S (ff_coefficient_ph_hpl_sph_lift_positive_body_steps) = S ((S (ff_i_ph_hpl_sph_lift_positive_body_steps)) * pc)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_steps_coefficient. pb = fs_q_ph_hpl_sph_lift_positive_body_steps_coefficient * S ((S (ff_i_ph_hpl_sph_lift_positive_body_steps)) * pc) + (ff_coefficient_ph_hpl_sph_lift_positive_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_lift_positive_body_steps_before. fs_h_ph_hpl_sph_lift_positive_body_steps_before + S (ff_previous_ph_hpl_sph_lift_positive_body_steps) = S ((S (ff_i_ph_hpl_sph_lift_positive_body_steps)) * ff_v_ph_hpl_sph_lift_positive)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_steps_before. ff_u_ph_hpl_sph_lift_positive = fs_q_ph_hpl_sph_lift_positive_body_steps_before * S ((S (ff_i_ph_hpl_sph_lift_positive_body_steps)) * ff_v_ph_hpl_sph_lift_positive) + (ff_previous_ph_hpl_sph_lift_positive_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_lift_positive_body_steps_after. fs_h_ph_hpl_sph_lift_positive_body_steps_after + S (ff_current_ph_hpl_sph_lift_positive_body_steps) = S ((S (S ff_i_ph_hpl_sph_lift_positive_body_steps)) * ff_v_ph_hpl_sph_lift_positive)) /\ exists fs_q_ph_hpl_sph_lift_positive_body_steps_after. ff_u_ph_hpl_sph_lift_positive = fs_q_ph_hpl_sph_lift_positive_body_steps_after * S ((S (S ff_i_ph_hpl_sph_lift_positive_body_steps)) * ff_v_ph_hpl_sph_lift_positive) + (ff_current_ph_hpl_sph_lift_positive_body_steps))) /\ ff_current_ph_hpl_sph_lift_positive_body_steps = ff_previous_ph_hpl_sph_lift_positive_body_steps * r + ff_coefficient_ph_hpl_sph_lift_positive_body_steps)))))) /\ ((exists ff_u_ph_hpl_sph_lift_negative ff_v_ph_hpl_sph_lift_negative. ((((exists fs_h_ph_hpl_sph_lift_negative_body_start. fs_h_ph_hpl_sph_lift_negative_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_sph_lift_negative)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_start. ff_u_ph_hpl_sph_lift_negative = fs_q_ph_hpl_sph_lift_negative_body_start * S ((S (0)) * ff_v_ph_hpl_sph_lift_negative) + (0))) /\ ((((exists fs_h_ph_hpl_sph_lift_negative_body_terminal. fs_h_ph_hpl_sph_lift_negative_body_terminal + S (sph_negative_lift) = S ((S (l)) * ff_v_ph_hpl_sph_lift_negative)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_terminal. ff_u_ph_hpl_sph_lift_negative = fs_q_ph_hpl_sph_lift_negative_body_terminal * S ((S (l)) * ff_v_ph_hpl_sph_lift_negative) + (sph_negative_lift))) /\ forall ff_i_ph_hpl_sph_lift_negative_body_steps. (exists ph_bound_hpl_sph_lift_negative_body_steps. ph_bound_hpl_sph_lift_negative_body_steps + S ff_i_ph_hpl_sph_lift_negative_body_steps = l) -> exists ff_coefficient_ph_hpl_sph_lift_negative_body_steps ff_previous_ph_hpl_sph_lift_negative_body_steps ff_current_ph_hpl_sph_lift_negative_body_steps. ((((exists fs_h_ph_hpl_sph_lift_negative_body_steps_coefficient. fs_h_ph_hpl_sph_lift_negative_body_steps_coefficient + S (ff_coefficient_ph_hpl_sph_lift_negative_body_steps) = S ((S (ff_i_ph_hpl_sph_lift_negative_body_steps)) * nc)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_steps_coefficient. nb = fs_q_ph_hpl_sph_lift_negative_body_steps_coefficient * S ((S (ff_i_ph_hpl_sph_lift_negative_body_steps)) * nc) + (ff_coefficient_ph_hpl_sph_lift_negative_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_lift_negative_body_steps_before. fs_h_ph_hpl_sph_lift_negative_body_steps_before + S (ff_previous_ph_hpl_sph_lift_negative_body_steps) = S ((S (ff_i_ph_hpl_sph_lift_negative_body_steps)) * ff_v_ph_hpl_sph_lift_negative)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_steps_before. ff_u_ph_hpl_sph_lift_negative = fs_q_ph_hpl_sph_lift_negative_body_steps_before * S ((S (ff_i_ph_hpl_sph_lift_negative_body_steps)) * ff_v_ph_hpl_sph_lift_negative) + (ff_previous_ph_hpl_sph_lift_negative_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_lift_negative_body_steps_after. fs_h_ph_hpl_sph_lift_negative_body_steps_after + S (ff_current_ph_hpl_sph_lift_negative_body_steps) = S ((S (S ff_i_ph_hpl_sph_lift_negative_body_steps)) * ff_v_ph_hpl_sph_lift_negative)) /\ exists fs_q_ph_hpl_sph_lift_negative_body_steps_after. ff_u_ph_hpl_sph_lift_negative = fs_q_ph_hpl_sph_lift_negative_body_steps_after * S ((S (S ff_i_ph_hpl_sph_lift_negative_body_steps)) * ff_v_ph_hpl_sph_lift_negative) + (ff_current_ph_hpl_sph_lift_negative_body_steps))) /\ ff_current_ph_hpl_sph_lift_negative_body_steps = ff_previous_ph_hpl_sph_lift_negative_body_steps * r + ff_coefficient_ph_hpl_sph_lift_negative_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. sph_positive_lift + M * hgcrt_mod_left_hpl_lift = sph_negative_lift + M * hgcrt_mod_right_hpl_lift))))))) -> (exists sph_vp_simple sph_dp_simple sph_vn_simple sph_dn_simple. ((((exists ff_u_hd_hpl_sph_simple_positive ff_v_hd_hpl_sph_simple_positive ff_d_hd_hpl_sph_simple_positive ff_e_hd_hpl_sph_simple_positive. ((((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_value_start. fs_h_ph_hd_hpl_sph_simple_positive_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_value_start. ff_u_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_value_start * S ((S (0)) * ff_v_hd_hpl_sph_simple_positive) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_value_terminal. fs_h_ph_hd_hpl_sph_simple_positive_body_value_terminal + S (sph_vp_simple) = S ((S (l)) * ff_v_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_value_terminal. ff_u_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_sph_simple_positive) + (sph_vp_simple))) /\ forall ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps. (exists ph_bound_hd_hpl_sph_simple_positive_body_value_steps. ph_bound_hd_hpl_sph_simple_positive_body_value_steps + S ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_simple_positive_body_value_steps ff_previous_ph_hd_hpl_sph_simple_positive_body_value_steps ff_current_ph_hd_hpl_sph_simple_positive_body_value_steps. ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_value_steps_coefficient. fs_h_ph_hd_hpl_sph_simple_positive_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_simple_positive_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps)) * pc)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_value_steps_coefficient. pb = fs_q_ph_hd_hpl_sph_simple_positive_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps)) * pc) + (ff_coefficient_ph_hd_hpl_sph_simple_positive_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_value_steps_before. fs_h_ph_hd_hpl_sph_simple_positive_body_value_steps_before + S (ff_previous_ph_hd_hpl_sph_simple_positive_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps)) * ff_v_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_value_steps_before. ff_u_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps)) * ff_v_hd_hpl_sph_simple_positive) + (ff_previous_ph_hd_hpl_sph_simple_positive_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_value_steps_after. fs_h_ph_hd_hpl_sph_simple_positive_body_value_steps_after + S (ff_current_ph_hd_hpl_sph_simple_positive_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps)) * ff_v_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_value_steps_after. ff_u_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_simple_positive_body_value_steps)) * ff_v_hd_hpl_sph_simple_positive) + (ff_current_ph_hd_hpl_sph_simple_positive_body_value_steps))) /\ ff_current_ph_hd_hpl_sph_simple_positive_body_value_steps = ff_previous_ph_hd_hpl_sph_simple_positive_body_value_steps * r + ff_coefficient_ph_hd_hpl_sph_simple_positive_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_start. fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_start. ff_d_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_sph_simple_positive) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_terminal. fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_terminal + S (sph_dp_simple) = S ((S (l)) * ff_e_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_terminal. ff_d_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_sph_simple_positive) + (sph_dp_simple))) /\ forall ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps. (exists ph_bound_hd_hpl_sph_simple_positive_body_derivative_steps. ph_bound_hd_hpl_sph_simple_positive_body_derivative_steps + S ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_simple_positive_body_derivative_steps ff_previous_ph_hd_hpl_sph_simple_positive_body_derivative_steps ff_current_ph_hd_hpl_sph_simple_positive_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_simple_positive_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps)) * ff_v_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_steps_coefficient. ff_u_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps)) * ff_v_hd_hpl_sph_simple_positive) + (ff_coefficient_ph_hd_hpl_sph_simple_positive_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_steps_before. fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_sph_simple_positive_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_steps_before. ff_d_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_positive) + (ff_previous_ph_hd_hpl_sph_simple_positive_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_steps_after. fs_h_ph_hd_hpl_sph_simple_positive_body_derivative_steps_after + S (ff_current_ph_hd_hpl_sph_simple_positive_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_positive)) /\ exists fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_steps_after. ff_d_hd_hpl_sph_simple_positive = fs_q_ph_hd_hpl_sph_simple_positive_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_simple_positive_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_positive) + (ff_current_ph_hd_hpl_sph_simple_positive_body_derivative_steps))) /\ ff_current_ph_hd_hpl_sph_simple_positive_body_derivative_steps = ff_previous_ph_hd_hpl_sph_simple_positive_body_derivative_steps * r + ff_coefficient_ph_hd_hpl_sph_simple_positive_body_derivative_steps)))))))) /\ (exists ff_u_hd_hpl_sph_simple_negative ff_v_hd_hpl_sph_simple_negative ff_d_hd_hpl_sph_simple_negative ff_e_hd_hpl_sph_simple_negative. ((((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_value_start. fs_h_ph_hd_hpl_sph_simple_negative_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_value_start. ff_u_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_value_start * S ((S (0)) * ff_v_hd_hpl_sph_simple_negative) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_value_terminal. fs_h_ph_hd_hpl_sph_simple_negative_body_value_terminal + S (sph_vn_simple) = S ((S (l)) * ff_v_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_value_terminal. ff_u_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_sph_simple_negative) + (sph_vn_simple))) /\ forall ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps. (exists ph_bound_hd_hpl_sph_simple_negative_body_value_steps. ph_bound_hd_hpl_sph_simple_negative_body_value_steps + S ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_simple_negative_body_value_steps ff_previous_ph_hd_hpl_sph_simple_negative_body_value_steps ff_current_ph_hd_hpl_sph_simple_negative_body_value_steps. ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_value_steps_coefficient. fs_h_ph_hd_hpl_sph_simple_negative_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_simple_negative_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps)) * nc)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_value_steps_coefficient. nb = fs_q_ph_hd_hpl_sph_simple_negative_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps)) * nc) + (ff_coefficient_ph_hd_hpl_sph_simple_negative_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_value_steps_before. fs_h_ph_hd_hpl_sph_simple_negative_body_value_steps_before + S (ff_previous_ph_hd_hpl_sph_simple_negative_body_value_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps)) * ff_v_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_value_steps_before. ff_u_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps)) * ff_v_hd_hpl_sph_simple_negative) + (ff_previous_ph_hd_hpl_sph_simple_negative_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_value_steps_after. fs_h_ph_hd_hpl_sph_simple_negative_body_value_steps_after + S (ff_current_ph_hd_hpl_sph_simple_negative_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps)) * ff_v_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_value_steps_after. ff_u_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_simple_negative_body_value_steps)) * ff_v_hd_hpl_sph_simple_negative) + (ff_current_ph_hd_hpl_sph_simple_negative_body_value_steps))) /\ ff_current_ph_hd_hpl_sph_simple_negative_body_value_steps = ff_previous_ph_hd_hpl_sph_simple_negative_body_value_steps * r + ff_coefficient_ph_hd_hpl_sph_simple_negative_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_start. fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_start. ff_d_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_sph_simple_negative) + (0))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_terminal. fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_terminal + S (sph_dn_simple) = S ((S (l)) * ff_e_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_terminal. ff_d_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_sph_simple_negative) + (sph_dn_simple))) /\ forall ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps. (exists ph_bound_hd_hpl_sph_simple_negative_body_derivative_steps. ph_bound_hd_hpl_sph_simple_negative_body_derivative_steps + S ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_sph_simple_negative_body_derivative_steps ff_previous_ph_hd_hpl_sph_simple_negative_body_derivative_steps ff_current_ph_hd_hpl_sph_simple_negative_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_sph_simple_negative_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps)) * ff_v_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_steps_coefficient. ff_u_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps)) * ff_v_hd_hpl_sph_simple_negative) + (ff_coefficient_ph_hd_hpl_sph_simple_negative_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_steps_before. fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_sph_simple_negative_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_steps_before. ff_d_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_negative) + (ff_previous_ph_hd_hpl_sph_simple_negative_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_steps_after. fs_h_ph_hd_hpl_sph_simple_negative_body_derivative_steps_after + S (ff_current_ph_hd_hpl_sph_simple_negative_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_negative)) /\ exists fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_steps_after. ff_d_hd_hpl_sph_simple_negative = fs_q_ph_hd_hpl_sph_simple_negative_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_sph_simple_negative_body_derivative_steps)) * ff_e_hd_hpl_sph_simple_negative) + (ff_current_ph_hd_hpl_sph_simple_negative_body_derivative_steps))) /\ ff_current_ph_hd_hpl_sph_simple_negative_body_derivative_steps = ff_previous_ph_hd_hpl_sph_simple_negative_body_derivative_steps * r + ff_coefficient_ph_hd_hpl_sph_simple_negative_body_derivative_steps)))))))))) /\ ((exists hgcrt_mod_left_hpl_simple hgcrt_mod_right_hpl_simple. sph_vp_simple + M * hgcrt_mod_left_hpl_simple = sph_vn_simple + M * hgcrt_mod_right_hpl_simple) /\ (exists sph_inverse_simple. ((exists hpl_gap_simple. hpl_gap_simple + S (sph_inverse_simple) = (p)) /\ (exists hgcrt_mod_left_hpl_simple hgcrt_mod_right_hpl_simple. (sph_dp_simple * sph_inverse_simple) + p * hgcrt_mod_left_hpl_simple = (1 + sph_dn_simple * sph_inverse_simple) + p * hgcrt_mod_right_hpl_simple))))))

Complete tactic proof in conservative notation

All 102 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

102 script commands · 19 reading checkpoints · 4 local claims

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
beta signed horner root value derivative existshensel signed derivative unit mod transport
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro pb
  2. L2
    intro pc
  3. L3
    intro nb
  4. L4
    intro nc
  5. L5
    intro a
  6. L6
    intro l
  7. L7
    intro vp
  8. L8
    intro dp
  9. L9
    intro vn
  10. L10
    intro dn
02Fix variables and assumptionsL11–19

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro m
  2. L12
    intro p
  3. L13
    intro s
  4. L14
    intro M
  5. L15
    intro r
  6. L16
    intro hpair
  7. L17
    intro hunit
  8. L18
    intro hfactor
  9. L19
    intro hlift
03Separate the logical casesL20–22

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L20
    cases hpair
  2. L21
    cases hlift
  3. L22
    cases hlift_right
04Establish hactualL23–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta signed horner root value derivative exists.

  1. L23
    have hactual : ∃ P. ∃ D. ∃ N. ∃ E. SignedHornerValueDerivative(pb,pc,nb,nc,r,l,P,D,N,E) ∧ ModEq(M,P,N)Definitions: SignedHornerValueDerivative(pb,pc,nb,nc,r,l,P,D,N,E)ModEq(M,P,N)Original native command in the exact edition
  2. L24
    specialize beta_signed_horner_root_value_derivative_exists pb
  3. L25
    specialize beta_signed_horner_root_value_derivative_exists pc
  4. L26
    specialize beta_signed_horner_root_value_derivative_exists nb
  5. L27
    specialize beta_signed_horner_root_value_derivative_exists nc
  6. L28
    specialize beta_signed_horner_root_value_derivative_exists r
  7. L29
    specialize beta_signed_horner_root_value_derivative_exists l
  8. L30
    specialize beta_signed_horner_root_value_derivative_exists M
  9. L31
    apply beta_signed_horner_root_value_derivative_exists
  10. L32
    exact hlift_right_right
05Separate the logical casesL33–38

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L33
    cases hactual
  2. L34
    cases hactual_witness
  3. L35
    cases hactual_witness_witness
  4. L36
    cases hactual_witness_witness_witness
  5. L37
    cases hactual_witness_witness_witness_witness
  6. L38
    cases hactual_witness_witness_witness_witness_left
06Establish hpointL39–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq of mod eq multiple.

  1. L39
    have hpoint : ModEq(p,a,r)Definitions: ModEq(p,a,r)Original native command in the exact edition
  2. L40
    specialize mod_eq_of_mod_eq_multiple p
  3. L41
    specialize mod_eq_of_mod_eq_multiple m
  4. L42
    specialize mod_eq_of_mod_eq_multiple a
  5. L43
    specialize mod_eq_of_mod_eq_multiple r
  6. L44
    apply mod_eq_of_mod_eq_multiple
07Construct an explicit witnessL45–45

Supply the displayed value, then prove that it has the required property.

  1. L45
    exists s
08Use earlier factsL46–51

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L46
    exact hfactor
  2. L47
    specialize mod_eq_symm m
  3. L48
    specialize mod_eq_symm r
  4. L49
    specialize mod_eq_symm a
  5. L50
    apply mod_eq_symm
  6. L51
    exact hlift_right_left
09Establish hpositiveL52–61

Establish this local claim before using it. It is not an additional assumption.

  1. L52
    have hpositive : ModEq(p,vp,x) ∧ ModEq(p,dp,x1)Definitions: ModEq(p,vp,x)ModEq(p,dp,x1)Original native command in the exact edition
  2. L53
    specialize beta_horner_derivative_mod_congruence pb
  3. L54
    specialize beta_horner_derivative_mod_congruence pc
  4. L55
    specialize beta_horner_derivative_mod_congruence p
  5. L56
    specialize beta_horner_derivative_mod_congruence a
  6. L57
    specialize beta_horner_derivative_mod_congruence r
  7. L58
    specialize beta_horner_derivative_mod_congruence l
  8. L59
    specialize beta_horner_derivative_mod_congruence vp
  9. L60
    specialize beta_horner_derivative_mod_congruence dp
  10. L61
    specialize beta_horner_derivative_mod_congruence x
10Use earlier factsL62–66

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L62
    specialize beta_horner_derivative_mod_congruence x1
  2. L63
    apply beta_horner_derivative_mod_congruence
  3. L64
    exact hpoint
  4. L65
    exact hpair_left
  5. L66
    exact hactual_witness_witness_witness_witness_left_left
11Separate the logical casesL67–67

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L67
    cases hpositive
12Establish hnegativeL68–77

Establish this local claim before using it. It is not an additional assumption.

  1. L68
    have hnegative : ModEq(p,vn,x2) ∧ ModEq(p,dn,x3)Definitions: ModEq(p,vn,x2)ModEq(p,dn,x3)Original native command in the exact edition
  2. L69
    specialize beta_horner_derivative_mod_congruence nb
  3. L70
    specialize beta_horner_derivative_mod_congruence nc
  4. L71
    specialize beta_horner_derivative_mod_congruence p
  5. L72
    specialize beta_horner_derivative_mod_congruence a
  6. L73
    specialize beta_horner_derivative_mod_congruence r
  7. L74
    specialize beta_horner_derivative_mod_congruence l
  8. L75
    specialize beta_horner_derivative_mod_congruence vn
  9. L76
    specialize beta_horner_derivative_mod_congruence dn
  10. L77
    specialize beta_horner_derivative_mod_congruence x2
13Use earlier factsL78–82

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L78
    specialize beta_horner_derivative_mod_congruence x3
  2. L79
    apply beta_horner_derivative_mod_congruence
  3. L80
    exact hpoint
  4. L81
    exact hpair_right
  5. L82
    exact hactual_witness_witness_witness_witness_left_right
14Separate the logical casesL83–83

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L83
    cases hnegative
15Construct an explicit witnessL84–87

Supply the displayed value, then prove that it has the required property.

  1. L84
    exists x
  2. L85
    exists x1
  3. L86
    exists x2
  4. L87
    exists x3
16Separate the logical casesL88–89

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L88
    split
  2. L89
    split
17Use earlier factsL90–91

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L90
    exact hactual_witness_witness_witness_witness_left_left
  2. L91
    exact hactual_witness_witness_witness_witness_left_right
18Separate the logical casesL92–92

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L92
    split
19Use earlier factsL93–102

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L93
    exact hactual_witness_witness_witness_witness_right
  2. L94
    specialize hensel_signed_derivative_unit_mod_transport p
  3. L95
    specialize hensel_signed_derivative_unit_mod_transport dp
  4. L96
    specialize hensel_signed_derivative_unit_mod_transport dn
  5. L97
    specialize hensel_signed_derivative_unit_mod_transport x1
  6. L98
    specialize hensel_signed_derivative_unit_mod_transport x3
  7. L99
    apply hensel_signed_derivative_unit_mod_transport
  8. L100
    exact hpositive_right
  9. L101
    exact hnegative_right
  10. L102
    exact hunit

Library-wide reading audit

Original defined command ledger · 102 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro a
  6. 0006intro l
  7. 0007intro vp
  8. 0008intro dp
  9. 0009intro vn
  10. 0010intro dn
  11. 0011intro m
  12. 0012intro p
  13. 0013intro s
  14. 0014intro M
  15. 0015intro r
  16. 0016intro hpair
  17. 0017intro hunit
  18. 0018intro hfactor
  19. 0019intro hlift
  20. 0020cases hpair
  21. 0021cases hlift
  22. 0022cases hlift_right
  23. 0023have hactual : ∃ P. ∃ D. ∃ N. ∃ E. SignedHornerValueDerivative(pb,pc,nb,nc,r,l,P,D,N,E) ∧ ModEq(M,P,N)
  24. 0024specialize beta_signed_horner_root_value_derivative_exists pb
  25. 0025specialize beta_signed_horner_root_value_derivative_exists pc
  26. 0026specialize beta_signed_horner_root_value_derivative_exists nb
  27. 0027specialize beta_signed_horner_root_value_derivative_exists nc
  28. 0028specialize beta_signed_horner_root_value_derivative_exists r
  29. 0029specialize beta_signed_horner_root_value_derivative_exists l
  30. 0030specialize beta_signed_horner_root_value_derivative_exists M
  31. 0031apply beta_signed_horner_root_value_derivative_exists
  32. 0032exact hlift_right_right
  33. 0033cases hactual
  34. 0034cases hactual_witness
  35. 0035cases hactual_witness_witness
  36. 0036cases hactual_witness_witness_witness
  37. 0037cases hactual_witness_witness_witness_witness
  38. 0038cases hactual_witness_witness_witness_witness_left
  39. 0039have hpoint : ModEq(p,a,r)
  40. 0040specialize mod_eq_of_mod_eq_multiple p
  41. 0041specialize mod_eq_of_mod_eq_multiple m
  42. 0042specialize mod_eq_of_mod_eq_multiple a
  43. 0043specialize mod_eq_of_mod_eq_multiple r
  44. 0044apply mod_eq_of_mod_eq_multiple
  45. 0045exists s
  46. 0046exact hfactor
  47. 0047specialize mod_eq_symm m
  48. 0048specialize mod_eq_symm r
  49. 0049specialize mod_eq_symm a
  50. 0050apply mod_eq_symm
  51. 0051exact hlift_right_left
  52. 0052have hpositive : ModEq(p,vp,x) ∧ ModEq(p,dp,x1)
  53. 0053specialize beta_horner_derivative_mod_congruence pb
  54. 0054specialize beta_horner_derivative_mod_congruence pc
  55. 0055specialize beta_horner_derivative_mod_congruence p
  56. 0056specialize beta_horner_derivative_mod_congruence a
  57. 0057specialize beta_horner_derivative_mod_congruence r
  58. 0058specialize beta_horner_derivative_mod_congruence l
  59. 0059specialize beta_horner_derivative_mod_congruence vp
  60. 0060specialize beta_horner_derivative_mod_congruence dp
  61. 0061specialize beta_horner_derivative_mod_congruence x
  62. 0062specialize beta_horner_derivative_mod_congruence x1
  63. 0063apply beta_horner_derivative_mod_congruence
  64. 0064exact hpoint
  65. 0065exact hpair_left
  66. 0066exact hactual_witness_witness_witness_witness_left_left
  67. 0067cases hpositive
  68. 0068have hnegative : ModEq(p,vn,x2) ∧ ModEq(p,dn,x3)
  69. 0069specialize beta_horner_derivative_mod_congruence nb
  70. 0070specialize beta_horner_derivative_mod_congruence nc
  71. 0071specialize beta_horner_derivative_mod_congruence p
  72. 0072specialize beta_horner_derivative_mod_congruence a
  73. 0073specialize beta_horner_derivative_mod_congruence r
  74. 0074specialize beta_horner_derivative_mod_congruence l
  75. 0075specialize beta_horner_derivative_mod_congruence vn
  76. 0076specialize beta_horner_derivative_mod_congruence dn
  77. 0077specialize beta_horner_derivative_mod_congruence x2
  78. 0078specialize beta_horner_derivative_mod_congruence x3
  79. 0079apply beta_horner_derivative_mod_congruence
  80. 0080exact hpoint
  81. 0081exact hpair_right
  82. 0082exact hactual_witness_witness_witness_witness_left_right
  83. 0083cases hnegative
  84. 0084exists x
  85. 0085exists x1
  86. 0086exists x2
  87. 0087exists x3
  88. 0088split
  89. 0089split
  90. 0090exact hactual_witness_witness_witness_witness_left_left
  91. 0091exact hactual_witness_witness_witness_witness_left_right
  92. 0092split
  93. 0093exact hactual_witness_witness_witness_witness_right
  94. 0094specialize hensel_signed_derivative_unit_mod_transport p
  95. 0095specialize hensel_signed_derivative_unit_mod_transport dp
  96. 0096specialize hensel_signed_derivative_unit_mod_transport dn
  97. 0097specialize hensel_signed_derivative_unit_mod_transport x1
  98. 0098specialize hensel_signed_derivative_unit_mod_transport x3
  99. 0099apply hensel_signed_derivative_unit_mod_transport
  100. 0100exact hpositive_right
  101. 0101exact hnegative_right
  102. 0102exact hunit