TH0004

beta_horner_eval_mod_congruence

Every arbitrary beta-coded natural polynomial preserves balanced congruence between evaluation points.

Alpha v34 checked-use · first admitted v25 · 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.

Historical partial components only: this chapter proves exact natural polynomial Taylor remainders, bounded corrections, and one-step divisibility lifts. G095 is now closed in the separate Alpha-v27 hensel-lifting branch for integer polynomials, unrestricted input roots, unique canonical representatives, and every positive prime power. Full G095 proof · Alpha v27

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ m. ∀ t. ∀ s. ∀ l. ∀ n. ∀ z. ModEq(m,t,s) → Horner(b,c,t,l,n) → Horner(b,c,s,l,z) → ModEq(m,n,z)

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

Definition DAG

Horner(b,c,x,ell,z) · 2ModEq(m,a,b) · 2

Actual proof prerequisites

beta_horner_eval_empty · checked external prerequisitebeta_horner_eval_successor_decompose · checked external prerequisitebeta_at_unique · checked external prerequisitemod_eq_refl · checked external prerequisitehorner_mod_congruence_successor_step
Original expanded first-order statement 
forall b c m t s l n z. (exists hgcrt_mod_left_pth_eval_base hgcrt_mod_right_pth_eval_base. t + m * hgcrt_mod_left_pth_eval_base = s + m * hgcrt_mod_right_pth_eval_base) -> (exists ff_u_ph_pth_eval_left ff_v_ph_pth_eval_left. ((((exists fs_h_ph_pth_eval_left_body_start. fs_h_ph_pth_eval_left_body_start + S (0) = S ((S (0)) * ff_v_ph_pth_eval_left)) /\ exists fs_q_ph_pth_eval_left_body_start. ff_u_ph_pth_eval_left = fs_q_ph_pth_eval_left_body_start * S ((S (0)) * ff_v_ph_pth_eval_left) + (0))) /\ ((((exists fs_h_ph_pth_eval_left_body_terminal. fs_h_ph_pth_eval_left_body_terminal + S (n) = S ((S (l)) * ff_v_ph_pth_eval_left)) /\ exists fs_q_ph_pth_eval_left_body_terminal. ff_u_ph_pth_eval_left = fs_q_ph_pth_eval_left_body_terminal * S ((S (l)) * ff_v_ph_pth_eval_left) + (n))) /\ forall ff_i_ph_pth_eval_left_body_steps. (exists ph_bound_pth_eval_left_body_steps. ph_bound_pth_eval_left_body_steps + S ff_i_ph_pth_eval_left_body_steps = l) -> exists ff_coefficient_ph_pth_eval_left_body_steps ff_previous_ph_pth_eval_left_body_steps ff_current_ph_pth_eval_left_body_steps. ((((exists fs_h_ph_pth_eval_left_body_steps_coefficient. fs_h_ph_pth_eval_left_body_steps_coefficient + S (ff_coefficient_ph_pth_eval_left_body_steps) = S ((S (ff_i_ph_pth_eval_left_body_steps)) * c)) /\ exists fs_q_ph_pth_eval_left_body_steps_coefficient. b = fs_q_ph_pth_eval_left_body_steps_coefficient * S ((S (ff_i_ph_pth_eval_left_body_steps)) * c) + (ff_coefficient_ph_pth_eval_left_body_steps))) /\ ((((exists fs_h_ph_pth_eval_left_body_steps_before. fs_h_ph_pth_eval_left_body_steps_before + S (ff_previous_ph_pth_eval_left_body_steps) = S ((S (ff_i_ph_pth_eval_left_body_steps)) * ff_v_ph_pth_eval_left)) /\ exists fs_q_ph_pth_eval_left_body_steps_before. ff_u_ph_pth_eval_left = fs_q_ph_pth_eval_left_body_steps_before * S ((S (ff_i_ph_pth_eval_left_body_steps)) * ff_v_ph_pth_eval_left) + (ff_previous_ph_pth_eval_left_body_steps))) /\ ((((exists fs_h_ph_pth_eval_left_body_steps_after. fs_h_ph_pth_eval_left_body_steps_after + S (ff_current_ph_pth_eval_left_body_steps) = S ((S (S ff_i_ph_pth_eval_left_body_steps)) * ff_v_ph_pth_eval_left)) /\ exists fs_q_ph_pth_eval_left_body_steps_after. ff_u_ph_pth_eval_left = fs_q_ph_pth_eval_left_body_steps_after * S ((S (S ff_i_ph_pth_eval_left_body_steps)) * ff_v_ph_pth_eval_left) + (ff_current_ph_pth_eval_left_body_steps))) /\ ff_current_ph_pth_eval_left_body_steps = ff_previous_ph_pth_eval_left_body_steps * t + ff_coefficient_ph_pth_eval_left_body_steps)))))) -> (exists ff_u_ph_pth_eval_right ff_v_ph_pth_eval_right. ((((exists fs_h_ph_pth_eval_right_body_start. fs_h_ph_pth_eval_right_body_start + S (0) = S ((S (0)) * ff_v_ph_pth_eval_right)) /\ exists fs_q_ph_pth_eval_right_body_start. ff_u_ph_pth_eval_right = fs_q_ph_pth_eval_right_body_start * S ((S (0)) * ff_v_ph_pth_eval_right) + (0))) /\ ((((exists fs_h_ph_pth_eval_right_body_terminal. fs_h_ph_pth_eval_right_body_terminal + S (z) = S ((S (l)) * ff_v_ph_pth_eval_right)) /\ exists fs_q_ph_pth_eval_right_body_terminal. ff_u_ph_pth_eval_right = fs_q_ph_pth_eval_right_body_terminal * S ((S (l)) * ff_v_ph_pth_eval_right) + (z))) /\ forall ff_i_ph_pth_eval_right_body_steps. (exists ph_bound_pth_eval_right_body_steps. ph_bound_pth_eval_right_body_steps + S ff_i_ph_pth_eval_right_body_steps = l) -> exists ff_coefficient_ph_pth_eval_right_body_steps ff_previous_ph_pth_eval_right_body_steps ff_current_ph_pth_eval_right_body_steps. ((((exists fs_h_ph_pth_eval_right_body_steps_coefficient. fs_h_ph_pth_eval_right_body_steps_coefficient + S (ff_coefficient_ph_pth_eval_right_body_steps) = S ((S (ff_i_ph_pth_eval_right_body_steps)) * c)) /\ exists fs_q_ph_pth_eval_right_body_steps_coefficient. b = fs_q_ph_pth_eval_right_body_steps_coefficient * S ((S (ff_i_ph_pth_eval_right_body_steps)) * c) + (ff_coefficient_ph_pth_eval_right_body_steps))) /\ ((((exists fs_h_ph_pth_eval_right_body_steps_before. fs_h_ph_pth_eval_right_body_steps_before + S (ff_previous_ph_pth_eval_right_body_steps) = S ((S (ff_i_ph_pth_eval_right_body_steps)) * ff_v_ph_pth_eval_right)) /\ exists fs_q_ph_pth_eval_right_body_steps_before. ff_u_ph_pth_eval_right = fs_q_ph_pth_eval_right_body_steps_before * S ((S (ff_i_ph_pth_eval_right_body_steps)) * ff_v_ph_pth_eval_right) + (ff_previous_ph_pth_eval_right_body_steps))) /\ ((((exists fs_h_ph_pth_eval_right_body_steps_after. fs_h_ph_pth_eval_right_body_steps_after + S (ff_current_ph_pth_eval_right_body_steps) = S ((S (S ff_i_ph_pth_eval_right_body_steps)) * ff_v_ph_pth_eval_right)) /\ exists fs_q_ph_pth_eval_right_body_steps_after. ff_u_ph_pth_eval_right = fs_q_ph_pth_eval_right_body_steps_after * S ((S (S ff_i_ph_pth_eval_right_body_steps)) * ff_v_ph_pth_eval_right) + (ff_current_ph_pth_eval_right_body_steps))) /\ ff_current_ph_pth_eval_right_body_steps = ff_previous_ph_pth_eval_right_body_steps * s + ff_coefficient_ph_pth_eval_right_body_steps)))))) -> (exists hgcrt_mod_left_pth_eval_result hgcrt_mod_right_pth_eval_result. n + m * hgcrt_mod_left_pth_eval_result = z + m * hgcrt_mod_right_pth_eval_result)

Complete unchanged native tactic proof

All 89 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

89 script commands · 15 reading checkpoints · 7 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 (1)
horner mod congruence successor step

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

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro m
  4. L4
    intro t
  5. L5
    intro s
02Induction on lL6–11

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L6
    induction l
  2. L7
    intro n
  3. L8
    intro z
  4. L9
    intro hbase
  5. L10
    intro hleft
  6. L11
    intro hright
03Establish hzero_leftL12–18

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

  1. L12
    have hzero_left : n = 0
  2. L13
    specialize beta_horner_eval_empty b
  3. L14
    specialize beta_horner_eval_empty c
  4. L15
    specialize beta_horner_eval_empty t
  5. L16
    specialize beta_horner_eval_empty n
  6. L17
    apply beta_horner_eval_empty
  7. L18
    exact hleft
04Establish hzero_rightL19–28

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

  1. L19
    have hzero_right : z = 0
  2. L20
    specialize beta_horner_eval_empty b
  3. L21
    specialize beta_horner_eval_empty c
  4. L22
    specialize beta_horner_eval_empty s
  5. L23
    specialize beta_horner_eval_empty z
  6. L24
    apply beta_horner_eval_empty
  7. L25
    exact hright
  8. L26
    rewrite hzero_left
  9. L27
    rewrite hzero_right
  10. L28
    specialize mod_eq_refl m
05Use earlier factsL29–30

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

  1. L29
    specialize mod_eq_refl 0
  2. L30
    apply mod_eq_refl
06Fix variables and assumptionsL31–35

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

  1. L31
    intro n
  2. L32
    intro z
  3. L33
    intro hbase
  4. L34
    intro hleft
  5. L35
    intro hright
07Establish hfirstL36–43

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

  1. L36
    have hfirst : ∃ a. ∃ r. Beta(b,c,l,a) ∧ (Horner(b,c,t,l,r) ∧ n = r · t + a)Definitions: BetaHornerOriginal native command in the exact edition
  2. L37
    specialize beta_horner_eval_successor_decompose b
  3. L38
    specialize beta_horner_eval_successor_decompose c
  4. L39
    specialize beta_horner_eval_successor_decompose t
  5. L40
    specialize beta_horner_eval_successor_decompose l
  6. L41
    specialize beta_horner_eval_successor_decompose n
  7. L42
    apply beta_horner_eval_successor_decompose
  8. L43
    exact hleft
08Separate the logical casesL44–47

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

  1. L44
    cases hfirst
  2. L45
    cases hfirst_witness
  3. L46
    cases hfirst_witness_witness
  4. L47
    cases hfirst_witness_witness_right
09Establish hsecondL48–55

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

  1. L48
    have hsecond : ∃ a. ∃ r. Beta(b,c,l,a) ∧ (Horner(b,c,s,l,r) ∧ z = r · s + a)Definitions: BetaHornerOriginal native command in the exact edition
  2. L49
    specialize beta_horner_eval_successor_decompose b
  3. L50
    specialize beta_horner_eval_successor_decompose c
  4. L51
    specialize beta_horner_eval_successor_decompose s
  5. L52
    specialize beta_horner_eval_successor_decompose l
  6. L53
    specialize beta_horner_eval_successor_decompose z
  7. L54
    apply beta_horner_eval_successor_decompose
  8. L55
    exact hright
10Separate the logical casesL56–59

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

  1. L56
    cases hsecond
  2. L57
    cases hsecond_witness
  3. L58
    cases hsecond_witness_witness
  4. L59
    cases hsecond_witness_witness_right
11Establish hcoefficientL60–68

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

  1. L60
    have hcoefficient : x = x2
  2. L61
    specialize beta_at_unique b
  3. L62
    specialize beta_at_unique c
  4. L63
    specialize beta_at_unique l
  5. L64
    specialize beta_at_unique x
  6. L65
    specialize beta_at_unique x2
  7. L66
    apply beta_at_unique
  8. L67
    exact hfirst_witness_witness_left
  9. L68
    exact hsecond_witness_witness_left
12Establish hprefixL69–75

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

  1. L69
    have hprefix : exists hgcrt_mod_left_pth_eval_prefix hgcrt_mod_right_pth_eval_prefix. x1 + m * hgcrt_mod_left_pth_eval_prefix = x3 + m * hgcrt_mod_right_pth_eval_prefix
  2. L70
    specialize IH x1
  3. L71
    specialize IH x3
  4. L72
    apply IH
  5. L73
    exact hbase
  6. L74
    exact hfirst_witness_witness_right_left
  7. L75
    exact hsecond_witness_witness_right_left
13Establish hstepL76–85

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply horner mod congruence successor step.

  1. L76
    have hstep : exists hgcrt_mod_left_pth_eval_step hgcrt_mod_right_pth_eval_step. (x1 * t + x) + m * hgcrt_mod_left_pth_eval_step = (x3 * s + x) + m * hgcrt_mod_right_pth_eval_step
  2. L77
    specialize horner_mod_congruence_successor_step m
  3. L78
    specialize horner_mod_congruence_successor_step t
  4. L79
    specialize horner_mod_congruence_successor_step s
  5. L80
    specialize horner_mod_congruence_successor_step x1
  6. L81
    specialize horner_mod_congruence_successor_step x3
  7. L82
    specialize horner_mod_congruence_successor_step x
  8. L83
    apply horner_mod_congruence_successor_step
  9. L84
    exact hbase
  10. L85
    exact hprefix
14Calculate and transport equalitiesL86–88

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

  1. L86
    rewrite hfirst_witness_witness_right_right
  2. L87
    rewrite hsecond_witness_witness_right_right
  3. L88
    rewrite <- hcoefficient
15Use earlier factsL89–89

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

  1. L89
    exact hstep

Library-wide reading audit

Original defined command ledger · 89 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro m
  4. 0004intro t
  5. 0005intro s
  6. 0006induction l
  7. 0007intro n
  8. 0008intro z
  9. 0009intro hbase
  10. 0010intro hleft
  11. 0011intro hright
  12. 0012have hzero_left : n = 0
  13. 0013specialize beta_horner_eval_empty b
  14. 0014specialize beta_horner_eval_empty c
  15. 0015specialize beta_horner_eval_empty t
  16. 0016specialize beta_horner_eval_empty n
  17. 0017apply beta_horner_eval_empty
  18. 0018exact hleft
  19. 0019have hzero_right : z = 0
  20. 0020specialize beta_horner_eval_empty b
  21. 0021specialize beta_horner_eval_empty c
  22. 0022specialize beta_horner_eval_empty s
  23. 0023specialize beta_horner_eval_empty z
  24. 0024apply beta_horner_eval_empty
  25. 0025exact hright
  26. 0026rewrite hzero_left
  27. 0027rewrite hzero_right
  28. 0028specialize mod_eq_refl m
  29. 0029specialize mod_eq_refl 0
  30. 0030apply mod_eq_refl
  31. 0031intro n
  32. 0032intro z
  33. 0033intro hbase
  34. 0034intro hleft
  35. 0035intro hright
  36. 0036have hfirst : exists a r. ((((exists fs_h_pth_eval_first_coefficient. fs_h_pth_eval_first_coefficient + S (a) = S ((S (l)) * c)) /\ exists fs_q_pth_eval_first_coefficient. b = fs_q_pth_eval_first_coefficient * S ((S (l)) * c) + (a))) /\ ((exists ff_u_ph_pth_eval_first_prefix ff_v_ph_pth_eval_first_prefix. ((((exists fs_h_ph_pth_eval_first_prefix_body_start. fs_h_ph_pth_eval_first_prefix_body_start + S (0) = S ((S (0)) * ff_v_ph_pth_eval_first_prefix)) /\ exists fs_q_ph_pth_eval_first_prefix_body_start. ff_u_ph_pth_eval_first_prefix = fs_q_ph_pth_eval_first_prefix_body_start * S ((S (0)) * ff_v_ph_pth_eval_first_prefix) + (0))) /\ ((((exists fs_h_ph_pth_eval_first_prefix_body_terminal. fs_h_ph_pth_eval_first_prefix_body_terminal + S (r) = S ((S (l)) * ff_v_ph_pth_eval_first_prefix)) /\ exists fs_q_ph_pth_eval_first_prefix_body_terminal. ff_u_ph_pth_eval_first_prefix = fs_q_ph_pth_eval_first_prefix_body_terminal * S ((S (l)) * ff_v_ph_pth_eval_first_prefix) + (r))) /\ forall ff_i_ph_pth_eval_first_prefix_body_steps. (exists ph_bound_pth_eval_first_prefix_body_steps. ph_bound_pth_eval_first_prefix_body_steps + S ff_i_ph_pth_eval_first_prefix_body_steps = l) -> exists ff_coefficient_ph_pth_eval_first_prefix_body_steps ff_previous_ph_pth_eval_first_prefix_body_steps ff_current_ph_pth_eval_first_prefix_body_steps. ((((exists fs_h_ph_pth_eval_first_prefix_body_steps_coefficient. fs_h_ph_pth_eval_first_prefix_body_steps_coefficient + S (ff_coefficient_ph_pth_eval_first_prefix_body_steps) = S ((S (ff_i_ph_pth_eval_first_prefix_body_steps)) * c)) /\ exists fs_q_ph_pth_eval_first_prefix_body_steps_coefficient. b = fs_q_ph_pth_eval_first_prefix_body_steps_coefficient * S ((S (ff_i_ph_pth_eval_first_prefix_body_steps)) * c) + (ff_coefficient_ph_pth_eval_first_prefix_body_steps))) /\ ((((exists fs_h_ph_pth_eval_first_prefix_body_steps_before. fs_h_ph_pth_eval_first_prefix_body_steps_before + S (ff_previous_ph_pth_eval_first_prefix_body_steps) = S ((S (ff_i_ph_pth_eval_first_prefix_body_steps)) * ff_v_ph_pth_eval_first_prefix)) /\ exists fs_q_ph_pth_eval_first_prefix_body_steps_before. ff_u_ph_pth_eval_first_prefix = fs_q_ph_pth_eval_first_prefix_body_steps_before * S ((S (ff_i_ph_pth_eval_first_prefix_body_steps)) * ff_v_ph_pth_eval_first_prefix) + (ff_previous_ph_pth_eval_first_prefix_body_steps))) /\ ((((exists fs_h_ph_pth_eval_first_prefix_body_steps_after. fs_h_ph_pth_eval_first_prefix_body_steps_after + S (ff_current_ph_pth_eval_first_prefix_body_steps) = S ((S (S ff_i_ph_pth_eval_first_prefix_body_steps)) * ff_v_ph_pth_eval_first_prefix)) /\ exists fs_q_ph_pth_eval_first_prefix_body_steps_after. ff_u_ph_pth_eval_first_prefix = fs_q_ph_pth_eval_first_prefix_body_steps_after * S ((S (S ff_i_ph_pth_eval_first_prefix_body_steps)) * ff_v_ph_pth_eval_first_prefix) + (ff_current_ph_pth_eval_first_prefix_body_steps))) /\ ff_current_ph_pth_eval_first_prefix_body_steps = ff_previous_ph_pth_eval_first_prefix_body_steps * t + ff_coefficient_ph_pth_eval_first_prefix_body_steps)))))) /\ n = r * t + a))
  37. 0037specialize beta_horner_eval_successor_decompose b
  38. 0038specialize beta_horner_eval_successor_decompose c
  39. 0039specialize beta_horner_eval_successor_decompose t
  40. 0040specialize beta_horner_eval_successor_decompose l
  41. 0041specialize beta_horner_eval_successor_decompose n
  42. 0042apply beta_horner_eval_successor_decompose
  43. 0043exact hleft
  44. 0044cases hfirst
  45. 0045cases hfirst_witness
  46. 0046cases hfirst_witness_witness
  47. 0047cases hfirst_witness_witness_right
  48. 0048have hsecond : exists a r. ((((exists fs_h_pth_eval_second_coefficient. fs_h_pth_eval_second_coefficient + S (a) = S ((S (l)) * c)) /\ exists fs_q_pth_eval_second_coefficient. b = fs_q_pth_eval_second_coefficient * S ((S (l)) * c) + (a))) /\ ((exists ff_u_ph_pth_eval_second_prefix ff_v_ph_pth_eval_second_prefix. ((((exists fs_h_ph_pth_eval_second_prefix_body_start. fs_h_ph_pth_eval_second_prefix_body_start + S (0) = S ((S (0)) * ff_v_ph_pth_eval_second_prefix)) /\ exists fs_q_ph_pth_eval_second_prefix_body_start. ff_u_ph_pth_eval_second_prefix = fs_q_ph_pth_eval_second_prefix_body_start * S ((S (0)) * ff_v_ph_pth_eval_second_prefix) + (0))) /\ ((((exists fs_h_ph_pth_eval_second_prefix_body_terminal. fs_h_ph_pth_eval_second_prefix_body_terminal + S (r) = S ((S (l)) * ff_v_ph_pth_eval_second_prefix)) /\ exists fs_q_ph_pth_eval_second_prefix_body_terminal. ff_u_ph_pth_eval_second_prefix = fs_q_ph_pth_eval_second_prefix_body_terminal * S ((S (l)) * ff_v_ph_pth_eval_second_prefix) + (r))) /\ forall ff_i_ph_pth_eval_second_prefix_body_steps. (exists ph_bound_pth_eval_second_prefix_body_steps. ph_bound_pth_eval_second_prefix_body_steps + S ff_i_ph_pth_eval_second_prefix_body_steps = l) -> exists ff_coefficient_ph_pth_eval_second_prefix_body_steps ff_previous_ph_pth_eval_second_prefix_body_steps ff_current_ph_pth_eval_second_prefix_body_steps. ((((exists fs_h_ph_pth_eval_second_prefix_body_steps_coefficient. fs_h_ph_pth_eval_second_prefix_body_steps_coefficient + S (ff_coefficient_ph_pth_eval_second_prefix_body_steps) = S ((S (ff_i_ph_pth_eval_second_prefix_body_steps)) * c)) /\ exists fs_q_ph_pth_eval_second_prefix_body_steps_coefficient. b = fs_q_ph_pth_eval_second_prefix_body_steps_coefficient * S ((S (ff_i_ph_pth_eval_second_prefix_body_steps)) * c) + (ff_coefficient_ph_pth_eval_second_prefix_body_steps))) /\ ((((exists fs_h_ph_pth_eval_second_prefix_body_steps_before. fs_h_ph_pth_eval_second_prefix_body_steps_before + S (ff_previous_ph_pth_eval_second_prefix_body_steps) = S ((S (ff_i_ph_pth_eval_second_prefix_body_steps)) * ff_v_ph_pth_eval_second_prefix)) /\ exists fs_q_ph_pth_eval_second_prefix_body_steps_before. ff_u_ph_pth_eval_second_prefix = fs_q_ph_pth_eval_second_prefix_body_steps_before * S ((S (ff_i_ph_pth_eval_second_prefix_body_steps)) * ff_v_ph_pth_eval_second_prefix) + (ff_previous_ph_pth_eval_second_prefix_body_steps))) /\ ((((exists fs_h_ph_pth_eval_second_prefix_body_steps_after. fs_h_ph_pth_eval_second_prefix_body_steps_after + S (ff_current_ph_pth_eval_second_prefix_body_steps) = S ((S (S ff_i_ph_pth_eval_second_prefix_body_steps)) * ff_v_ph_pth_eval_second_prefix)) /\ exists fs_q_ph_pth_eval_second_prefix_body_steps_after. ff_u_ph_pth_eval_second_prefix = fs_q_ph_pth_eval_second_prefix_body_steps_after * S ((S (S ff_i_ph_pth_eval_second_prefix_body_steps)) * ff_v_ph_pth_eval_second_prefix) + (ff_current_ph_pth_eval_second_prefix_body_steps))) /\ ff_current_ph_pth_eval_second_prefix_body_steps = ff_previous_ph_pth_eval_second_prefix_body_steps * s + ff_coefficient_ph_pth_eval_second_prefix_body_steps)))))) /\ z = r * s + a))
  49. 0049specialize beta_horner_eval_successor_decompose b
  50. 0050specialize beta_horner_eval_successor_decompose c
  51. 0051specialize beta_horner_eval_successor_decompose s
  52. 0052specialize beta_horner_eval_successor_decompose l
  53. 0053specialize beta_horner_eval_successor_decompose z
  54. 0054apply beta_horner_eval_successor_decompose
  55. 0055exact hright
  56. 0056cases hsecond
  57. 0057cases hsecond_witness
  58. 0058cases hsecond_witness_witness
  59. 0059cases hsecond_witness_witness_right
  60. 0060have hcoefficient : x = x2
  61. 0061specialize beta_at_unique b
  62. 0062specialize beta_at_unique c
  63. 0063specialize beta_at_unique l
  64. 0064specialize beta_at_unique x
  65. 0065specialize beta_at_unique x2
  66. 0066apply beta_at_unique
  67. 0067exact hfirst_witness_witness_left
  68. 0068exact hsecond_witness_witness_left
  69. 0069have hprefix : exists hgcrt_mod_left_pth_eval_prefix hgcrt_mod_right_pth_eval_prefix. x1 + m * hgcrt_mod_left_pth_eval_prefix = x3 + m * hgcrt_mod_right_pth_eval_prefix
  70. 0070specialize IH x1
  71. 0071specialize IH x3
  72. 0072apply IH
  73. 0073exact hbase
  74. 0074exact hfirst_witness_witness_right_left
  75. 0075exact hsecond_witness_witness_right_left
  76. 0076have hstep : exists hgcrt_mod_left_pth_eval_step hgcrt_mod_right_pth_eval_step. (x1 * t + x) + m * hgcrt_mod_left_pth_eval_step = (x3 * s + x) + m * hgcrt_mod_right_pth_eval_step
  77. 0077specialize horner_mod_congruence_successor_step m
  78. 0078specialize horner_mod_congruence_successor_step t
  79. 0079specialize horner_mod_congruence_successor_step s
  80. 0080specialize horner_mod_congruence_successor_step x1
  81. 0081specialize horner_mod_congruence_successor_step x3
  82. 0082specialize horner_mod_congruence_successor_step x
  83. 0083apply horner_mod_congruence_successor_step
  84. 0084exact hbase
  85. 0085exact hprefix
  86. 0086rewrite hfirst_witness_witness_right_right
  87. 0087rewrite hsecond_witness_witness_right_right
  88. 0088rewrite <- hcoefficient
  89. 0089exact hstep