PQ004A

prime_field_polynomial_synthetic_quotient_bounded

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

The constructively encoded quotient has canonical coefficients at every one of its n positions; this includes an empty quotient for constants.

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_bounded_prime pfa_factor_right_bounded_prime. (p) = pfa_factor_left_bounded_prime * pfa_factor_right_bounded_prime -> pfa_factor_left_bounded_prime = 1 \/ pfa_factor_right_bounded_prime = 1) -> (exists pfs_history_code_bounded_division pfs_history_scale_bounded_division. ((((exists pfa_gap_bounded_divisiontracebase. pfa_gap_bounded_divisiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_bounded_divisiontraceinitial. ff_h_pfp_bounded_divisiontraceinitial + S (0) = S ((S (0)) * pfs_history_scale_bounded_division)) /\ exists ff_q_pfp_bounded_divisiontraceinitial. pfs_history_code_bounded_division = ff_q_pfp_bounded_divisiontraceinitial * S ((S (0)) * pfs_history_scale_bounded_division) + (0))) /\ (((((exists ff_h_pfp_bounded_divisiontraceterminal. ff_h_pfp_bounded_divisiontraceterminal + S (r) = S ((S (S (n))) * pfs_history_scale_bounded_division)) /\ exists ff_q_pfp_bounded_divisiontraceterminal. pfs_history_code_bounded_division = ff_q_pfp_bounded_divisiontraceterminal * S ((S (S (n))) * pfs_history_scale_bounded_division) + (r))) /\ ((forall pfh_index_bounded_divisiontracesteps. (exists pfa_gap_bounded_divisiontracestepsindex. pfa_gap_bounded_divisiontracestepsindex + S (pfh_index_bounded_divisiontracesteps) = (S (n))) -> (exists pfh_coefficient_bounded_divisiontracestepsstep pfh_before_bounded_divisiontracestepsstep pfh_after_bounded_divisiontracestepsstep pfh_product_bounded_divisiontracestepsstep. ((((exists ff_h_pfp_bounded_divisiontracestepsstepcoefficient. ff_h_pfp_bounded_divisiontracestepsstepcoefficient + S (pfh_coefficient_bounded_divisiontracestepsstep) = S ((S (pfh_index_bounded_divisiontracesteps)) * c)) /\ exists ff_q_pfp_bounded_divisiontracestepsstepcoefficient. b = ff_q_pfp_bounded_divisiontracestepsstepcoefficient * S ((S (pfh_index_bounded_divisiontracesteps)) * c) + (pfh_coefficient_bounded_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_bounded_divisiontracestepsstepbefore. ff_h_pfp_bounded_divisiontracestepsstepbefore + S (pfh_before_bounded_divisiontracestepsstep) = S ((S (pfh_index_bounded_divisiontracesteps)) * pfs_history_scale_bounded_division)) /\ exists ff_q_pfp_bounded_divisiontracestepsstepbefore. pfs_history_code_bounded_division = ff_q_pfp_bounded_divisiontracestepsstepbefore * S ((S (pfh_index_bounded_divisiontracesteps)) * pfs_history_scale_bounded_division) + (pfh_before_bounded_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_bounded_divisiontracestepsstepafter. ff_h_pfp_bounded_divisiontracestepsstepafter + S (pfh_after_bounded_divisiontracestepsstep) = S ((S (S (pfh_index_bounded_divisiontracesteps))) * pfs_history_scale_bounded_division)) /\ exists ff_q_pfp_bounded_divisiontracestepsstepafter. pfs_history_code_bounded_division = ff_q_pfp_bounded_divisiontracestepsstepafter * S ((S (S (pfh_index_bounded_divisiontracesteps))) * pfs_history_scale_bounded_division) + (pfh_after_bounded_divisiontracestepsstep))) /\ (((((exists pfa_gap_bounded_divisiontracestepsstepmultiplyleft. pfa_gap_bounded_divisiontracestepsstepmultiplyleft + S (pfh_before_bounded_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_bounded_divisiontracestepsstepmultiplyright. pfa_gap_bounded_divisiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_bounded_divisiontracestepsstepmultiplyresultbound. pfa_gap_bounded_divisiontracestepsstepmultiplyresultbound + S (pfh_product_bounded_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_bounded_divisiontracestepsstepmultiplyresultcongruence pfa_offset_right_bounded_divisiontracestepsstepmultiplyresultcongruence. ((pfh_before_bounded_divisiontracestepsstep) * (a)) + (p) * pfa_offset_left_bounded_divisiontracestepsstepmultiplyresultcongruence = (pfh_product_bounded_divisiontracestepsstep) + (p) * pfa_offset_right_bounded_divisiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_bounded_divisiontracestepsstepaddleft. pfa_gap_bounded_divisiontracestepsstepaddleft + S (pfh_product_bounded_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_bounded_divisiontracestepsstepaddright. pfa_gap_bounded_divisiontracestepsstepaddright + S (pfh_coefficient_bounded_divisiontracestepsstep) = (p)) /\ ((((exists pfa_gap_bounded_divisiontracestepsstepaddresultbound. pfa_gap_bounded_divisiontracestepsstepaddresultbound + S (pfh_after_bounded_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_bounded_divisiontracestepsstepaddresultcongruence pfa_offset_right_bounded_divisiontracestepsstepaddresultcongruence. ((pfh_product_bounded_divisiontracestepsstep) + (pfh_coefficient_bounded_divisiontracestepsstep)) + (p) * pfa_offset_left_bounded_divisiontracestepsstepaddresultcongruence = (pfh_after_bounded_divisiontracestepsstep) + (p) * pfa_offset_right_bounded_divisiontracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_bounded_divisionquotient ff_source_mcp_pfs_bounded_divisionquotient ff_target_mcp_pfs_bounded_divisionquotient. (exists mcp_gap_pfs_bounded_divisionquotient_bound. mcp_gap_pfs_bounded_divisionquotient_bound + S (ff_index_mcp_pfs_bounded_divisionquotient) = (n)) -> (((exists fs_h_mcp_pfs_bounded_divisionquotient_source. fs_h_mcp_pfs_bounded_divisionquotient_source + S (ff_source_mcp_pfs_bounded_divisionquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_bounded_divisionquotient)) * pfs_history_scale_bounded_division)) /\ exists fs_q_mcp_pfs_bounded_divisionquotient_source. pfs_history_code_bounded_division = fs_q_mcp_pfs_bounded_divisionquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_bounded_divisionquotient)) * pfs_history_scale_bounded_division) + (ff_source_mcp_pfs_bounded_divisionquotient))) -> (((exists fs_h_mcp_pfs_bounded_divisionquotient_target. fs_h_mcp_pfs_bounded_divisionquotient_target + S (ff_target_mcp_pfs_bounded_divisionquotient) = S ((S (ff_index_mcp_pfs_bounded_divisionquotient)) * qc)) /\ exists fs_q_mcp_pfs_bounded_divisionquotient_target. qb = fs_q_mcp_pfs_bounded_divisionquotient_target * S ((S (ff_index_mcp_pfs_bounded_divisionquotient)) * qc) + (ff_target_mcp_pfs_bounded_divisionquotient))) -> ff_target_mcp_pfs_bounded_divisionquotient = ff_source_mcp_pfs_bounded_divisionquotient)))) -> (forall fom_index_pfp_bounded_quotient. (exists fom_gap_pfp_bounded_quotient_index_bound. fom_gap_pfp_bounded_quotient_index_bound + S (fom_index_pfp_bounded_quotient) = n) -> exists fom_value_pfp_bounded_quotient. ((((exists fom_beta_height_pfp_bounded_quotient_entry. fom_beta_height_pfp_bounded_quotient_entry + S (fom_value_pfp_bounded_quotient) = S ((S (fom_index_pfp_bounded_quotient)) * qc)) /\ exists fom_beta_quotient_pfp_bounded_quotient_entry. qb = fom_beta_quotient_pfp_bounded_quotient_entry * S ((S (fom_index_pfp_bounded_quotient)) * qc) + (fom_value_pfp_bounded_quotient))) /\ (exists fom_gap_pfp_bounded_quotient_value_bound. fom_gap_pfp_bounded_quotient_value_bound + S (fom_value_pfp_bounded_quotient) = p)))

Constructive proof overview

Generated structural guide

The constructively encoded quotient has canonical coefficients at every one of its n positions; this includes an empty quotient for constants.

The unchanged tactic script uses 3 declared prerequisites and contains 43 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized prime_field_polynomial_horner_result_bounded Alpha theorem; checked-use authorized PQ0049 prime_field_polynomial_synthetic_quotient_entry

Direct dependents

PQ0052 prime_field_polynomial_synthetic_represented_degree

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

43 script commands · 9 reading checkpoints · 1 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 quotient entry
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
02Fix variables and assumptionsL11–12

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

  1. L11
    intro i
  2. L12
    intro hi
03Establish heL13–17

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

  1. L13
    have he : exists h. (((exists ff_h_pfp_bounded_entry. ff_h_pfp_bounded_entry + S (h) = S ((S (i)) * qc)) /\ exists ff_q_pfp_bounded_entry. qb = ff_q_pfp_bounded_entry * S ((S (i)) * qc) + (h)))
  2. L14
    specialize beta_at_exists (qb)
  3. L15
    specialize beta_at_exists (qc)
  4. L16
    specialize beta_at_exists (i)
  5. L17
    apply beta_at_exists
04Separate the logical casesL18–18

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

  1. L18
    cases he
05Construct an explicit witnessL19–19

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

  1. L19
    exists x
06Separate the logical casesL20–20

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

  1. L20
    split
07Use earlier factsL21–30

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

  1. L21
    exact he_witness
  2. L22
    specialize prime_field_polynomial_horner_result_bounded (p)
  3. L23
    specialize prime_field_polynomial_horner_result_bounded (b)
  4. L24
    specialize prime_field_polynomial_horner_result_bounded (c)
  5. L25
    specialize prime_field_polynomial_horner_result_bounded (a)
  6. L26
    specialize prime_field_polynomial_horner_result_bounded (S i)
  7. L27
    specialize prime_field_polynomial_horner_result_bounded (x)
  8. L28
    apply prime_field_polynomial_horner_result_bounded
  9. L29
    exact hp
  10. L30
    specialize prime_field_polynomial_synthetic_quotient_entry (p)
08Use earlier factsL31–40

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

  1. L31
    specialize prime_field_polynomial_synthetic_quotient_entry (b)
  2. L32
    specialize prime_field_polynomial_synthetic_quotient_entry (c)
  3. L33
    specialize prime_field_polynomial_synthetic_quotient_entry (a)
  4. L34
    specialize prime_field_polynomial_synthetic_quotient_entry (n)
  5. L35
    specialize prime_field_polynomial_synthetic_quotient_entry (qb)
  6. L36
    specialize prime_field_polynomial_synthetic_quotient_entry (qc)
  7. L37
    specialize prime_field_polynomial_synthetic_quotient_entry (r)
  8. L38
    specialize prime_field_polynomial_synthetic_quotient_entry (i)
  9. L39
    specialize prime_field_polynomial_synthetic_quotient_entry (x)
  10. L40
    apply prime_field_polynomial_synthetic_quotient_entry
09Use earlier factsL41–43

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

  1. L41
    exact hs
  2. L42
    exact hi
  3. L43
    exact he_witness

Library-wide reading audit

Original exact command ledger · 43 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. 0011intro i
  12. 0012intro hi
  13. 0013have he : exists h. (((exists ff_h_pfp_bounded_entry. ff_h_pfp_bounded_entry + S (h) = S ((S (i)) * qc)) /\ exists ff_q_pfp_bounded_entry. qb = ff_q_pfp_bounded_entry * S ((S (i)) * qc) + (h)))
  14. 0014specialize beta_at_exists (qb)
  15. 0015specialize beta_at_exists (qc)
  16. 0016specialize beta_at_exists (i)
  17. 0017apply beta_at_exists
  18. 0018cases he
  19. 0019exists x
  20. 0020split
  21. 0021exact he_witness
  22. 0022specialize prime_field_polynomial_horner_result_bounded (p)
  23. 0023specialize prime_field_polynomial_horner_result_bounded (b)
  24. 0024specialize prime_field_polynomial_horner_result_bounded (c)
  25. 0025specialize prime_field_polynomial_horner_result_bounded (a)
  26. 0026specialize prime_field_polynomial_horner_result_bounded (S i)
  27. 0027specialize prime_field_polynomial_horner_result_bounded (x)
  28. 0028apply prime_field_polynomial_horner_result_bounded
  29. 0029exact hp
  30. 0030specialize prime_field_polynomial_synthetic_quotient_entry (p)
  31. 0031specialize prime_field_polynomial_synthetic_quotient_entry (b)
  32. 0032specialize prime_field_polynomial_synthetic_quotient_entry (c)
  33. 0033specialize prime_field_polynomial_synthetic_quotient_entry (a)
  34. 0034specialize prime_field_polynomial_synthetic_quotient_entry (n)
  35. 0035specialize prime_field_polynomial_synthetic_quotient_entry (qb)
  36. 0036specialize prime_field_polynomial_synthetic_quotient_entry (qc)
  37. 0037specialize prime_field_polynomial_synthetic_quotient_entry (r)
  38. 0038specialize prime_field_polynomial_synthetic_quotient_entry (i)
  39. 0039specialize prime_field_polynomial_synthetic_quotient_entry (x)
  40. 0040apply prime_field_polynomial_synthetic_quotient_entry
  41. 0041exact hs
  42. 0042exact hi
  43. 0043exact he_witness