PQ002E

prime_field_polynomial_trim_represented_degree

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

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

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 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))))))))))

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

PQ0023 prime_field_polynomial_trim_output_coefficients succ_ne_zero Stable theorem; checked-use authorized

Direct dependents

PQ002F prime_field_polynomial_trim_nonempty_degree_exists

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

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.

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 exact 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