PQ0053

prime_field_polynomial_synthetic_constant

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

A constant has an empty quotient and its own coefficient as remainder, without assigning a degree to the empty quotient.

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 qb qc r v. (~((p) = 1) /\ forall pfa_factor_left_constant_division_prime pfa_factor_right_constant_division_prime. (p) = pfa_factor_left_constant_division_prime * pfa_factor_right_constant_division_prime -> pfa_factor_left_constant_division_prime = 1 \/ pfa_factor_right_constant_division_prime = 1) -> (exists pfs_history_code_constant_division pfs_history_scale_constant_division. ((((exists pfa_gap_constant_divisiontracebase. pfa_gap_constant_divisiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_constant_divisiontraceinitial. ff_h_pfp_constant_divisiontraceinitial + S (0) = S ((S (0)) * pfs_history_scale_constant_division)) /\ exists ff_q_pfp_constant_divisiontraceinitial. pfs_history_code_constant_division = ff_q_pfp_constant_divisiontraceinitial * S ((S (0)) * pfs_history_scale_constant_division) + (0))) /\ (((((exists ff_h_pfp_constant_divisiontraceterminal. ff_h_pfp_constant_divisiontraceterminal + S (r) = S ((S (S (0))) * pfs_history_scale_constant_division)) /\ exists ff_q_pfp_constant_divisiontraceterminal. pfs_history_code_constant_division = ff_q_pfp_constant_divisiontraceterminal * S ((S (S (0))) * pfs_history_scale_constant_division) + (r))) /\ ((forall pfh_index_constant_divisiontracesteps. (exists pfa_gap_constant_divisiontracestepsindex. pfa_gap_constant_divisiontracestepsindex + S (pfh_index_constant_divisiontracesteps) = (S (0))) -> (exists pfh_coefficient_constant_divisiontracestepsstep pfh_before_constant_divisiontracestepsstep pfh_after_constant_divisiontracestepsstep pfh_product_constant_divisiontracestepsstep. ((((exists ff_h_pfp_constant_divisiontracestepsstepcoefficient. ff_h_pfp_constant_divisiontracestepsstepcoefficient + S (pfh_coefficient_constant_divisiontracestepsstep) = S ((S (pfh_index_constant_divisiontracesteps)) * c)) /\ exists ff_q_pfp_constant_divisiontracestepsstepcoefficient. b = ff_q_pfp_constant_divisiontracestepsstepcoefficient * S ((S (pfh_index_constant_divisiontracesteps)) * c) + (pfh_coefficient_constant_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_constant_divisiontracestepsstepbefore. ff_h_pfp_constant_divisiontracestepsstepbefore + S (pfh_before_constant_divisiontracestepsstep) = S ((S (pfh_index_constant_divisiontracesteps)) * pfs_history_scale_constant_division)) /\ exists ff_q_pfp_constant_divisiontracestepsstepbefore. pfs_history_code_constant_division = ff_q_pfp_constant_divisiontracestepsstepbefore * S ((S (pfh_index_constant_divisiontracesteps)) * pfs_history_scale_constant_division) + (pfh_before_constant_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_constant_divisiontracestepsstepafter. ff_h_pfp_constant_divisiontracestepsstepafter + S (pfh_after_constant_divisiontracestepsstep) = S ((S (S (pfh_index_constant_divisiontracesteps))) * pfs_history_scale_constant_division)) /\ exists ff_q_pfp_constant_divisiontracestepsstepafter. pfs_history_code_constant_division = ff_q_pfp_constant_divisiontracestepsstepafter * S ((S (S (pfh_index_constant_divisiontracesteps))) * pfs_history_scale_constant_division) + (pfh_after_constant_divisiontracestepsstep))) /\ (((((exists pfa_gap_constant_divisiontracestepsstepmultiplyleft. pfa_gap_constant_divisiontracestepsstepmultiplyleft + S (pfh_before_constant_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_constant_divisiontracestepsstepmultiplyright. pfa_gap_constant_divisiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_constant_divisiontracestepsstepmultiplyresultbound. pfa_gap_constant_divisiontracestepsstepmultiplyresultbound + S (pfh_product_constant_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_constant_divisiontracestepsstepmultiplyresultcongruence pfa_offset_right_constant_divisiontracestepsstepmultiplyresultcongruence. ((pfh_before_constant_divisiontracestepsstep) * (a)) + (p) * pfa_offset_left_constant_divisiontracestepsstepmultiplyresultcongruence = (pfh_product_constant_divisiontracestepsstep) + (p) * pfa_offset_right_constant_divisiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_constant_divisiontracestepsstepaddleft. pfa_gap_constant_divisiontracestepsstepaddleft + S (pfh_product_constant_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_constant_divisiontracestepsstepaddright. pfa_gap_constant_divisiontracestepsstepaddright + S (pfh_coefficient_constant_divisiontracestepsstep) = (p)) /\ ((((exists pfa_gap_constant_divisiontracestepsstepaddresultbound. pfa_gap_constant_divisiontracestepsstepaddresultbound + S (pfh_after_constant_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_constant_divisiontracestepsstepaddresultcongruence pfa_offset_right_constant_divisiontracestepsstepaddresultcongruence. ((pfh_product_constant_divisiontracestepsstep) + (pfh_coefficient_constant_divisiontracestepsstep)) + (p) * pfa_offset_left_constant_divisiontracestepsstepaddresultcongruence = (pfh_after_constant_divisiontracestepsstep) + (p) * pfa_offset_right_constant_divisiontracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_constant_divisionquotient ff_source_mcp_pfs_constant_divisionquotient ff_target_mcp_pfs_constant_divisionquotient. (exists mcp_gap_pfs_constant_divisionquotient_bound. mcp_gap_pfs_constant_divisionquotient_bound + S (ff_index_mcp_pfs_constant_divisionquotient) = (0)) -> (((exists fs_h_mcp_pfs_constant_divisionquotient_source. fs_h_mcp_pfs_constant_divisionquotient_source + S (ff_source_mcp_pfs_constant_divisionquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_constant_divisionquotient)) * pfs_history_scale_constant_division)) /\ exists fs_q_mcp_pfs_constant_divisionquotient_source. pfs_history_code_constant_division = fs_q_mcp_pfs_constant_divisionquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_constant_divisionquotient)) * pfs_history_scale_constant_division) + (ff_source_mcp_pfs_constant_divisionquotient))) -> (((exists fs_h_mcp_pfs_constant_divisionquotient_target. fs_h_mcp_pfs_constant_divisionquotient_target + S (ff_target_mcp_pfs_constant_divisionquotient) = S ((S (ff_index_mcp_pfs_constant_divisionquotient)) * qc)) /\ exists fs_q_mcp_pfs_constant_divisionquotient_target. qb = fs_q_mcp_pfs_constant_divisionquotient_target * S ((S (ff_index_mcp_pfs_constant_divisionquotient)) * qc) + (ff_target_mcp_pfs_constant_divisionquotient))) -> ff_target_mcp_pfs_constant_divisionquotient = ff_source_mcp_pfs_constant_divisionquotient)))) -> (((exists ff_h_pfp_constant_division_coefficient. ff_h_pfp_constant_division_coefficient + S (v) = S ((S (0)) * c)) /\ exists ff_q_pfp_constant_division_coefficient. b = ff_q_pfp_constant_division_coefficient * S ((S (0)) * c) + (v))) -> r=v

Constructive proof overview

Generated structural guide

A constant has an empty quotient and its own coefficient as remainder, without assigning a degree to the empty quotient.

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

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

Proof neighborhood

Direct dependencies

PQ004D prime_field_polynomial_horner_constant_value 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

30 script commands · 4 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 (2)
prime field polynomial horner constant valueprime 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 qb
  6. L6
    intro qc
  7. L7
    intro r
  8. L8
    intro v
  9. L9
    intro hp
  10. L10
    intro hs
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hv
03Use earlier factsL12–21

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

  1. L12
    specialize prime_field_polynomial_horner_constant_value (p)
  2. L13
    specialize prime_field_polynomial_horner_constant_value (b)
  3. L14
    specialize prime_field_polynomial_horner_constant_value (c)
  4. L15
    specialize prime_field_polynomial_horner_constant_value (a)
  5. L16
    specialize prime_field_polynomial_horner_constant_value (r)
  6. L17
    specialize prime_field_polynomial_horner_constant_value (v)
  7. L18
    apply prime_field_polynomial_horner_constant_value
  8. L19
    exact hp
  9. L20
    specialize prime_field_polynomial_synthetic_remainder_execution (p)
  10. L21
    specialize prime_field_polynomial_synthetic_remainder_execution (b)
04Use earlier factsL22–30

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

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

Library-wide reading audit

Original exact command ledger · 30 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro a
  5. 0005intro qb
  6. 0006intro qc
  7. 0007intro r
  8. 0008intro v
  9. 0009intro hp
  10. 0010intro hs
  11. 0011intro hv
  12. 0012specialize prime_field_polynomial_horner_constant_value (p)
  13. 0013specialize prime_field_polynomial_horner_constant_value (b)
  14. 0014specialize prime_field_polynomial_horner_constant_value (c)
  15. 0015specialize prime_field_polynomial_horner_constant_value (a)
  16. 0016specialize prime_field_polynomial_horner_constant_value (r)
  17. 0017specialize prime_field_polynomial_horner_constant_value (v)
  18. 0018apply prime_field_polynomial_horner_constant_value
  19. 0019exact hp
  20. 0020specialize prime_field_polynomial_synthetic_remainder_execution (p)
  21. 0021specialize prime_field_polynomial_synthetic_remainder_execution (b)
  22. 0022specialize prime_field_polynomial_synthetic_remainder_execution (c)
  23. 0023specialize prime_field_polynomial_synthetic_remainder_execution (a)
  24. 0024specialize prime_field_polynomial_synthetic_remainder_execution (0)
  25. 0025specialize prime_field_polynomial_synthetic_remainder_execution (qb)
  26. 0026specialize prime_field_polynomial_synthetic_remainder_execution (qc)
  27. 0027specialize prime_field_polynomial_synthetic_remainder_execution (r)
  28. 0028apply prime_field_polynomial_synthetic_remainder_execution
  29. 0029exact hs
  30. 0030exact hv