PP0022

prime_field_polynomial_horner_exists

Every canonical coefficient prefix and canonical base have an actual finite modular Horner history; no trace or norm invariant is supplied.

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. Prime(p) → BetaPrefixInto(b,c,l,p) → Lt(t,p) → ∃ x. FpHorner(p,b,c,t,l,x)

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) · 1FpCoefficientReduction(p,b,c,d,e,l) · 1FpHornerTrace(p,b,c,x,l,r,u,v) · 1FpHorner(p,b,c,x,l,r) · 1Lt(a,b) · 1Prime(p) · 1

Actual proof prerequisites

beta_horner_eval_exists · checked external prerequisiteprime_field_polynomial_normalization_existsprime_nonzero · checked external prerequisiteprime_field_polynomial_horner_trace_from_normalization
Original expanded first-order statement 
forall p b c t l. (~((p) = 1) /\ forall pfa_factor_left_exists_prime pfa_factor_right_exists_prime. (p) = pfa_factor_left_exists_prime * pfa_factor_right_exists_prime -> pfa_factor_left_exists_prime = 1 \/ pfa_factor_right_exists_prime = 1) -> (forall fom_index_pfp_exists_coefficients. (exists fom_gap_pfp_exists_coefficients_index_bound. fom_gap_pfp_exists_coefficients_index_bound + S (fom_index_pfp_exists_coefficients) = l) -> exists fom_value_pfp_exists_coefficients. ((((exists fom_beta_height_pfp_exists_coefficients_entry. fom_beta_height_pfp_exists_coefficients_entry + S (fom_value_pfp_exists_coefficients) = S ((S (fom_index_pfp_exists_coefficients)) * c)) /\ exists fom_beta_quotient_pfp_exists_coefficients_entry. b = fom_beta_quotient_pfp_exists_coefficients_entry * S ((S (fom_index_pfp_exists_coefficients)) * c) + (fom_value_pfp_exists_coefficients))) /\ (exists fom_gap_pfp_exists_coefficients_value_bound. fom_gap_pfp_exists_coefficients_value_bound + S (fom_value_pfp_exists_coefficients) = p))) -> (exists pfa_gap_exists_base. pfa_gap_exists_base + S (t) = (p)) -> exists r. (exists pfh_trace_code_exists_execution pfh_trace_scale_exists_execution. (((exists pfa_gap_exists_executiontracebase. pfa_gap_exists_executiontracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_exists_executiontraceinitial. ff_h_pfp_exists_executiontraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_exists_execution)) /\ exists ff_q_pfp_exists_executiontraceinitial. pfh_trace_code_exists_execution = ff_q_pfp_exists_executiontraceinitial * S ((S (0)) * pfh_trace_scale_exists_execution) + (0))) /\ (((((exists ff_h_pfp_exists_executiontraceterminal. ff_h_pfp_exists_executiontraceterminal + S (r) = S ((S (l)) * pfh_trace_scale_exists_execution)) /\ exists ff_q_pfp_exists_executiontraceterminal. pfh_trace_code_exists_execution = ff_q_pfp_exists_executiontraceterminal * S ((S (l)) * pfh_trace_scale_exists_execution) + (r))) /\ ((forall pfh_index_exists_executiontracesteps. (exists pfa_gap_exists_executiontracestepsindex. pfa_gap_exists_executiontracestepsindex + S (pfh_index_exists_executiontracesteps) = (l)) -> (exists pfh_coefficient_exists_executiontracestepsstep pfh_before_exists_executiontracestepsstep pfh_after_exists_executiontracestepsstep pfh_product_exists_executiontracestepsstep. ((((exists ff_h_pfp_exists_executiontracestepsstepcoefficient. ff_h_pfp_exists_executiontracestepsstepcoefficient + S (pfh_coefficient_exists_executiontracestepsstep) = S ((S (pfh_index_exists_executiontracesteps)) * c)) /\ exists ff_q_pfp_exists_executiontracestepsstepcoefficient. b = ff_q_pfp_exists_executiontracestepsstepcoefficient * S ((S (pfh_index_exists_executiontracesteps)) * c) + (pfh_coefficient_exists_executiontracestepsstep))) /\ (((((exists ff_h_pfp_exists_executiontracestepsstepbefore. ff_h_pfp_exists_executiontracestepsstepbefore + S (pfh_before_exists_executiontracestepsstep) = S ((S (pfh_index_exists_executiontracesteps)) * pfh_trace_scale_exists_execution)) /\ exists ff_q_pfp_exists_executiontracestepsstepbefore. pfh_trace_code_exists_execution = ff_q_pfp_exists_executiontracestepsstepbefore * S ((S (pfh_index_exists_executiontracesteps)) * pfh_trace_scale_exists_execution) + (pfh_before_exists_executiontracestepsstep))) /\ (((((exists ff_h_pfp_exists_executiontracestepsstepafter. ff_h_pfp_exists_executiontracestepsstepafter + S (pfh_after_exists_executiontracestepsstep) = S ((S (S (pfh_index_exists_executiontracesteps))) * pfh_trace_scale_exists_execution)) /\ exists ff_q_pfp_exists_executiontracestepsstepafter. pfh_trace_code_exists_execution = ff_q_pfp_exists_executiontracestepsstepafter * S ((S (S (pfh_index_exists_executiontracesteps))) * pfh_trace_scale_exists_execution) + (pfh_after_exists_executiontracestepsstep))) /\ (((((exists pfa_gap_exists_executiontracestepsstepmultiplyleft. pfa_gap_exists_executiontracestepsstepmultiplyleft + S (pfh_before_exists_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_exists_executiontracestepsstepmultiplyright. pfa_gap_exists_executiontracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_exists_executiontracestepsstepmultiplyresultbound. pfa_gap_exists_executiontracestepsstepmultiplyresultbound + S (pfh_product_exists_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_exists_executiontracestepsstepmultiplyresultcongruence pfa_offset_right_exists_executiontracestepsstepmultiplyresultcongruence. ((pfh_before_exists_executiontracestepsstep) * (t)) + (p) * pfa_offset_left_exists_executiontracestepsstepmultiplyresultcongruence = (pfh_product_exists_executiontracestepsstep) + (p) * pfa_offset_right_exists_executiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_exists_executiontracestepsstepaddleft. pfa_gap_exists_executiontracestepsstepaddleft + S (pfh_product_exists_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_exists_executiontracestepsstepaddright. pfa_gap_exists_executiontracestepsstepaddright + S (pfh_coefficient_exists_executiontracestepsstep) = (p)) /\ ((((exists pfa_gap_exists_executiontracestepsstepaddresultbound. pfa_gap_exists_executiontracestepsstepaddresultbound + S (pfh_after_exists_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_exists_executiontracestepsstepaddresultcongruence pfa_offset_right_exists_executiontracestepsstepaddresultcongruence. ((pfh_product_exists_executiontracestepsstep) + (pfh_coefficient_exists_executiontracestepsstep)) + (p) * pfa_offset_left_exists_executiontracestepsstepaddresultcongruence = (pfh_after_exists_executiontracestepsstep) + (p) * pfa_offset_right_exists_executiontracestepsstepaddresultcongruence)))))))))))))))))))))))))))

Complete tactic proof in conservative notation

All 53 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

53 script commands · 11 reading checkpoints · 3 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 (2)
prime field polynomial normalization existsprime field polynomial horner trace from normalization
01Fix variables and assumptionsL1–8

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 hp
  7. L7
    intro hc
  8. L8
    intro ht
02Establish hnL9–14

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

  1. L9
    have hn : ∃ n. Horner(b,c,t,l,n)Definitions: Horner(b,c,t,l,n)Original native command in the exact edition
  2. L10
    specialize beta_horner_eval_exists (b)
  3. L11
    specialize beta_horner_eval_exists (c)
  4. L12
    specialize beta_horner_eval_exists (t)
  5. L13
    specialize beta_horner_eval_exists (l)
  6. L14
    apply beta_horner_eval_exists
03Separate the logical casesL15–17

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

  1. L15
    cases hn
  2. L16
    cases hn_witness
  3. L17
    cases hn_witness_witness
04Establish hrL18–27

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

  1. L18
    have hr : ∃ U. ∃ V. FpCoefficientReduction(p,x1,x2,U,V,S l)Definitions: FpCoefficientReduction(p,x1,x2,U,V,S l)Original native command in the exact edition
  2. L19
    specialize prime_field_polynomial_normalization_exists (p)
  3. L20
    specialize prime_field_polynomial_normalization_exists (x1)
  4. L21
    specialize prime_field_polynomial_normalization_exists (x2)
  5. L22
    specialize prime_field_polynomial_normalization_exists (S l)
  6. L23
    apply prime_field_polynomial_normalization_exists
  7. L24
    intro hz
  8. L25
    specialize prime_nonzero (p)
  9. L26
    apply prime_nonzero
  10. L27
    exact hp
05Use earlier factsL28–28

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

  1. L28
    exact hz
06Separate the logical casesL29–30

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

  1. L29
    cases hr
  2. L30
    cases hr_witness
07Establish heL31–40

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

  1. L31
    have he : ∃ r. FpHornerTrace(p,b,c,t,l,r,x3,x4) ∧ CanonicalModularResidue(p,x,r)Definitions: FpHornerTrace(p,b,c,t,l,r,x3,x4)CanonicalModularResidue(p,x,r)Original native command in the exact edition
  2. L32
    specialize prime_field_polynomial_horner_trace_from_normalization (p)
  3. L33
    specialize prime_field_polynomial_horner_trace_from_normalization (b)
  4. L34
    specialize prime_field_polynomial_horner_trace_from_normalization (c)
  5. L35
    specialize prime_field_polynomial_horner_trace_from_normalization (t)
  6. L36
    specialize prime_field_polynomial_horner_trace_from_normalization (l)
  7. L37
    specialize prime_field_polynomial_horner_trace_from_normalization (x)
  8. L38
    specialize prime_field_polynomial_horner_trace_from_normalization (x1)
  9. L39
    specialize prime_field_polynomial_horner_trace_from_normalization (x2)
  10. L40
    specialize prime_field_polynomial_horner_trace_from_normalization (x3)
08Use earlier factsL41–47

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

  1. L41
    specialize prime_field_polynomial_horner_trace_from_normalization (x4)
  2. L42
    apply prime_field_polynomial_horner_trace_from_normalization
  3. L43
    exact hp
  4. L44
    exact hc
  5. L45
    exact ht
  6. L46
    exact hn_witness_witness_witness
  7. L47
    exact hr_witness_witness
09Separate the logical casesL48–49

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

  1. L48
    cases he
  2. L49
    cases he_witness
10Construct an explicit witnessL50–52

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

  1. L50
    exists x5
  2. L51
    exists x3
  3. L52
    exists x4
11Use earlier factsL53–53

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

  1. L53
    exact he_witness_left

Library-wide reading audit

Original defined command ledger · 53 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro l
  6. 0006intro hp
  7. 0007intro hc
  8. 0008intro ht
  9. 0009have hn : ∃ n. Horner(b,c,t,l,n)
  10. 0010specialize beta_horner_eval_exists (b)
  11. 0011specialize beta_horner_eval_exists (c)
  12. 0012specialize beta_horner_eval_exists (t)
  13. 0013specialize beta_horner_eval_exists (l)
  14. 0014apply beta_horner_eval_exists
  15. 0015cases hn
  16. 0016cases hn_witness
  17. 0017cases hn_witness_witness
  18. 0018have hr : ∃ U. ∃ V. FpCoefficientReduction(p,x1,x2,U,V,S l)
  19. 0019specialize prime_field_polynomial_normalization_exists (p)
  20. 0020specialize prime_field_polynomial_normalization_exists (x1)
  21. 0021specialize prime_field_polynomial_normalization_exists (x2)
  22. 0022specialize prime_field_polynomial_normalization_exists (S l)
  23. 0023apply prime_field_polynomial_normalization_exists
  24. 0024intro hz
  25. 0025specialize prime_nonzero (p)
  26. 0026apply prime_nonzero
  27. 0027exact hp
  28. 0028exact hz
  29. 0029cases hr
  30. 0030cases hr_witness
  31. 0031have he : ∃ r. FpHornerTrace(p,b,c,t,l,r,x3,x4) ∧ CanonicalModularResidue(p,x,r)
  32. 0032specialize prime_field_polynomial_horner_trace_from_normalization (p)
  33. 0033specialize prime_field_polynomial_horner_trace_from_normalization (b)
  34. 0034specialize prime_field_polynomial_horner_trace_from_normalization (c)
  35. 0035specialize prime_field_polynomial_horner_trace_from_normalization (t)
  36. 0036specialize prime_field_polynomial_horner_trace_from_normalization (l)
  37. 0037specialize prime_field_polynomial_horner_trace_from_normalization (x)
  38. 0038specialize prime_field_polynomial_horner_trace_from_normalization (x1)
  39. 0039specialize prime_field_polynomial_horner_trace_from_normalization (x2)
  40. 0040specialize prime_field_polynomial_horner_trace_from_normalization (x3)
  41. 0041specialize prime_field_polynomial_horner_trace_from_normalization (x4)
  42. 0042apply prime_field_polynomial_horner_trace_from_normalization
  43. 0043exact hp
  44. 0044exact hc
  45. 0045exact ht
  46. 0046exact hn_witness_witness_witness
  47. 0047exact hr_witness_witness
  48. 0048cases he
  49. 0049cases he_witness
  50. 0050exists x5
  51. 0051exists x3
  52. 0052exists x4
  53. 0053exact he_witness_left