PQ0049

prime_field_polynomial_synthetic_quotient_entry

Each decoded quotient coefficient is precisely the actual Horner value of the corresponding nonempty input prefix.

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

All coefficients retain the established highest-degree-first order. Trimming handles empty and all-zero prefixes; monic normalization requires a nonzero leading coefficient. Synthetic division has a nonempty input of length S n and a quotient of length n, unique in decoded values. Its coefficient recurrence, actual evaluation remainder and positive-degree drop are checked. General polynomial Euclidean division, gcd/Bezout, an arbitrary-convolution factor theorem, irreducible-polynomial existence and the full G091 prime-power-field endpoint remain open. These exact theorems are first admitted to Alpha v32; Stable remains unchanged.

Exact theorem in conservative defined notation

∀ p. ∀ b. ∀ c. ∀ a. ∀ n. ∀ qb. ∀ qc. ∀ r. ∀ i. ∀ h. FpSyntheticDivision(p,b,c,a,n,qb,qc,r) → Lt(i,n) → BetaAt(qb,qc,i,h) → FpHorner(p,b,c,a,S i,h)

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

Definition DAG

FpHorner(p,b,c,x,l,r) · 2FpSyntheticDivision(p,b,c,a,n,qb,qc,r) · 1Lt(a,b) · 1BetaAt(b,c,i,x) · 3

Actual proof prerequisites

beta_at_exists · checked external prerequisiteone_mul · checked external prerequisiteadd_succ_left · checked external prerequisitezero_add · checked external prerequisiteprime_field_polynomial_horner_trace_prefixle_succ · checked external prerequisite
Original expanded first-order statement 
forall p b c a n qb qc r i h. (exists pfs_history_code_entry_division pfs_history_scale_entry_division. ((((exists pfa_gap_entry_divisiontracebase. pfa_gap_entry_divisiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_entry_divisiontraceinitial. ff_h_pfp_entry_divisiontraceinitial + S (0) = S ((S (0)) * pfs_history_scale_entry_division)) /\ exists ff_q_pfp_entry_divisiontraceinitial. pfs_history_code_entry_division = ff_q_pfp_entry_divisiontraceinitial * S ((S (0)) * pfs_history_scale_entry_division) + (0))) /\ (((((exists ff_h_pfp_entry_divisiontraceterminal. ff_h_pfp_entry_divisiontraceterminal + S (r) = S ((S (S (n))) * pfs_history_scale_entry_division)) /\ exists ff_q_pfp_entry_divisiontraceterminal. pfs_history_code_entry_division = ff_q_pfp_entry_divisiontraceterminal * S ((S (S (n))) * pfs_history_scale_entry_division) + (r))) /\ ((forall pfh_index_entry_divisiontracesteps. (exists pfa_gap_entry_divisiontracestepsindex. pfa_gap_entry_divisiontracestepsindex + S (pfh_index_entry_divisiontracesteps) = (S (n))) -> (exists pfh_coefficient_entry_divisiontracestepsstep pfh_before_entry_divisiontracestepsstep pfh_after_entry_divisiontracestepsstep pfh_product_entry_divisiontracestepsstep. ((((exists ff_h_pfp_entry_divisiontracestepsstepcoefficient. ff_h_pfp_entry_divisiontracestepsstepcoefficient + S (pfh_coefficient_entry_divisiontracestepsstep) = S ((S (pfh_index_entry_divisiontracesteps)) * c)) /\ exists ff_q_pfp_entry_divisiontracestepsstepcoefficient. b = ff_q_pfp_entry_divisiontracestepsstepcoefficient * S ((S (pfh_index_entry_divisiontracesteps)) * c) + (pfh_coefficient_entry_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_entry_divisiontracestepsstepbefore. ff_h_pfp_entry_divisiontracestepsstepbefore + S (pfh_before_entry_divisiontracestepsstep) = S ((S (pfh_index_entry_divisiontracesteps)) * pfs_history_scale_entry_division)) /\ exists ff_q_pfp_entry_divisiontracestepsstepbefore. pfs_history_code_entry_division = ff_q_pfp_entry_divisiontracestepsstepbefore * S ((S (pfh_index_entry_divisiontracesteps)) * pfs_history_scale_entry_division) + (pfh_before_entry_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_entry_divisiontracestepsstepafter. ff_h_pfp_entry_divisiontracestepsstepafter + S (pfh_after_entry_divisiontracestepsstep) = S ((S (S (pfh_index_entry_divisiontracesteps))) * pfs_history_scale_entry_division)) /\ exists ff_q_pfp_entry_divisiontracestepsstepafter. pfs_history_code_entry_division = ff_q_pfp_entry_divisiontracestepsstepafter * S ((S (S (pfh_index_entry_divisiontracesteps))) * pfs_history_scale_entry_division) + (pfh_after_entry_divisiontracestepsstep))) /\ (((((exists pfa_gap_entry_divisiontracestepsstepmultiplyleft. pfa_gap_entry_divisiontracestepsstepmultiplyleft + S (pfh_before_entry_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_entry_divisiontracestepsstepmultiplyright. pfa_gap_entry_divisiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_entry_divisiontracestepsstepmultiplyresultbound. pfa_gap_entry_divisiontracestepsstepmultiplyresultbound + S (pfh_product_entry_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_entry_divisiontracestepsstepmultiplyresultcongruence pfa_offset_right_entry_divisiontracestepsstepmultiplyresultcongruence. ((pfh_before_entry_divisiontracestepsstep) * (a)) + (p) * pfa_offset_left_entry_divisiontracestepsstepmultiplyresultcongruence = (pfh_product_entry_divisiontracestepsstep) + (p) * pfa_offset_right_entry_divisiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_entry_divisiontracestepsstepaddleft. pfa_gap_entry_divisiontracestepsstepaddleft + S (pfh_product_entry_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_entry_divisiontracestepsstepaddright. pfa_gap_entry_divisiontracestepsstepaddright + S (pfh_coefficient_entry_divisiontracestepsstep) = (p)) /\ ((((exists pfa_gap_entry_divisiontracestepsstepaddresultbound. pfa_gap_entry_divisiontracestepsstepaddresultbound + S (pfh_after_entry_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_entry_divisiontracestepsstepaddresultcongruence pfa_offset_right_entry_divisiontracestepsstepaddresultcongruence. ((pfh_product_entry_divisiontracestepsstep) + (pfh_coefficient_entry_divisiontracestepsstep)) + (p) * pfa_offset_left_entry_divisiontracestepsstepaddresultcongruence = (pfh_after_entry_divisiontracestepsstep) + (p) * pfa_offset_right_entry_divisiontracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_entry_divisionquotient ff_source_mcp_pfs_entry_divisionquotient ff_target_mcp_pfs_entry_divisionquotient. (exists mcp_gap_pfs_entry_divisionquotient_bound. mcp_gap_pfs_entry_divisionquotient_bound + S (ff_index_mcp_pfs_entry_divisionquotient) = (n)) -> (((exists fs_h_mcp_pfs_entry_divisionquotient_source. fs_h_mcp_pfs_entry_divisionquotient_source + S (ff_source_mcp_pfs_entry_divisionquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_entry_divisionquotient)) * pfs_history_scale_entry_division)) /\ exists fs_q_mcp_pfs_entry_divisionquotient_source. pfs_history_code_entry_division = fs_q_mcp_pfs_entry_divisionquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_entry_divisionquotient)) * pfs_history_scale_entry_division) + (ff_source_mcp_pfs_entry_divisionquotient))) -> (((exists fs_h_mcp_pfs_entry_divisionquotient_target. fs_h_mcp_pfs_entry_divisionquotient_target + S (ff_target_mcp_pfs_entry_divisionquotient) = S ((S (ff_index_mcp_pfs_entry_divisionquotient)) * qc)) /\ exists fs_q_mcp_pfs_entry_divisionquotient_target. qb = fs_q_mcp_pfs_entry_divisionquotient_target * S ((S (ff_index_mcp_pfs_entry_divisionquotient)) * qc) + (ff_target_mcp_pfs_entry_divisionquotient))) -> ff_target_mcp_pfs_entry_divisionquotient = ff_source_mcp_pfs_entry_divisionquotient)))) -> (exists pfa_gap_entry_index. pfa_gap_entry_index + S (i) = (n)) -> (((exists ff_h_pfp_entry_quotient. ff_h_pfp_entry_quotient + S (h) = S ((S (i)) * qc)) /\ exists ff_q_pfp_entry_quotient. qb = ff_q_pfp_entry_quotient * S ((S (i)) * qc) + (h))) -> (exists pfh_trace_code_entry_execution pfh_trace_scale_entry_execution. (((exists pfa_gap_entry_executiontracebase. pfa_gap_entry_executiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_entry_executiontraceinitial. ff_h_pfp_entry_executiontraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_entry_execution)) /\ exists ff_q_pfp_entry_executiontraceinitial. pfh_trace_code_entry_execution = ff_q_pfp_entry_executiontraceinitial * S ((S (0)) * pfh_trace_scale_entry_execution) + (0))) /\ (((((exists ff_h_pfp_entry_executiontraceterminal. ff_h_pfp_entry_executiontraceterminal + S (h) = S ((S (S i)) * pfh_trace_scale_entry_execution)) /\ exists ff_q_pfp_entry_executiontraceterminal. pfh_trace_code_entry_execution = ff_q_pfp_entry_executiontraceterminal * S ((S (S i)) * pfh_trace_scale_entry_execution) + (h))) /\ ((forall pfh_index_entry_executiontracesteps. (exists pfa_gap_entry_executiontracestepsindex. pfa_gap_entry_executiontracestepsindex + S (pfh_index_entry_executiontracesteps) = (S i)) -> (exists pfh_coefficient_entry_executiontracestepsstep pfh_before_entry_executiontracestepsstep pfh_after_entry_executiontracestepsstep pfh_product_entry_executiontracestepsstep. ((((exists ff_h_pfp_entry_executiontracestepsstepcoefficient. ff_h_pfp_entry_executiontracestepsstepcoefficient + S (pfh_coefficient_entry_executiontracestepsstep) = S ((S (pfh_index_entry_executiontracesteps)) * c)) /\ exists ff_q_pfp_entry_executiontracestepsstepcoefficient. b = ff_q_pfp_entry_executiontracestepsstepcoefficient * S ((S (pfh_index_entry_executiontracesteps)) * c) + (pfh_coefficient_entry_executiontracestepsstep))) /\ (((((exists ff_h_pfp_entry_executiontracestepsstepbefore. ff_h_pfp_entry_executiontracestepsstepbefore + S (pfh_before_entry_executiontracestepsstep) = S ((S (pfh_index_entry_executiontracesteps)) * pfh_trace_scale_entry_execution)) /\ exists ff_q_pfp_entry_executiontracestepsstepbefore. pfh_trace_code_entry_execution = ff_q_pfp_entry_executiontracestepsstepbefore * S ((S (pfh_index_entry_executiontracesteps)) * pfh_trace_scale_entry_execution) + (pfh_before_entry_executiontracestepsstep))) /\ (((((exists ff_h_pfp_entry_executiontracestepsstepafter. ff_h_pfp_entry_executiontracestepsstepafter + S (pfh_after_entry_executiontracestepsstep) = S ((S (S (pfh_index_entry_executiontracesteps))) * pfh_trace_scale_entry_execution)) /\ exists ff_q_pfp_entry_executiontracestepsstepafter. pfh_trace_code_entry_execution = ff_q_pfp_entry_executiontracestepsstepafter * S ((S (S (pfh_index_entry_executiontracesteps))) * pfh_trace_scale_entry_execution) + (pfh_after_entry_executiontracestepsstep))) /\ (((((exists pfa_gap_entry_executiontracestepsstepmultiplyleft. pfa_gap_entry_executiontracestepsstepmultiplyleft + S (pfh_before_entry_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_entry_executiontracestepsstepmultiplyright. pfa_gap_entry_executiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_entry_executiontracestepsstepmultiplyresultbound. pfa_gap_entry_executiontracestepsstepmultiplyresultbound + S (pfh_product_entry_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_entry_executiontracestepsstepmultiplyresultcongruence pfa_offset_right_entry_executiontracestepsstepmultiplyresultcongruence. ((pfh_before_entry_executiontracestepsstep) * (a)) + (p) * pfa_offset_left_entry_executiontracestepsstepmultiplyresultcongruence = (pfh_product_entry_executiontracestepsstep) + (p) * pfa_offset_right_entry_executiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_entry_executiontracestepsstepaddleft. pfa_gap_entry_executiontracestepsstepaddleft + S (pfh_product_entry_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_entry_executiontracestepsstepaddright. pfa_gap_entry_executiontracestepsstepaddright + S (pfh_coefficient_entry_executiontracestepsstep) = (p)) /\ ((((exists pfa_gap_entry_executiontracestepsstepaddresultbound. pfa_gap_entry_executiontracestepsstepaddresultbound + S (pfh_after_entry_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_entry_executiontracestepsstepaddresultcongruence pfa_offset_right_entry_executiontracestepsstepaddresultcongruence. ((pfh_product_entry_executiontracestepsstep) + (pfh_coefficient_entry_executiontracestepsstep)) + (p) * pfa_offset_left_entry_executiontracestepsstepaddresultcongruence = (pfh_after_entry_executiontracestepsstep) + (p) * pfa_offset_right_entry_executiontracestepsstepaddresultcongruence)))))))))))))))))))))))))))

Complete tactic proof in conservative notation

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

60 script commands · 11 reading checkpoints · 6 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)
prime field polynomial horner trace prefix
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 a
  5. L5
    intro n
  6. L6
    intro qb
  7. L7
    intro qc
  8. L8
    intro r
  9. L9
    intro i
  10. L10
    intro h
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hs
  2. L12
    intro hi
  3. L13
    intro hh
03Separate the logical casesL14–16

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

  1. L14
    cases hs
  2. L15
    cases hs_witness
  3. L16
    cases hs_witness_witness
04Establish heL17–21

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

  1. L17
    have he : ∃ z. BetaAt(x,x1,S i,z)Definitions: BetaAt(x,x1,S i,z)Original native command in the exact edition
  2. L18
    specialize beta_at_exists (x)
  3. L19
    specialize beta_at_exists (x1)
  4. L20
    specialize beta_at_exists (S i)
  5. L21
    apply beta_at_exists
05Separate the logical casesL22–22

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

  1. L22
    cases he
06Establish hindexL23–24

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

  1. L23
    have hindex : 1+1*i=S i
  2. L24
    simp [one_mul,add_succ_left,zero_add]
07Establish hshiftL25–28

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

  1. L25
    have hshift : BetaAt(x,x1,1 + 1 · i,x2)Definitions: BetaAt(x,x1,1 + 1 · i,x2)Original native command in the exact edition
  2. L26
    rewrite hindex
  3. L27
    rewrite hindex
  4. L28
    exact he_witness
08Establish heqL29–36

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

  1. L29
    have heq : h=x2
  2. L30
    specialize hs_witness_witness_right (i)
  3. L31
    specialize hs_witness_witness_right (x2)
  4. L32
    specialize hs_witness_witness_right (h)
  5. L33
    apply hs_witness_witness_right
  6. L34
    exact hi
  7. L35
    exact hshift
  8. L36
    exact hh
09Establish hexL37–46

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

  1. L37
    have hex : FpHorner(p,b,c,a,S i,x2)Definitions: FpHorner(p,b,c,a,S i,x2)Original native command in the exact edition
  2. L38
    specialize prime_field_polynomial_horner_trace_prefix (p)
  3. L39
    specialize prime_field_polynomial_horner_trace_prefix (b)
  4. L40
    specialize prime_field_polynomial_horner_trace_prefix (c)
  5. L41
    specialize prime_field_polynomial_horner_trace_prefix (a)
  6. L42
    specialize prime_field_polynomial_horner_trace_prefix (S n)
  7. L43
    specialize prime_field_polynomial_horner_trace_prefix (r)
  8. L44
    specialize prime_field_polynomial_horner_trace_prefix (x)
  9. L45
    specialize prime_field_polynomial_horner_trace_prefix (x1)
  10. L46
    specialize prime_field_polynomial_horner_trace_prefix (S i)
10Use earlier factsL47–54

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

  1. L47
    specialize prime_field_polynomial_horner_trace_prefix (x2)
  2. L48
    apply prime_field_polynomial_horner_trace_prefix
  3. L49
    exact hs_witness_witness_left
  4. L50
    specialize le_succ (S i)
  5. L51
    specialize le_succ (n)
  6. L52
    apply le_succ
  7. L53
    exact hi
  8. L54
    exact he_witness
11Establish hbackL55–60

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

  1. L55
    have hback : x2=h
  2. L56
    symm
  3. L57
    exact heq
  4. L58
    rewrite hback at hex
  5. L59
    rewrite hback at hex
  6. L60
    exact hex

Library-wide reading audit

Original defined command ledger · 60 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro a
  5. 0005intro n
  6. 0006intro qb
  7. 0007intro qc
  8. 0008intro r
  9. 0009intro i
  10. 0010intro h
  11. 0011intro hs
  12. 0012intro hi
  13. 0013intro hh
  14. 0014cases hs
  15. 0015cases hs_witness
  16. 0016cases hs_witness_witness
  17. 0017have he : ∃ z. BetaAt(x,x1,S i,z)
  18. 0018specialize beta_at_exists (x)
  19. 0019specialize beta_at_exists (x1)
  20. 0020specialize beta_at_exists (S i)
  21. 0021apply beta_at_exists
  22. 0022cases he
  23. 0023have hindex : 1+1*i=S i
  24. 0024simp [one_mul,add_succ_left,zero_add]
  25. 0025have hshift : BetaAt(x,x1,1 + 1 · i,x2)
  26. 0026rewrite hindex
  27. 0027rewrite hindex
  28. 0028exact he_witness
  29. 0029have heq : h=x2
  30. 0030specialize hs_witness_witness_right (i)
  31. 0031specialize hs_witness_witness_right (x2)
  32. 0032specialize hs_witness_witness_right (h)
  33. 0033apply hs_witness_witness_right
  34. 0034exact hi
  35. 0035exact hshift
  36. 0036exact hh
  37. 0037have hex : FpHorner(p,b,c,a,S i,x2)
  38. 0038specialize prime_field_polynomial_horner_trace_prefix (p)
  39. 0039specialize prime_field_polynomial_horner_trace_prefix (b)
  40. 0040specialize prime_field_polynomial_horner_trace_prefix (c)
  41. 0041specialize prime_field_polynomial_horner_trace_prefix (a)
  42. 0042specialize prime_field_polynomial_horner_trace_prefix (S n)
  43. 0043specialize prime_field_polynomial_horner_trace_prefix (r)
  44. 0044specialize prime_field_polynomial_horner_trace_prefix (x)
  45. 0045specialize prime_field_polynomial_horner_trace_prefix (x1)
  46. 0046specialize prime_field_polynomial_horner_trace_prefix (S i)
  47. 0047specialize prime_field_polynomial_horner_trace_prefix (x2)
  48. 0048apply prime_field_polynomial_horner_trace_prefix
  49. 0049exact hs_witness_witness_left
  50. 0050specialize le_succ (S i)
  51. 0051specialize le_succ (n)
  52. 0052apply le_succ
  53. 0053exact hi
  54. 0054exact he_witness
  55. 0055have hback : x2=h
  56. 0056symm
  57. 0057exact heq
  58. 0058rewrite hback at hex
  59. 0059rewrite hback at hex
  60. 0060exact hex