PQ004A

prime_field_polynomial_synthetic_quotient_bounded

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

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) → BetaPrefixInto(qb,qc,n,p)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 1FpSyntheticDivision(p,b,c,a,n,qb,qc,r) · 1Prime(p) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

beta_at_exists · checked external prerequisiteprime_field_polynomial_horner_result_bounded · checked external prerequisiteprime_field_polynomial_synthetic_quotient_entry
Original expanded first-order 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)))

Complete tactic proof in conservative notation

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

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.

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 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 : ∃ h. BetaAt(qb,qc,i,h)Definitions: BetaAt(qb,qc,i,h)Original native command in the exact edition
  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 defined 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 : ∃ h. BetaAt(qb,qc,i,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