PP0029

prime_field_polynomial_horner_functional

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

Every actual modular execution of the same coefficient prefix and base has the same canonical result.

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 expanded first-order arithmetic statement

forall p b c t l r s. (~((p) = 1) /\ forall pfa_factor_left_functional_prime pfa_factor_right_functional_prime. (p) = pfa_factor_left_functional_prime * pfa_factor_right_functional_prime -> pfa_factor_left_functional_prime = 1 \/ pfa_factor_right_functional_prime = 1) -> (exists pfh_trace_code_functional_first pfh_trace_scale_functional_first. (((exists pfa_gap_functional_firsttracebase. pfa_gap_functional_firsttracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_functional_firsttraceinitial. ff_h_pfp_functional_firsttraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttraceinitial. pfh_trace_code_functional_first = ff_q_pfp_functional_firsttraceinitial * S ((S (0)) * pfh_trace_scale_functional_first) + (0))) /\ (((((exists ff_h_pfp_functional_firsttraceterminal. ff_h_pfp_functional_firsttraceterminal + S (r) = S ((S (l)) * pfh_trace_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttraceterminal. pfh_trace_code_functional_first = ff_q_pfp_functional_firsttraceterminal * S ((S (l)) * pfh_trace_scale_functional_first) + (r))) /\ ((forall pfh_index_functional_firsttracesteps. (exists pfa_gap_functional_firsttracestepsindex. pfa_gap_functional_firsttracestepsindex + S (pfh_index_functional_firsttracesteps) = (l)) -> (exists pfh_coefficient_functional_firsttracestepsstep pfh_before_functional_firsttracestepsstep pfh_after_functional_firsttracestepsstep pfh_product_functional_firsttracestepsstep. ((((exists ff_h_pfp_functional_firsttracestepsstepcoefficient. ff_h_pfp_functional_firsttracestepsstepcoefficient + S (pfh_coefficient_functional_firsttracestepsstep) = S ((S (pfh_index_functional_firsttracesteps)) * c)) /\ exists ff_q_pfp_functional_firsttracestepsstepcoefficient. b = ff_q_pfp_functional_firsttracestepsstepcoefficient * S ((S (pfh_index_functional_firsttracesteps)) * c) + (pfh_coefficient_functional_firsttracestepsstep))) /\ (((((exists ff_h_pfp_functional_firsttracestepsstepbefore. ff_h_pfp_functional_firsttracestepsstepbefore + S (pfh_before_functional_firsttracestepsstep) = S ((S (pfh_index_functional_firsttracesteps)) * pfh_trace_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttracestepsstepbefore. pfh_trace_code_functional_first = ff_q_pfp_functional_firsttracestepsstepbefore * S ((S (pfh_index_functional_firsttracesteps)) * pfh_trace_scale_functional_first) + (pfh_before_functional_firsttracestepsstep))) /\ (((((exists ff_h_pfp_functional_firsttracestepsstepafter. ff_h_pfp_functional_firsttracestepsstepafter + S (pfh_after_functional_firsttracestepsstep) = S ((S (S (pfh_index_functional_firsttracesteps))) * pfh_trace_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttracestepsstepafter. pfh_trace_code_functional_first = ff_q_pfp_functional_firsttracestepsstepafter * S ((S (S (pfh_index_functional_firsttracesteps))) * pfh_trace_scale_functional_first) + (pfh_after_functional_firsttracestepsstep))) /\ (((((exists pfa_gap_functional_firsttracestepsstepmultiplyleft. pfa_gap_functional_firsttracestepsstepmultiplyleft + S (pfh_before_functional_firsttracestepsstep) = (p)) /\ (((exists pfa_gap_functional_firsttracestepsstepmultiplyright. pfa_gap_functional_firsttracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_functional_firsttracestepsstepmultiplyresultbound. pfa_gap_functional_firsttracestepsstepmultiplyresultbound + S (pfh_product_functional_firsttracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_firsttracestepsstepmultiplyresultcongruence pfa_offset_right_functional_firsttracestepsstepmultiplyresultcongruence. ((pfh_before_functional_firsttracestepsstep) * (t)) + (p) * pfa_offset_left_functional_firsttracestepsstepmultiplyresultcongruence = (pfh_product_functional_firsttracestepsstep) + (p) * pfa_offset_right_functional_firsttracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_functional_firsttracestepsstepaddleft. pfa_gap_functional_firsttracestepsstepaddleft + S (pfh_product_functional_firsttracestepsstep) = (p)) /\ (((exists pfa_gap_functional_firsttracestepsstepaddright. pfa_gap_functional_firsttracestepsstepaddright + S (pfh_coefficient_functional_firsttracestepsstep) = (p)) /\ ((((exists pfa_gap_functional_firsttracestepsstepaddresultbound. pfa_gap_functional_firsttracestepsstepaddresultbound + S (pfh_after_functional_firsttracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_firsttracestepsstepaddresultcongruence pfa_offset_right_functional_firsttracestepsstepaddresultcongruence. ((pfh_product_functional_firsttracestepsstep) + (pfh_coefficient_functional_firsttracestepsstep)) + (p) * pfa_offset_left_functional_firsttracestepsstepaddresultcongruence = (pfh_after_functional_firsttracestepsstep) + (p) * pfa_offset_right_functional_firsttracestepsstepaddresultcongruence))))))))))))))))))))))))))) -> (exists pfh_trace_code_functional_second pfh_trace_scale_functional_second. (((exists pfa_gap_functional_secondtracebase. pfa_gap_functional_secondtracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_functional_secondtraceinitial. ff_h_pfp_functional_secondtraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtraceinitial. pfh_trace_code_functional_second = ff_q_pfp_functional_secondtraceinitial * S ((S (0)) * pfh_trace_scale_functional_second) + (0))) /\ (((((exists ff_h_pfp_functional_secondtraceterminal. ff_h_pfp_functional_secondtraceterminal + S (s) = S ((S (l)) * pfh_trace_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtraceterminal. pfh_trace_code_functional_second = ff_q_pfp_functional_secondtraceterminal * S ((S (l)) * pfh_trace_scale_functional_second) + (s))) /\ ((forall pfh_index_functional_secondtracesteps. (exists pfa_gap_functional_secondtracestepsindex. pfa_gap_functional_secondtracestepsindex + S (pfh_index_functional_secondtracesteps) = (l)) -> (exists pfh_coefficient_functional_secondtracestepsstep pfh_before_functional_secondtracestepsstep pfh_after_functional_secondtracestepsstep pfh_product_functional_secondtracestepsstep. ((((exists ff_h_pfp_functional_secondtracestepsstepcoefficient. ff_h_pfp_functional_secondtracestepsstepcoefficient + S (pfh_coefficient_functional_secondtracestepsstep) = S ((S (pfh_index_functional_secondtracesteps)) * c)) /\ exists ff_q_pfp_functional_secondtracestepsstepcoefficient. b = ff_q_pfp_functional_secondtracestepsstepcoefficient * S ((S (pfh_index_functional_secondtracesteps)) * c) + (pfh_coefficient_functional_secondtracestepsstep))) /\ (((((exists ff_h_pfp_functional_secondtracestepsstepbefore. ff_h_pfp_functional_secondtracestepsstepbefore + S (pfh_before_functional_secondtracestepsstep) = S ((S (pfh_index_functional_secondtracesteps)) * pfh_trace_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtracestepsstepbefore. pfh_trace_code_functional_second = ff_q_pfp_functional_secondtracestepsstepbefore * S ((S (pfh_index_functional_secondtracesteps)) * pfh_trace_scale_functional_second) + (pfh_before_functional_secondtracestepsstep))) /\ (((((exists ff_h_pfp_functional_secondtracestepsstepafter. ff_h_pfp_functional_secondtracestepsstepafter + S (pfh_after_functional_secondtracestepsstep) = S ((S (S (pfh_index_functional_secondtracesteps))) * pfh_trace_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtracestepsstepafter. pfh_trace_code_functional_second = ff_q_pfp_functional_secondtracestepsstepafter * S ((S (S (pfh_index_functional_secondtracesteps))) * pfh_trace_scale_functional_second) + (pfh_after_functional_secondtracestepsstep))) /\ (((((exists pfa_gap_functional_secondtracestepsstepmultiplyleft. pfa_gap_functional_secondtracestepsstepmultiplyleft + S (pfh_before_functional_secondtracestepsstep) = (p)) /\ (((exists pfa_gap_functional_secondtracestepsstepmultiplyright. pfa_gap_functional_secondtracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_functional_secondtracestepsstepmultiplyresultbound. pfa_gap_functional_secondtracestepsstepmultiplyresultbound + S (pfh_product_functional_secondtracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_secondtracestepsstepmultiplyresultcongruence pfa_offset_right_functional_secondtracestepsstepmultiplyresultcongruence. ((pfh_before_functional_secondtracestepsstep) * (t)) + (p) * pfa_offset_left_functional_secondtracestepsstepmultiplyresultcongruence = (pfh_product_functional_secondtracestepsstep) + (p) * pfa_offset_right_functional_secondtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_functional_secondtracestepsstepaddleft. pfa_gap_functional_secondtracestepsstepaddleft + S (pfh_product_functional_secondtracestepsstep) = (p)) /\ (((exists pfa_gap_functional_secondtracestepsstepaddright. pfa_gap_functional_secondtracestepsstepaddright + S (pfh_coefficient_functional_secondtracestepsstep) = (p)) /\ ((((exists pfa_gap_functional_secondtracestepsstepaddresultbound. pfa_gap_functional_secondtracestepsstepaddresultbound + S (pfh_after_functional_secondtracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_secondtracestepsstepaddresultcongruence pfa_offset_right_functional_secondtracestepsstepaddresultcongruence. ((pfh_product_functional_secondtracestepsstep) + (pfh_coefficient_functional_secondtracestepsstep)) + (p) * pfa_offset_left_functional_secondtracestepsstepaddresultcongruence = (pfh_after_functional_secondtracestepsstep) + (p) * pfa_offset_right_functional_secondtracestepsstepaddresultcongruence))))))))))))))))))))))))))) -> r=s

Constructive proof overview

Generated structural guide

Every actual modular execution of the same coefficient prefix and base has the same canonical result.

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

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

Proof neighborhood

Direct dependencies

beta_horner_eval_exists Alpha theorem; checked-use authorized PP0028 prime_field_polynomial_horner_residue binary_canonical_residue_functional Alpha theorem; checked-use authorized

Direct dependents

PP002A prime_field_polynomial_horner_exists_unique PP002C prime_field_polynomial_horner_successor_construct

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

44 script commands · 6 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.

Named ingredients (1)
prime field polynomial horner residue

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 p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro t
  5. L5
    intro l
  6. L6
    intro r
  7. L7
    intro s
  8. L8
    intro hp
  9. L9
    intro hr
  10. L10
    intro hs
02Establish hnL11–16

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

  1. L11
    have hn : ∃ n. Horner(b,c,t,l,n)Definitions: Horner
  2. L12
    specialize beta_horner_eval_exists (b)
  3. L13
    specialize beta_horner_eval_exists (c)
  4. L14
    specialize beta_horner_eval_exists (t)
  5. L15
    specialize beta_horner_eval_exists (l)
  6. L16
    apply beta_horner_eval_exists
03Separate the logical casesL17–17

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

  1. L17
    cases hn
04Use earlier factsL18–27

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

  1. L18
    specialize binary_canonical_residue_functional (p)
  2. L19
    specialize binary_canonical_residue_functional (x)
  3. L20
    specialize binary_canonical_residue_functional (r)
  4. L21
    specialize binary_canonical_residue_functional (s)
  5. L22
    apply binary_canonical_residue_functional
  6. L23
    specialize prime_field_polynomial_horner_residue (p)
  7. L24
    specialize prime_field_polynomial_horner_residue (b)
  8. L25
    specialize prime_field_polynomial_horner_residue (c)
  9. L26
    specialize prime_field_polynomial_horner_residue (t)
  10. L27
    specialize prime_field_polynomial_horner_residue (l)
05Use earlier factsL28–37

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

  1. L28
    specialize prime_field_polynomial_horner_residue (x)
  2. L29
    specialize prime_field_polynomial_horner_residue (r)
  3. L30
    apply prime_field_polynomial_horner_residue
  4. L31
    exact hp
  5. L32
    exact hn_witness
  6. L33
    exact hr
  7. L34
    specialize prime_field_polynomial_horner_residue (p)
  8. L35
    specialize prime_field_polynomial_horner_residue (b)
  9. L36
    specialize prime_field_polynomial_horner_residue (c)
  10. L37
    specialize prime_field_polynomial_horner_residue (t)
06Use earlier factsL38–44

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

  1. L38
    specialize prime_field_polynomial_horner_residue (l)
  2. L39
    specialize prime_field_polynomial_horner_residue (x)
  3. L40
    specialize prime_field_polynomial_horner_residue (s)
  4. L41
    apply prime_field_polynomial_horner_residue
  5. L42
    exact hp
  6. L43
    exact hn_witness
  7. L44
    exact hs

Library-wide reading audit

Original exact command ledger · 44 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro l
  6. 0006intro r
  7. 0007intro s
  8. 0008intro hp
  9. 0009intro hr
  10. 0010intro hs
  11. 0011have hn : exists n. (exists ff_u_ph_pfh_functional_natural ff_v_ph_pfh_functional_natural. ((((exists fs_h_ph_pfh_functional_natural_body_start. fs_h_ph_pfh_functional_natural_body_start + S (0) = S ((S (0)) * ff_v_ph_pfh_functional_natural)) /\ exists fs_q_ph_pfh_functional_natural_body_start. ff_u_ph_pfh_functional_natural = fs_q_ph_pfh_functional_natural_body_start * S ((S (0)) * ff_v_ph_pfh_functional_natural) + (0))) /\ ((((exists fs_h_ph_pfh_functional_natural_body_terminal. fs_h_ph_pfh_functional_natural_body_terminal + S (n) = S ((S (l)) * ff_v_ph_pfh_functional_natural)) /\ exists fs_q_ph_pfh_functional_natural_body_terminal. ff_u_ph_pfh_functional_natural = fs_q_ph_pfh_functional_natural_body_terminal * S ((S (l)) * ff_v_ph_pfh_functional_natural) + (n))) /\ forall ff_i_ph_pfh_functional_natural_body_steps. (exists ph_bound_pfh_functional_natural_body_steps. ph_bound_pfh_functional_natural_body_steps + S ff_i_ph_pfh_functional_natural_body_steps = l) -> exists ff_coefficient_ph_pfh_functional_natural_body_steps ff_previous_ph_pfh_functional_natural_body_steps ff_current_ph_pfh_functional_natural_body_steps. ((((exists fs_h_ph_pfh_functional_natural_body_steps_coefficient. fs_h_ph_pfh_functional_natural_body_steps_coefficient + S (ff_coefficient_ph_pfh_functional_natural_body_steps) = S ((S (ff_i_ph_pfh_functional_natural_body_steps)) * c)) /\ exists fs_q_ph_pfh_functional_natural_body_steps_coefficient. b = fs_q_ph_pfh_functional_natural_body_steps_coefficient * S ((S (ff_i_ph_pfh_functional_natural_body_steps)) * c) + (ff_coefficient_ph_pfh_functional_natural_body_steps))) /\ ((((exists fs_h_ph_pfh_functional_natural_body_steps_before. fs_h_ph_pfh_functional_natural_body_steps_before + S (ff_previous_ph_pfh_functional_natural_body_steps) = S ((S (ff_i_ph_pfh_functional_natural_body_steps)) * ff_v_ph_pfh_functional_natural)) /\ exists fs_q_ph_pfh_functional_natural_body_steps_before. ff_u_ph_pfh_functional_natural = fs_q_ph_pfh_functional_natural_body_steps_before * S ((S (ff_i_ph_pfh_functional_natural_body_steps)) * ff_v_ph_pfh_functional_natural) + (ff_previous_ph_pfh_functional_natural_body_steps))) /\ ((((exists fs_h_ph_pfh_functional_natural_body_steps_after. fs_h_ph_pfh_functional_natural_body_steps_after + S (ff_current_ph_pfh_functional_natural_body_steps) = S ((S (S ff_i_ph_pfh_functional_natural_body_steps)) * ff_v_ph_pfh_functional_natural)) /\ exists fs_q_ph_pfh_functional_natural_body_steps_after. ff_u_ph_pfh_functional_natural = fs_q_ph_pfh_functional_natural_body_steps_after * S ((S (S ff_i_ph_pfh_functional_natural_body_steps)) * ff_v_ph_pfh_functional_natural) + (ff_current_ph_pfh_functional_natural_body_steps))) /\ ff_current_ph_pfh_functional_natural_body_steps = ff_previous_ph_pfh_functional_natural_body_steps * t + ff_coefficient_ph_pfh_functional_natural_body_steps))))))
  12. 0012specialize beta_horner_eval_exists (b)
  13. 0013specialize beta_horner_eval_exists (c)
  14. 0014specialize beta_horner_eval_exists (t)
  15. 0015specialize beta_horner_eval_exists (l)
  16. 0016apply beta_horner_eval_exists
  17. 0017cases hn
  18. 0018specialize binary_canonical_residue_functional (p)
  19. 0019specialize binary_canonical_residue_functional (x)
  20. 0020specialize binary_canonical_residue_functional (r)
  21. 0021specialize binary_canonical_residue_functional (s)
  22. 0022apply binary_canonical_residue_functional
  23. 0023specialize prime_field_polynomial_horner_residue (p)
  24. 0024specialize prime_field_polynomial_horner_residue (b)
  25. 0025specialize prime_field_polynomial_horner_residue (c)
  26. 0026specialize prime_field_polynomial_horner_residue (t)
  27. 0027specialize prime_field_polynomial_horner_residue (l)
  28. 0028specialize prime_field_polynomial_horner_residue (x)
  29. 0029specialize prime_field_polynomial_horner_residue (r)
  30. 0030apply prime_field_polynomial_horner_residue
  31. 0031exact hp
  32. 0032exact hn_witness
  33. 0033exact hr
  34. 0034specialize prime_field_polynomial_horner_residue (p)
  35. 0035specialize prime_field_polynomial_horner_residue (b)
  36. 0036specialize prime_field_polynomial_horner_residue (c)
  37. 0037specialize prime_field_polynomial_horner_residue (t)
  38. 0038specialize prime_field_polynomial_horner_residue (l)
  39. 0039specialize prime_field_polynomial_horner_residue (x)
  40. 0040specialize prime_field_polynomial_horner_residue (s)
  41. 0041apply prime_field_polynomial_horner_residue
  42. 0042exact hp
  43. 0043exact hn_witness
  44. 0044exact hs