PQ0053

prime_field_polynomial_synthetic_constant

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

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. ∀ qb. ∀ qc. ∀ r. ∀ v. Prime(p) → FpSyntheticDivision(p,b,c,a,0,qb,qc,r) → BetaAt(b,c,0,v) → r = v

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

Definition DAG

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

Actual proof prerequisites

prime_field_polynomial_horner_constant_valueprime_field_polynomial_synthetic_remainder_execution
Original expanded first-order 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

Complete tactic proof in conservative notation

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

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.

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 (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 defined 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