HL0016

beta_horner_coefficient_blend_value_derivative

For every finite coefficient list, the actual recoded polynomial and its actual formal derivative are the exact weighted combinations of their 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. ∀ gb. ∀ gc. ∀ h. ∀ a. ∀ l. ∀ vp. ∀ dp. ∀ vn. ∀ dn. ∀ vg. ∀ dg. HornerCoefficientBlend(pb,pc,nb,nc,gb,gc,h,l) → HornerDerivative(pb,pc,a,l,vp,dp) → HornerDerivative(nb,nc,a,l,vn,dn) → HornerDerivative(gb,gc,a,l,vg,dg) → vg = vp + h · vn ∧ dg = dp + h · dn

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

Definition DAG

Beta(b,c,i,x) · 3HornerDerivative(b,c,t,l,n,z) · 6HornerCoefficientBlend(pb,pc,nb,nc,gb,gc,h,l) · 2

Actual proof prerequisites

beta_horner_derivative_empty · checked external prerequisitebeta_horner_derivative_successor_decompose · checked external prerequisitele_succ · checked external prerequisitele_refl · checked external prerequisitehensel_horner_linear_successor_identity
Original expanded first-order statement 
forall pb pc nb nc gb gc h a l vp dp vn dn vg dg. (forall sph_i_blend sph_A_blend sph_B_blend sph_C_blend. (exists hpl_gap_blend. hpl_gap_blend + S (sph_i_blend) = (l)) -> (((exists fs_h_sph_blend_positive. fs_h_sph_blend_positive + S (sph_A_blend) = S ((S (sph_i_blend)) * pc)) /\ exists fs_q_sph_blend_positive. pb = fs_q_sph_blend_positive * S ((S (sph_i_blend)) * pc) + (sph_A_blend))) -> (((exists fs_h_sph_blend_negative. fs_h_sph_blend_negative + S (sph_B_blend) = S ((S (sph_i_blend)) * nc)) /\ exists fs_q_sph_blend_negative. nb = fs_q_sph_blend_negative * S ((S (sph_i_blend)) * nc) + (sph_B_blend))) -> (((exists fs_h_sph_blend_combined. fs_h_sph_blend_combined + S (sph_C_blend) = S ((S (sph_i_blend)) * gc)) /\ exists fs_q_sph_blend_combined. gb = fs_q_sph_blend_combined * S ((S (sph_i_blend)) * gc) + (sph_C_blend))) -> sph_C_blend = sph_A_blend + h * sph_B_blend) -> (exists ff_u_hd_hpl_pair ff_v_hd_hpl_pair ff_d_hd_hpl_pair ff_e_hd_hpl_pair. ((((((exists fs_h_ph_hd_hpl_pair_body_value_start. fs_h_ph_hd_hpl_pair_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_start. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_start * S ((S (0)) * ff_v_hd_hpl_pair) + (0))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_terminal. fs_h_ph_hd_hpl_pair_body_value_terminal + S (vp) = S ((S (l)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_terminal. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_pair) + (vp))) /\ forall ff_i_ph_hd_hpl_pair_body_value_steps. (exists ph_bound_hd_hpl_pair_body_value_steps. ph_bound_hd_hpl_pair_body_value_steps + S ff_i_ph_hd_hpl_pair_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_pair_body_value_steps ff_previous_ph_hd_hpl_pair_body_value_steps ff_current_ph_hd_hpl_pair_body_value_steps. ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_coefficient. fs_h_ph_hd_hpl_pair_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_pair_body_value_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * pc)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_coefficient. pb = fs_q_ph_hd_hpl_pair_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * pc) + (ff_coefficient_ph_hd_hpl_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_before. fs_h_ph_hd_hpl_pair_body_value_steps_before + S (ff_previous_ph_hd_hpl_pair_body_value_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_before. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair) + (ff_previous_ph_hd_hpl_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_after. fs_h_ph_hd_hpl_pair_body_value_steps_after + S (ff_current_ph_hd_hpl_pair_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_after. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair) + (ff_current_ph_hd_hpl_pair_body_value_steps))) /\ ff_current_ph_hd_hpl_pair_body_value_steps = ff_previous_ph_hd_hpl_pair_body_value_steps * a + ff_coefficient_ph_hd_hpl_pair_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_pair_body_derivative_start. fs_h_ph_hd_hpl_pair_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_start. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_pair) + (0))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_terminal. fs_h_ph_hd_hpl_pair_body_derivative_terminal + S (dp) = S ((S (l)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_terminal. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_pair) + (dp))) /\ forall ff_i_ph_hd_hpl_pair_body_derivative_steps. (exists ph_bound_hd_hpl_pair_body_derivative_steps. ph_bound_hd_hpl_pair_body_derivative_steps + S ff_i_ph_hd_hpl_pair_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_pair_body_derivative_steps ff_previous_ph_hd_hpl_pair_body_derivative_steps ff_current_ph_hd_hpl_pair_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_pair_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_coefficient. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_v_hd_hpl_pair) + (ff_coefficient_ph_hd_hpl_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_before. fs_h_ph_hd_hpl_pair_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_before. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair) + (ff_previous_ph_hd_hpl_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_after. fs_h_ph_hd_hpl_pair_body_derivative_steps_after + S (ff_current_ph_hd_hpl_pair_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_after. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair) + (ff_current_ph_hd_hpl_pair_body_derivative_steps))) /\ ff_current_ph_hd_hpl_pair_body_derivative_steps = ff_previous_ph_hd_hpl_pair_body_derivative_steps * a + ff_coefficient_ph_hd_hpl_pair_body_derivative_steps)))))))) -> (exists ff_u_hd_hpl_pair ff_v_hd_hpl_pair ff_d_hd_hpl_pair ff_e_hd_hpl_pair. ((((((exists fs_h_ph_hd_hpl_pair_body_value_start. fs_h_ph_hd_hpl_pair_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_start. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_start * S ((S (0)) * ff_v_hd_hpl_pair) + (0))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_terminal. fs_h_ph_hd_hpl_pair_body_value_terminal + S (vn) = S ((S (l)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_terminal. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_pair) + (vn))) /\ forall ff_i_ph_hd_hpl_pair_body_value_steps. (exists ph_bound_hd_hpl_pair_body_value_steps. ph_bound_hd_hpl_pair_body_value_steps + S ff_i_ph_hd_hpl_pair_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_pair_body_value_steps ff_previous_ph_hd_hpl_pair_body_value_steps ff_current_ph_hd_hpl_pair_body_value_steps. ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_coefficient. fs_h_ph_hd_hpl_pair_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_pair_body_value_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * nc)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_coefficient. nb = fs_q_ph_hd_hpl_pair_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * nc) + (ff_coefficient_ph_hd_hpl_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_before. fs_h_ph_hd_hpl_pair_body_value_steps_before + S (ff_previous_ph_hd_hpl_pair_body_value_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_before. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair) + (ff_previous_ph_hd_hpl_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_after. fs_h_ph_hd_hpl_pair_body_value_steps_after + S (ff_current_ph_hd_hpl_pair_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_after. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair) + (ff_current_ph_hd_hpl_pair_body_value_steps))) /\ ff_current_ph_hd_hpl_pair_body_value_steps = ff_previous_ph_hd_hpl_pair_body_value_steps * a + ff_coefficient_ph_hd_hpl_pair_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_pair_body_derivative_start. fs_h_ph_hd_hpl_pair_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_start. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_pair) + (0))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_terminal. fs_h_ph_hd_hpl_pair_body_derivative_terminal + S (dn) = S ((S (l)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_terminal. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_pair) + (dn))) /\ forall ff_i_ph_hd_hpl_pair_body_derivative_steps. (exists ph_bound_hd_hpl_pair_body_derivative_steps. ph_bound_hd_hpl_pair_body_derivative_steps + S ff_i_ph_hd_hpl_pair_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_pair_body_derivative_steps ff_previous_ph_hd_hpl_pair_body_derivative_steps ff_current_ph_hd_hpl_pair_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_pair_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_coefficient. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_v_hd_hpl_pair) + (ff_coefficient_ph_hd_hpl_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_before. fs_h_ph_hd_hpl_pair_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_before. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair) + (ff_previous_ph_hd_hpl_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_after. fs_h_ph_hd_hpl_pair_body_derivative_steps_after + S (ff_current_ph_hd_hpl_pair_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_after. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair) + (ff_current_ph_hd_hpl_pair_body_derivative_steps))) /\ ff_current_ph_hd_hpl_pair_body_derivative_steps = ff_previous_ph_hd_hpl_pair_body_derivative_steps * a + ff_coefficient_ph_hd_hpl_pair_body_derivative_steps)))))))) -> (exists ff_u_hd_hpl_pair ff_v_hd_hpl_pair ff_d_hd_hpl_pair ff_e_hd_hpl_pair. ((((((exists fs_h_ph_hd_hpl_pair_body_value_start. fs_h_ph_hd_hpl_pair_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_start. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_start * S ((S (0)) * ff_v_hd_hpl_pair) + (0))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_terminal. fs_h_ph_hd_hpl_pair_body_value_terminal + S (vg) = S ((S (l)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_terminal. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_pair) + (vg))) /\ forall ff_i_ph_hd_hpl_pair_body_value_steps. (exists ph_bound_hd_hpl_pair_body_value_steps. ph_bound_hd_hpl_pair_body_value_steps + S ff_i_ph_hd_hpl_pair_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_pair_body_value_steps ff_previous_ph_hd_hpl_pair_body_value_steps ff_current_ph_hd_hpl_pair_body_value_steps. ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_coefficient. fs_h_ph_hd_hpl_pair_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_pair_body_value_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * gc)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_coefficient. gb = fs_q_ph_hd_hpl_pair_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * gc) + (ff_coefficient_ph_hd_hpl_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_before. fs_h_ph_hd_hpl_pair_body_value_steps_before + S (ff_previous_ph_hd_hpl_pair_body_value_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_before. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair) + (ff_previous_ph_hd_hpl_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_after. fs_h_ph_hd_hpl_pair_body_value_steps_after + S (ff_current_ph_hd_hpl_pair_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_after. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair) + (ff_current_ph_hd_hpl_pair_body_value_steps))) /\ ff_current_ph_hd_hpl_pair_body_value_steps = ff_previous_ph_hd_hpl_pair_body_value_steps * a + ff_coefficient_ph_hd_hpl_pair_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_pair_body_derivative_start. fs_h_ph_hd_hpl_pair_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_start. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_pair) + (0))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_terminal. fs_h_ph_hd_hpl_pair_body_derivative_terminal + S (dg) = S ((S (l)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_terminal. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_pair) + (dg))) /\ forall ff_i_ph_hd_hpl_pair_body_derivative_steps. (exists ph_bound_hd_hpl_pair_body_derivative_steps. ph_bound_hd_hpl_pair_body_derivative_steps + S ff_i_ph_hd_hpl_pair_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_pair_body_derivative_steps ff_previous_ph_hd_hpl_pair_body_derivative_steps ff_current_ph_hd_hpl_pair_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_pair_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_coefficient. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_v_hd_hpl_pair) + (ff_coefficient_ph_hd_hpl_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_before. fs_h_ph_hd_hpl_pair_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_before. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair) + (ff_previous_ph_hd_hpl_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_after. fs_h_ph_hd_hpl_pair_body_derivative_steps_after + S (ff_current_ph_hd_hpl_pair_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_after. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair) + (ff_current_ph_hd_hpl_pair_body_derivative_steps))) /\ ff_current_ph_hd_hpl_pair_body_derivative_steps = ff_previous_ph_hd_hpl_pair_body_derivative_steps * a + ff_coefficient_ph_hd_hpl_pair_body_derivative_steps)))))))) -> vg = vp + h * vn /\ dg = dp + h * dn

Complete tactic proof in conservative notation

All 180 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

180 script commands · 30 reading checkpoints · 9 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 (1)
hensel horner linear successor identity
01Fix variables and assumptionsL1–8

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 gb
  6. L6
    intro gc
  7. L7
    intro h
  8. L8
    intro a
02Induction on lL9–18

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L9
    induction l
  2. L10
    intro vp
  3. L11
    intro dp
  4. L12
    intro vn
  5. L13
    intro dn
  6. L14
    intro vg
  7. L15
    intro dg
  8. L16
    intro hblend
  9. L17
    intro hpositive
  10. L18
    intro hnegative
03Fix variables and assumptionsL19–19

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

  1. L19
    intro hcombined
04Establish hPL20–27

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

  1. L20
    have hP : vp = 0 /\ dp = 0
  2. L21
    specialize beta_horner_derivative_empty pb
  3. L22
    specialize beta_horner_derivative_empty pc
  4. L23
    specialize beta_horner_derivative_empty a
  5. L24
    specialize beta_horner_derivative_empty vp
  6. L25
    specialize beta_horner_derivative_empty dp
  7. L26
    apply beta_horner_derivative_empty
  8. L27
    exact hpositive
05Separate the logical casesL28–28

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

  1. L28
    cases hP
06Establish hNL29–36

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

  1. L29
    have hN : vn = 0 /\ dn = 0
  2. L30
    specialize beta_horner_derivative_empty nb
  3. L31
    specialize beta_horner_derivative_empty nc
  4. L32
    specialize beta_horner_derivative_empty a
  5. L33
    specialize beta_horner_derivative_empty vn
  6. L34
    specialize beta_horner_derivative_empty dn
  7. L35
    apply beta_horner_derivative_empty
  8. L36
    exact hnegative
07Separate the logical casesL37–37

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

  1. L37
    cases hN
08Establish hGL38–45

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

  1. L38
    have hG : vg = 0 /\ dg = 0
  2. L39
    specialize beta_horner_derivative_empty gb
  3. L40
    specialize beta_horner_derivative_empty gc
  4. L41
    specialize beta_horner_derivative_empty a
  5. L42
    specialize beta_horner_derivative_empty vg
  6. L43
    specialize beta_horner_derivative_empty dg
  7. L44
    apply beta_horner_derivative_empty
  8. L45
    exact hcombined
09Separate the logical casesL46–47

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

  1. L46
    cases hG
  2. L47
    split
10Calculate and transport equalitiesL48–55

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L48
    rewrite hG_left
  2. L49
    rewrite hP_left
  3. L50
    rewrite hN_left
  4. L51
    simp
  5. L52
    rewrite hG_right
  6. L53
    rewrite hP_right
  7. L54
    rewrite hN_right
  8. L55
    simp
11Fix variables and assumptionsL56–65

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

  1. L56
    intro vp
  2. L57
    intro dp
  3. L58
    intro vn
  4. L59
    intro dn
  5. L60
    intro vg
  6. L61
    intro dg
  7. L62
    intro hblend
  8. L63
    intro hpositive
  9. L64
    intro hnegative
  10. L65
    intro hcombined
12Establish hPL66–74

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner derivative successor decompose.

  1. L66
    have hP : ∃ sph_coefficient_positive. ∃ sph_value_positive. ∃ sph_derivative_positive. Beta(pb,pc,l,sph_coefficient_positive) ∧ (HornerDerivative(pb,pc,a,l,sph_value_positive,sph_derivative_positive) ∧ (vp = sph_value_positive · a + sph_coefficient_positive ∧ dp = sph_derivative_positive · a + sph_value_positive))Definitions: Beta(pb,pc,l,sph_coefficient_positive)HornerDerivative(pb,pc,a,l,sph_value_positive,sph_derivative_positive)Original native command in the exact edition
  2. L67
    specialize beta_horner_derivative_successor_decompose pb
  3. L68
    specialize beta_horner_derivative_successor_decompose pc
  4. L69
    specialize beta_horner_derivative_successor_decompose a
  5. L70
    specialize beta_horner_derivative_successor_decompose l
  6. L71
    specialize beta_horner_derivative_successor_decompose vp
  7. L72
    specialize beta_horner_derivative_successor_decompose dp
  8. L73
    apply beta_horner_derivative_successor_decompose
  9. L74
    exact hpositive
13Separate the logical casesL75–80

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

  1. L75
    cases hP
  2. L76
    cases hP_witness
  3. L77
    cases hP_witness_witness
  4. L78
    cases hP_witness_witness_witness
  5. L79
    cases hP_witness_witness_witness_right
  6. L80
    cases hP_witness_witness_witness_right_right
14Establish hNL81–89

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner derivative successor decompose.

  1. L81
    have hN : ∃ sph_coefficient_negative. ∃ sph_value_negative. ∃ sph_derivative_negative. Beta(nb,nc,l,sph_coefficient_negative) ∧ (HornerDerivative(nb,nc,a,l,sph_value_negative,sph_derivative_negative) ∧ (vn = sph_value_negative · a + sph_coefficient_negative ∧ dn = sph_derivative_negative · a + sph_value_negative))Definitions: Beta(nb,nc,l,sph_coefficient_negative)HornerDerivative(nb,nc,a,l,sph_value_negative,sph_derivative_negative)Original native command in the exact edition
  2. L82
    specialize beta_horner_derivative_successor_decompose nb
  3. L83
    specialize beta_horner_derivative_successor_decompose nc
  4. L84
    specialize beta_horner_derivative_successor_decompose a
  5. L85
    specialize beta_horner_derivative_successor_decompose l
  6. L86
    specialize beta_horner_derivative_successor_decompose vn
  7. L87
    specialize beta_horner_derivative_successor_decompose dn
  8. L88
    apply beta_horner_derivative_successor_decompose
  9. L89
    exact hnegative
15Separate the logical casesL90–95

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

  1. L90
    cases hN
  2. L91
    cases hN_witness
  3. L92
    cases hN_witness_witness
  4. L93
    cases hN_witness_witness_witness
  5. L94
    cases hN_witness_witness_witness_right
  6. L95
    cases hN_witness_witness_witness_right_right
16Establish hGL96–104

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner derivative successor decompose.

  1. L96
    have hG : ∃ sph_coefficient_combined. ∃ sph_value_combined. ∃ sph_derivative_combined. Beta(gb,gc,l,sph_coefficient_combined) ∧ (HornerDerivative(gb,gc,a,l,sph_value_combined,sph_derivative_combined) ∧ (vg = sph_value_combined · a + sph_coefficient_combined ∧ dg = sph_derivative_combined · a + sph_value_combined))Definitions: Beta(gb,gc,l,sph_coefficient_combined)HornerDerivative(gb,gc,a,l,sph_value_combined,sph_derivative_combined)Original native command in the exact edition
  2. L97
    specialize beta_horner_derivative_successor_decompose gb
  3. L98
    specialize beta_horner_derivative_successor_decompose gc
  4. L99
    specialize beta_horner_derivative_successor_decompose a
  5. L100
    specialize beta_horner_derivative_successor_decompose l
  6. L101
    specialize beta_horner_derivative_successor_decompose vg
  7. L102
    specialize beta_horner_derivative_successor_decompose dg
  8. L103
    apply beta_horner_derivative_successor_decompose
  9. L104
    exact hcombined
17Separate the logical casesL105–110

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

  1. L105
    cases hG
  2. L106
    cases hG_witness
  3. L107
    cases hG_witness_witness
  4. L108
    cases hG_witness_witness_witness
  5. L109
    cases hG_witness_witness_witness_right
  6. L110
    cases hG_witness_witness_witness_right_right
18Establish hprefix_blendL111–120

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

  1. L111
    have hprefix_blend : HornerCoefficientBlend(pb,pc,nb,nc,gb,gc,h,l)Definitions: HornerCoefficientBlend(pb,pc,nb,nc,gb,gc,h,l)Original native command in the exact edition
  2. L112
    intro i
  3. L113
    intro A
  4. L114
    intro B
  5. L115
    intro C
  6. L116
    intro hi
  7. L117
    intro hA
  8. L118
    intro hB
  9. L119
    intro hC
  10. L120
    specialize hblend i
19Use earlier factsL121–130

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

  1. L121
    specialize hblend A
  2. L122
    specialize hblend B
  3. L123
    specialize hblend C
  4. L124
    apply hblend
  5. L125
    specialize le_succ (S i)
  6. L126
    specialize le_succ l
  7. L127
    apply le_succ
  8. L128
    exact hi
  9. L129
    exact hA
  10. L130
    exact hB
20Use earlier factsL131–131

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

  1. L131
    exact hC
21Establish hprefixL132–141

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L132
    have hprefix : x7 = x1 + h * x4 /\ x8 = x2 + h * x5
  2. L133
    specialize IH x1
  3. L134
    specialize IH x2
  4. L135
    specialize IH x4
  5. L136
    specialize IH x5
  6. L137
    specialize IH x7
  7. L138
    specialize IH x8
  8. L139
    apply IH
  9. L140
    exact hprefix_blend
  10. L141
    exact hP_witness_witness_witness_right_left
22Use earlier factsL142–143

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

  1. L142
    exact hN_witness_witness_witness_right_left
  2. L143
    exact hG_witness_witness_witness_right_left
23Separate the logical casesL144–144

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

  1. L144
    cases hprefix
24Establish hlastL145–154

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hblend.

  1. L145
    have hlast : x6 = x + h * x3
  2. L146
    specialize hblend l
  3. L147
    specialize hblend x
  4. L148
    specialize hblend x3
  5. L149
    specialize hblend x6
  6. L150
    apply hblend
  7. L151
    specialize le_refl (S l)
  8. L152
    apply le_refl
  9. L153
    exact hP_witness_witness_witness_left
  10. L154
    exact hN_witness_witness_witness_left
25Use earlier factsL155–155

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

  1. L155
    exact hG_witness_witness_witness_left
26Separate the logical casesL156–156

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

  1. L156
    split
27Calculate and transport equalitiesL157–161

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L157
    rewrite hG_witness_witness_witness_right_right_left
  2. L158
    rewrite hP_witness_witness_witness_right_right_left
  3. L159
    rewrite hN_witness_witness_witness_right_right_left
  4. L160
    rewrite hprefix_left
  5. L161
    rewrite hlast
28Use earlier factsL162–168

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

  1. L162
    specialize hensel_horner_linear_successor_identity h
  2. L163
    specialize hensel_horner_linear_successor_identity a
  3. L164
    specialize hensel_horner_linear_successor_identity x1
  4. L165
    specialize hensel_horner_linear_successor_identity x4
  5. L166
    specialize hensel_horner_linear_successor_identity x
  6. L167
    specialize hensel_horner_linear_successor_identity x3
  7. L168
    apply hensel_horner_linear_successor_identity
29Calculate and transport equalitiesL169–173

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L169
    rewrite hG_witness_witness_witness_right_right_right
  2. L170
    rewrite hP_witness_witness_witness_right_right_right
  3. L171
    rewrite hN_witness_witness_witness_right_right_right
  4. L172
    rewrite hprefix_right
  5. L173
    rewrite hprefix_left
30Use earlier factsL174–180

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

  1. L174
    specialize hensel_horner_linear_successor_identity h
  2. L175
    specialize hensel_horner_linear_successor_identity a
  3. L176
    specialize hensel_horner_linear_successor_identity x2
  4. L177
    specialize hensel_horner_linear_successor_identity x5
  5. L178
    specialize hensel_horner_linear_successor_identity x1
  6. L179
    specialize hensel_horner_linear_successor_identity x4
  7. L180
    apply hensel_horner_linear_successor_identity

Library-wide reading audit

Original defined command ledger · 180 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro gb
  6. 0006intro gc
  7. 0007intro h
  8. 0008intro a
  9. 0009induction l
  10. 0010intro vp
  11. 0011intro dp
  12. 0012intro vn
  13. 0013intro dn
  14. 0014intro vg
  15. 0015intro dg
  16. 0016intro hblend
  17. 0017intro hpositive
  18. 0018intro hnegative
  19. 0019intro hcombined
  20. 0020have hP : vp = 0 /\ dp = 0
  21. 0021specialize beta_horner_derivative_empty pb
  22. 0022specialize beta_horner_derivative_empty pc
  23. 0023specialize beta_horner_derivative_empty a
  24. 0024specialize beta_horner_derivative_empty vp
  25. 0025specialize beta_horner_derivative_empty dp
  26. 0026apply beta_horner_derivative_empty
  27. 0027exact hpositive
  28. 0028cases hP
  29. 0029have hN : vn = 0 /\ dn = 0
  30. 0030specialize beta_horner_derivative_empty nb
  31. 0031specialize beta_horner_derivative_empty nc
  32. 0032specialize beta_horner_derivative_empty a
  33. 0033specialize beta_horner_derivative_empty vn
  34. 0034specialize beta_horner_derivative_empty dn
  35. 0035apply beta_horner_derivative_empty
  36. 0036exact hnegative
  37. 0037cases hN
  38. 0038have hG : vg = 0 /\ dg = 0
  39. 0039specialize beta_horner_derivative_empty gb
  40. 0040specialize beta_horner_derivative_empty gc
  41. 0041specialize beta_horner_derivative_empty a
  42. 0042specialize beta_horner_derivative_empty vg
  43. 0043specialize beta_horner_derivative_empty dg
  44. 0044apply beta_horner_derivative_empty
  45. 0045exact hcombined
  46. 0046cases hG
  47. 0047split
  48. 0048rewrite hG_left
  49. 0049rewrite hP_left
  50. 0050rewrite hN_left
  51. 0051simp
  52. 0052rewrite hG_right
  53. 0053rewrite hP_right
  54. 0054rewrite hN_right
  55. 0055simp
  56. 0056intro vp
  57. 0057intro dp
  58. 0058intro vn
  59. 0059intro dn
  60. 0060intro vg
  61. 0061intro dg
  62. 0062intro hblend
  63. 0063intro hpositive
  64. 0064intro hnegative
  65. 0065intro hcombined
  66. 0066have hP : ∃ sph_coefficient_positive. ∃ sph_value_positive. ∃ sph_derivative_positive. Beta(pb,pc,l,sph_coefficient_positive) ∧ (HornerDerivative(pb,pc,a,l,sph_value_positive,sph_derivative_positive) ∧ (vp = sph_value_positive · a + sph_coefficient_positive ∧ dp = sph_derivative_positive · a + sph_value_positive))
  67. 0067specialize beta_horner_derivative_successor_decompose pb
  68. 0068specialize beta_horner_derivative_successor_decompose pc
  69. 0069specialize beta_horner_derivative_successor_decompose a
  70. 0070specialize beta_horner_derivative_successor_decompose l
  71. 0071specialize beta_horner_derivative_successor_decompose vp
  72. 0072specialize beta_horner_derivative_successor_decompose dp
  73. 0073apply beta_horner_derivative_successor_decompose
  74. 0074exact hpositive
  75. 0075cases hP
  76. 0076cases hP_witness
  77. 0077cases hP_witness_witness
  78. 0078cases hP_witness_witness_witness
  79. 0079cases hP_witness_witness_witness_right
  80. 0080cases hP_witness_witness_witness_right_right
  81. 0081have hN : ∃ sph_coefficient_negative. ∃ sph_value_negative. ∃ sph_derivative_negative. Beta(nb,nc,l,sph_coefficient_negative) ∧ (HornerDerivative(nb,nc,a,l,sph_value_negative,sph_derivative_negative) ∧ (vn = sph_value_negative · a + sph_coefficient_negative ∧ dn = sph_derivative_negative · a + sph_value_negative))
  82. 0082specialize beta_horner_derivative_successor_decompose nb
  83. 0083specialize beta_horner_derivative_successor_decompose nc
  84. 0084specialize beta_horner_derivative_successor_decompose a
  85. 0085specialize beta_horner_derivative_successor_decompose l
  86. 0086specialize beta_horner_derivative_successor_decompose vn
  87. 0087specialize beta_horner_derivative_successor_decompose dn
  88. 0088apply beta_horner_derivative_successor_decompose
  89. 0089exact hnegative
  90. 0090cases hN
  91. 0091cases hN_witness
  92. 0092cases hN_witness_witness
  93. 0093cases hN_witness_witness_witness
  94. 0094cases hN_witness_witness_witness_right
  95. 0095cases hN_witness_witness_witness_right_right
  96. 0096have hG : ∃ sph_coefficient_combined. ∃ sph_value_combined. ∃ sph_derivative_combined. Beta(gb,gc,l,sph_coefficient_combined) ∧ (HornerDerivative(gb,gc,a,l,sph_value_combined,sph_derivative_combined) ∧ (vg = sph_value_combined · a + sph_coefficient_combined ∧ dg = sph_derivative_combined · a + sph_value_combined))
  97. 0097specialize beta_horner_derivative_successor_decompose gb
  98. 0098specialize beta_horner_derivative_successor_decompose gc
  99. 0099specialize beta_horner_derivative_successor_decompose a
  100. 0100specialize beta_horner_derivative_successor_decompose l
  101. 0101specialize beta_horner_derivative_successor_decompose vg
  102. 0102specialize beta_horner_derivative_successor_decompose dg
  103. 0103apply beta_horner_derivative_successor_decompose
  104. 0104exact hcombined
  105. 0105cases hG
  106. 0106cases hG_witness
  107. 0107cases hG_witness_witness
  108. 0108cases hG_witness_witness_witness
  109. 0109cases hG_witness_witness_witness_right
  110. 0110cases hG_witness_witness_witness_right_right
  111. 0111have hprefix_blend : HornerCoefficientBlend(pb,pc,nb,nc,gb,gc,h,l)
  112. 0112intro i
  113. 0113intro A
  114. 0114intro B
  115. 0115intro C
  116. 0116intro hi
  117. 0117intro hA
  118. 0118intro hB
  119. 0119intro hC
  120. 0120specialize hblend i
  121. 0121specialize hblend A
  122. 0122specialize hblend B
  123. 0123specialize hblend C
  124. 0124apply hblend
  125. 0125specialize le_succ (S i)
  126. 0126specialize le_succ l
  127. 0127apply le_succ
  128. 0128exact hi
  129. 0129exact hA
  130. 0130exact hB
  131. 0131exact hC
  132. 0132have hprefix : x7 = x1 + h * x4 /\ x8 = x2 + h * x5
  133. 0133specialize IH x1
  134. 0134specialize IH x2
  135. 0135specialize IH x4
  136. 0136specialize IH x5
  137. 0137specialize IH x7
  138. 0138specialize IH x8
  139. 0139apply IH
  140. 0140exact hprefix_blend
  141. 0141exact hP_witness_witness_witness_right_left
  142. 0142exact hN_witness_witness_witness_right_left
  143. 0143exact hG_witness_witness_witness_right_left
  144. 0144cases hprefix
  145. 0145have hlast : x6 = x + h * x3
  146. 0146specialize hblend l
  147. 0147specialize hblend x
  148. 0148specialize hblend x3
  149. 0149specialize hblend x6
  150. 0150apply hblend
  151. 0151specialize le_refl (S l)
  152. 0152apply le_refl
  153. 0153exact hP_witness_witness_witness_left
  154. 0154exact hN_witness_witness_witness_left
  155. 0155exact hG_witness_witness_witness_left
  156. 0156split
  157. 0157rewrite hG_witness_witness_witness_right_right_left
  158. 0158rewrite hP_witness_witness_witness_right_right_left
  159. 0159rewrite hN_witness_witness_witness_right_right_left
  160. 0160rewrite hprefix_left
  161. 0161rewrite hlast
  162. 0162specialize hensel_horner_linear_successor_identity h
  163. 0163specialize hensel_horner_linear_successor_identity a
  164. 0164specialize hensel_horner_linear_successor_identity x1
  165. 0165specialize hensel_horner_linear_successor_identity x4
  166. 0166specialize hensel_horner_linear_successor_identity x
  167. 0167specialize hensel_horner_linear_successor_identity x3
  168. 0168apply hensel_horner_linear_successor_identity
  169. 0169rewrite hG_witness_witness_witness_right_right_right
  170. 0170rewrite hP_witness_witness_witness_right_right_right
  171. 0171rewrite hN_witness_witness_witness_right_right_right
  172. 0172rewrite hprefix_right
  173. 0173rewrite hprefix_left
  174. 0174specialize hensel_horner_linear_successor_identity h
  175. 0175specialize hensel_horner_linear_successor_identity a
  176. 0176specialize hensel_horner_linear_successor_identity x2
  177. 0177specialize hensel_horner_linear_successor_identity x5
  178. 0178specialize hensel_horner_linear_successor_identity x1
  179. 0179specialize hensel_horner_linear_successor_identity x4
  180. 0180apply hensel_horner_linear_successor_identity