HL0010

beta_horner_prime_power_hensel_lift_exists_unique

A positive prime-power-level simple root at an unrestricted input has a unique canonical lift and an actual next-power witness; the theorem even permits every nonzero base.

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

∀ b. ∀ c. ∀ a. ∀ l. ∀ n. ∀ d. ∀ p. ∀ k. ∀ m. ¬p = 0 → ¬k = 0 → Pow(p,k,m) → HornerDerivative(b,c,a,l,n,d) → ModEq(m,n,0) → Coprime(d,p) → ∃ x. Pow(p,S k,x) ∧ (∃ y. CanonicalHornerLift(b,c,l,m,a,x,y) ∧ (∀ z. CanonicalHornerLift(b,c,l,m,a,x,z) → z = y))

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

Definition DAG

HornerDerivative(b,c,t,l,n,z) · 1CanonicalHornerLift(b,c,l,m,a,M,r) · 2Dvd(d,n) · 1Coprime(a,b) · 1ModEq(m,a,b) · 1Pow(a,e,z) · 2

Actual proof prerequisites

hensel_positive_power_factorpow_successor_compose · checked external prerequisitemul_comm · checked external prerequisitebeta_horner_simple_root_hensel_lift_exists_unique
Original expanded first-order statement 
forall b c a l n d p k m. ~(p = 0) -> ~(k = 0) -> (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 = k) -> (((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 (m) = S ((S (k)) * 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 (k)) * pa_v_hpl_power_product) + (m))) /\ 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 = k) -> 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 ff_u_hd_hpl_pair ff_v_hd_hpl_pair ff_d_hd_hpl_pair ff_e_hd_hpl_pair. ((((((exists fs_h_ph_hd_hpl_pair_body_value_start. fs_h_ph_hd_hpl_pair_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_start. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_start * S ((S (0)) * ff_v_hd_hpl_pair) + (0))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_terminal. fs_h_ph_hd_hpl_pair_body_value_terminal + S (n) = S ((S (l)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_terminal. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_pair) + (n))) /\ forall ff_i_ph_hd_hpl_pair_body_value_steps. (exists ph_bound_hd_hpl_pair_body_value_steps. ph_bound_hd_hpl_pair_body_value_steps + S ff_i_ph_hd_hpl_pair_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_pair_body_value_steps ff_previous_ph_hd_hpl_pair_body_value_steps ff_current_ph_hd_hpl_pair_body_value_steps. ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_coefficient. fs_h_ph_hd_hpl_pair_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_pair_body_value_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * c)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_coefficient. b = fs_q_ph_hd_hpl_pair_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * c) + (ff_coefficient_ph_hd_hpl_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_before. fs_h_ph_hd_hpl_pair_body_value_steps_before + S (ff_previous_ph_hd_hpl_pair_body_value_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_before. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair) + (ff_previous_ph_hd_hpl_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_after. fs_h_ph_hd_hpl_pair_body_value_steps_after + S (ff_current_ph_hd_hpl_pair_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_after. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair) + (ff_current_ph_hd_hpl_pair_body_value_steps))) /\ ff_current_ph_hd_hpl_pair_body_value_steps = ff_previous_ph_hd_hpl_pair_body_value_steps * a + ff_coefficient_ph_hd_hpl_pair_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_pair_body_derivative_start. fs_h_ph_hd_hpl_pair_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_start. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_pair) + (0))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_terminal. fs_h_ph_hd_hpl_pair_body_derivative_terminal + S (d) = S ((S (l)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_terminal. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_pair) + (d))) /\ forall ff_i_ph_hd_hpl_pair_body_derivative_steps. (exists ph_bound_hd_hpl_pair_body_derivative_steps. ph_bound_hd_hpl_pair_body_derivative_steps + S ff_i_ph_hd_hpl_pair_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_pair_body_derivative_steps ff_previous_ph_hd_hpl_pair_body_derivative_steps ff_current_ph_hd_hpl_pair_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_pair_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_coefficient. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_v_hd_hpl_pair) + (ff_coefficient_ph_hd_hpl_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_before. fs_h_ph_hd_hpl_pair_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_before. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair) + (ff_previous_ph_hd_hpl_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_after. fs_h_ph_hd_hpl_pair_body_derivative_steps_after + S (ff_current_ph_hd_hpl_pair_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_after. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair) + (ff_current_ph_hd_hpl_pair_body_derivative_steps))) /\ ff_current_ph_hd_hpl_pair_body_derivative_steps = ff_previous_ph_hd_hpl_pair_body_derivative_steps * a + ff_coefficient_ph_hd_hpl_pair_body_derivative_steps)))))))) -> (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. n + m * hgcrt_mod_left_hpl_mod = 0 + m * hgcrt_mod_right_hpl_mod) -> (forall hmi_divisor_hpl_coprime. (exists hmi_left_factor_hpl_coprime. d = hmi_divisor_hpl_coprime * hmi_left_factor_hpl_coprime) -> (exists hmi_right_factor_hpl_coprime. p = hmi_divisor_hpl_coprime * hmi_right_factor_hpl_coprime) -> hmi_divisor_hpl_coprime = 1) -> exists M. ((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 = S k) -> (((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 (M) = S ((S (S k)) * 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 (S k)) * pa_v_hpl_power_product) + (M))) /\ 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 = S k) -> 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)) /\ ((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 hpl_value_lift. ((exists ff_u_ph_hpl_lift ff_v_ph_hpl_lift. ((((exists fs_h_ph_hpl_lift_body_start. fs_h_ph_hpl_lift_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_start. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_start * S ((S (0)) * ff_v_ph_hpl_lift) + (0))) /\ ((((exists fs_h_ph_hpl_lift_body_terminal. fs_h_ph_hpl_lift_body_terminal + S (hpl_value_lift) = S ((S (l)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_terminal. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_terminal * S ((S (l)) * ff_v_ph_hpl_lift) + (hpl_value_lift))) /\ forall ff_i_ph_hpl_lift_body_steps. (exists ph_bound_hpl_lift_body_steps. ph_bound_hpl_lift_body_steps + S ff_i_ph_hpl_lift_body_steps = l) -> exists ff_coefficient_ph_hpl_lift_body_steps ff_previous_ph_hpl_lift_body_steps ff_current_ph_hpl_lift_body_steps. ((((exists fs_h_ph_hpl_lift_body_steps_coefficient. fs_h_ph_hpl_lift_body_steps_coefficient + S (ff_coefficient_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * c)) /\ exists fs_q_ph_hpl_lift_body_steps_coefficient. b = fs_q_ph_hpl_lift_body_steps_coefficient * S ((S (ff_i_ph_hpl_lift_body_steps)) * c) + (ff_coefficient_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_before. fs_h_ph_hpl_lift_body_steps_before + S (ff_previous_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_before. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_before * S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_previous_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_after. fs_h_ph_hpl_lift_body_steps_after + S (ff_current_ph_hpl_lift_body_steps) = S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_after. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_after * S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_current_ph_hpl_lift_body_steps))) /\ ff_current_ph_hpl_lift_body_steps = ff_previous_ph_hpl_lift_body_steps * r + ff_coefficient_ph_hpl_lift_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. hpl_value_lift + M * hgcrt_mod_left_hpl_lift = 0 + M * hgcrt_mod_right_hpl_lift)))))) /\ forall z. (((exists hpl_gap_lift. hpl_gap_lift + S (z) = (M)) /\ ((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 hpl_value_lift. ((exists ff_u_ph_hpl_lift ff_v_ph_hpl_lift. ((((exists fs_h_ph_hpl_lift_body_start. fs_h_ph_hpl_lift_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_start. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_start * S ((S (0)) * ff_v_ph_hpl_lift) + (0))) /\ ((((exists fs_h_ph_hpl_lift_body_terminal. fs_h_ph_hpl_lift_body_terminal + S (hpl_value_lift) = S ((S (l)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_terminal. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_terminal * S ((S (l)) * ff_v_ph_hpl_lift) + (hpl_value_lift))) /\ forall ff_i_ph_hpl_lift_body_steps. (exists ph_bound_hpl_lift_body_steps. ph_bound_hpl_lift_body_steps + S ff_i_ph_hpl_lift_body_steps = l) -> exists ff_coefficient_ph_hpl_lift_body_steps ff_previous_ph_hpl_lift_body_steps ff_current_ph_hpl_lift_body_steps. ((((exists fs_h_ph_hpl_lift_body_steps_coefficient. fs_h_ph_hpl_lift_body_steps_coefficient + S (ff_coefficient_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * c)) /\ exists fs_q_ph_hpl_lift_body_steps_coefficient. b = fs_q_ph_hpl_lift_body_steps_coefficient * S ((S (ff_i_ph_hpl_lift_body_steps)) * c) + (ff_coefficient_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_before. fs_h_ph_hpl_lift_body_steps_before + S (ff_previous_ph_hpl_lift_body_steps) = S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_before. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_before * S ((S (ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_previous_ph_hpl_lift_body_steps))) /\ ((((exists fs_h_ph_hpl_lift_body_steps_after. fs_h_ph_hpl_lift_body_steps_after + S (ff_current_ph_hpl_lift_body_steps) = S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift)) /\ exists fs_q_ph_hpl_lift_body_steps_after. ff_u_ph_hpl_lift = fs_q_ph_hpl_lift_body_steps_after * S ((S (S ff_i_ph_hpl_lift_body_steps)) * ff_v_ph_hpl_lift) + (ff_current_ph_hpl_lift_body_steps))) /\ ff_current_ph_hpl_lift_body_steps = ff_previous_ph_hpl_lift_body_steps * z + ff_coefficient_ph_hpl_lift_body_steps)))))) /\ (exists hgcrt_mod_left_hpl_lift hgcrt_mod_right_hpl_lift. hpl_value_lift + M * hgcrt_mod_left_hpl_lift = 0 + M * hgcrt_mod_right_hpl_lift)))))) -> z = r))

Complete tactic proof in conservative notation

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

50 script commands · 9 reading checkpoints · 1 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)
hensel positive power factorbeta horner simple root hensel lift exists unique
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro a
  4. L4
    intro l
  5. L5
    intro n
  6. L6
    intro d
  7. L7
    intro p
  8. L8
    intro k
  9. L9
    intro m
  10. L10
    intro hp
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hk
  2. L12
    intro hpower
  3. L13
    intro hpair
  4. L14
    intro hroot
  5. L15
    intro hcop
03Establish hfactorL16–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hensel positive power factor.

  1. L16
    have hfactor : ¬m = 0 ∧ Dvd(p,m)Definitions: Dvd(p,m)Original native command in the exact edition
  2. L17
    specialize hensel_positive_power_factor p
  3. L18
    specialize hensel_positive_power_factor k
  4. L19
    specialize hensel_positive_power_factor m
  5. L20
    apply hensel_positive_power_factor
  6. L21
    exact hp
  7. L22
    exact hk
  8. L23
    exact hpower
04Separate the logical casesL24–25

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

  1. L24
    cases hfactor
  2. L25
    cases hfactor_right
05Construct an explicit witnessL26–26

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

  1. L26
    exists p * m
06Separate the logical casesL27–27

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

  1. L27
    split
07Use earlier factsL28–37

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

  1. L28
    specialize pow_successor_compose p
  2. L29
    specialize pow_successor_compose k
  3. L30
    specialize pow_successor_compose m
  4. L31
    specialize pow_successor_compose (p * m)
  5. L32
    apply pow_successor_compose
  6. L33
    exact hpower
  7. L34
    apply mul_comm
  8. L35
    specialize beta_horner_simple_root_hensel_lift_exists_unique b
  9. L36
    specialize beta_horner_simple_root_hensel_lift_exists_unique c
  10. L37
    specialize beta_horner_simple_root_hensel_lift_exists_unique a
08Use earlier factsL38–47

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

  1. L38
    specialize beta_horner_simple_root_hensel_lift_exists_unique l
  2. L39
    specialize beta_horner_simple_root_hensel_lift_exists_unique n
  3. L40
    specialize beta_horner_simple_root_hensel_lift_exists_unique d
  4. L41
    specialize beta_horner_simple_root_hensel_lift_exists_unique m
  5. L42
    specialize beta_horner_simple_root_hensel_lift_exists_unique p
  6. L43
    specialize beta_horner_simple_root_hensel_lift_exists_unique x
  7. L44
    apply beta_horner_simple_root_hensel_lift_exists_unique
  8. L45
    exact hp
  9. L46
    exact hfactor_left
  10. L47
    exact hpair
09Use earlier factsL48–50

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

  1. L48
    exact hfactor_right_witness
  2. L49
    exact hroot
  3. L50
    exact hcop

Library-wide reading audit

Original defined command ledger · 50 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro l
  5. 0005intro n
  6. 0006intro d
  7. 0007intro p
  8. 0008intro k
  9. 0009intro m
  10. 0010intro hp
  11. 0011intro hk
  12. 0012intro hpower
  13. 0013intro hpair
  14. 0014intro hroot
  15. 0015intro hcop
  16. 0016have hfactor : ¬m = 0 ∧ Dvd(p,m)
  17. 0017specialize hensel_positive_power_factor p
  18. 0018specialize hensel_positive_power_factor k
  19. 0019specialize hensel_positive_power_factor m
  20. 0020apply hensel_positive_power_factor
  21. 0021exact hp
  22. 0022exact hk
  23. 0023exact hpower
  24. 0024cases hfactor
  25. 0025cases hfactor_right
  26. 0026exists p * m
  27. 0027split
  28. 0028specialize pow_successor_compose p
  29. 0029specialize pow_successor_compose k
  30. 0030specialize pow_successor_compose m
  31. 0031specialize pow_successor_compose (p * m)
  32. 0032apply pow_successor_compose
  33. 0033exact hpower
  34. 0034apply mul_comm
  35. 0035specialize beta_horner_simple_root_hensel_lift_exists_unique b
  36. 0036specialize beta_horner_simple_root_hensel_lift_exists_unique c
  37. 0037specialize beta_horner_simple_root_hensel_lift_exists_unique a
  38. 0038specialize beta_horner_simple_root_hensel_lift_exists_unique l
  39. 0039specialize beta_horner_simple_root_hensel_lift_exists_unique n
  40. 0040specialize beta_horner_simple_root_hensel_lift_exists_unique d
  41. 0041specialize beta_horner_simple_root_hensel_lift_exists_unique m
  42. 0042specialize beta_horner_simple_root_hensel_lift_exists_unique p
  43. 0043specialize beta_horner_simple_root_hensel_lift_exists_unique x
  44. 0044apply beta_horner_simple_root_hensel_lift_exists_unique
  45. 0045exact hp
  46. 0046exact hfactor_left
  47. 0047exact hpair
  48. 0048exact hfactor_right_witness
  49. 0049exact hroot
  50. 0050exact hcop