PQ004B

prime_field_polynomial_synthetic_remainder_bounded

Every actual synthetic remainder is a canonical field value.

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. Prime(p) → FpSyntheticDivision(p,b,c,a,n,qb,qc,r) → Lt(r,p)

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

Definition DAG

FpSyntheticDivision(p,b,c,a,n,qb,qc,r) · 1Lt(a,b) · 1Prime(p) · 1

Actual proof prerequisites

prime_field_polynomial_horner_result_bounded · checked external prerequisiteprime_field_polynomial_synthetic_remainder_execution
Original expanded first-order statement 
forall p b c a n qb qc r. (~((p) = 1) /\ forall pfa_factor_left_rbound_prime pfa_factor_right_rbound_prime. (p) = pfa_factor_left_rbound_prime * pfa_factor_right_rbound_prime -> pfa_factor_left_rbound_prime = 1 \/ pfa_factor_right_rbound_prime = 1) -> (exists pfs_history_code_rbound_division pfs_history_scale_rbound_division. ((((exists pfa_gap_rbound_divisiontracebase. pfa_gap_rbound_divisiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_rbound_divisiontraceinitial. ff_h_pfp_rbound_divisiontraceinitial + S (0) = S ((S (0)) * pfs_history_scale_rbound_division)) /\ exists ff_q_pfp_rbound_divisiontraceinitial. pfs_history_code_rbound_division = ff_q_pfp_rbound_divisiontraceinitial * S ((S (0)) * pfs_history_scale_rbound_division) + (0))) /\ (((((exists ff_h_pfp_rbound_divisiontraceterminal. ff_h_pfp_rbound_divisiontraceterminal + S (r) = S ((S (S (n))) * pfs_history_scale_rbound_division)) /\ exists ff_q_pfp_rbound_divisiontraceterminal. pfs_history_code_rbound_division = ff_q_pfp_rbound_divisiontraceterminal * S ((S (S (n))) * pfs_history_scale_rbound_division) + (r))) /\ ((forall pfh_index_rbound_divisiontracesteps. (exists pfa_gap_rbound_divisiontracestepsindex. pfa_gap_rbound_divisiontracestepsindex + S (pfh_index_rbound_divisiontracesteps) = (S (n))) -> (exists pfh_coefficient_rbound_divisiontracestepsstep pfh_before_rbound_divisiontracestepsstep pfh_after_rbound_divisiontracestepsstep pfh_product_rbound_divisiontracestepsstep. ((((exists ff_h_pfp_rbound_divisiontracestepsstepcoefficient. ff_h_pfp_rbound_divisiontracestepsstepcoefficient + S (pfh_coefficient_rbound_divisiontracestepsstep) = S ((S (pfh_index_rbound_divisiontracesteps)) * c)) /\ exists ff_q_pfp_rbound_divisiontracestepsstepcoefficient. b = ff_q_pfp_rbound_divisiontracestepsstepcoefficient * S ((S (pfh_index_rbound_divisiontracesteps)) * c) + (pfh_coefficient_rbound_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_rbound_divisiontracestepsstepbefore. ff_h_pfp_rbound_divisiontracestepsstepbefore + S (pfh_before_rbound_divisiontracestepsstep) = S ((S (pfh_index_rbound_divisiontracesteps)) * pfs_history_scale_rbound_division)) /\ exists ff_q_pfp_rbound_divisiontracestepsstepbefore. pfs_history_code_rbound_division = ff_q_pfp_rbound_divisiontracestepsstepbefore * S ((S (pfh_index_rbound_divisiontracesteps)) * pfs_history_scale_rbound_division) + (pfh_before_rbound_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_rbound_divisiontracestepsstepafter. ff_h_pfp_rbound_divisiontracestepsstepafter + S (pfh_after_rbound_divisiontracestepsstep) = S ((S (S (pfh_index_rbound_divisiontracesteps))) * pfs_history_scale_rbound_division)) /\ exists ff_q_pfp_rbound_divisiontracestepsstepafter. pfs_history_code_rbound_division = ff_q_pfp_rbound_divisiontracestepsstepafter * S ((S (S (pfh_index_rbound_divisiontracesteps))) * pfs_history_scale_rbound_division) + (pfh_after_rbound_divisiontracestepsstep))) /\ (((((exists pfa_gap_rbound_divisiontracestepsstepmultiplyleft. pfa_gap_rbound_divisiontracestepsstepmultiplyleft + S (pfh_before_rbound_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_rbound_divisiontracestepsstepmultiplyright. pfa_gap_rbound_divisiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_rbound_divisiontracestepsstepmultiplyresultbound. pfa_gap_rbound_divisiontracestepsstepmultiplyresultbound + S (pfh_product_rbound_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_rbound_divisiontracestepsstepmultiplyresultcongruence pfa_offset_right_rbound_divisiontracestepsstepmultiplyresultcongruence. ((pfh_before_rbound_divisiontracestepsstep) * (a)) + (p) * pfa_offset_left_rbound_divisiontracestepsstepmultiplyresultcongruence = (pfh_product_rbound_divisiontracestepsstep) + (p) * pfa_offset_right_rbound_divisiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_rbound_divisiontracestepsstepaddleft. pfa_gap_rbound_divisiontracestepsstepaddleft + S (pfh_product_rbound_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_rbound_divisiontracestepsstepaddright. pfa_gap_rbound_divisiontracestepsstepaddright + S (pfh_coefficient_rbound_divisiontracestepsstep) = (p)) /\ ((((exists pfa_gap_rbound_divisiontracestepsstepaddresultbound. pfa_gap_rbound_divisiontracestepsstepaddresultbound + S (pfh_after_rbound_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_rbound_divisiontracestepsstepaddresultcongruence pfa_offset_right_rbound_divisiontracestepsstepaddresultcongruence. ((pfh_product_rbound_divisiontracestepsstep) + (pfh_coefficient_rbound_divisiontracestepsstep)) + (p) * pfa_offset_left_rbound_divisiontracestepsstepaddresultcongruence = (pfh_after_rbound_divisiontracestepsstep) + (p) * pfa_offset_right_rbound_divisiontracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_rbound_divisionquotient ff_source_mcp_pfs_rbound_divisionquotient ff_target_mcp_pfs_rbound_divisionquotient. (exists mcp_gap_pfs_rbound_divisionquotient_bound. mcp_gap_pfs_rbound_divisionquotient_bound + S (ff_index_mcp_pfs_rbound_divisionquotient) = (n)) -> (((exists fs_h_mcp_pfs_rbound_divisionquotient_source. fs_h_mcp_pfs_rbound_divisionquotient_source + S (ff_source_mcp_pfs_rbound_divisionquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_rbound_divisionquotient)) * pfs_history_scale_rbound_division)) /\ exists fs_q_mcp_pfs_rbound_divisionquotient_source. pfs_history_code_rbound_division = fs_q_mcp_pfs_rbound_divisionquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_rbound_divisionquotient)) * pfs_history_scale_rbound_division) + (ff_source_mcp_pfs_rbound_divisionquotient))) -> (((exists fs_h_mcp_pfs_rbound_divisionquotient_target. fs_h_mcp_pfs_rbound_divisionquotient_target + S (ff_target_mcp_pfs_rbound_divisionquotient) = S ((S (ff_index_mcp_pfs_rbound_divisionquotient)) * qc)) /\ exists fs_q_mcp_pfs_rbound_divisionquotient_target. qb = fs_q_mcp_pfs_rbound_divisionquotient_target * S ((S (ff_index_mcp_pfs_rbound_divisionquotient)) * qc) + (ff_target_mcp_pfs_rbound_divisionquotient))) -> ff_target_mcp_pfs_rbound_divisionquotient = ff_source_mcp_pfs_rbound_divisionquotient)))) -> (exists pfa_gap_rbound_result. pfa_gap_rbound_result + S (r) = (p))

Complete tactic proof in conservative notation

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

28 script commands · 3 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 (1)
prime 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 hp
  10. L10
    intro hs
02Use earlier factsL11–20

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

  1. L11
    specialize prime_field_polynomial_horner_result_bounded (p)
  2. L12
    specialize prime_field_polynomial_horner_result_bounded (b)
  3. L13
    specialize prime_field_polynomial_horner_result_bounded (c)
  4. L14
    specialize prime_field_polynomial_horner_result_bounded (a)
  5. L15
    specialize prime_field_polynomial_horner_result_bounded (S n)
  6. L16
    specialize prime_field_polynomial_horner_result_bounded (r)
  7. L17
    apply prime_field_polynomial_horner_result_bounded
  8. L18
    exact hp
  9. L19
    specialize prime_field_polynomial_synthetic_remainder_execution (p)
  10. L20
    specialize prime_field_polynomial_synthetic_remainder_execution (b)
03Use earlier factsL21–28

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

  1. L21
    specialize prime_field_polynomial_synthetic_remainder_execution (c)
  2. L22
    specialize prime_field_polynomial_synthetic_remainder_execution (a)
  3. L23
    specialize prime_field_polynomial_synthetic_remainder_execution (n)
  4. L24
    specialize prime_field_polynomial_synthetic_remainder_execution (qb)
  5. L25
    specialize prime_field_polynomial_synthetic_remainder_execution (qc)
  6. L26
    specialize prime_field_polynomial_synthetic_remainder_execution (r)
  7. L27
    apply prime_field_polynomial_synthetic_remainder_execution
  8. L28
    exact hs

Library-wide reading audit

Original defined command ledger · 28 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 hp
  10. 0010intro hs
  11. 0011specialize prime_field_polynomial_horner_result_bounded (p)
  12. 0012specialize prime_field_polynomial_horner_result_bounded (b)
  13. 0013specialize prime_field_polynomial_horner_result_bounded (c)
  14. 0014specialize prime_field_polynomial_horner_result_bounded (a)
  15. 0015specialize prime_field_polynomial_horner_result_bounded (S n)
  16. 0016specialize prime_field_polynomial_horner_result_bounded (r)
  17. 0017apply prime_field_polynomial_horner_result_bounded
  18. 0018exact hp
  19. 0019specialize prime_field_polynomial_synthetic_remainder_execution (p)
  20. 0020specialize prime_field_polynomial_synthetic_remainder_execution (b)
  21. 0021specialize prime_field_polynomial_synthetic_remainder_execution (c)
  22. 0022specialize prime_field_polynomial_synthetic_remainder_execution (a)
  23. 0023specialize prime_field_polynomial_synthetic_remainder_execution (n)
  24. 0024specialize prime_field_polynomial_synthetic_remainder_execution (qb)
  25. 0025specialize prime_field_polynomial_synthetic_remainder_execution (qc)
  26. 0026specialize prime_field_polynomial_synthetic_remainder_execution (r)
  27. 0027apply prime_field_polynomial_synthetic_remainder_execution
  28. 0028exact hs