TH0013

beta_horner_hensel_lift_exists

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

Every genuinely evaluated coprime simple root modulo a p-divisible modulus has an actual bounded correction and an actual polynomial root modulo the next modulus.

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) -> (exists ff_u_hd_pth_lift_pair ff_v_hd_pth_lift_pair ff_d_hd_pth_lift_pair ff_e_hd_pth_lift_pair. ((((((exists fs_h_ph_hd_pth_lift_pair_body_value_start. fs_h_ph_hd_pth_lift_pair_body_value_start + S (0) = S ((S (0)) * ff_v_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_value_start. ff_u_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_value_start * S ((S (0)) * ff_v_hd_pth_lift_pair) + (0))) /\ ((((exists fs_h_ph_hd_pth_lift_pair_body_value_terminal. fs_h_ph_hd_pth_lift_pair_body_value_terminal + S (n) = S ((S (l)) * ff_v_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_value_terminal. ff_u_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_value_terminal * S ((S (l)) * ff_v_hd_pth_lift_pair) + (n))) /\ forall ff_i_ph_hd_pth_lift_pair_body_value_steps. (exists ph_bound_hd_pth_lift_pair_body_value_steps. ph_bound_hd_pth_lift_pair_body_value_steps + S ff_i_ph_hd_pth_lift_pair_body_value_steps = l) -> exists ff_coefficient_ph_hd_pth_lift_pair_body_value_steps ff_previous_ph_hd_pth_lift_pair_body_value_steps ff_current_ph_hd_pth_lift_pair_body_value_steps. ((((exists fs_h_ph_hd_pth_lift_pair_body_value_steps_coefficient. fs_h_ph_hd_pth_lift_pair_body_value_steps_coefficient + S (ff_coefficient_ph_hd_pth_lift_pair_body_value_steps) = S ((S (ff_i_ph_hd_pth_lift_pair_body_value_steps)) * c)) /\ exists fs_q_ph_hd_pth_lift_pair_body_value_steps_coefficient. b = fs_q_ph_hd_pth_lift_pair_body_value_steps_coefficient * S ((S (ff_i_ph_hd_pth_lift_pair_body_value_steps)) * c) + (ff_coefficient_ph_hd_pth_lift_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_lift_pair_body_value_steps_before. fs_h_ph_hd_pth_lift_pair_body_value_steps_before + S (ff_previous_ph_hd_pth_lift_pair_body_value_steps) = S ((S (ff_i_ph_hd_pth_lift_pair_body_value_steps)) * ff_v_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_value_steps_before. ff_u_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_value_steps_before * S ((S (ff_i_ph_hd_pth_lift_pair_body_value_steps)) * ff_v_hd_pth_lift_pair) + (ff_previous_ph_hd_pth_lift_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_lift_pair_body_value_steps_after. fs_h_ph_hd_pth_lift_pair_body_value_steps_after + S (ff_current_ph_hd_pth_lift_pair_body_value_steps) = S ((S (S ff_i_ph_hd_pth_lift_pair_body_value_steps)) * ff_v_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_value_steps_after. ff_u_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_value_steps_after * S ((S (S ff_i_ph_hd_pth_lift_pair_body_value_steps)) * ff_v_hd_pth_lift_pair) + (ff_current_ph_hd_pth_lift_pair_body_value_steps))) /\ ff_current_ph_hd_pth_lift_pair_body_value_steps = ff_previous_ph_hd_pth_lift_pair_body_value_steps * a + ff_coefficient_ph_hd_pth_lift_pair_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_pth_lift_pair_body_derivative_start. fs_h_ph_hd_pth_lift_pair_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_derivative_start. ff_d_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_derivative_start * S ((S (0)) * ff_e_hd_pth_lift_pair) + (0))) /\ ((((exists fs_h_ph_hd_pth_lift_pair_body_derivative_terminal. fs_h_ph_hd_pth_lift_pair_body_derivative_terminal + S (d) = S ((S (l)) * ff_e_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_derivative_terminal. ff_d_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_derivative_terminal * S ((S (l)) * ff_e_hd_pth_lift_pair) + (d))) /\ forall ff_i_ph_hd_pth_lift_pair_body_derivative_steps. (exists ph_bound_hd_pth_lift_pair_body_derivative_steps. ph_bound_hd_pth_lift_pair_body_derivative_steps + S ff_i_ph_hd_pth_lift_pair_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_pth_lift_pair_body_derivative_steps ff_previous_ph_hd_pth_lift_pair_body_derivative_steps ff_current_ph_hd_pth_lift_pair_body_derivative_steps. ((((exists fs_h_ph_hd_pth_lift_pair_body_derivative_steps_coefficient. fs_h_ph_hd_pth_lift_pair_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_pth_lift_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_lift_pair_body_derivative_steps)) * ff_v_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_derivative_steps_coefficient. ff_u_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_pth_lift_pair_body_derivative_steps)) * ff_v_hd_pth_lift_pair) + (ff_coefficient_ph_hd_pth_lift_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_lift_pair_body_derivative_steps_before. fs_h_ph_hd_pth_lift_pair_body_derivative_steps_before + S (ff_previous_ph_hd_pth_lift_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_lift_pair_body_derivative_steps)) * ff_e_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_derivative_steps_before. ff_d_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_derivative_steps_before * S ((S (ff_i_ph_hd_pth_lift_pair_body_derivative_steps)) * ff_e_hd_pth_lift_pair) + (ff_previous_ph_hd_pth_lift_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_lift_pair_body_derivative_steps_after. fs_h_ph_hd_pth_lift_pair_body_derivative_steps_after + S (ff_current_ph_hd_pth_lift_pair_body_derivative_steps) = S ((S (S ff_i_ph_hd_pth_lift_pair_body_derivative_steps)) * ff_e_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_derivative_steps_after. ff_d_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_derivative_steps_after * S ((S (S ff_i_ph_hd_pth_lift_pair_body_derivative_steps)) * ff_e_hd_pth_lift_pair) + (ff_current_ph_hd_pth_lift_pair_body_derivative_steps))) /\ ff_current_ph_hd_pth_lift_pair_body_derivative_steps = ff_previous_ph_hd_pth_lift_pair_body_derivative_steps * a + ff_coefficient_ph_hd_pth_lift_pair_body_derivative_steps)))))))) -> m = p * s -> n = m * q -> (forall hmi_divisor_pth_correction. (exists hmi_left_factor_pth_correction. d = hmi_divisor_pth_correction * hmi_left_factor_pth_correction) -> (exists hmi_right_factor_pth_correction. p = hmi_divisor_pth_correction * hmi_right_factor_pth_correction) -> hmi_divisor_pth_correction = 1) -> exists t y. ((((exists ff_lt_pth_lift_correction_bound. ff_lt_pth_lift_correction_bound + S t = p) /\ (exists hgcrt_mod_left_pth_lift_correction_annihilation hgcrt_mod_right_pth_lift_correction_annihilation. (q + d * t) + p * hgcrt_mod_left_pth_lift_correction_annihilation = 0 + p * hgcrt_mod_right_pth_lift_correction_annihilation))) /\ ((exists ff_u_ph_pth_lift_value ff_v_ph_pth_lift_value. ((((exists fs_h_ph_pth_lift_value_body_start. fs_h_ph_pth_lift_value_body_start + S (0) = S ((S (0)) * ff_v_ph_pth_lift_value)) /\ exists fs_q_ph_pth_lift_value_body_start. ff_u_ph_pth_lift_value = fs_q_ph_pth_lift_value_body_start * S ((S (0)) * ff_v_ph_pth_lift_value) + (0))) /\ ((((exists fs_h_ph_pth_lift_value_body_terminal. fs_h_ph_pth_lift_value_body_terminal + S (y) = S ((S (l)) * ff_v_ph_pth_lift_value)) /\ exists fs_q_ph_pth_lift_value_body_terminal. ff_u_ph_pth_lift_value = fs_q_ph_pth_lift_value_body_terminal * S ((S (l)) * ff_v_ph_pth_lift_value) + (y))) /\ forall ff_i_ph_pth_lift_value_body_steps. (exists ph_bound_pth_lift_value_body_steps. ph_bound_pth_lift_value_body_steps + S ff_i_ph_pth_lift_value_body_steps = l) -> exists ff_coefficient_ph_pth_lift_value_body_steps ff_previous_ph_pth_lift_value_body_steps ff_current_ph_pth_lift_value_body_steps. ((((exists fs_h_ph_pth_lift_value_body_steps_coefficient. fs_h_ph_pth_lift_value_body_steps_coefficient + S (ff_coefficient_ph_pth_lift_value_body_steps) = S ((S (ff_i_ph_pth_lift_value_body_steps)) * c)) /\ exists fs_q_ph_pth_lift_value_body_steps_coefficient. b = fs_q_ph_pth_lift_value_body_steps_coefficient * S ((S (ff_i_ph_pth_lift_value_body_steps)) * c) + (ff_coefficient_ph_pth_lift_value_body_steps))) /\ ((((exists fs_h_ph_pth_lift_value_body_steps_before. fs_h_ph_pth_lift_value_body_steps_before + S (ff_previous_ph_pth_lift_value_body_steps) = S ((S (ff_i_ph_pth_lift_value_body_steps)) * ff_v_ph_pth_lift_value)) /\ exists fs_q_ph_pth_lift_value_body_steps_before. ff_u_ph_pth_lift_value = fs_q_ph_pth_lift_value_body_steps_before * S ((S (ff_i_ph_pth_lift_value_body_steps)) * ff_v_ph_pth_lift_value) + (ff_previous_ph_pth_lift_value_body_steps))) /\ ((((exists fs_h_ph_pth_lift_value_body_steps_after. fs_h_ph_pth_lift_value_body_steps_after + S (ff_current_ph_pth_lift_value_body_steps) = S ((S (S ff_i_ph_pth_lift_value_body_steps)) * ff_v_ph_pth_lift_value)) /\ exists fs_q_ph_pth_lift_value_body_steps_after. ff_u_ph_pth_lift_value = fs_q_ph_pth_lift_value_body_steps_after * S ((S (S ff_i_ph_pth_lift_value_body_steps)) * ff_v_ph_pth_lift_value) + (ff_current_ph_pth_lift_value_body_steps))) /\ ff_current_ph_pth_lift_value_body_steps = ff_previous_ph_pth_lift_value_body_steps * (a + m * t) + ff_coefficient_ph_pth_lift_value_body_steps)))))) /\ exists w. y = (p * m) * w))

Constructive proof overview

Generated structural guide

Every genuinely evaluated coprime simple root modulo a p-divisible modulus has an actual bounded correction and an actual polynomial root modulo the next modulus.

The unchanged tactic script uses 3 declared prerequisites and contains 55 exact native proof lines.

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

Proof neighborhood

Direct dependencies

TH0009 hensel_correction_exists beta_horner_eval_exists Alpha theorem; checked-use authorized TH0012 beta_horner_hensel_lift_divisibility

Direct dependents

none

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

55 script commands · 12 reading checkpoints · 2 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 (2)
hensel correction existsbeta horner hensel lift divisibility

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–15

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

  1. L11
    intro hp
  2. L12
    intro hpair
  3. L13
    intro hfactor
  4. L14
    intro hroot
  5. L15
    intro hcop
03Establish hcorrectionL16–22

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

  1. L16
    have hcorrection : exists t. (((exists ff_lt_pth_lift_exists_correction_bound. ff_lt_pth_lift_exists_correction_bound + S t = p) /\ (exists hgcrt_mod_left_pth_lift_exists_correction_annihilation hgcrt_mod_right_pth_lift_exists_correction_annihilation. (q + d * t) + p * hgcrt_mod_left_pth_lift_exists_correction_annihilation = 0 + p * hgcrt_mod_right_pth_lift_exists_correction_annihilation)))
  2. L17
    specialize hensel_correction_exists d
  3. L18
    specialize hensel_correction_exists p
  4. L19
    specialize hensel_correction_exists q
  5. L20
    apply hensel_correction_exists
  6. L21
    exact hp
  7. L22
    exact hcop
04Separate the logical casesL23–23

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

  1. L23
    cases hcorrection
05Establish hvalueL24–29

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

  1. L24
    have hvalue : ∃ y. Horner(b,c,a + m · x,l,y)Definitions: Horner
  2. L25
    specialize beta_horner_eval_exists b
  3. L26
    specialize beta_horner_eval_exists c
  4. L27
    specialize beta_horner_eval_exists (a + m * x)
  5. L28
    specialize beta_horner_eval_exists l
  6. L29
    exact beta_horner_eval_exists
06Separate the logical casesL30–30

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

  1. L30
    cases hvalue
07Construct an explicit witnessL31–32

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

  1. L31
    exists x
  2. L32
    exists x1
08Separate the logical casesL33–33

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

  1. L33
    split
09Use earlier factsL34–34

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

  1. L34
    exact hcorrection_witness
10Separate the logical casesL35–35

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

  1. L35
    split
11Use earlier factsL36–45

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

  1. L36
    exact hvalue_witness
  2. L37
    specialize beta_horner_hensel_lift_divisibility b
  3. L38
    specialize beta_horner_hensel_lift_divisibility c
  4. L39
    specialize beta_horner_hensel_lift_divisibility a
  5. L40
    specialize beta_horner_hensel_lift_divisibility l
  6. L41
    specialize beta_horner_hensel_lift_divisibility n
  7. L42
    specialize beta_horner_hensel_lift_divisibility d
  8. L43
    specialize beta_horner_hensel_lift_divisibility m
  9. L44
    specialize beta_horner_hensel_lift_divisibility p
  10. L45
    specialize beta_horner_hensel_lift_divisibility s
12Use earlier factsL46–55

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

  1. L46
    specialize beta_horner_hensel_lift_divisibility q
  2. L47
    specialize beta_horner_hensel_lift_divisibility x
  3. L48
    specialize beta_horner_hensel_lift_divisibility x1
  4. L49
    apply beta_horner_hensel_lift_divisibility
  5. L50
    exact hp
  6. L51
    exact hpair
  7. L52
    exact hvalue_witness
  8. L53
    exact hfactor
  9. L54
    exact hroot
  10. L55
    exact hcorrection_witness

Library-wide reading audit

Original exact command ledger · 55 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 hpair
  13. 0013intro hfactor
  14. 0014intro hroot
  15. 0015intro hcop
  16. 0016have hcorrection : exists t. (((exists ff_lt_pth_lift_exists_correction_bound. ff_lt_pth_lift_exists_correction_bound + S t = p) /\ (exists hgcrt_mod_left_pth_lift_exists_correction_annihilation hgcrt_mod_right_pth_lift_exists_correction_annihilation. (q + d * t) + p * hgcrt_mod_left_pth_lift_exists_correction_annihilation = 0 + p * hgcrt_mod_right_pth_lift_exists_correction_annihilation)))
  17. 0017specialize hensel_correction_exists d
  18. 0018specialize hensel_correction_exists p
  19. 0019specialize hensel_correction_exists q
  20. 0020apply hensel_correction_exists
  21. 0021exact hp
  22. 0022exact hcop
  23. 0023cases hcorrection
  24. 0024have hvalue : exists y. (exists ff_u_ph_pth_lift_exists_value ff_v_ph_pth_lift_exists_value. ((((exists fs_h_ph_pth_lift_exists_value_body_start. fs_h_ph_pth_lift_exists_value_body_start + S (0) = S ((S (0)) * ff_v_ph_pth_lift_exists_value)) /\ exists fs_q_ph_pth_lift_exists_value_body_start. ff_u_ph_pth_lift_exists_value = fs_q_ph_pth_lift_exists_value_body_start * S ((S (0)) * ff_v_ph_pth_lift_exists_value) + (0))) /\ ((((exists fs_h_ph_pth_lift_exists_value_body_terminal. fs_h_ph_pth_lift_exists_value_body_terminal + S (y) = S ((S (l)) * ff_v_ph_pth_lift_exists_value)) /\ exists fs_q_ph_pth_lift_exists_value_body_terminal. ff_u_ph_pth_lift_exists_value = fs_q_ph_pth_lift_exists_value_body_terminal * S ((S (l)) * ff_v_ph_pth_lift_exists_value) + (y))) /\ forall ff_i_ph_pth_lift_exists_value_body_steps. (exists ph_bound_pth_lift_exists_value_body_steps. ph_bound_pth_lift_exists_value_body_steps + S ff_i_ph_pth_lift_exists_value_body_steps = l) -> exists ff_coefficient_ph_pth_lift_exists_value_body_steps ff_previous_ph_pth_lift_exists_value_body_steps ff_current_ph_pth_lift_exists_value_body_steps. ((((exists fs_h_ph_pth_lift_exists_value_body_steps_coefficient. fs_h_ph_pth_lift_exists_value_body_steps_coefficient + S (ff_coefficient_ph_pth_lift_exists_value_body_steps) = S ((S (ff_i_ph_pth_lift_exists_value_body_steps)) * c)) /\ exists fs_q_ph_pth_lift_exists_value_body_steps_coefficient. b = fs_q_ph_pth_lift_exists_value_body_steps_coefficient * S ((S (ff_i_ph_pth_lift_exists_value_body_steps)) * c) + (ff_coefficient_ph_pth_lift_exists_value_body_steps))) /\ ((((exists fs_h_ph_pth_lift_exists_value_body_steps_before. fs_h_ph_pth_lift_exists_value_body_steps_before + S (ff_previous_ph_pth_lift_exists_value_body_steps) = S ((S (ff_i_ph_pth_lift_exists_value_body_steps)) * ff_v_ph_pth_lift_exists_value)) /\ exists fs_q_ph_pth_lift_exists_value_body_steps_before. ff_u_ph_pth_lift_exists_value = fs_q_ph_pth_lift_exists_value_body_steps_before * S ((S (ff_i_ph_pth_lift_exists_value_body_steps)) * ff_v_ph_pth_lift_exists_value) + (ff_previous_ph_pth_lift_exists_value_body_steps))) /\ ((((exists fs_h_ph_pth_lift_exists_value_body_steps_after. fs_h_ph_pth_lift_exists_value_body_steps_after + S (ff_current_ph_pth_lift_exists_value_body_steps) = S ((S (S ff_i_ph_pth_lift_exists_value_body_steps)) * ff_v_ph_pth_lift_exists_value)) /\ exists fs_q_ph_pth_lift_exists_value_body_steps_after. ff_u_ph_pth_lift_exists_value = fs_q_ph_pth_lift_exists_value_body_steps_after * S ((S (S ff_i_ph_pth_lift_exists_value_body_steps)) * ff_v_ph_pth_lift_exists_value) + (ff_current_ph_pth_lift_exists_value_body_steps))) /\ ff_current_ph_pth_lift_exists_value_body_steps = ff_previous_ph_pth_lift_exists_value_body_steps * (a + m * x) + ff_coefficient_ph_pth_lift_exists_value_body_steps))))))
  25. 0025specialize beta_horner_eval_exists b
  26. 0026specialize beta_horner_eval_exists c
  27. 0027specialize beta_horner_eval_exists (a + m * x)
  28. 0028specialize beta_horner_eval_exists l
  29. 0029exact beta_horner_eval_exists
  30. 0030cases hvalue
  31. 0031exists x
  32. 0032exists x1
  33. 0033split
  34. 0034exact hcorrection_witness
  35. 0035split
  36. 0036exact hvalue_witness
  37. 0037specialize beta_horner_hensel_lift_divisibility b
  38. 0038specialize beta_horner_hensel_lift_divisibility c
  39. 0039specialize beta_horner_hensel_lift_divisibility a
  40. 0040specialize beta_horner_hensel_lift_divisibility l
  41. 0041specialize beta_horner_hensel_lift_divisibility n
  42. 0042specialize beta_horner_hensel_lift_divisibility d
  43. 0043specialize beta_horner_hensel_lift_divisibility m
  44. 0044specialize beta_horner_hensel_lift_divisibility p
  45. 0045specialize beta_horner_hensel_lift_divisibility s
  46. 0046specialize beta_horner_hensel_lift_divisibility q
  47. 0047specialize beta_horner_hensel_lift_divisibility x
  48. 0048specialize beta_horner_hensel_lift_divisibility x1
  49. 0049apply beta_horner_hensel_lift_divisibility
  50. 0050exact hp
  51. 0051exact hpair
  52. 0052exact hvalue_witness
  53. 0053exact hfactor
  54. 0054exact hroot
  55. 0055exact hcorrection_witness

Separate complete second-wave branches: Full G095 proof · Alpha v27.