HL0008

hensel_canonical_horner_lift_exists_unique

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

A canonical old simple root has exactly one bounded next-modulus lift among all roots in its old residue class.

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.

Exact expanded first-order arithmetic statement

forall b c a l n d m p s q. ~(p = 0) -> ~(m = 0) -> (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)))))))) -> m = p * s -> n = m * q -> (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 hpl_gap_bound. hpl_gap_bound + S (a) = (m)) -> exists r. ((((exists hpl_gap_lift. hpl_gap_lift + S (r) = (p * 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 + (p * m) * hgcrt_mod_left_hpl_lift = 0 + (p * m) * hgcrt_mod_right_hpl_lift)))))) /\ forall z. (((exists hpl_gap_lift. hpl_gap_lift + S (z) = (p * 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 + (p * m) * hgcrt_mod_left_hpl_lift = 0 + (p * m) * hgcrt_mod_right_hpl_lift)))))) -> z = r)

Constructive proof overview

Generated structural guide

A canonical old simple root has exactly one bounded next-modulus lift among all roots in its old residue class.

The unchanged tactic script uses 6 declared prerequisites and contains 117 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_horner_hensel_lift_exists Alpha theorem; checked-use authorized HL0004 hensel_lift_digit_bound multiple_implies_balanced_zero_congruence Alpha theorem; checked-use authorized HL0005 hensel_canonical_lift_digit_decompose HL0007 hensel_lift_correction_of_root hensel_correction_unique Alpha theorem; checked-use authorized

Direct dependents

HL000A beta_horner_simple_root_hensel_lift_exists_unique

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

117 script commands · 30 reading checkpoints · 5 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.

Named ingredients (3)
hensel lift digit boundhensel canonical lift digit decomposehensel lift correction of root

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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 m
  8. L8
    intro p
  9. L9
    intro s
  10. L10
    intro q
02Fix variables and assumptionsL11–17

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

  1. L11
    intro hp
  2. L12
    intro hm
  3. L13
    intro hpair
  4. L14
    intro hfactor
  5. L15
    intro hn
  6. L16
    intro hcop
  7. L17
    intro ha
03Establish hstepL18–27

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

  1. L18
    have hstep : ∃ t. ∃ y. Lt(t,p) ∧ ModEq(p,q + d · t,0) ∧ (Horner(b,c,a + m · t,l,y) ∧ Dvd(p · m,y))Definitions: HornerLtDvdModEq
  2. L19
    specialize beta_horner_hensel_lift_exists b
  3. L20
    specialize beta_horner_hensel_lift_exists c
  4. L21
    specialize beta_horner_hensel_lift_exists a
  5. L22
    specialize beta_horner_hensel_lift_exists l
  6. L23
    specialize beta_horner_hensel_lift_exists n
  7. L24
    specialize beta_horner_hensel_lift_exists d
  8. L25
    specialize beta_horner_hensel_lift_exists m
  9. L26
    specialize beta_horner_hensel_lift_exists p
  10. L27
    specialize beta_horner_hensel_lift_exists s
04Use earlier factsL28–34

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

  1. L28
    specialize beta_horner_hensel_lift_exists q
  2. L29
    apply beta_horner_hensel_lift_exists
  3. L30
    exact hp
  4. L31
    exact hpair
  5. L32
    exact hfactor
  6. L33
    exact hn
  7. L34
    exact hcop
05Separate the logical casesL35–38

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

  1. L35
    cases hstep
  2. L36
    cases hstep_witness
  3. L37
    cases hstep_witness_witness
  4. L38
    cases hstep_witness_witness_right
06Establish htL39–39

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

  1. L39
    have ht : exists hpl_gap_bound. hpl_gap_bound + S (x) = (p)
07Separate the logical casesL40–40

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

  1. L40
    cases hstep_witness_witness_left
08Use earlier factsL41–41

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

  1. L41
    exact hstep_witness_witness_left_left
09Construct an explicit witnessL42–42

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

  1. L42
    exists a + m * x
10Separate the logical casesL43–44

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

  1. L43
    split
  2. L44
    split
11Use earlier factsL45–51

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

  1. L45
    specialize hensel_lift_digit_bound m
  2. L46
    specialize hensel_lift_digit_bound p
  3. L47
    specialize hensel_lift_digit_bound a
  4. L48
    specialize hensel_lift_digit_bound x
  5. L49
    apply hensel_lift_digit_bound
  6. L50
    exact ha
  7. L51
    exact ht
12Separate the logical casesL52–52

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

  1. L52
    split
13Construct an explicit witnessL53–54

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

  1. L53
    exists 0
  2. L54
    exists x
14Calculate and transport equalitiesL55–55

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

  1. L55
    simp
15Construct an explicit witnessL56–56

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

  1. L56
    exists x1
16Separate the logical casesL57–57

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

  1. L57
    split
17Use earlier factsL58–62

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

  1. L58
    exact hstep_witness_witness_right_left
  2. L59
    specialize multiple_implies_balanced_zero_congruence (p * m)
  3. L60
    specialize multiple_implies_balanced_zero_congruence x1
  4. L61
    apply multiple_implies_balanced_zero_congruence
  5. L62
    exact hstep_witness_witness_right_right
18Fix variables and assumptionsL63–64

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

  1. L63
    intro z
  2. L64
    intro hz
19Separate the logical casesL65–66

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

  1. L65
    cases hz
  2. L66
    cases hz_right
20Establish hdigitL67–76

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hensel canonical lift digit decompose.

  1. L67
    have hdigit : exists t. ((exists hpl_gap_bound. hpl_gap_bound + S (t) = (p)) /\ z = a + m * t)
  2. L68
    specialize hensel_canonical_lift_digit_decompose m
  3. L69
    specialize hensel_canonical_lift_digit_decompose p
  4. L70
    specialize hensel_canonical_lift_digit_decompose a
  5. L71
    specialize hensel_canonical_lift_digit_decompose z
  6. L72
    apply hensel_canonical_lift_digit_decompose
  7. L73
    exact hm
  8. L74
    exact ha
  9. L75
    exact hz_left
  10. L76
    exact hz_right_left
21Separate the logical casesL77–80

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

  1. L77
    cases hdigit
  2. L78
    cases hdigit_witness
  3. L79
    cases hz_right_right
  4. L80
    cases hz_right_right_witness
22Establish hcorrectionL81–90

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

  1. L81
    have hcorrection : ((exists ff_lt_pth_hpl_correction_bound. ff_lt_pth_hpl_correction_bound + S x2 = p) /\ (exists hgcrt_mod_left_pth_hpl_correction_annihilation hgcrt_mod_right_pth_hpl_correction_annihilation. (q + d * x2) + p * hgcrt_mod_left_pth_hpl_correction_annihilation = 0 + p * hgcrt_mod_right_pth_hpl_correction_annihilation))
  2. L82
    specialize hensel_lift_correction_of_root b
  3. L83
    specialize hensel_lift_correction_of_root c
  4. L84
    specialize hensel_lift_correction_of_root a
  5. L85
    specialize hensel_lift_correction_of_root l
  6. L86
    specialize hensel_lift_correction_of_root n
  7. L87
    specialize hensel_lift_correction_of_root d
  8. L88
    specialize hensel_lift_correction_of_root m
  9. L89
    specialize hensel_lift_correction_of_root p
  10. L90
    specialize hensel_lift_correction_of_root s
23Use earlier factsL91–96

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

  1. L91
    specialize hensel_lift_correction_of_root q
  2. L92
    specialize hensel_lift_correction_of_root x2
  3. L93
    specialize hensel_lift_correction_of_root x3
  4. L94
    apply hensel_lift_correction_of_root
  5. L95
    exact hm
  6. L96
    exact hpair
24Calculate and transport equalitiesL97–97

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

  1. L97
    rewrite <- hdigit_witness_right
25Use earlier factsL98–102

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

  1. L98
    exact hz_right_right_witness_left
  2. L99
    exact hfactor
  3. L100
    exact hn
  4. L101
    exact hdigit_witness_left
  5. L102
    exact hz_right_right_witness_right
26Establish heqL103–112

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

  1. L103
    have heq : x2 = x
  2. L104
    specialize hensel_correction_unique d
  3. L105
    specialize hensel_correction_unique p
  4. L106
    specialize hensel_correction_unique q
  5. L107
    specialize hensel_correction_unique x2
  6. L108
    specialize hensel_correction_unique x
  7. L109
    apply hensel_correction_unique
  8. L110
    exact hp
  9. L111
    exact hcop
  10. L112
    exact hcorrection
27Use earlier factsL113–113

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

  1. L113
    exact hstep_witness_witness_left
28Calculate and transport equalitiesL114–114

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

  1. L114
    trans a + m * x2
29Use earlier factsL115–115

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

  1. L115
    exact hdigit_witness_right
30Calculate and transport equalitiesL116–117

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

  1. L116
    rewrite heq
  2. L117
    refl

Library-wide reading audit

Original exact command ledger · 117 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro l
  5. 0005intro n
  6. 0006intro d
  7. 0007intro m
  8. 0008intro p
  9. 0009intro s
  10. 0010intro q
  11. 0011intro hp
  12. 0012intro hm
  13. 0013intro hpair
  14. 0014intro hfactor
  15. 0015intro hn
  16. 0016intro hcop
  17. 0017intro ha
  18. 0018have hstep : exists t y. ((((exists ff_lt_pth_hpl_correction_bound. ff_lt_pth_hpl_correction_bound + S t = p) /\ (exists hgcrt_mod_left_pth_hpl_correction_annihilation hgcrt_mod_right_pth_hpl_correction_annihilation. (q + d * t) + p * hgcrt_mod_left_pth_hpl_correction_annihilation = 0 + p * hgcrt_mod_right_pth_hpl_correction_annihilation))) /\ ((exists ff_u_ph_hpl_eval ff_v_ph_hpl_eval. ((((exists fs_h_ph_hpl_eval_body_start. fs_h_ph_hpl_eval_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_eval)) /\ exists fs_q_ph_hpl_eval_body_start. ff_u_ph_hpl_eval = fs_q_ph_hpl_eval_body_start * S ((S (0)) * ff_v_ph_hpl_eval) + (0))) /\ ((((exists fs_h_ph_hpl_eval_body_terminal. fs_h_ph_hpl_eval_body_terminal + S (y) = S ((S (l)) * ff_v_ph_hpl_eval)) /\ exists fs_q_ph_hpl_eval_body_terminal. ff_u_ph_hpl_eval = fs_q_ph_hpl_eval_body_terminal * S ((S (l)) * ff_v_ph_hpl_eval) + (y))) /\ forall ff_i_ph_hpl_eval_body_steps. (exists ph_bound_hpl_eval_body_steps. ph_bound_hpl_eval_body_steps + S ff_i_ph_hpl_eval_body_steps = l) -> exists ff_coefficient_ph_hpl_eval_body_steps ff_previous_ph_hpl_eval_body_steps ff_current_ph_hpl_eval_body_steps. ((((exists fs_h_ph_hpl_eval_body_steps_coefficient. fs_h_ph_hpl_eval_body_steps_coefficient + S (ff_coefficient_ph_hpl_eval_body_steps) = S ((S (ff_i_ph_hpl_eval_body_steps)) * c)) /\ exists fs_q_ph_hpl_eval_body_steps_coefficient. b = fs_q_ph_hpl_eval_body_steps_coefficient * S ((S (ff_i_ph_hpl_eval_body_steps)) * c) + (ff_coefficient_ph_hpl_eval_body_steps))) /\ ((((exists fs_h_ph_hpl_eval_body_steps_before. fs_h_ph_hpl_eval_body_steps_before + S (ff_previous_ph_hpl_eval_body_steps) = S ((S (ff_i_ph_hpl_eval_body_steps)) * ff_v_ph_hpl_eval)) /\ exists fs_q_ph_hpl_eval_body_steps_before. ff_u_ph_hpl_eval = fs_q_ph_hpl_eval_body_steps_before * S ((S (ff_i_ph_hpl_eval_body_steps)) * ff_v_ph_hpl_eval) + (ff_previous_ph_hpl_eval_body_steps))) /\ ((((exists fs_h_ph_hpl_eval_body_steps_after. fs_h_ph_hpl_eval_body_steps_after + S (ff_current_ph_hpl_eval_body_steps) = S ((S (S ff_i_ph_hpl_eval_body_steps)) * ff_v_ph_hpl_eval)) /\ exists fs_q_ph_hpl_eval_body_steps_after. ff_u_ph_hpl_eval = fs_q_ph_hpl_eval_body_steps_after * S ((S (S ff_i_ph_hpl_eval_body_steps)) * ff_v_ph_hpl_eval) + (ff_current_ph_hpl_eval_body_steps))) /\ ff_current_ph_hpl_eval_body_steps = ff_previous_ph_hpl_eval_body_steps * (a + m * t) + ff_coefficient_ph_hpl_eval_body_steps)))))) /\ exists w. y = (p * m) * w))
  19. 0019specialize beta_horner_hensel_lift_exists b
  20. 0020specialize beta_horner_hensel_lift_exists c
  21. 0021specialize beta_horner_hensel_lift_exists a
  22. 0022specialize beta_horner_hensel_lift_exists l
  23. 0023specialize beta_horner_hensel_lift_exists n
  24. 0024specialize beta_horner_hensel_lift_exists d
  25. 0025specialize beta_horner_hensel_lift_exists m
  26. 0026specialize beta_horner_hensel_lift_exists p
  27. 0027specialize beta_horner_hensel_lift_exists s
  28. 0028specialize beta_horner_hensel_lift_exists q
  29. 0029apply beta_horner_hensel_lift_exists
  30. 0030exact hp
  31. 0031exact hpair
  32. 0032exact hfactor
  33. 0033exact hn
  34. 0034exact hcop
  35. 0035cases hstep
  36. 0036cases hstep_witness
  37. 0037cases hstep_witness_witness
  38. 0038cases hstep_witness_witness_right
  39. 0039have ht : exists hpl_gap_bound. hpl_gap_bound + S (x) = (p)
  40. 0040cases hstep_witness_witness_left
  41. 0041exact hstep_witness_witness_left_left
  42. 0042exists a + m * x
  43. 0043split
  44. 0044split
  45. 0045specialize hensel_lift_digit_bound m
  46. 0046specialize hensel_lift_digit_bound p
  47. 0047specialize hensel_lift_digit_bound a
  48. 0048specialize hensel_lift_digit_bound x
  49. 0049apply hensel_lift_digit_bound
  50. 0050exact ha
  51. 0051exact ht
  52. 0052split
  53. 0053exists 0
  54. 0054exists x
  55. 0055simp
  56. 0056exists x1
  57. 0057split
  58. 0058exact hstep_witness_witness_right_left
  59. 0059specialize multiple_implies_balanced_zero_congruence (p * m)
  60. 0060specialize multiple_implies_balanced_zero_congruence x1
  61. 0061apply multiple_implies_balanced_zero_congruence
  62. 0062exact hstep_witness_witness_right_right
  63. 0063intro z
  64. 0064intro hz
  65. 0065cases hz
  66. 0066cases hz_right
  67. 0067have hdigit : exists t. ((exists hpl_gap_bound. hpl_gap_bound + S (t) = (p)) /\ z = a + m * t)
  68. 0068specialize hensel_canonical_lift_digit_decompose m
  69. 0069specialize hensel_canonical_lift_digit_decompose p
  70. 0070specialize hensel_canonical_lift_digit_decompose a
  71. 0071specialize hensel_canonical_lift_digit_decompose z
  72. 0072apply hensel_canonical_lift_digit_decompose
  73. 0073exact hm
  74. 0074exact ha
  75. 0075exact hz_left
  76. 0076exact hz_right_left
  77. 0077cases hdigit
  78. 0078cases hdigit_witness
  79. 0079cases hz_right_right
  80. 0080cases hz_right_right_witness
  81. 0081have hcorrection : ((exists ff_lt_pth_hpl_correction_bound. ff_lt_pth_hpl_correction_bound + S x2 = p) /\ (exists hgcrt_mod_left_pth_hpl_correction_annihilation hgcrt_mod_right_pth_hpl_correction_annihilation. (q + d * x2) + p * hgcrt_mod_left_pth_hpl_correction_annihilation = 0 + p * hgcrt_mod_right_pth_hpl_correction_annihilation))
  82. 0082specialize hensel_lift_correction_of_root b
  83. 0083specialize hensel_lift_correction_of_root c
  84. 0084specialize hensel_lift_correction_of_root a
  85. 0085specialize hensel_lift_correction_of_root l
  86. 0086specialize hensel_lift_correction_of_root n
  87. 0087specialize hensel_lift_correction_of_root d
  88. 0088specialize hensel_lift_correction_of_root m
  89. 0089specialize hensel_lift_correction_of_root p
  90. 0090specialize hensel_lift_correction_of_root s
  91. 0091specialize hensel_lift_correction_of_root q
  92. 0092specialize hensel_lift_correction_of_root x2
  93. 0093specialize hensel_lift_correction_of_root x3
  94. 0094apply hensel_lift_correction_of_root
  95. 0095exact hm
  96. 0096exact hpair
  97. 0097rewrite <- hdigit_witness_right
  98. 0098exact hz_right_right_witness_left
  99. 0099exact hfactor
  100. 0100exact hn
  101. 0101exact hdigit_witness_left
  102. 0102exact hz_right_right_witness_right
  103. 0103have heq : x2 = x
  104. 0104specialize hensel_correction_unique d
  105. 0105specialize hensel_correction_unique p
  106. 0106specialize hensel_correction_unique q
  107. 0107specialize hensel_correction_unique x2
  108. 0108specialize hensel_correction_unique x
  109. 0109apply hensel_correction_unique
  110. 0110exact hp
  111. 0111exact hcop
  112. 0112exact hcorrection
  113. 0113exact hstep_witness_witness_left
  114. 0114trans a + m * x2
  115. 0115exact hdigit_witness_right
  116. 0116rewrite heq
  117. 0117refl