HL001B

beta_signed_horner_blend_root_equivalence

At every natural point the recoded natural root condition is equivalent to the original integer-polynomial root condition, not merely implied by it.

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. ∀ M. ∀ m. M = S h → Dvd(m,M) → HornerCoefficientBlend(pb,pc,nb,nc,gb,gc,h,l) → (HornerRootModulo(gb,gc,a,l,m) → SignedHornerRoot(pb,pc,nb,nc,a,l,m)) ∧ (SignedHornerRoot(pb,pc,nb,nc,a,l,m) → HornerRootModulo(gb,gc,a,l,m))

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

Definition DAG

HornerDerivative(b,c,t,l,n,z) · 3HornerRootModulo(b,c,a,l,m) · 2HornerCoefficientBlend(pb,pc,nb,nc,gb,gc,h,l) · 1SignedHornerRoot(pb,pc,nb,nc,a,l,m) · 2Dvd(d,n) · 1ModEq(m,a,b) · 4

Actual proof prerequisites

beta_horner_derivative_value_exists · checked external prerequisitebeta_horner_coefficient_blend_value_derivativehensel_signed_blend_zero_iffbeta_horner_derivative_value_projection · checked external prerequisitebeta_horner_eval_functional · checked external prerequisite
Original expanded first-order statement 
forall pb pc nb nc gb gc h a l M m. M = S h -> (exists q. M = m * q) -> (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 hpl_value_root. ((exists ff_u_ph_hpl_root ff_v_ph_hpl_root. ((((exists fs_h_ph_hpl_root_body_start. fs_h_ph_hpl_root_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_start. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_start * S ((S (0)) * ff_v_ph_hpl_root) + (0))) /\ ((((exists fs_h_ph_hpl_root_body_terminal. fs_h_ph_hpl_root_body_terminal + S (hpl_value_root) = S ((S (l)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_terminal. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_terminal * S ((S (l)) * ff_v_ph_hpl_root) + (hpl_value_root))) /\ forall ff_i_ph_hpl_root_body_steps. (exists ph_bound_hpl_root_body_steps. ph_bound_hpl_root_body_steps + S ff_i_ph_hpl_root_body_steps = l) -> exists ff_coefficient_ph_hpl_root_body_steps ff_previous_ph_hpl_root_body_steps ff_current_ph_hpl_root_body_steps. ((((exists fs_h_ph_hpl_root_body_steps_coefficient. fs_h_ph_hpl_root_body_steps_coefficient + S (ff_coefficient_ph_hpl_root_body_steps) = S ((S (ff_i_ph_hpl_root_body_steps)) * gc)) /\ exists fs_q_ph_hpl_root_body_steps_coefficient. gb = fs_q_ph_hpl_root_body_steps_coefficient * S ((S (ff_i_ph_hpl_root_body_steps)) * gc) + (ff_coefficient_ph_hpl_root_body_steps))) /\ ((((exists fs_h_ph_hpl_root_body_steps_before. fs_h_ph_hpl_root_body_steps_before + S (ff_previous_ph_hpl_root_body_steps) = S ((S (ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_steps_before. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_steps_before * S ((S (ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root) + (ff_previous_ph_hpl_root_body_steps))) /\ ((((exists fs_h_ph_hpl_root_body_steps_after. fs_h_ph_hpl_root_body_steps_after + S (ff_current_ph_hpl_root_body_steps) = S ((S (S ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_steps_after. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_steps_after * S ((S (S ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root) + (ff_current_ph_hpl_root_body_steps))) /\ ff_current_ph_hpl_root_body_steps = ff_previous_ph_hpl_root_body_steps * a + ff_coefficient_ph_hpl_root_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_root hgcrt_mod_right_hpl_root. hpl_value_root + m * hgcrt_mod_left_hpl_root = 0 + m * hgcrt_mod_right_hpl_root))) -> (exists sph_positive_root sph_negative_root. ((exists ff_u_ph_hpl_sph_root_positive ff_v_ph_hpl_sph_root_positive. ((((exists fs_h_ph_hpl_sph_root_positive_body_start. fs_h_ph_hpl_sph_root_positive_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_sph_root_positive)) /\ exists fs_q_ph_hpl_sph_root_positive_body_start. ff_u_ph_hpl_sph_root_positive = fs_q_ph_hpl_sph_root_positive_body_start * S ((S (0)) * ff_v_ph_hpl_sph_root_positive) + (0))) /\ ((((exists fs_h_ph_hpl_sph_root_positive_body_terminal. fs_h_ph_hpl_sph_root_positive_body_terminal + S (sph_positive_root) = S ((S (l)) * ff_v_ph_hpl_sph_root_positive)) /\ exists fs_q_ph_hpl_sph_root_positive_body_terminal. ff_u_ph_hpl_sph_root_positive = fs_q_ph_hpl_sph_root_positive_body_terminal * S ((S (l)) * ff_v_ph_hpl_sph_root_positive) + (sph_positive_root))) /\ forall ff_i_ph_hpl_sph_root_positive_body_steps. (exists ph_bound_hpl_sph_root_positive_body_steps. ph_bound_hpl_sph_root_positive_body_steps + S ff_i_ph_hpl_sph_root_positive_body_steps = l) -> exists ff_coefficient_ph_hpl_sph_root_positive_body_steps ff_previous_ph_hpl_sph_root_positive_body_steps ff_current_ph_hpl_sph_root_positive_body_steps. ((((exists fs_h_ph_hpl_sph_root_positive_body_steps_coefficient. fs_h_ph_hpl_sph_root_positive_body_steps_coefficient + S (ff_coefficient_ph_hpl_sph_root_positive_body_steps) = S ((S (ff_i_ph_hpl_sph_root_positive_body_steps)) * pc)) /\ exists fs_q_ph_hpl_sph_root_positive_body_steps_coefficient. pb = fs_q_ph_hpl_sph_root_positive_body_steps_coefficient * S ((S (ff_i_ph_hpl_sph_root_positive_body_steps)) * pc) + (ff_coefficient_ph_hpl_sph_root_positive_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_root_positive_body_steps_before. fs_h_ph_hpl_sph_root_positive_body_steps_before + S (ff_previous_ph_hpl_sph_root_positive_body_steps) = S ((S (ff_i_ph_hpl_sph_root_positive_body_steps)) * ff_v_ph_hpl_sph_root_positive)) /\ exists fs_q_ph_hpl_sph_root_positive_body_steps_before. ff_u_ph_hpl_sph_root_positive = fs_q_ph_hpl_sph_root_positive_body_steps_before * S ((S (ff_i_ph_hpl_sph_root_positive_body_steps)) * ff_v_ph_hpl_sph_root_positive) + (ff_previous_ph_hpl_sph_root_positive_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_root_positive_body_steps_after. fs_h_ph_hpl_sph_root_positive_body_steps_after + S (ff_current_ph_hpl_sph_root_positive_body_steps) = S ((S (S ff_i_ph_hpl_sph_root_positive_body_steps)) * ff_v_ph_hpl_sph_root_positive)) /\ exists fs_q_ph_hpl_sph_root_positive_body_steps_after. ff_u_ph_hpl_sph_root_positive = fs_q_ph_hpl_sph_root_positive_body_steps_after * S ((S (S ff_i_ph_hpl_sph_root_positive_body_steps)) * ff_v_ph_hpl_sph_root_positive) + (ff_current_ph_hpl_sph_root_positive_body_steps))) /\ ff_current_ph_hpl_sph_root_positive_body_steps = ff_previous_ph_hpl_sph_root_positive_body_steps * a + ff_coefficient_ph_hpl_sph_root_positive_body_steps)))))) /\ ((exists ff_u_ph_hpl_sph_root_negative ff_v_ph_hpl_sph_root_negative. ((((exists fs_h_ph_hpl_sph_root_negative_body_start. fs_h_ph_hpl_sph_root_negative_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_sph_root_negative)) /\ exists fs_q_ph_hpl_sph_root_negative_body_start. ff_u_ph_hpl_sph_root_negative = fs_q_ph_hpl_sph_root_negative_body_start * S ((S (0)) * ff_v_ph_hpl_sph_root_negative) + (0))) /\ ((((exists fs_h_ph_hpl_sph_root_negative_body_terminal. fs_h_ph_hpl_sph_root_negative_body_terminal + S (sph_negative_root) = S ((S (l)) * ff_v_ph_hpl_sph_root_negative)) /\ exists fs_q_ph_hpl_sph_root_negative_body_terminal. ff_u_ph_hpl_sph_root_negative = fs_q_ph_hpl_sph_root_negative_body_terminal * S ((S (l)) * ff_v_ph_hpl_sph_root_negative) + (sph_negative_root))) /\ forall ff_i_ph_hpl_sph_root_negative_body_steps. (exists ph_bound_hpl_sph_root_negative_body_steps. ph_bound_hpl_sph_root_negative_body_steps + S ff_i_ph_hpl_sph_root_negative_body_steps = l) -> exists ff_coefficient_ph_hpl_sph_root_negative_body_steps ff_previous_ph_hpl_sph_root_negative_body_steps ff_current_ph_hpl_sph_root_negative_body_steps. ((((exists fs_h_ph_hpl_sph_root_negative_body_steps_coefficient. fs_h_ph_hpl_sph_root_negative_body_steps_coefficient + S (ff_coefficient_ph_hpl_sph_root_negative_body_steps) = S ((S (ff_i_ph_hpl_sph_root_negative_body_steps)) * nc)) /\ exists fs_q_ph_hpl_sph_root_negative_body_steps_coefficient. nb = fs_q_ph_hpl_sph_root_negative_body_steps_coefficient * S ((S (ff_i_ph_hpl_sph_root_negative_body_steps)) * nc) + (ff_coefficient_ph_hpl_sph_root_negative_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_root_negative_body_steps_before. fs_h_ph_hpl_sph_root_negative_body_steps_before + S (ff_previous_ph_hpl_sph_root_negative_body_steps) = S ((S (ff_i_ph_hpl_sph_root_negative_body_steps)) * ff_v_ph_hpl_sph_root_negative)) /\ exists fs_q_ph_hpl_sph_root_negative_body_steps_before. ff_u_ph_hpl_sph_root_negative = fs_q_ph_hpl_sph_root_negative_body_steps_before * S ((S (ff_i_ph_hpl_sph_root_negative_body_steps)) * ff_v_ph_hpl_sph_root_negative) + (ff_previous_ph_hpl_sph_root_negative_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_root_negative_body_steps_after. fs_h_ph_hpl_sph_root_negative_body_steps_after + S (ff_current_ph_hpl_sph_root_negative_body_steps) = S ((S (S ff_i_ph_hpl_sph_root_negative_body_steps)) * ff_v_ph_hpl_sph_root_negative)) /\ exists fs_q_ph_hpl_sph_root_negative_body_steps_after. ff_u_ph_hpl_sph_root_negative = fs_q_ph_hpl_sph_root_negative_body_steps_after * S ((S (S ff_i_ph_hpl_sph_root_negative_body_steps)) * ff_v_ph_hpl_sph_root_negative) + (ff_current_ph_hpl_sph_root_negative_body_steps))) /\ ff_current_ph_hpl_sph_root_negative_body_steps = ff_previous_ph_hpl_sph_root_negative_body_steps * a + ff_coefficient_ph_hpl_sph_root_negative_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_root hgcrt_mod_right_hpl_root. sph_positive_root + m * hgcrt_mod_left_hpl_root = sph_negative_root + m * hgcrt_mod_right_hpl_root))))) /\ ((exists sph_positive_root sph_negative_root. ((exists ff_u_ph_hpl_sph_root_positive ff_v_ph_hpl_sph_root_positive. ((((exists fs_h_ph_hpl_sph_root_positive_body_start. fs_h_ph_hpl_sph_root_positive_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_sph_root_positive)) /\ exists fs_q_ph_hpl_sph_root_positive_body_start. ff_u_ph_hpl_sph_root_positive = fs_q_ph_hpl_sph_root_positive_body_start * S ((S (0)) * ff_v_ph_hpl_sph_root_positive) + (0))) /\ ((((exists fs_h_ph_hpl_sph_root_positive_body_terminal. fs_h_ph_hpl_sph_root_positive_body_terminal + S (sph_positive_root) = S ((S (l)) * ff_v_ph_hpl_sph_root_positive)) /\ exists fs_q_ph_hpl_sph_root_positive_body_terminal. ff_u_ph_hpl_sph_root_positive = fs_q_ph_hpl_sph_root_positive_body_terminal * S ((S (l)) * ff_v_ph_hpl_sph_root_positive) + (sph_positive_root))) /\ forall ff_i_ph_hpl_sph_root_positive_body_steps. (exists ph_bound_hpl_sph_root_positive_body_steps. ph_bound_hpl_sph_root_positive_body_steps + S ff_i_ph_hpl_sph_root_positive_body_steps = l) -> exists ff_coefficient_ph_hpl_sph_root_positive_body_steps ff_previous_ph_hpl_sph_root_positive_body_steps ff_current_ph_hpl_sph_root_positive_body_steps. ((((exists fs_h_ph_hpl_sph_root_positive_body_steps_coefficient. fs_h_ph_hpl_sph_root_positive_body_steps_coefficient + S (ff_coefficient_ph_hpl_sph_root_positive_body_steps) = S ((S (ff_i_ph_hpl_sph_root_positive_body_steps)) * pc)) /\ exists fs_q_ph_hpl_sph_root_positive_body_steps_coefficient. pb = fs_q_ph_hpl_sph_root_positive_body_steps_coefficient * S ((S (ff_i_ph_hpl_sph_root_positive_body_steps)) * pc) + (ff_coefficient_ph_hpl_sph_root_positive_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_root_positive_body_steps_before. fs_h_ph_hpl_sph_root_positive_body_steps_before + S (ff_previous_ph_hpl_sph_root_positive_body_steps) = S ((S (ff_i_ph_hpl_sph_root_positive_body_steps)) * ff_v_ph_hpl_sph_root_positive)) /\ exists fs_q_ph_hpl_sph_root_positive_body_steps_before. ff_u_ph_hpl_sph_root_positive = fs_q_ph_hpl_sph_root_positive_body_steps_before * S ((S (ff_i_ph_hpl_sph_root_positive_body_steps)) * ff_v_ph_hpl_sph_root_positive) + (ff_previous_ph_hpl_sph_root_positive_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_root_positive_body_steps_after. fs_h_ph_hpl_sph_root_positive_body_steps_after + S (ff_current_ph_hpl_sph_root_positive_body_steps) = S ((S (S ff_i_ph_hpl_sph_root_positive_body_steps)) * ff_v_ph_hpl_sph_root_positive)) /\ exists fs_q_ph_hpl_sph_root_positive_body_steps_after. ff_u_ph_hpl_sph_root_positive = fs_q_ph_hpl_sph_root_positive_body_steps_after * S ((S (S ff_i_ph_hpl_sph_root_positive_body_steps)) * ff_v_ph_hpl_sph_root_positive) + (ff_current_ph_hpl_sph_root_positive_body_steps))) /\ ff_current_ph_hpl_sph_root_positive_body_steps = ff_previous_ph_hpl_sph_root_positive_body_steps * a + ff_coefficient_ph_hpl_sph_root_positive_body_steps)))))) /\ ((exists ff_u_ph_hpl_sph_root_negative ff_v_ph_hpl_sph_root_negative. ((((exists fs_h_ph_hpl_sph_root_negative_body_start. fs_h_ph_hpl_sph_root_negative_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_sph_root_negative)) /\ exists fs_q_ph_hpl_sph_root_negative_body_start. ff_u_ph_hpl_sph_root_negative = fs_q_ph_hpl_sph_root_negative_body_start * S ((S (0)) * ff_v_ph_hpl_sph_root_negative) + (0))) /\ ((((exists fs_h_ph_hpl_sph_root_negative_body_terminal. fs_h_ph_hpl_sph_root_negative_body_terminal + S (sph_negative_root) = S ((S (l)) * ff_v_ph_hpl_sph_root_negative)) /\ exists fs_q_ph_hpl_sph_root_negative_body_terminal. ff_u_ph_hpl_sph_root_negative = fs_q_ph_hpl_sph_root_negative_body_terminal * S ((S (l)) * ff_v_ph_hpl_sph_root_negative) + (sph_negative_root))) /\ forall ff_i_ph_hpl_sph_root_negative_body_steps. (exists ph_bound_hpl_sph_root_negative_body_steps. ph_bound_hpl_sph_root_negative_body_steps + S ff_i_ph_hpl_sph_root_negative_body_steps = l) -> exists ff_coefficient_ph_hpl_sph_root_negative_body_steps ff_previous_ph_hpl_sph_root_negative_body_steps ff_current_ph_hpl_sph_root_negative_body_steps. ((((exists fs_h_ph_hpl_sph_root_negative_body_steps_coefficient. fs_h_ph_hpl_sph_root_negative_body_steps_coefficient + S (ff_coefficient_ph_hpl_sph_root_negative_body_steps) = S ((S (ff_i_ph_hpl_sph_root_negative_body_steps)) * nc)) /\ exists fs_q_ph_hpl_sph_root_negative_body_steps_coefficient. nb = fs_q_ph_hpl_sph_root_negative_body_steps_coefficient * S ((S (ff_i_ph_hpl_sph_root_negative_body_steps)) * nc) + (ff_coefficient_ph_hpl_sph_root_negative_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_root_negative_body_steps_before. fs_h_ph_hpl_sph_root_negative_body_steps_before + S (ff_previous_ph_hpl_sph_root_negative_body_steps) = S ((S (ff_i_ph_hpl_sph_root_negative_body_steps)) * ff_v_ph_hpl_sph_root_negative)) /\ exists fs_q_ph_hpl_sph_root_negative_body_steps_before. ff_u_ph_hpl_sph_root_negative = fs_q_ph_hpl_sph_root_negative_body_steps_before * S ((S (ff_i_ph_hpl_sph_root_negative_body_steps)) * ff_v_ph_hpl_sph_root_negative) + (ff_previous_ph_hpl_sph_root_negative_body_steps))) /\ ((((exists fs_h_ph_hpl_sph_root_negative_body_steps_after. fs_h_ph_hpl_sph_root_negative_body_steps_after + S (ff_current_ph_hpl_sph_root_negative_body_steps) = S ((S (S ff_i_ph_hpl_sph_root_negative_body_steps)) * ff_v_ph_hpl_sph_root_negative)) /\ exists fs_q_ph_hpl_sph_root_negative_body_steps_after. ff_u_ph_hpl_sph_root_negative = fs_q_ph_hpl_sph_root_negative_body_steps_after * S ((S (S ff_i_ph_hpl_sph_root_negative_body_steps)) * ff_v_ph_hpl_sph_root_negative) + (ff_current_ph_hpl_sph_root_negative_body_steps))) /\ ff_current_ph_hpl_sph_root_negative_body_steps = ff_previous_ph_hpl_sph_root_negative_body_steps * a + ff_coefficient_ph_hpl_sph_root_negative_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_root hgcrt_mod_right_hpl_root. sph_positive_root + m * hgcrt_mod_left_hpl_root = sph_negative_root + m * hgcrt_mod_right_hpl_root)))) -> (exists hpl_value_root. ((exists ff_u_ph_hpl_root ff_v_ph_hpl_root. ((((exists fs_h_ph_hpl_root_body_start. fs_h_ph_hpl_root_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_start. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_start * S ((S (0)) * ff_v_ph_hpl_root) + (0))) /\ ((((exists fs_h_ph_hpl_root_body_terminal. fs_h_ph_hpl_root_body_terminal + S (hpl_value_root) = S ((S (l)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_terminal. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_terminal * S ((S (l)) * ff_v_ph_hpl_root) + (hpl_value_root))) /\ forall ff_i_ph_hpl_root_body_steps. (exists ph_bound_hpl_root_body_steps. ph_bound_hpl_root_body_steps + S ff_i_ph_hpl_root_body_steps = l) -> exists ff_coefficient_ph_hpl_root_body_steps ff_previous_ph_hpl_root_body_steps ff_current_ph_hpl_root_body_steps. ((((exists fs_h_ph_hpl_root_body_steps_coefficient. fs_h_ph_hpl_root_body_steps_coefficient + S (ff_coefficient_ph_hpl_root_body_steps) = S ((S (ff_i_ph_hpl_root_body_steps)) * gc)) /\ exists fs_q_ph_hpl_root_body_steps_coefficient. gb = fs_q_ph_hpl_root_body_steps_coefficient * S ((S (ff_i_ph_hpl_root_body_steps)) * gc) + (ff_coefficient_ph_hpl_root_body_steps))) /\ ((((exists fs_h_ph_hpl_root_body_steps_before. fs_h_ph_hpl_root_body_steps_before + S (ff_previous_ph_hpl_root_body_steps) = S ((S (ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_steps_before. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_steps_before * S ((S (ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root) + (ff_previous_ph_hpl_root_body_steps))) /\ ((((exists fs_h_ph_hpl_root_body_steps_after. fs_h_ph_hpl_root_body_steps_after + S (ff_current_ph_hpl_root_body_steps) = S ((S (S ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root)) /\ exists fs_q_ph_hpl_root_body_steps_after. ff_u_ph_hpl_root = fs_q_ph_hpl_root_body_steps_after * S ((S (S ff_i_ph_hpl_root_body_steps)) * ff_v_ph_hpl_root) + (ff_current_ph_hpl_root_body_steps))) /\ ff_current_ph_hpl_root_body_steps = ff_previous_ph_hpl_root_body_steps * a + ff_coefficient_ph_hpl_root_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_root hgcrt_mod_right_hpl_root. hpl_value_root + m * hgcrt_mod_left_hpl_root = 0 + m * hgcrt_mod_right_hpl_root)))))

Complete tactic proof in conservative notation

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

169 script commands · 37 reading checkpoints · 8 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 horner coefficient blend value derivativehensel signed blend zero iff
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 gb
  6. L6
    intro gc
  7. L7
    intro h
  8. L8
    intro a
  9. L9
    intro l
  10. L10
    intro M
02Fix variables and assumptionsL11–14

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

  1. L11
    intro m
  2. L12
    intro hM
  3. L13
    intro hdiv
  4. L14
    intro hblend
03Establish hPL15–20

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

  1. L15
    have hP : ∃ vp. ∃ dp. HornerDerivative(pb,pc,a,l,vp,dp)Definitions: HornerDerivative(pb,pc,a,l,vp,dp)Original native command in the exact edition
  2. L16
    specialize beta_horner_derivative_value_exists pb
  3. L17
    specialize beta_horner_derivative_value_exists pc
  4. L18
    specialize beta_horner_derivative_value_exists a
  5. L19
    specialize beta_horner_derivative_value_exists l
  6. L20
    apply beta_horner_derivative_value_exists
04Separate the logical casesL21–22

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

  1. L21
    cases hP
  2. L22
    cases hP_witness
05Establish hNL23–28

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

  1. L23
    have hN : ∃ vn. ∃ dn. HornerDerivative(nb,nc,a,l,vn,dn)Definitions: HornerDerivative(nb,nc,a,l,vn,dn)Original native command in the exact edition
  2. L24
    specialize beta_horner_derivative_value_exists nb
  3. L25
    specialize beta_horner_derivative_value_exists nc
  4. L26
    specialize beta_horner_derivative_value_exists a
  5. L27
    specialize beta_horner_derivative_value_exists l
  6. L28
    apply beta_horner_derivative_value_exists
06Separate the logical casesL29–30

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

  1. L29
    cases hN
  2. L30
    cases hN_witness
07Establish hGL31–36

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

  1. L31
    have hG : ∃ vg. ∃ dg. HornerDerivative(gb,gc,a,l,vg,dg)Definitions: HornerDerivative(gb,gc,a,l,vg,dg)Original native command in the exact edition
  2. L32
    specialize beta_horner_derivative_value_exists gb
  3. L33
    specialize beta_horner_derivative_value_exists gc
  4. L34
    specialize beta_horner_derivative_value_exists a
  5. L35
    specialize beta_horner_derivative_value_exists l
  6. L36
    apply beta_horner_derivative_value_exists
08Separate the logical casesL37–38

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

  1. L37
    cases hG
  2. L38
    cases hG_witness
09Establish hlinearL39–48

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

  1. L39
    have hlinear : x4 = x + h * x2 /\ x5 = x1 + h * x3
  2. L40
    specialize beta_horner_coefficient_blend_value_derivative pb
  3. L41
    specialize beta_horner_coefficient_blend_value_derivative pc
  4. L42
    specialize beta_horner_coefficient_blend_value_derivative nb
  5. L43
    specialize beta_horner_coefficient_blend_value_derivative nc
  6. L44
    specialize beta_horner_coefficient_blend_value_derivative gb
  7. L45
    specialize beta_horner_coefficient_blend_value_derivative gc
  8. L46
    specialize beta_horner_coefficient_blend_value_derivative h
  9. L47
    specialize beta_horner_coefficient_blend_value_derivative a
  10. L48
    specialize beta_horner_coefficient_blend_value_derivative l
10Use earlier factsL49–58

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

  1. L49
    specialize beta_horner_coefficient_blend_value_derivative x
  2. L50
    specialize beta_horner_coefficient_blend_value_derivative x1
  3. L51
    specialize beta_horner_coefficient_blend_value_derivative x2
  4. L52
    specialize beta_horner_coefficient_blend_value_derivative x3
  5. L53
    specialize beta_horner_coefficient_blend_value_derivative x4
  6. L54
    specialize beta_horner_coefficient_blend_value_derivative x5
  7. L55
    apply beta_horner_coefficient_blend_value_derivative
  8. L56
    exact hblend
  9. L57
    exact hP_witness_witness
  10. L58
    exact hN_witness_witness
11Use earlier factsL59–59

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

  1. L59
    exact hG_witness_witness
12Separate the logical casesL60–60

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

  1. L60
    cases hlinear
13Establish hiffL61–70

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hensel signed blend zero iff.

  1. L61
    have hiff : (ModEq(m,x4,0) → ModEq(m,x,x2)) ∧ (ModEq(m,x,x2) → ModEq(m,x4,0))Definitions: ModEq(m,x4,0)ModEq(m,x,x2)Original native command in the exact edition
  2. L62
    specialize hensel_signed_blend_zero_iff m
  3. L63
    specialize hensel_signed_blend_zero_iff M
  4. L64
    specialize hensel_signed_blend_zero_iff h
  5. L65
    specialize hensel_signed_blend_zero_iff x
  6. L66
    specialize hensel_signed_blend_zero_iff x2
  7. L67
    specialize hensel_signed_blend_zero_iff x4
  8. L68
    apply hensel_signed_blend_zero_iff
  9. L69
    exact hM
  10. L70
    exact hdiv
14Use earlier factsL71–71

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

  1. L71
    exact hlinear_left
15Separate the logical casesL72–73

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

  1. L72
    cases hiff
  2. L73
    split
16Fix variables and assumptionsL74–74

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

  1. L74
    intro hnatural
17Separate the logical casesL75–76

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

  1. L75
    cases hnatural
  2. L76
    cases hnatural_witness
18Establish hvalueL77–86

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

  1. L77
    have hvalue : x4 = x6
  2. L78
    specialize beta_horner_eval_functional gb
  3. L79
    specialize beta_horner_eval_functional gc
  4. L80
    specialize beta_horner_eval_functional a
  5. L81
    specialize beta_horner_eval_functional l
  6. L82
    specialize beta_horner_eval_functional x4
  7. L83
    specialize beta_horner_eval_functional x6
  8. L84
    apply beta_horner_eval_functional
  9. L85
    specialize beta_horner_derivative_value_projection gb
  10. L86
    specialize beta_horner_derivative_value_projection gc
19Use earlier factsL87–93

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

  1. L87
    specialize beta_horner_derivative_value_projection a
  2. L88
    specialize beta_horner_derivative_value_projection l
  3. L89
    specialize beta_horner_derivative_value_projection x4
  4. L90
    specialize beta_horner_derivative_value_projection x5
  5. L91
    apply beta_horner_derivative_value_projection
  6. L92
    exact hG_witness_witness
  7. L93
    exact hnatural_witness_left
20Construct an explicit witnessL94–95

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

  1. L94
    exists x
  2. L95
    exists x2
21Separate the logical casesL96–96

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

  1. L96
    split
22Use earlier factsL97–104

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

  1. L97
    specialize beta_horner_derivative_value_projection pb
  2. L98
    specialize beta_horner_derivative_value_projection pc
  3. L99
    specialize beta_horner_derivative_value_projection a
  4. L100
    specialize beta_horner_derivative_value_projection l
  5. L101
    specialize beta_horner_derivative_value_projection x
  6. L102
    specialize beta_horner_derivative_value_projection x1
  7. L103
    apply beta_horner_derivative_value_projection
  8. L104
    exact hP_witness_witness
23Separate the logical casesL105–105

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

  1. L105
    split
24Use earlier factsL106–114

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

  1. L106
    specialize beta_horner_derivative_value_projection nb
  2. L107
    specialize beta_horner_derivative_value_projection nc
  3. L108
    specialize beta_horner_derivative_value_projection a
  4. L109
    specialize beta_horner_derivative_value_projection l
  5. L110
    specialize beta_horner_derivative_value_projection x2
  6. L111
    specialize beta_horner_derivative_value_projection x3
  7. L112
    apply beta_horner_derivative_value_projection
  8. L113
    exact hN_witness_witness
  9. L114
    apply hiff_left
25Calculate and transport equalitiesL115–115

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

  1. L115
    rewrite hvalue
26Use earlier factsL116–116

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

  1. L116
    exact hnatural_witness_right
27Fix variables and assumptionsL117–117

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

  1. L117
    intro hsigned
28Separate the logical casesL118–121

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

  1. L118
    cases hsigned
  2. L119
    cases hsigned_witness
  3. L120
    cases hsigned_witness_witness
  4. L121
    cases hsigned_witness_witness_right
29Establish hpositiveL122–131

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

  1. L122
    have hpositive : x = x6
  2. L123
    specialize beta_horner_eval_functional pb
  3. L124
    specialize beta_horner_eval_functional pc
  4. L125
    specialize beta_horner_eval_functional a
  5. L126
    specialize beta_horner_eval_functional l
  6. L127
    specialize beta_horner_eval_functional x
  7. L128
    specialize beta_horner_eval_functional x6
  8. L129
    apply beta_horner_eval_functional
  9. L130
    specialize beta_horner_derivative_value_projection pb
  10. L131
    specialize beta_horner_derivative_value_projection pc
30Use earlier factsL132–138

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

  1. L132
    specialize beta_horner_derivative_value_projection a
  2. L133
    specialize beta_horner_derivative_value_projection l
  3. L134
    specialize beta_horner_derivative_value_projection x
  4. L135
    specialize beta_horner_derivative_value_projection x1
  5. L136
    apply beta_horner_derivative_value_projection
  6. L137
    exact hP_witness_witness
  7. L138
    exact hsigned_witness_witness_left
31Establish hnegativeL139–148

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

  1. L139
    have hnegative : x2 = x7
  2. L140
    specialize beta_horner_eval_functional nb
  3. L141
    specialize beta_horner_eval_functional nc
  4. L142
    specialize beta_horner_eval_functional a
  5. L143
    specialize beta_horner_eval_functional l
  6. L144
    specialize beta_horner_eval_functional x2
  7. L145
    specialize beta_horner_eval_functional x7
  8. L146
    apply beta_horner_eval_functional
  9. L147
    specialize beta_horner_derivative_value_projection nb
  10. L148
    specialize beta_horner_derivative_value_projection nc
32Use earlier factsL149–155

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

  1. L149
    specialize beta_horner_derivative_value_projection a
  2. L150
    specialize beta_horner_derivative_value_projection l
  3. L151
    specialize beta_horner_derivative_value_projection x2
  4. L152
    specialize beta_horner_derivative_value_projection x3
  5. L153
    apply beta_horner_derivative_value_projection
  6. L154
    exact hN_witness_witness
  7. L155
    exact hsigned_witness_witness_right_left
33Construct an explicit witnessL156–156

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

  1. L156
    exists x4
34Separate the logical casesL157–157

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

  1. L157
    split
35Use earlier factsL158–166

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

  1. L158
    specialize beta_horner_derivative_value_projection gb
  2. L159
    specialize beta_horner_derivative_value_projection gc
  3. L160
    specialize beta_horner_derivative_value_projection a
  4. L161
    specialize beta_horner_derivative_value_projection l
  5. L162
    specialize beta_horner_derivative_value_projection x4
  6. L163
    specialize beta_horner_derivative_value_projection x5
  7. L164
    apply beta_horner_derivative_value_projection
  8. L165
    exact hG_witness_witness
  9. L166
    apply hiff_right
36Calculate and transport equalitiesL167–168

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

  1. L167
    rewrite hpositive
  2. L168
    rewrite hnegative
37Use earlier factsL169–169

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

  1. L169
    exact hsigned_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 169 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. 0009intro l
  10. 0010intro M
  11. 0011intro m
  12. 0012intro hM
  13. 0013intro hdiv
  14. 0014intro hblend
  15. 0015have hP : ∃ vp. ∃ dp. HornerDerivative(pb,pc,a,l,vp,dp)
  16. 0016specialize beta_horner_derivative_value_exists pb
  17. 0017specialize beta_horner_derivative_value_exists pc
  18. 0018specialize beta_horner_derivative_value_exists a
  19. 0019specialize beta_horner_derivative_value_exists l
  20. 0020apply beta_horner_derivative_value_exists
  21. 0021cases hP
  22. 0022cases hP_witness
  23. 0023have hN : ∃ vn. ∃ dn. HornerDerivative(nb,nc,a,l,vn,dn)
  24. 0024specialize beta_horner_derivative_value_exists nb
  25. 0025specialize beta_horner_derivative_value_exists nc
  26. 0026specialize beta_horner_derivative_value_exists a
  27. 0027specialize beta_horner_derivative_value_exists l
  28. 0028apply beta_horner_derivative_value_exists
  29. 0029cases hN
  30. 0030cases hN_witness
  31. 0031have hG : ∃ vg. ∃ dg. HornerDerivative(gb,gc,a,l,vg,dg)
  32. 0032specialize beta_horner_derivative_value_exists gb
  33. 0033specialize beta_horner_derivative_value_exists gc
  34. 0034specialize beta_horner_derivative_value_exists a
  35. 0035specialize beta_horner_derivative_value_exists l
  36. 0036apply beta_horner_derivative_value_exists
  37. 0037cases hG
  38. 0038cases hG_witness
  39. 0039have hlinear : x4 = x + h * x2 /\ x5 = x1 + h * x3
  40. 0040specialize beta_horner_coefficient_blend_value_derivative pb
  41. 0041specialize beta_horner_coefficient_blend_value_derivative pc
  42. 0042specialize beta_horner_coefficient_blend_value_derivative nb
  43. 0043specialize beta_horner_coefficient_blend_value_derivative nc
  44. 0044specialize beta_horner_coefficient_blend_value_derivative gb
  45. 0045specialize beta_horner_coefficient_blend_value_derivative gc
  46. 0046specialize beta_horner_coefficient_blend_value_derivative h
  47. 0047specialize beta_horner_coefficient_blend_value_derivative a
  48. 0048specialize beta_horner_coefficient_blend_value_derivative l
  49. 0049specialize beta_horner_coefficient_blend_value_derivative x
  50. 0050specialize beta_horner_coefficient_blend_value_derivative x1
  51. 0051specialize beta_horner_coefficient_blend_value_derivative x2
  52. 0052specialize beta_horner_coefficient_blend_value_derivative x3
  53. 0053specialize beta_horner_coefficient_blend_value_derivative x4
  54. 0054specialize beta_horner_coefficient_blend_value_derivative x5
  55. 0055apply beta_horner_coefficient_blend_value_derivative
  56. 0056exact hblend
  57. 0057exact hP_witness_witness
  58. 0058exact hN_witness_witness
  59. 0059exact hG_witness_witness
  60. 0060cases hlinear
  61. 0061have hiff : (ModEq(m,x4,0) → ModEq(m,x,x2)) ∧ (ModEq(m,x,x2) → ModEq(m,x4,0))
  62. 0062specialize hensel_signed_blend_zero_iff m
  63. 0063specialize hensel_signed_blend_zero_iff M
  64. 0064specialize hensel_signed_blend_zero_iff h
  65. 0065specialize hensel_signed_blend_zero_iff x
  66. 0066specialize hensel_signed_blend_zero_iff x2
  67. 0067specialize hensel_signed_blend_zero_iff x4
  68. 0068apply hensel_signed_blend_zero_iff
  69. 0069exact hM
  70. 0070exact hdiv
  71. 0071exact hlinear_left
  72. 0072cases hiff
  73. 0073split
  74. 0074intro hnatural
  75. 0075cases hnatural
  76. 0076cases hnatural_witness
  77. 0077have hvalue : x4 = x6
  78. 0078specialize beta_horner_eval_functional gb
  79. 0079specialize beta_horner_eval_functional gc
  80. 0080specialize beta_horner_eval_functional a
  81. 0081specialize beta_horner_eval_functional l
  82. 0082specialize beta_horner_eval_functional x4
  83. 0083specialize beta_horner_eval_functional x6
  84. 0084apply beta_horner_eval_functional
  85. 0085specialize beta_horner_derivative_value_projection gb
  86. 0086specialize beta_horner_derivative_value_projection gc
  87. 0087specialize beta_horner_derivative_value_projection a
  88. 0088specialize beta_horner_derivative_value_projection l
  89. 0089specialize beta_horner_derivative_value_projection x4
  90. 0090specialize beta_horner_derivative_value_projection x5
  91. 0091apply beta_horner_derivative_value_projection
  92. 0092exact hG_witness_witness
  93. 0093exact hnatural_witness_left
  94. 0094exists x
  95. 0095exists x2
  96. 0096split
  97. 0097specialize beta_horner_derivative_value_projection pb
  98. 0098specialize beta_horner_derivative_value_projection pc
  99. 0099specialize beta_horner_derivative_value_projection a
  100. 0100specialize beta_horner_derivative_value_projection l
  101. 0101specialize beta_horner_derivative_value_projection x
  102. 0102specialize beta_horner_derivative_value_projection x1
  103. 0103apply beta_horner_derivative_value_projection
  104. 0104exact hP_witness_witness
  105. 0105split
  106. 0106specialize beta_horner_derivative_value_projection nb
  107. 0107specialize beta_horner_derivative_value_projection nc
  108. 0108specialize beta_horner_derivative_value_projection a
  109. 0109specialize beta_horner_derivative_value_projection l
  110. 0110specialize beta_horner_derivative_value_projection x2
  111. 0111specialize beta_horner_derivative_value_projection x3
  112. 0112apply beta_horner_derivative_value_projection
  113. 0113exact hN_witness_witness
  114. 0114apply hiff_left
  115. 0115rewrite hvalue
  116. 0116exact hnatural_witness_right
  117. 0117intro hsigned
  118. 0118cases hsigned
  119. 0119cases hsigned_witness
  120. 0120cases hsigned_witness_witness
  121. 0121cases hsigned_witness_witness_right
  122. 0122have hpositive : x = x6
  123. 0123specialize beta_horner_eval_functional pb
  124. 0124specialize beta_horner_eval_functional pc
  125. 0125specialize beta_horner_eval_functional a
  126. 0126specialize beta_horner_eval_functional l
  127. 0127specialize beta_horner_eval_functional x
  128. 0128specialize beta_horner_eval_functional x6
  129. 0129apply beta_horner_eval_functional
  130. 0130specialize beta_horner_derivative_value_projection pb
  131. 0131specialize beta_horner_derivative_value_projection pc
  132. 0132specialize beta_horner_derivative_value_projection a
  133. 0133specialize beta_horner_derivative_value_projection l
  134. 0134specialize beta_horner_derivative_value_projection x
  135. 0135specialize beta_horner_derivative_value_projection x1
  136. 0136apply beta_horner_derivative_value_projection
  137. 0137exact hP_witness_witness
  138. 0138exact hsigned_witness_witness_left
  139. 0139have hnegative : x2 = x7
  140. 0140specialize beta_horner_eval_functional nb
  141. 0141specialize beta_horner_eval_functional nc
  142. 0142specialize beta_horner_eval_functional a
  143. 0143specialize beta_horner_eval_functional l
  144. 0144specialize beta_horner_eval_functional x2
  145. 0145specialize beta_horner_eval_functional x7
  146. 0146apply beta_horner_eval_functional
  147. 0147specialize beta_horner_derivative_value_projection nb
  148. 0148specialize beta_horner_derivative_value_projection nc
  149. 0149specialize beta_horner_derivative_value_projection a
  150. 0150specialize beta_horner_derivative_value_projection l
  151. 0151specialize beta_horner_derivative_value_projection x2
  152. 0152specialize beta_horner_derivative_value_projection x3
  153. 0153apply beta_horner_derivative_value_projection
  154. 0154exact hN_witness_witness
  155. 0155exact hsigned_witness_witness_right_left
  156. 0156exists x4
  157. 0157split
  158. 0158specialize beta_horner_derivative_value_projection gb
  159. 0159specialize beta_horner_derivative_value_projection gc
  160. 0160specialize beta_horner_derivative_value_projection a
  161. 0161specialize beta_horner_derivative_value_projection l
  162. 0162specialize beta_horner_derivative_value_projection x4
  163. 0163specialize beta_horner_derivative_value_projection x5
  164. 0164apply beta_horner_derivative_value_projection
  165. 0165exact hG_witness_witness
  166. 0166apply hiff_right
  167. 0167rewrite hpositive
  168. 0168rewrite hnegative
  169. 0169exact hsigned_witness_witness_right_right