HL001F

beta_signed_horner_hensel_iterated_exists_unique

Every arbitrary integer-coefficient simple root has unique canonical lifts through any finite number of prime-power steps; both existence and all-root uniqueness transport from an actually constructed natural polynomial.

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. ∀ j. ∀ q. ¬p = 0 → ¬m = 0 → m = p · s → SignedHornerValueDerivative(pb,pc,nb,nc,a,l,vp,dp,vn,dn) → ModEq(m,vp,vn) → SignedDerivativeUnit(p,dp,dn) → Pow(p,j,q) → ∃ x. CanonicalSignedHornerLift(pb,pc,nb,nc,l,m,a,m · q,x) ∧ (∀ y. CanonicalSignedHornerLift(pb,pc,nb,nc,l,m,a,m · q,y) → y = x)

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

Definition DAG

HornerDerivative(b,c,t,l,n,z) · 1HornerRootModulo(b,c,a,l,m) · 2CanonicalHornerLift(b,c,l,m,a,M,r) · 4HornerCoefficientBlend(pb,pc,nb,nc,gb,gc,h,l) · 1SignedHornerValueDerivative(pb,pc,nb,nc,a,l,vp,dp,vn,dn) · 1SignedDerivativeUnit(p,dp,dn) · 1SignedHornerRoot(pb,pc,nb,nc,a,l,m) · 2CanonicalSignedHornerLift(pb,pc,nb,nc,l,m,a,M,r) · 2Coprime(a,b) · 1ModEq(m,a,b) · 6Pow(a,e,z) · 2

Actual proof prerequisites

pow_nonzero_of_one_le · checked external prerequisiteone_le_of_ne_zero · checked external prerequisitemul_ne_zero · checked external prerequisitenonzero_is_succ · checked external prerequisitemul_assoc · checked external prerequisitemul_one · checked external prerequisitebeta_horner_coefficient_blend_existsbeta_horner_derivative_value_exists · checked external prerequisitebeta_horner_coefficient_blend_value_derivativehensel_signed_blend_zero_iffhensel_signed_blend_unit_coprimebeta_horner_hensel_iterated_exists_uniquebeta_signed_horner_blend_root_equivalence
Original expanded first-order statement 
forall pb pc nb nc a l vp dp vn dn m p s j q. ~(p = 0) -> ~(m = 0) -> m = p * s -> (((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 hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. vp + m * hgcrt_mod_left_hpl_mod = vn + m * hgcrt_mod_right_hpl_mod) -> (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))) -> (exists pa_b_hpl_power pa_c_hpl_power. ((forall pa_i_hpl_power_repeat. (exists pa_lt_hpl_power_repeat_bound. pa_lt_hpl_power_repeat_bound + S pa_i_hpl_power_repeat = j) -> (((exists pa_h_hpl_power_repeat_decoded. pa_h_hpl_power_repeat_decoded + S (p) = S ((S (pa_i_hpl_power_repeat)) * pa_c_hpl_power)) /\ exists pa_q_hpl_power_repeat_decoded. pa_b_hpl_power = pa_q_hpl_power_repeat_decoded * S ((S (pa_i_hpl_power_repeat)) * pa_c_hpl_power) + (p)))) /\ (exists pa_u_hpl_power_product pa_v_hpl_power_product. ((((exists pa_h_hpl_power_product_start. pa_h_hpl_power_product_start + S (1) = S ((S (0)) * pa_v_hpl_power_product)) /\ exists pa_q_hpl_power_product_start. pa_u_hpl_power_product = pa_q_hpl_power_product_start * S ((S (0)) * pa_v_hpl_power_product) + (1))) /\ ((((exists pa_h_hpl_power_product_terminal. pa_h_hpl_power_product_terminal + S (q) = S ((S (j)) * pa_v_hpl_power_product)) /\ exists pa_q_hpl_power_product_terminal. pa_u_hpl_power_product = pa_q_hpl_power_product_terminal * S ((S (j)) * pa_v_hpl_power_product) + (q))) /\ forall pa_i_hpl_power_product. (exists pa_lt_hpl_power_product_bound. pa_lt_hpl_power_product_bound + S pa_i_hpl_power_product = j) -> exists pa_p_hpl_power_product pa_r_hpl_power_product pa_s_hpl_power_product. ((((exists pa_h_hpl_power_product_factor. pa_h_hpl_power_product_factor + S (pa_p_hpl_power_product) = S ((S (pa_i_hpl_power_product)) * pa_c_hpl_power)) /\ exists pa_q_hpl_power_product_factor. pa_b_hpl_power = pa_q_hpl_power_product_factor * S ((S (pa_i_hpl_power_product)) * pa_c_hpl_power) + (pa_p_hpl_power_product))) /\ ((((exists pa_h_hpl_power_product_partial. pa_h_hpl_power_product_partial + S (pa_r_hpl_power_product) = S ((S (pa_i_hpl_power_product)) * pa_v_hpl_power_product)) /\ exists pa_q_hpl_power_product_partial. pa_u_hpl_power_product = pa_q_hpl_power_product_partial * S ((S (pa_i_hpl_power_product)) * pa_v_hpl_power_product) + (pa_r_hpl_power_product))) /\ ((((exists pa_h_hpl_power_product_successor. pa_h_hpl_power_product_successor + S (pa_s_hpl_power_product) = S ((S (S pa_i_hpl_power_product)) * pa_v_hpl_power_product)) /\ exists pa_q_hpl_power_product_successor. pa_u_hpl_power_product = pa_q_hpl_power_product_successor * S ((S (S pa_i_hpl_power_product)) * pa_v_hpl_power_product) + (pa_s_hpl_power_product))) /\ pa_s_hpl_power_product = pa_r_hpl_power_product * pa_p_hpl_power_product)))))))) -> exists r. ((((exists hpl_gap_lift. hpl_gap_lift + S (r) = (m * q)) /\ ((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 * q) * hgcrt_mod_left_hpl_lift = sph_negative_lift + (m * q) * hgcrt_mod_right_hpl_lift))))))) /\ forall z. (((exists hpl_gap_lift. hpl_gap_lift + S (z) = (m * q)) /\ ((exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. z + 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 * z + 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 * z + ff_coefficient_ph_hpl_sph_lift_negative_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. sph_positive_lift + (m * q) * hgcrt_mod_left_hpl_lift = sph_negative_lift + (m * q) * hgcrt_mod_right_hpl_lift))))))) -> z = r)

Complete tactic proof in conservative notation

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

186 script commands · 53 reading checkpoints · 12 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 (6)
beta horner coefficient blend existsbeta horner coefficient blend value derivativehensel signed blend zero iffhensel signed blend unit coprimebeta horner hensel iterated exists uniquebeta signed horner blend root equivalence
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–20

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 j
  5. L15
    intro q
  6. L16
    intro hp
  7. L17
    intro hm
  8. L18
    intro hfactor
  9. L19
    intro hpair
  10. L20
    intro hroot
03Fix variables and assumptionsL21–22

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

  1. L21
    intro hunit
  2. L22
    intro hpower
04Separate the logical casesL23–23

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

  1. L23
    cases hpair
05Establish hqL24–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow nonzero of one le.

  1. L24
    have hq : ~(q = 0)
  2. L25
    intro hzero
  3. L26
    specialize pow_nonzero_of_one_le p
  4. L27
    specialize pow_nonzero_of_one_le j
  5. L28
    specialize pow_nonzero_of_one_le q
  6. L29
    apply pow_nonzero_of_one_le
  7. L30
    specialize one_le_of_ne_zero p
  8. L31
    apply one_le_of_ne_zero
  9. L32
    exact hp
  10. L33
    exact hpower
06Use earlier factsL34–34

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

  1. L34
    exact hzero
07Establish hnonzeroL35–42

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

  1. L35
    have hnonzero : ~(m * q = 0)
  2. L36
    intro hzero
  3. L37
    specialize mul_ne_zero m
  4. L38
    specialize mul_ne_zero q
  5. L39
    apply mul_ne_zero
  6. L40
    exact hm
  7. L41
    exact hq
  8. L42
    exact hzero
08Establish hmodulusL43–46

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

  1. L43
    have hmodulus : exists h. m * q = S h
  2. L44
    specialize nonzero_is_succ (m * q)
  3. L45
    apply nonzero_is_succ
  4. L46
    exact hnonzero
09Separate the logical casesL47–47

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

  1. L47
    cases hmodulus
10Establish hrecodedL48–55

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

  1. L48
    have hrecoded : ∃ gb. ∃ gc. HornerCoefficientBlend(pb,pc,nb,nc,gb,gc,x,l)Definitions: HornerCoefficientBlend(pb,pc,nb,nc,gb,gc,x,l)Original native command in the exact edition
  2. L49
    specialize beta_horner_coefficient_blend_exists pb
  3. L50
    specialize beta_horner_coefficient_blend_exists pc
  4. L51
    specialize beta_horner_coefficient_blend_exists nb
  5. L52
    specialize beta_horner_coefficient_blend_exists nc
  6. L53
    specialize beta_horner_coefficient_blend_exists x
  7. L54
    specialize beta_horner_coefficient_blend_exists l
  8. L55
    apply beta_horner_coefficient_blend_exists
11Separate the logical casesL56–57

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

  1. L56
    cases hrecoded
  2. L57
    cases hrecoded_witness
12Establish hGL58–63

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

  1. L58
    have hG : ∃ v. ∃ d. HornerDerivative(x1,x2,a,l,v,d)Definitions: HornerDerivative(x1,x2,a,l,v,d)Original native command in the exact edition
  2. L59
    specialize beta_horner_derivative_value_exists x1
  3. L60
    specialize beta_horner_derivative_value_exists x2
  4. L61
    specialize beta_horner_derivative_value_exists a
  5. L62
    specialize beta_horner_derivative_value_exists l
  6. L63
    apply beta_horner_derivative_value_exists
13Separate the logical casesL64–65

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

  1. L64
    cases hG
  2. L65
    cases hG_witness
14Establish hlinearL66–75

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

  1. L66
    have hlinear : x3 = vp + x * vn /\ x4 = dp + x * dn
  2. L67
    specialize beta_horner_coefficient_blend_value_derivative pb
  3. L68
    specialize beta_horner_coefficient_blend_value_derivative pc
  4. L69
    specialize beta_horner_coefficient_blend_value_derivative nb
  5. L70
    specialize beta_horner_coefficient_blend_value_derivative nc
  6. L71
    specialize beta_horner_coefficient_blend_value_derivative x1
  7. L72
    specialize beta_horner_coefficient_blend_value_derivative x2
  8. L73
    specialize beta_horner_coefficient_blend_value_derivative x
  9. L74
    specialize beta_horner_coefficient_blend_value_derivative a
  10. L75
    specialize beta_horner_coefficient_blend_value_derivative l
15Use earlier factsL76–85

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

  1. L76
    specialize beta_horner_coefficient_blend_value_derivative vp
  2. L77
    specialize beta_horner_coefficient_blend_value_derivative dp
  3. L78
    specialize beta_horner_coefficient_blend_value_derivative vn
  4. L79
    specialize beta_horner_coefficient_blend_value_derivative dn
  5. L80
    specialize beta_horner_coefficient_blend_value_derivative x3
  6. L81
    specialize beta_horner_coefficient_blend_value_derivative x4
  7. L82
    apply beta_horner_coefficient_blend_value_derivative
  8. L83
    exact hrecoded_witness_witness
  9. L84
    exact hpair_left
  10. L85
    exact hpair_right
16Use earlier factsL86–86

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

  1. L86
    exact hG_witness_witness
17Separate the logical casesL87–87

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

  1. L87
    cases hlinear
18Establish hrootGL88–88

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

  1. L88
    have hrootG : ModEq(m,x3,0)Definitions: ModEq(m,x3,0)Original native command in the exact edition
19Establish hiffL89–97

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

  1. L89
    have hiff : (ModEq(m,x3,0) → ModEq(m,vp,vn)) ∧ (ModEq(m,vp,vn) → ModEq(m,x3,0))Definitions: ModEq(m,x3,0)ModEq(m,vp,vn)Original native command in the exact edition
  2. L90
    specialize hensel_signed_blend_zero_iff m
  3. L91
    specialize hensel_signed_blend_zero_iff (m * q)
  4. L92
    specialize hensel_signed_blend_zero_iff x
  5. L93
    specialize hensel_signed_blend_zero_iff vp
  6. L94
    specialize hensel_signed_blend_zero_iff vn
  7. L95
    specialize hensel_signed_blend_zero_iff x3
  8. L96
    apply hensel_signed_blend_zero_iff
  9. L97
    exact hmodulus_witness
20Construct an explicit witnessL98–98

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

  1. L98
    exists q
21Calculate and transport equalitiesL99–99

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

  1. L99
    refl
22Use earlier factsL100–100

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

  1. L100
    exact hlinear_left
23Separate the logical casesL101–101

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

  1. L101
    cases hiff
24Use earlier factsL102–103

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

  1. L102
    apply hiff_right
  2. L103
    exact hroot
25Establish hcopGL104–112

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

  1. L104
    have hcopG : Coprime(x4,p)Definitions: Coprime(x4,p)Original native command in the exact edition
  2. L105
    specialize hensel_signed_blend_unit_coprime p
  3. L106
    specialize hensel_signed_blend_unit_coprime (m * q)
  4. L107
    specialize hensel_signed_blend_unit_coprime x
  5. L108
    specialize hensel_signed_blend_unit_coprime dp
  6. L109
    specialize hensel_signed_blend_unit_coprime dn
  7. L110
    specialize hensel_signed_blend_unit_coprime x4
  8. L111
    apply hensel_signed_blend_unit_coprime
  9. L112
    exact hmodulus_witness
26Construct an explicit witnessL113–113

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

  1. L113
    exists s * q
27Calculate and transport equalitiesL114–114

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

  1. L114
    rewrite hfactor
28Use earlier factsL115–117

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

  1. L115
    apply mul_assoc
  2. L116
    exact hlinear_right
  3. L117
    exact hunit
29Establish hiterationL118–127

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

  1. L118
    have hiteration : ∀ e. ∀ Q. Pow(p,e,Q) → ∃ x. CanonicalHornerLift(x1,x2,l,m,a,m · Q,x) ∧ (∀ y. CanonicalHornerLift(x1,x2,l,m,a,m · Q,y) → y = x)Definitions: Pow(p,e,Q)CanonicalHornerLift(x1,x2,l,m,a,m · Q,x)CanonicalHornerLift(x1,x2,l,m,a,m · Q,y)Original native command in the exact edition
  2. L119
    specialize beta_horner_hensel_iterated_exists_unique x1
  3. L120
    specialize beta_horner_hensel_iterated_exists_unique x2
  4. L121
    specialize beta_horner_hensel_iterated_exists_unique a
  5. L122
    specialize beta_horner_hensel_iterated_exists_unique l
  6. L123
    specialize beta_horner_hensel_iterated_exists_unique x3
  7. L124
    specialize beta_horner_hensel_iterated_exists_unique x4
  8. L125
    specialize beta_horner_hensel_iterated_exists_unique m
  9. L126
    specialize beta_horner_hensel_iterated_exists_unique p
  10. L127
    specialize beta_horner_hensel_iterated_exists_unique s
30Use earlier factsL128–134

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

  1. L128
    apply beta_horner_hensel_iterated_exists_unique
  2. L129
    exact hp
  3. L130
    exact hm
  4. L131
    exact hG_witness_witness
  5. L132
    exact hfactor
  6. L133
    exact hrootG
  7. L134
    exact hcopG
31Establish hresultL135–139

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

  1. L135
    have hresult : ∃ r. CanonicalHornerLift(x1,x2,l,m,a,m · q,r) ∧ (∀ x. CanonicalHornerLift(x1,x2,l,m,a,m · q,x) → x = r)Definitions: CanonicalHornerLift(x1,x2,l,m,a,m · q,r)CanonicalHornerLift(x1,x2,l,m,a,m · q,x)Original native command in the exact edition
  2. L136
    specialize hiteration j
  3. L137
    specialize hiteration q
  4. L138
    apply hiteration
  5. L139
    exact hpower
32Establish hequivalenceL140–149

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

  1. L140
    have hequivalence : ∀ t. (HornerRootModulo(x1,x2,t,l,m · q) → SignedHornerRoot(pb,pc,nb,nc,t,l,m · q)) ∧ (SignedHornerRoot(pb,pc,nb,nc,t,l,m · q) → HornerRootModulo(x1,x2,t,l,m · q))Definitions: HornerRootModulo(x1,x2,t,l,m · q)SignedHornerRoot(pb,pc,nb,nc,t,l,m · q)Original native command in the exact edition
  2. L141
    intro t
  3. L142
    specialize beta_signed_horner_blend_root_equivalence pb
  4. L143
    specialize beta_signed_horner_blend_root_equivalence pc
  5. L144
    specialize beta_signed_horner_blend_root_equivalence nb
  6. L145
    specialize beta_signed_horner_blend_root_equivalence nc
  7. L146
    specialize beta_signed_horner_blend_root_equivalence x1
  8. L147
    specialize beta_signed_horner_blend_root_equivalence x2
  9. L148
    specialize beta_signed_horner_blend_root_equivalence x
  10. L149
    specialize beta_signed_horner_blend_root_equivalence t
33Use earlier factsL150–154

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

  1. L150
    specialize beta_signed_horner_blend_root_equivalence l
  2. L151
    specialize beta_signed_horner_blend_root_equivalence (m * q)
  3. L152
    specialize beta_signed_horner_blend_root_equivalence (m * q)
  4. L153
    apply beta_signed_horner_blend_root_equivalence
  5. L154
    exact hmodulus_witness
34Construct an explicit witnessL155–155

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

  1. L155
    exists 1
35Calculate and transport equalitiesL156–156

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

  1. L156
    symm
36Use earlier factsL157–158

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

  1. L157
    apply mul_one
  2. L158
    exact hrecoded_witness_witness
37Separate the logical casesL159–162

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

  1. L159
    cases hresult
  2. L160
    cases hresult_witness
  3. L161
    cases hresult_witness_left
  4. L162
    cases hresult_witness_left_right
38Construct an explicit witnessL163–163

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

  1. L163
    exists x5
39Separate the logical casesL164–165

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

  1. L164
    split
  2. L165
    split
40Use earlier factsL166–166

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

  1. L166
    exact hresult_witness_left_left
41Separate the logical casesL167–167

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

  1. L167
    split
42Use earlier factsL168–169

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

  1. L168
    exact hresult_witness_left_right_left
  2. L169
    specialize hequivalence x5
43Separate the logical casesL170–170

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

  1. L170
    cases hequivalence
44Use earlier factsL171–172

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

  1. L171
    apply hequivalence_left
  2. L172
    exact hresult_witness_left_right_right
45Fix variables and assumptionsL173–174

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

  1. L173
    intro z
  2. L174
    intro hz
46Separate the logical casesL175–176

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

  1. L175
    cases hz
  2. L176
    cases hz_right
47Use earlier factsL177–178

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

  1. L177
    specialize hresult_witness_right z
  2. L178
    apply hresult_witness_right
48Separate the logical casesL179–179

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

  1. L179
    split
49Use earlier factsL180–180

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

  1. L180
    exact hz_left
50Separate the logical casesL181–181

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

  1. L181
    split
51Use earlier factsL182–183

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

  1. L182
    exact hz_right_left
  2. L183
    specialize hequivalence z
52Separate the logical casesL184–184

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

  1. L184
    cases hequivalence
53Use earlier factsL185–186

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

  1. L185
    apply hequivalence_right
  2. L186
    exact hz_right_right

Library-wide reading audit

Original defined command ledger · 186 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 j
  15. 0015intro q
  16. 0016intro hp
  17. 0017intro hm
  18. 0018intro hfactor
  19. 0019intro hpair
  20. 0020intro hroot
  21. 0021intro hunit
  22. 0022intro hpower
  23. 0023cases hpair
  24. 0024have hq : ~(q = 0)
  25. 0025intro hzero
  26. 0026specialize pow_nonzero_of_one_le p
  27. 0027specialize pow_nonzero_of_one_le j
  28. 0028specialize pow_nonzero_of_one_le q
  29. 0029apply pow_nonzero_of_one_le
  30. 0030specialize one_le_of_ne_zero p
  31. 0031apply one_le_of_ne_zero
  32. 0032exact hp
  33. 0033exact hpower
  34. 0034exact hzero
  35. 0035have hnonzero : ~(m * q = 0)
  36. 0036intro hzero
  37. 0037specialize mul_ne_zero m
  38. 0038specialize mul_ne_zero q
  39. 0039apply mul_ne_zero
  40. 0040exact hm
  41. 0041exact hq
  42. 0042exact hzero
  43. 0043have hmodulus : exists h. m * q = S h
  44. 0044specialize nonzero_is_succ (m * q)
  45. 0045apply nonzero_is_succ
  46. 0046exact hnonzero
  47. 0047cases hmodulus
  48. 0048have hrecoded : ∃ gb. ∃ gc. HornerCoefficientBlend(pb,pc,nb,nc,gb,gc,x,l)
  49. 0049specialize beta_horner_coefficient_blend_exists pb
  50. 0050specialize beta_horner_coefficient_blend_exists pc
  51. 0051specialize beta_horner_coefficient_blend_exists nb
  52. 0052specialize beta_horner_coefficient_blend_exists nc
  53. 0053specialize beta_horner_coefficient_blend_exists x
  54. 0054specialize beta_horner_coefficient_blend_exists l
  55. 0055apply beta_horner_coefficient_blend_exists
  56. 0056cases hrecoded
  57. 0057cases hrecoded_witness
  58. 0058have hG : ∃ v. ∃ d. HornerDerivative(x1,x2,a,l,v,d)
  59. 0059specialize beta_horner_derivative_value_exists x1
  60. 0060specialize beta_horner_derivative_value_exists x2
  61. 0061specialize beta_horner_derivative_value_exists a
  62. 0062specialize beta_horner_derivative_value_exists l
  63. 0063apply beta_horner_derivative_value_exists
  64. 0064cases hG
  65. 0065cases hG_witness
  66. 0066have hlinear : x3 = vp + x * vn /\ x4 = dp + x * dn
  67. 0067specialize beta_horner_coefficient_blend_value_derivative pb
  68. 0068specialize beta_horner_coefficient_blend_value_derivative pc
  69. 0069specialize beta_horner_coefficient_blend_value_derivative nb
  70. 0070specialize beta_horner_coefficient_blend_value_derivative nc
  71. 0071specialize beta_horner_coefficient_blend_value_derivative x1
  72. 0072specialize beta_horner_coefficient_blend_value_derivative x2
  73. 0073specialize beta_horner_coefficient_blend_value_derivative x
  74. 0074specialize beta_horner_coefficient_blend_value_derivative a
  75. 0075specialize beta_horner_coefficient_blend_value_derivative l
  76. 0076specialize beta_horner_coefficient_blend_value_derivative vp
  77. 0077specialize beta_horner_coefficient_blend_value_derivative dp
  78. 0078specialize beta_horner_coefficient_blend_value_derivative vn
  79. 0079specialize beta_horner_coefficient_blend_value_derivative dn
  80. 0080specialize beta_horner_coefficient_blend_value_derivative x3
  81. 0081specialize beta_horner_coefficient_blend_value_derivative x4
  82. 0082apply beta_horner_coefficient_blend_value_derivative
  83. 0083exact hrecoded_witness_witness
  84. 0084exact hpair_left
  85. 0085exact hpair_right
  86. 0086exact hG_witness_witness
  87. 0087cases hlinear
  88. 0088have hrootG : ModEq(m,x3,0)
  89. 0089have hiff : (ModEq(m,x3,0) → ModEq(m,vp,vn)) ∧ (ModEq(m,vp,vn) → ModEq(m,x3,0))
  90. 0090specialize hensel_signed_blend_zero_iff m
  91. 0091specialize hensel_signed_blend_zero_iff (m * q)
  92. 0092specialize hensel_signed_blend_zero_iff x
  93. 0093specialize hensel_signed_blend_zero_iff vp
  94. 0094specialize hensel_signed_blend_zero_iff vn
  95. 0095specialize hensel_signed_blend_zero_iff x3
  96. 0096apply hensel_signed_blend_zero_iff
  97. 0097exact hmodulus_witness
  98. 0098exists q
  99. 0099refl
  100. 0100exact hlinear_left
  101. 0101cases hiff
  102. 0102apply hiff_right
  103. 0103exact hroot
  104. 0104have hcopG : Coprime(x4,p)
  105. 0105specialize hensel_signed_blend_unit_coprime p
  106. 0106specialize hensel_signed_blend_unit_coprime (m * q)
  107. 0107specialize hensel_signed_blend_unit_coprime x
  108. 0108specialize hensel_signed_blend_unit_coprime dp
  109. 0109specialize hensel_signed_blend_unit_coprime dn
  110. 0110specialize hensel_signed_blend_unit_coprime x4
  111. 0111apply hensel_signed_blend_unit_coprime
  112. 0112exact hmodulus_witness
  113. 0113exists s * q
  114. 0114rewrite hfactor
  115. 0115apply mul_assoc
  116. 0116exact hlinear_right
  117. 0117exact hunit
  118. 0118have hiteration : ∀ e. ∀ Q. Pow(p,e,Q) → ∃ x. CanonicalHornerLift(x1,x2,l,m,a,m · Q,x) ∧ (∀ y. CanonicalHornerLift(x1,x2,l,m,a,m · Q,y) → y = x)
  119. 0119specialize beta_horner_hensel_iterated_exists_unique x1
  120. 0120specialize beta_horner_hensel_iterated_exists_unique x2
  121. 0121specialize beta_horner_hensel_iterated_exists_unique a
  122. 0122specialize beta_horner_hensel_iterated_exists_unique l
  123. 0123specialize beta_horner_hensel_iterated_exists_unique x3
  124. 0124specialize beta_horner_hensel_iterated_exists_unique x4
  125. 0125specialize beta_horner_hensel_iterated_exists_unique m
  126. 0126specialize beta_horner_hensel_iterated_exists_unique p
  127. 0127specialize beta_horner_hensel_iterated_exists_unique s
  128. 0128apply beta_horner_hensel_iterated_exists_unique
  129. 0129exact hp
  130. 0130exact hm
  131. 0131exact hG_witness_witness
  132. 0132exact hfactor
  133. 0133exact hrootG
  134. 0134exact hcopG
  135. 0135have hresult : ∃ r. CanonicalHornerLift(x1,x2,l,m,a,m · q,r) ∧ (∀ x. CanonicalHornerLift(x1,x2,l,m,a,m · q,x) → x = r)
  136. 0136specialize hiteration j
  137. 0137specialize hiteration q
  138. 0138apply hiteration
  139. 0139exact hpower
  140. 0140have hequivalence : ∀ t. (HornerRootModulo(x1,x2,t,l,m · q) → SignedHornerRoot(pb,pc,nb,nc,t,l,m · q)) ∧ (SignedHornerRoot(pb,pc,nb,nc,t,l,m · q) → HornerRootModulo(x1,x2,t,l,m · q))
  141. 0141intro t
  142. 0142specialize beta_signed_horner_blend_root_equivalence pb
  143. 0143specialize beta_signed_horner_blend_root_equivalence pc
  144. 0144specialize beta_signed_horner_blend_root_equivalence nb
  145. 0145specialize beta_signed_horner_blend_root_equivalence nc
  146. 0146specialize beta_signed_horner_blend_root_equivalence x1
  147. 0147specialize beta_signed_horner_blend_root_equivalence x2
  148. 0148specialize beta_signed_horner_blend_root_equivalence x
  149. 0149specialize beta_signed_horner_blend_root_equivalence t
  150. 0150specialize beta_signed_horner_blend_root_equivalence l
  151. 0151specialize beta_signed_horner_blend_root_equivalence (m * q)
  152. 0152specialize beta_signed_horner_blend_root_equivalence (m * q)
  153. 0153apply beta_signed_horner_blend_root_equivalence
  154. 0154exact hmodulus_witness
  155. 0155exists 1
  156. 0156symm
  157. 0157apply mul_one
  158. 0158exact hrecoded_witness_witness
  159. 0159cases hresult
  160. 0160cases hresult_witness
  161. 0161cases hresult_witness_left
  162. 0162cases hresult_witness_left_right
  163. 0163exists x5
  164. 0164split
  165. 0165split
  166. 0166exact hresult_witness_left_left
  167. 0167split
  168. 0168exact hresult_witness_left_right_left
  169. 0169specialize hequivalence x5
  170. 0170cases hequivalence
  171. 0171apply hequivalence_left
  172. 0172exact hresult_witness_left_right_right
  173. 0173intro z
  174. 0174intro hz
  175. 0175cases hz
  176. 0176cases hz_right
  177. 0177specialize hresult_witness_right z
  178. 0178apply hresult_witness_right
  179. 0179split
  180. 0180exact hz_left
  181. 0181split
  182. 0182exact hz_right_left
  183. 0183specialize hequivalence z
  184. 0184cases hequivalence
  185. 0185apply hequivalence_right
  186. 0186exact hz_right_right