PP0028

prime_field_polynomial_horner_residue

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

Actual modular evaluation has exactly the canonical residue of the existing natural T12 Horner value.

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 n r. (~((p) = 1) /\ forall pfa_factor_left_residue_prime pfa_factor_right_residue_prime. (p) = pfa_factor_left_residue_prime * pfa_factor_right_residue_prime -> pfa_factor_left_residue_prime = 1 \/ pfa_factor_right_residue_prime = 1) -> (exists ff_u_ph_pfh_residue_natural ff_v_ph_pfh_residue_natural. ((((exists fs_h_ph_pfh_residue_natural_body_start. fs_h_ph_pfh_residue_natural_body_start + S (0) = S ((S (0)) * ff_v_ph_pfh_residue_natural)) /\ exists fs_q_ph_pfh_residue_natural_body_start. ff_u_ph_pfh_residue_natural = fs_q_ph_pfh_residue_natural_body_start * S ((S (0)) * ff_v_ph_pfh_residue_natural) + (0))) /\ ((((exists fs_h_ph_pfh_residue_natural_body_terminal. fs_h_ph_pfh_residue_natural_body_terminal + S (n) = S ((S (l)) * ff_v_ph_pfh_residue_natural)) /\ exists fs_q_ph_pfh_residue_natural_body_terminal. ff_u_ph_pfh_residue_natural = fs_q_ph_pfh_residue_natural_body_terminal * S ((S (l)) * ff_v_ph_pfh_residue_natural) + (n))) /\ forall ff_i_ph_pfh_residue_natural_body_steps. (exists ph_bound_pfh_residue_natural_body_steps. ph_bound_pfh_residue_natural_body_steps + S ff_i_ph_pfh_residue_natural_body_steps = l) -> exists ff_coefficient_ph_pfh_residue_natural_body_steps ff_previous_ph_pfh_residue_natural_body_steps ff_current_ph_pfh_residue_natural_body_steps. ((((exists fs_h_ph_pfh_residue_natural_body_steps_coefficient. fs_h_ph_pfh_residue_natural_body_steps_coefficient + S (ff_coefficient_ph_pfh_residue_natural_body_steps) = S ((S (ff_i_ph_pfh_residue_natural_body_steps)) * c)) /\ exists fs_q_ph_pfh_residue_natural_body_steps_coefficient. b = fs_q_ph_pfh_residue_natural_body_steps_coefficient * S ((S (ff_i_ph_pfh_residue_natural_body_steps)) * c) + (ff_coefficient_ph_pfh_residue_natural_body_steps))) /\ ((((exists fs_h_ph_pfh_residue_natural_body_steps_before. fs_h_ph_pfh_residue_natural_body_steps_before + S (ff_previous_ph_pfh_residue_natural_body_steps) = S ((S (ff_i_ph_pfh_residue_natural_body_steps)) * ff_v_ph_pfh_residue_natural)) /\ exists fs_q_ph_pfh_residue_natural_body_steps_before. ff_u_ph_pfh_residue_natural = fs_q_ph_pfh_residue_natural_body_steps_before * S ((S (ff_i_ph_pfh_residue_natural_body_steps)) * ff_v_ph_pfh_residue_natural) + (ff_previous_ph_pfh_residue_natural_body_steps))) /\ ((((exists fs_h_ph_pfh_residue_natural_body_steps_after. fs_h_ph_pfh_residue_natural_body_steps_after + S (ff_current_ph_pfh_residue_natural_body_steps) = S ((S (S ff_i_ph_pfh_residue_natural_body_steps)) * ff_v_ph_pfh_residue_natural)) /\ exists fs_q_ph_pfh_residue_natural_body_steps_after. ff_u_ph_pfh_residue_natural = fs_q_ph_pfh_residue_natural_body_steps_after * S ((S (S ff_i_ph_pfh_residue_natural_body_steps)) * ff_v_ph_pfh_residue_natural) + (ff_current_ph_pfh_residue_natural_body_steps))) /\ ff_current_ph_pfh_residue_natural_body_steps = ff_previous_ph_pfh_residue_natural_body_steps * t + ff_coefficient_ph_pfh_residue_natural_body_steps)))))) -> (exists pfh_trace_code_residue_execution pfh_trace_scale_residue_execution. (((exists pfa_gap_residue_executiontracebase. pfa_gap_residue_executiontracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_residue_executiontraceinitial. ff_h_pfp_residue_executiontraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_residue_execution)) /\ exists ff_q_pfp_residue_executiontraceinitial. pfh_trace_code_residue_execution = ff_q_pfp_residue_executiontraceinitial * S ((S (0)) * pfh_trace_scale_residue_execution) + (0))) /\ (((((exists ff_h_pfp_residue_executiontraceterminal. ff_h_pfp_residue_executiontraceterminal + S (r) = S ((S (l)) * pfh_trace_scale_residue_execution)) /\ exists ff_q_pfp_residue_executiontraceterminal. pfh_trace_code_residue_execution = ff_q_pfp_residue_executiontraceterminal * S ((S (l)) * pfh_trace_scale_residue_execution) + (r))) /\ ((forall pfh_index_residue_executiontracesteps. (exists pfa_gap_residue_executiontracestepsindex. pfa_gap_residue_executiontracestepsindex + S (pfh_index_residue_executiontracesteps) = (l)) -> (exists pfh_coefficient_residue_executiontracestepsstep pfh_before_residue_executiontracestepsstep pfh_after_residue_executiontracestepsstep pfh_product_residue_executiontracestepsstep. ((((exists ff_h_pfp_residue_executiontracestepsstepcoefficient. ff_h_pfp_residue_executiontracestepsstepcoefficient + S (pfh_coefficient_residue_executiontracestepsstep) = S ((S (pfh_index_residue_executiontracesteps)) * c)) /\ exists ff_q_pfp_residue_executiontracestepsstepcoefficient. b = ff_q_pfp_residue_executiontracestepsstepcoefficient * S ((S (pfh_index_residue_executiontracesteps)) * c) + (pfh_coefficient_residue_executiontracestepsstep))) /\ (((((exists ff_h_pfp_residue_executiontracestepsstepbefore. ff_h_pfp_residue_executiontracestepsstepbefore + S (pfh_before_residue_executiontracestepsstep) = S ((S (pfh_index_residue_executiontracesteps)) * pfh_trace_scale_residue_execution)) /\ exists ff_q_pfp_residue_executiontracestepsstepbefore. pfh_trace_code_residue_execution = ff_q_pfp_residue_executiontracestepsstepbefore * S ((S (pfh_index_residue_executiontracesteps)) * pfh_trace_scale_residue_execution) + (pfh_before_residue_executiontracestepsstep))) /\ (((((exists ff_h_pfp_residue_executiontracestepsstepafter. ff_h_pfp_residue_executiontracestepsstepafter + S (pfh_after_residue_executiontracestepsstep) = S ((S (S (pfh_index_residue_executiontracesteps))) * pfh_trace_scale_residue_execution)) /\ exists ff_q_pfp_residue_executiontracestepsstepafter. pfh_trace_code_residue_execution = ff_q_pfp_residue_executiontracestepsstepafter * S ((S (S (pfh_index_residue_executiontracesteps))) * pfh_trace_scale_residue_execution) + (pfh_after_residue_executiontracestepsstep))) /\ (((((exists pfa_gap_residue_executiontracestepsstepmultiplyleft. pfa_gap_residue_executiontracestepsstepmultiplyleft + S (pfh_before_residue_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_residue_executiontracestepsstepmultiplyright. pfa_gap_residue_executiontracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_residue_executiontracestepsstepmultiplyresultbound. pfa_gap_residue_executiontracestepsstepmultiplyresultbound + S (pfh_product_residue_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_residue_executiontracestepsstepmultiplyresultcongruence pfa_offset_right_residue_executiontracestepsstepmultiplyresultcongruence. ((pfh_before_residue_executiontracestepsstep) * (t)) + (p) * pfa_offset_left_residue_executiontracestepsstepmultiplyresultcongruence = (pfh_product_residue_executiontracestepsstep) + (p) * pfa_offset_right_residue_executiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_residue_executiontracestepsstepaddleft. pfa_gap_residue_executiontracestepsstepaddleft + S (pfh_product_residue_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_residue_executiontracestepsstepaddright. pfa_gap_residue_executiontracestepsstepaddright + S (pfh_coefficient_residue_executiontracestepsstep) = (p)) /\ ((((exists pfa_gap_residue_executiontracestepsstepaddresultbound. pfa_gap_residue_executiontracestepsstepaddresultbound + S (pfh_after_residue_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_residue_executiontracestepsstepaddresultcongruence pfa_offset_right_residue_executiontracestepsstepaddresultcongruence. ((pfh_product_residue_executiontracestepsstep) + (pfh_coefficient_residue_executiontracestepsstep)) + (p) * pfa_offset_left_residue_executiontracestepsstepaddresultcongruence = (pfh_after_residue_executiontracestepsstep) + (p) * pfa_offset_right_residue_executiontracestepsstepaddresultcongruence))))))))))))))))))))))))))) -> (((exists pfa_gap_residue_resultbound. pfa_gap_residue_resultbound + S (r) = (p)) /\ ((exists pfa_offset_left_residue_resultcongruence pfa_offset_right_residue_resultcongruence. (n) + (p) * pfa_offset_left_residue_resultcongruence = (r) + (p) * pfa_offset_right_residue_resultcongruence))))

Constructive proof overview

Generated structural guide

Actual modular evaluation has exactly the canonical residue of the existing natural T12 Horner value.

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

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

Proof neighborhood

Direct dependencies

PP0027 prime_field_polynomial_horner_normalization_residue PP0006 prime_field_polynomial_normalization_reflexive PP0023 prime_field_polynomial_horner_input_bounds

Direct dependents

PP0029 prime_field_polynomial_horner_functional PP0030 prime_field_polynomial_horner_result_bounded

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

39 script commands · 5 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 (3)
prime field polynomial horner normalization residueprime field polynomial normalization reflexiveprime field polynomial horner input bounds

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 n
  7. L7
    intro r
  8. L8
    intro hp
  9. L9
    intro hn
  10. L10
    intro hr
02Establish hboundsL11–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial horner input bounds.

  1. L11
    have hbounds : Lt(t,p) ∧ BetaPrefixInto(b,c,l,p)Definitions: BetaPrefixIntoLt
  2. L12
    specialize prime_field_polynomial_horner_input_bounds (p)
  3. L13
    specialize prime_field_polynomial_horner_input_bounds (b)
  4. L14
    specialize prime_field_polynomial_horner_input_bounds (c)
  5. L15
    specialize prime_field_polynomial_horner_input_bounds (t)
  6. L16
    specialize prime_field_polynomial_horner_input_bounds (l)
  7. L17
    specialize prime_field_polynomial_horner_input_bounds (r)
  8. L18
    apply prime_field_polynomial_horner_input_bounds
  9. L19
    exact hr
03Separate the logical casesL20–20

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

  1. L20
    cases hbounds
04Use earlier factsL21–30

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

  1. L21
    specialize prime_field_polynomial_horner_normalization_residue (p)
  2. L22
    specialize prime_field_polynomial_horner_normalization_residue (b)
  3. L23
    specialize prime_field_polynomial_horner_normalization_residue (c)
  4. L24
    specialize prime_field_polynomial_horner_normalization_residue (b)
  5. L25
    specialize prime_field_polynomial_horner_normalization_residue (c)
  6. L26
    specialize prime_field_polynomial_horner_normalization_residue (t)
  7. L27
    specialize prime_field_polynomial_horner_normalization_residue (l)
  8. L28
    specialize prime_field_polynomial_horner_normalization_residue (n)
  9. L29
    specialize prime_field_polynomial_horner_normalization_residue (r)
  10. L30
    apply prime_field_polynomial_horner_normalization_residue
05Use earlier factsL31–39

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

  1. L31
    exact hp
  2. L32
    specialize prime_field_polynomial_normalization_reflexive (p)
  3. L33
    specialize prime_field_polynomial_normalization_reflexive (b)
  4. L34
    specialize prime_field_polynomial_normalization_reflexive (c)
  5. L35
    specialize prime_field_polynomial_normalization_reflexive (l)
  6. L36
    apply prime_field_polynomial_normalization_reflexive
  7. L37
    exact hbounds_right
  8. L38
    exact hn
  9. L39
    exact hr

Library-wide reading audit

Original exact command ledger · 39 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro l
  6. 0006intro n
  7. 0007intro r
  8. 0008intro hp
  9. 0009intro hn
  10. 0010intro hr
  11. 0011have hbounds : ((exists pfa_gap_residue_base_bound. pfa_gap_residue_base_bound + S (t) = (p)) /\ ((forall fom_index_pfp_residue_coefficients. (exists fom_gap_pfp_residue_coefficients_index_bound. fom_gap_pfp_residue_coefficients_index_bound + S (fom_index_pfp_residue_coefficients) = l) -> exists fom_value_pfp_residue_coefficients. ((((exists fom_beta_height_pfp_residue_coefficients_entry. fom_beta_height_pfp_residue_coefficients_entry + S (fom_value_pfp_residue_coefficients) = S ((S (fom_index_pfp_residue_coefficients)) * c)) /\ exists fom_beta_quotient_pfp_residue_coefficients_entry. b = fom_beta_quotient_pfp_residue_coefficients_entry * S ((S (fom_index_pfp_residue_coefficients)) * c) + (fom_value_pfp_residue_coefficients))) /\ (exists fom_gap_pfp_residue_coefficients_value_bound. fom_gap_pfp_residue_coefficients_value_bound + S (fom_value_pfp_residue_coefficients) = p)))))
  12. 0012specialize prime_field_polynomial_horner_input_bounds (p)
  13. 0013specialize prime_field_polynomial_horner_input_bounds (b)
  14. 0014specialize prime_field_polynomial_horner_input_bounds (c)
  15. 0015specialize prime_field_polynomial_horner_input_bounds (t)
  16. 0016specialize prime_field_polynomial_horner_input_bounds (l)
  17. 0017specialize prime_field_polynomial_horner_input_bounds (r)
  18. 0018apply prime_field_polynomial_horner_input_bounds
  19. 0019exact hr
  20. 0020cases hbounds
  21. 0021specialize prime_field_polynomial_horner_normalization_residue (p)
  22. 0022specialize prime_field_polynomial_horner_normalization_residue (b)
  23. 0023specialize prime_field_polynomial_horner_normalization_residue (c)
  24. 0024specialize prime_field_polynomial_horner_normalization_residue (b)
  25. 0025specialize prime_field_polynomial_horner_normalization_residue (c)
  26. 0026specialize prime_field_polynomial_horner_normalization_residue (t)
  27. 0027specialize prime_field_polynomial_horner_normalization_residue (l)
  28. 0028specialize prime_field_polynomial_horner_normalization_residue (n)
  29. 0029specialize prime_field_polynomial_horner_normalization_residue (r)
  30. 0030apply prime_field_polynomial_horner_normalization_residue
  31. 0031exact hp
  32. 0032specialize prime_field_polynomial_normalization_reflexive (p)
  33. 0033specialize prime_field_polynomial_normalization_reflexive (b)
  34. 0034specialize prime_field_polynomial_normalization_reflexive (c)
  35. 0035specialize prime_field_polynomial_normalization_reflexive (l)
  36. 0036apply prime_field_polynomial_normalization_reflexive
  37. 0037exact hbounds_right
  38. 0038exact hn
  39. 0039exact hr