PQ0051

prime_field_polynomial_synthetic_final_coefficient

The remainder satisfies r=a*q[last]+f[last] by genuine canonical multiplication and addition.

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. ∀ h. ∀ v. Prime(p) → FpSyntheticDivision(p,b,c,a,S n,qb,qc,r) → BetaAt(qb,qc,n,h) → BetaAt(b,c,S n,v) → ∃ x. FpMul(p,h,a,x) ∧ FpAdd(p,x,v,r)

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

Definition DAG

FpAdd(p,a,b,c) · 1FpMul(p,a,b,c) · 1FpSyntheticDivision(p,b,c,a,n,qb,qc,r) · 1Prime(p) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

prime_field_polynomial_horner_transition_valuesprime_field_polynomial_synthetic_quotient_entryzero_add · checked external prerequisiteprime_field_polynomial_synthetic_remainder_execution
Original expanded first-order statement 
forall p b c a n qb qc r h v. (~((p) = 1) /\ forall pfa_factor_left_final_prime pfa_factor_right_final_prime. (p) = pfa_factor_left_final_prime * pfa_factor_right_final_prime -> pfa_factor_left_final_prime = 1 \/ pfa_factor_right_final_prime = 1) -> (exists pfs_history_code_final_division pfs_history_scale_final_division. ((((exists pfa_gap_final_divisiontracebase. pfa_gap_final_divisiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_final_divisiontraceinitial. ff_h_pfp_final_divisiontraceinitial + S (0) = S ((S (0)) * pfs_history_scale_final_division)) /\ exists ff_q_pfp_final_divisiontraceinitial. pfs_history_code_final_division = ff_q_pfp_final_divisiontraceinitial * S ((S (0)) * pfs_history_scale_final_division) + (0))) /\ (((((exists ff_h_pfp_final_divisiontraceterminal. ff_h_pfp_final_divisiontraceterminal + S (r) = S ((S (S (S n))) * pfs_history_scale_final_division)) /\ exists ff_q_pfp_final_divisiontraceterminal. pfs_history_code_final_division = ff_q_pfp_final_divisiontraceterminal * S ((S (S (S n))) * pfs_history_scale_final_division) + (r))) /\ ((forall pfh_index_final_divisiontracesteps. (exists pfa_gap_final_divisiontracestepsindex. pfa_gap_final_divisiontracestepsindex + S (pfh_index_final_divisiontracesteps) = (S (S n))) -> (exists pfh_coefficient_final_divisiontracestepsstep pfh_before_final_divisiontracestepsstep pfh_after_final_divisiontracestepsstep pfh_product_final_divisiontracestepsstep. ((((exists ff_h_pfp_final_divisiontracestepsstepcoefficient. ff_h_pfp_final_divisiontracestepsstepcoefficient + S (pfh_coefficient_final_divisiontracestepsstep) = S ((S (pfh_index_final_divisiontracesteps)) * c)) /\ exists ff_q_pfp_final_divisiontracestepsstepcoefficient. b = ff_q_pfp_final_divisiontracestepsstepcoefficient * S ((S (pfh_index_final_divisiontracesteps)) * c) + (pfh_coefficient_final_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_final_divisiontracestepsstepbefore. ff_h_pfp_final_divisiontracestepsstepbefore + S (pfh_before_final_divisiontracestepsstep) = S ((S (pfh_index_final_divisiontracesteps)) * pfs_history_scale_final_division)) /\ exists ff_q_pfp_final_divisiontracestepsstepbefore. pfs_history_code_final_division = ff_q_pfp_final_divisiontracestepsstepbefore * S ((S (pfh_index_final_divisiontracesteps)) * pfs_history_scale_final_division) + (pfh_before_final_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_final_divisiontracestepsstepafter. ff_h_pfp_final_divisiontracestepsstepafter + S (pfh_after_final_divisiontracestepsstep) = S ((S (S (pfh_index_final_divisiontracesteps))) * pfs_history_scale_final_division)) /\ exists ff_q_pfp_final_divisiontracestepsstepafter. pfs_history_code_final_division = ff_q_pfp_final_divisiontracestepsstepafter * S ((S (S (pfh_index_final_divisiontracesteps))) * pfs_history_scale_final_division) + (pfh_after_final_divisiontracestepsstep))) /\ (((((exists pfa_gap_final_divisiontracestepsstepmultiplyleft. pfa_gap_final_divisiontracestepsstepmultiplyleft + S (pfh_before_final_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_final_divisiontracestepsstepmultiplyright. pfa_gap_final_divisiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_final_divisiontracestepsstepmultiplyresultbound. pfa_gap_final_divisiontracestepsstepmultiplyresultbound + S (pfh_product_final_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_final_divisiontracestepsstepmultiplyresultcongruence pfa_offset_right_final_divisiontracestepsstepmultiplyresultcongruence. ((pfh_before_final_divisiontracestepsstep) * (a)) + (p) * pfa_offset_left_final_divisiontracestepsstepmultiplyresultcongruence = (pfh_product_final_divisiontracestepsstep) + (p) * pfa_offset_right_final_divisiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_final_divisiontracestepsstepaddleft. pfa_gap_final_divisiontracestepsstepaddleft + S (pfh_product_final_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_final_divisiontracestepsstepaddright. pfa_gap_final_divisiontracestepsstepaddright + S (pfh_coefficient_final_divisiontracestepsstep) = (p)) /\ ((((exists pfa_gap_final_divisiontracestepsstepaddresultbound. pfa_gap_final_divisiontracestepsstepaddresultbound + S (pfh_after_final_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_final_divisiontracestepsstepaddresultcongruence pfa_offset_right_final_divisiontracestepsstepaddresultcongruence. ((pfh_product_final_divisiontracestepsstep) + (pfh_coefficient_final_divisiontracestepsstep)) + (p) * pfa_offset_left_final_divisiontracestepsstepaddresultcongruence = (pfh_after_final_divisiontracestepsstep) + (p) * pfa_offset_right_final_divisiontracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_final_divisionquotient ff_source_mcp_pfs_final_divisionquotient ff_target_mcp_pfs_final_divisionquotient. (exists mcp_gap_pfs_final_divisionquotient_bound. mcp_gap_pfs_final_divisionquotient_bound + S (ff_index_mcp_pfs_final_divisionquotient) = (S n)) -> (((exists fs_h_mcp_pfs_final_divisionquotient_source. fs_h_mcp_pfs_final_divisionquotient_source + S (ff_source_mcp_pfs_final_divisionquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_final_divisionquotient)) * pfs_history_scale_final_division)) /\ exists fs_q_mcp_pfs_final_divisionquotient_source. pfs_history_code_final_division = fs_q_mcp_pfs_final_divisionquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_final_divisionquotient)) * pfs_history_scale_final_division) + (ff_source_mcp_pfs_final_divisionquotient))) -> (((exists fs_h_mcp_pfs_final_divisionquotient_target. fs_h_mcp_pfs_final_divisionquotient_target + S (ff_target_mcp_pfs_final_divisionquotient) = S ((S (ff_index_mcp_pfs_final_divisionquotient)) * qc)) /\ exists fs_q_mcp_pfs_final_divisionquotient_target. qb = fs_q_mcp_pfs_final_divisionquotient_target * S ((S (ff_index_mcp_pfs_final_divisionquotient)) * qc) + (ff_target_mcp_pfs_final_divisionquotient))) -> ff_target_mcp_pfs_final_divisionquotient = ff_source_mcp_pfs_final_divisionquotient)))) -> (((exists ff_h_pfp_final_quotient. ff_h_pfp_final_quotient + S (h) = S ((S (n)) * qc)) /\ exists ff_q_pfp_final_quotient. qb = ff_q_pfp_final_quotient * S ((S (n)) * qc) + (h))) -> (((exists ff_h_pfp_final_input. ff_h_pfp_final_input + S (v) = S ((S (S n)) * c)) /\ exists ff_q_pfp_final_input. b = ff_q_pfp_final_input * S ((S (S n)) * c) + (v))) -> exists k. ((((exists pfa_gap_final_productleft. pfa_gap_final_productleft + S (h) = (p)) /\ (((exists pfa_gap_final_productright. pfa_gap_final_productright + S (a) = (p)) /\ ((((exists pfa_gap_final_productresultbound. pfa_gap_final_productresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_final_productresultcongruence pfa_offset_right_final_productresultcongruence. ((h) * (a)) + (p) * pfa_offset_left_final_productresultcongruence = (k) + (p) * pfa_offset_right_final_productresultcongruence))))))))) /\ ((((exists pfa_gap_final_sumleft. pfa_gap_final_sumleft + S (k) = (p)) /\ (((exists pfa_gap_final_sumright. pfa_gap_final_sumright + S (v) = (p)) /\ ((((exists pfa_gap_final_sumresultbound. pfa_gap_final_sumresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_final_sumresultcongruence pfa_offset_right_final_sumresultcongruence. ((k) + (v)) + (p) * pfa_offset_left_final_sumresultcongruence = (r) + (p) * pfa_offset_right_final_sumresultcongruence)))))))))))

Complete tactic proof in conservative notation

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

50 script commands · 8 reading checkpoints · 0 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 transition valuesprime field polynomial synthetic quotient entryprime field polynomial synthetic remainder execution
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 h
  10. L10
    intro v
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hp
  2. L12
    intro hs
  3. L13
    intro hh
  4. L14
    intro hv
03Use earlier factsL15–24

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

  1. L15
    specialize prime_field_polynomial_horner_transition_values (p)
  2. L16
    specialize prime_field_polynomial_horner_transition_values (b)
  3. L17
    specialize prime_field_polynomial_horner_transition_values (c)
  4. L18
    specialize prime_field_polynomial_horner_transition_values (a)
  5. L19
    specialize prime_field_polynomial_horner_transition_values (S n)
  6. L20
    specialize prime_field_polynomial_horner_transition_values (h)
  7. L21
    specialize prime_field_polynomial_horner_transition_values (v)
  8. L22
    specialize prime_field_polynomial_horner_transition_values (r)
  9. L23
    apply prime_field_polynomial_horner_transition_values
  10. L24
    exact hp
04Use earlier factsL25–34

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

  1. L25
    specialize prime_field_polynomial_synthetic_quotient_entry (p)
  2. L26
    specialize prime_field_polynomial_synthetic_quotient_entry (b)
  3. L27
    specialize prime_field_polynomial_synthetic_quotient_entry (c)
  4. L28
    specialize prime_field_polynomial_synthetic_quotient_entry (a)
  5. L29
    specialize prime_field_polynomial_synthetic_quotient_entry (S n)
  6. L30
    specialize prime_field_polynomial_synthetic_quotient_entry (qb)
  7. L31
    specialize prime_field_polynomial_synthetic_quotient_entry (qc)
  8. L32
    specialize prime_field_polynomial_synthetic_quotient_entry (r)
  9. L33
    specialize prime_field_polynomial_synthetic_quotient_entry (n)
  10. L34
    specialize prime_field_polynomial_synthetic_quotient_entry (h)
05Use earlier factsL35–36

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

  1. L35
    apply prime_field_polynomial_synthetic_quotient_entry
  2. L36
    exact hs
06Construct an explicit witnessL37–37

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

  1. L37
    exists 0
07Use earlier factsL38–47

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

  1. L38
    apply zero_add
  2. L39
    exact hh
  3. L40
    specialize prime_field_polynomial_synthetic_remainder_execution (p)
  4. L41
    specialize prime_field_polynomial_synthetic_remainder_execution (b)
  5. L42
    specialize prime_field_polynomial_synthetic_remainder_execution (c)
  6. L43
    specialize prime_field_polynomial_synthetic_remainder_execution (a)
  7. L44
    specialize prime_field_polynomial_synthetic_remainder_execution (S n)
  8. L45
    specialize prime_field_polynomial_synthetic_remainder_execution (qb)
  9. L46
    specialize prime_field_polynomial_synthetic_remainder_execution (qc)
  10. L47
    specialize prime_field_polynomial_synthetic_remainder_execution (r)
08Use earlier factsL48–50

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

  1. L48
    apply prime_field_polynomial_synthetic_remainder_execution
  2. L49
    exact hs
  3. L50
    exact hv

Library-wide reading audit

Original defined command ledger · 50 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 h
  10. 0010intro v
  11. 0011intro hp
  12. 0012intro hs
  13. 0013intro hh
  14. 0014intro hv
  15. 0015specialize prime_field_polynomial_horner_transition_values (p)
  16. 0016specialize prime_field_polynomial_horner_transition_values (b)
  17. 0017specialize prime_field_polynomial_horner_transition_values (c)
  18. 0018specialize prime_field_polynomial_horner_transition_values (a)
  19. 0019specialize prime_field_polynomial_horner_transition_values (S n)
  20. 0020specialize prime_field_polynomial_horner_transition_values (h)
  21. 0021specialize prime_field_polynomial_horner_transition_values (v)
  22. 0022specialize prime_field_polynomial_horner_transition_values (r)
  23. 0023apply prime_field_polynomial_horner_transition_values
  24. 0024exact hp
  25. 0025specialize prime_field_polynomial_synthetic_quotient_entry (p)
  26. 0026specialize prime_field_polynomial_synthetic_quotient_entry (b)
  27. 0027specialize prime_field_polynomial_synthetic_quotient_entry (c)
  28. 0028specialize prime_field_polynomial_synthetic_quotient_entry (a)
  29. 0029specialize prime_field_polynomial_synthetic_quotient_entry (S n)
  30. 0030specialize prime_field_polynomial_synthetic_quotient_entry (qb)
  31. 0031specialize prime_field_polynomial_synthetic_quotient_entry (qc)
  32. 0032specialize prime_field_polynomial_synthetic_quotient_entry (r)
  33. 0033specialize prime_field_polynomial_synthetic_quotient_entry (n)
  34. 0034specialize prime_field_polynomial_synthetic_quotient_entry (h)
  35. 0035apply prime_field_polynomial_synthetic_quotient_entry
  36. 0036exact hs
  37. 0037exists 0
  38. 0038apply zero_add
  39. 0039exact hh
  40. 0040specialize prime_field_polynomial_synthetic_remainder_execution (p)
  41. 0041specialize prime_field_polynomial_synthetic_remainder_execution (b)
  42. 0042specialize prime_field_polynomial_synthetic_remainder_execution (c)
  43. 0043specialize prime_field_polynomial_synthetic_remainder_execution (a)
  44. 0044specialize prime_field_polynomial_synthetic_remainder_execution (S n)
  45. 0045specialize prime_field_polynomial_synthetic_remainder_execution (qb)
  46. 0046specialize prime_field_polynomial_synthetic_remainder_execution (qc)
  47. 0047specialize prime_field_polynomial_synthetic_remainder_execution (r)
  48. 0048apply prime_field_polynomial_synthetic_remainder_execution
  49. 0049exact hs
  50. 0050exact hv