PP0028

prime_field_polynomial_horner_residue

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

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

Length is representation length, not polynomial degree. Leading zeros and the empty zero polynomial are allowed; the canonical argument guard x<p also applies to the empty case. Evaluation is defined by actual field-operation steps, not an assumed residue invariant. Polynomial division, gcd, irreducibles and general prime-power extension fields remain open; this does not close G091.

Exact theorem in conservative defined notation

∀ p. ∀ b. ∀ c. ∀ t. ∀ l. ∀ n. ∀ r. Prime(p) → Horner(b,c,t,l,n) → FpHorner(p,b,c,t,l,r) → CanonicalModularResidue(p,n,r)

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

Definition DAG

Horner(b,c,x,ell,z) · 1CanonicalModularResidue(m,a,r) · 1BetaPrefixInto(b,c,l,B) · 1FpHorner(p,b,c,x,l,r) · 1Lt(a,b) · 1Prime(p) · 1

Actual proof prerequisites

prime_field_polynomial_horner_normalization_residueprime_field_polynomial_normalization_reflexiveprime_field_polynomial_horner_input_bounds
Original expanded first-order 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))))

Complete tactic proof in conservative notation

All 39 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

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 (3)
prime field polynomial horner input boundsprime field polynomial horner normalization residueprime field polynomial normalization reflexive
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: Lt(t,p)BetaPrefixInto(b,c,l,p)Original native command in the exact edition
  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 defined 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 : Lt(t,p) ∧ BetaPrefixInto(b,c,l,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