PQ004B

prime_field_polynomial_synthetic_remainder_bounded

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every actual synthetic remainder is a canonical field value.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic 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))

Constructive proof overview

Generated structural guide

Every actual synthetic remainder is a canonical field value.

The unchanged tactic script uses 2 declared prerequisites and contains 28 exact native proof lines.

Alpha v34 checked-use · first admitted v32 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

prime_field_polynomial_horner_result_bounded Alpha theorem; checked-use authorized PQ0048 prime_field_polynomial_synthetic_remainder_execution

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 exact 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