PQ002E

prime_field_polynomial_trim_represented_degree

Every nonempty actual trim has the existing represented degree given by the predecessor of its retained length; the zero polynomial receives no degree.

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. ∀ L. ∀ t. ∀ d. ∀ e. ∀ M. ∀ q. FpPolynomialTrim(p,b,c,L,t,d,e,M) → M = S q → FpRepresentedDegree(p,d,e,M,q)

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

Definition DAG

FpRepresentedDegree(p,b,c,L,d) · 1FpPolynomialTrim(p,b,c,L,t,d,e,M) · 1

Actual proof prerequisites

prime_field_polynomial_trim_output_coefficientssucc_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall p b c L t d e M q. ((((L)=(t)+(M)) /\ (((forall fom_index_pfp_trim_degree_inputinput. (exists fom_gap_pfp_trim_degree_inputinput_index_bound. fom_gap_pfp_trim_degree_inputinput_index_bound + S (fom_index_pfp_trim_degree_inputinput) = L) -> exists fom_value_pfp_trim_degree_inputinput. ((((exists fom_beta_height_pfp_trim_degree_inputinput_entry. fom_beta_height_pfp_trim_degree_inputinput_entry + S (fom_value_pfp_trim_degree_inputinput) = S ((S (fom_index_pfp_trim_degree_inputinput)) * c)) /\ exists fom_beta_quotient_pfp_trim_degree_inputinput_entry. b = fom_beta_quotient_pfp_trim_degree_inputinput_entry * S ((S (fom_index_pfp_trim_degree_inputinput)) * c) + (fom_value_pfp_trim_degree_inputinput))) /\ (exists fom_gap_pfp_trim_degree_inputinput_value_bound. fom_gap_pfp_trim_degree_inputinput_value_bound + S (fom_value_pfp_trim_degree_inputinput) = p))) /\ (((forall pfp_repeat_index_trim_degree_inputremoved. (exists pfa_gap_trim_degree_inputremovedindex. pfa_gap_trim_degree_inputremovedindex + S (pfp_repeat_index_trim_degree_inputremoved) = (t)) -> (((exists ff_h_pfp_trim_degree_inputremovedentry. ff_h_pfp_trim_degree_inputremovedentry + S (0) = S ((S (pfp_repeat_index_trim_degree_inputremoved)) * c)) /\ exists ff_q_pfp_trim_degree_inputremovedentry. b = ff_q_pfp_trim_degree_inputremovedentry * S ((S (pfp_repeat_index_trim_degree_inputremoved)) * c) + (0)))) /\ (((forall pftrim_index_trim_degree_inputsuffix pftrim_value_trim_degree_inputsuffix. (exists pfa_gap_trim_degree_inputsuffixbound. pfa_gap_trim_degree_inputsuffixbound + S (pftrim_index_trim_degree_inputsuffix) = (M)) -> (((exists ff_h_pfp_trim_degree_inputsuffixsource. ff_h_pfp_trim_degree_inputsuffixsource + S (pftrim_value_trim_degree_inputsuffix) = S ((S ((t)+pftrim_index_trim_degree_inputsuffix)) * c)) /\ exists ff_q_pfp_trim_degree_inputsuffixsource. b = ff_q_pfp_trim_degree_inputsuffixsource * S ((S ((t)+pftrim_index_trim_degree_inputsuffix)) * c) + (pftrim_value_trim_degree_inputsuffix))) -> (((exists ff_h_pfp_trim_degree_inputsuffixoutput. ff_h_pfp_trim_degree_inputsuffixoutput + S (pftrim_value_trim_degree_inputsuffix) = S ((S (pftrim_index_trim_degree_inputsuffix)) * e)) /\ exists ff_q_pfp_trim_degree_inputsuffixoutput. d = ff_q_pfp_trim_degree_inputsuffixoutput * S ((S (pftrim_index_trim_degree_inputsuffix)) * e) + (pftrim_value_trim_degree_inputsuffix)))) /\ (((M)=0 \/ (exists pftrim_leading_trim_degree_inputnormal. ((((exists ff_h_pfp_trim_degree_inputnormalentry. ff_h_pfp_trim_degree_inputnormalentry + S (pftrim_leading_trim_degree_inputnormal) = S ((S (0)) * e)) /\ exists ff_q_pfp_trim_degree_inputnormalentry. d = ff_q_pfp_trim_degree_inputnormalentry * S ((S (0)) * e) + (pftrim_leading_trim_degree_inputnormal))) /\ ((~(pftrim_leading_trim_degree_inputnormal=0))))))))))))))) -> M=S q -> ((((M)=S (q)) /\ (((forall fom_index_pfp_trim_degree_resultcoefficients. (exists fom_gap_pfp_trim_degree_resultcoefficients_index_bound. fom_gap_pfp_trim_degree_resultcoefficients_index_bound + S (fom_index_pfp_trim_degree_resultcoefficients) = M) -> exists fom_value_pfp_trim_degree_resultcoefficients. ((((exists fom_beta_height_pfp_trim_degree_resultcoefficients_entry. fom_beta_height_pfp_trim_degree_resultcoefficients_entry + S (fom_value_pfp_trim_degree_resultcoefficients) = S ((S (fom_index_pfp_trim_degree_resultcoefficients)) * e)) /\ exists fom_beta_quotient_pfp_trim_degree_resultcoefficients_entry. d = fom_beta_quotient_pfp_trim_degree_resultcoefficients_entry * S ((S (fom_index_pfp_trim_degree_resultcoefficients)) * e) + (fom_value_pfp_trim_degree_resultcoefficients))) /\ (exists fom_gap_pfp_trim_degree_resultcoefficients_value_bound. fom_gap_pfp_trim_degree_resultcoefficients_value_bound + S (fom_value_pfp_trim_degree_resultcoefficients) = p))) /\ ((exists pfd_leading_trim_degree_result. ((((exists ff_h_pfp_trim_degree_resultentry. ff_h_pfp_trim_degree_resultentry + S (pfd_leading_trim_degree_result) = S ((S (0)) * e)) /\ exists ff_q_pfp_trim_degree_resultentry. d = ff_q_pfp_trim_degree_resultentry * S ((S (0)) * e) + (pfd_leading_trim_degree_result))) /\ ((~(pfd_leading_trim_degree_result=0))))))))))

Complete tactic proof in conservative notation

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

39 script commands · 8 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 trim output coefficients
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 L
  5. L5
    intro t
  6. L6
    intro d
  7. L7
    intro e
  8. L8
    intro M
  9. L9
    intro q
  10. L10
    intro h
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hlen
03Separate the logical casesL12–12

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

  1. L12
    split
04Use earlier factsL13–13

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

  1. L13
    exact hlen
05Separate the logical casesL14–14

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

  1. L14
    split
06Use earlier factsL15–24

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

  1. L15
    specialize prime_field_polynomial_trim_output_coefficients (p)
  2. L16
    specialize prime_field_polynomial_trim_output_coefficients (b)
  3. L17
    specialize prime_field_polynomial_trim_output_coefficients (c)
  4. L18
    specialize prime_field_polynomial_trim_output_coefficients (L)
  5. L19
    specialize prime_field_polynomial_trim_output_coefficients (t)
  6. L20
    specialize prime_field_polynomial_trim_output_coefficients (d)
  7. L21
    specialize prime_field_polynomial_trim_output_coefficients (e)
  8. L22
    specialize prime_field_polynomial_trim_output_coefficients (M)
  9. L23
    apply prime_field_polynomial_trim_output_coefficients
  10. L24
    exact h
07Separate the logical casesL25–30

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

  1. L25
    cases h
  2. L26
    cases h_right
  3. L27
    cases h_right_right
  4. L28
    cases h_right_right_right
  5. L29
    cases h_right_right_right_right
  6. L30
    exfalso
08Establish hzL31–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ ne zero.

  1. L31
    have hz : S q=0
  2. L32
    trans M
  3. L33
    symm
  4. L34
    exact hlen
  5. L35
    exact h_right_right_right_right_left
  6. L36
    specialize succ_ne_zero (q)
  7. L37
    apply succ_ne_zero
  8. L38
    exact hz
  9. L39
    exact h_right_right_right_right_right

Library-wide reading audit

Original defined command ledger · 39 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro L
  5. 0005intro t
  6. 0006intro d
  7. 0007intro e
  8. 0008intro M
  9. 0009intro q
  10. 0010intro h
  11. 0011intro hlen
  12. 0012split
  13. 0013exact hlen
  14. 0014split
  15. 0015specialize prime_field_polynomial_trim_output_coefficients (p)
  16. 0016specialize prime_field_polynomial_trim_output_coefficients (b)
  17. 0017specialize prime_field_polynomial_trim_output_coefficients (c)
  18. 0018specialize prime_field_polynomial_trim_output_coefficients (L)
  19. 0019specialize prime_field_polynomial_trim_output_coefficients (t)
  20. 0020specialize prime_field_polynomial_trim_output_coefficients (d)
  21. 0021specialize prime_field_polynomial_trim_output_coefficients (e)
  22. 0022specialize prime_field_polynomial_trim_output_coefficients (M)
  23. 0023apply prime_field_polynomial_trim_output_coefficients
  24. 0024exact h
  25. 0025cases h
  26. 0026cases h_right
  27. 0027cases h_right_right
  28. 0028cases h_right_right_right
  29. 0029cases h_right_right_right_right
  30. 0030exfalso
  31. 0031have hz : S q=0
  32. 0032trans M
  33. 0033symm
  34. 0034exact hlen
  35. 0035exact h_right_right_right_right_left
  36. 0036specialize succ_ne_zero (q)
  37. 0037apply succ_ne_zero
  38. 0038exact hz
  39. 0039exact h_right_right_right_right_right