PQ002A

prime_field_polynomial_trim_removed_count_unique

The number of removed leading zero coefficients is uniquely determined by the annotated input prefix.

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. ∀ u. ∀ f. ∀ g. ∀ N. FpPolynomialTrim(p,b,c,L,t,d,e,M) → FpPolynomialTrim(p,b,c,L,u,f,g,N) → t = u

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

Definition DAG

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

Actual proof prerequisites

le_antisymm · checked external prerequisiteprime_field_polynomial_trim_removed_le
Original expanded first-order statement 
forall p b c L t d e M u f g N. ((((L)=(t)+(M)) /\ (((forall fom_index_pfp_unique_firstinput. (exists fom_gap_pfp_unique_firstinput_index_bound. fom_gap_pfp_unique_firstinput_index_bound + S (fom_index_pfp_unique_firstinput) = L) -> exists fom_value_pfp_unique_firstinput. ((((exists fom_beta_height_pfp_unique_firstinput_entry. fom_beta_height_pfp_unique_firstinput_entry + S (fom_value_pfp_unique_firstinput) = S ((S (fom_index_pfp_unique_firstinput)) * c)) /\ exists fom_beta_quotient_pfp_unique_firstinput_entry. b = fom_beta_quotient_pfp_unique_firstinput_entry * S ((S (fom_index_pfp_unique_firstinput)) * c) + (fom_value_pfp_unique_firstinput))) /\ (exists fom_gap_pfp_unique_firstinput_value_bound. fom_gap_pfp_unique_firstinput_value_bound + S (fom_value_pfp_unique_firstinput) = p))) /\ (((forall pfp_repeat_index_unique_firstremoved. (exists pfa_gap_unique_firstremovedindex. pfa_gap_unique_firstremovedindex + S (pfp_repeat_index_unique_firstremoved) = (t)) -> (((exists ff_h_pfp_unique_firstremovedentry. ff_h_pfp_unique_firstremovedentry + S (0) = S ((S (pfp_repeat_index_unique_firstremoved)) * c)) /\ exists ff_q_pfp_unique_firstremovedentry. b = ff_q_pfp_unique_firstremovedentry * S ((S (pfp_repeat_index_unique_firstremoved)) * c) + (0)))) /\ (((forall pftrim_index_unique_firstsuffix pftrim_value_unique_firstsuffix. (exists pfa_gap_unique_firstsuffixbound. pfa_gap_unique_firstsuffixbound + S (pftrim_index_unique_firstsuffix) = (M)) -> (((exists ff_h_pfp_unique_firstsuffixsource. ff_h_pfp_unique_firstsuffixsource + S (pftrim_value_unique_firstsuffix) = S ((S ((t)+pftrim_index_unique_firstsuffix)) * c)) /\ exists ff_q_pfp_unique_firstsuffixsource. b = ff_q_pfp_unique_firstsuffixsource * S ((S ((t)+pftrim_index_unique_firstsuffix)) * c) + (pftrim_value_unique_firstsuffix))) -> (((exists ff_h_pfp_unique_firstsuffixoutput. ff_h_pfp_unique_firstsuffixoutput + S (pftrim_value_unique_firstsuffix) = S ((S (pftrim_index_unique_firstsuffix)) * e)) /\ exists ff_q_pfp_unique_firstsuffixoutput. d = ff_q_pfp_unique_firstsuffixoutput * S ((S (pftrim_index_unique_firstsuffix)) * e) + (pftrim_value_unique_firstsuffix)))) /\ (((M)=0 \/ (exists pftrim_leading_unique_firstnormal. ((((exists ff_h_pfp_unique_firstnormalentry. ff_h_pfp_unique_firstnormalentry + S (pftrim_leading_unique_firstnormal) = S ((S (0)) * e)) /\ exists ff_q_pfp_unique_firstnormalentry. d = ff_q_pfp_unique_firstnormalentry * S ((S (0)) * e) + (pftrim_leading_unique_firstnormal))) /\ ((~(pftrim_leading_unique_firstnormal=0))))))))))))))) -> ((((L)=(u)+(N)) /\ (((forall fom_index_pfp_unique_secondinput. (exists fom_gap_pfp_unique_secondinput_index_bound. fom_gap_pfp_unique_secondinput_index_bound + S (fom_index_pfp_unique_secondinput) = L) -> exists fom_value_pfp_unique_secondinput. ((((exists fom_beta_height_pfp_unique_secondinput_entry. fom_beta_height_pfp_unique_secondinput_entry + S (fom_value_pfp_unique_secondinput) = S ((S (fom_index_pfp_unique_secondinput)) * c)) /\ exists fom_beta_quotient_pfp_unique_secondinput_entry. b = fom_beta_quotient_pfp_unique_secondinput_entry * S ((S (fom_index_pfp_unique_secondinput)) * c) + (fom_value_pfp_unique_secondinput))) /\ (exists fom_gap_pfp_unique_secondinput_value_bound. fom_gap_pfp_unique_secondinput_value_bound + S (fom_value_pfp_unique_secondinput) = p))) /\ (((forall pfp_repeat_index_unique_secondremoved. (exists pfa_gap_unique_secondremovedindex. pfa_gap_unique_secondremovedindex + S (pfp_repeat_index_unique_secondremoved) = (u)) -> (((exists ff_h_pfp_unique_secondremovedentry. ff_h_pfp_unique_secondremovedentry + S (0) = S ((S (pfp_repeat_index_unique_secondremoved)) * c)) /\ exists ff_q_pfp_unique_secondremovedentry. b = ff_q_pfp_unique_secondremovedentry * S ((S (pfp_repeat_index_unique_secondremoved)) * c) + (0)))) /\ (((forall pftrim_index_unique_secondsuffix pftrim_value_unique_secondsuffix. (exists pfa_gap_unique_secondsuffixbound. pfa_gap_unique_secondsuffixbound + S (pftrim_index_unique_secondsuffix) = (N)) -> (((exists ff_h_pfp_unique_secondsuffixsource. ff_h_pfp_unique_secondsuffixsource + S (pftrim_value_unique_secondsuffix) = S ((S ((u)+pftrim_index_unique_secondsuffix)) * c)) /\ exists ff_q_pfp_unique_secondsuffixsource. b = ff_q_pfp_unique_secondsuffixsource * S ((S ((u)+pftrim_index_unique_secondsuffix)) * c) + (pftrim_value_unique_secondsuffix))) -> (((exists ff_h_pfp_unique_secondsuffixoutput. ff_h_pfp_unique_secondsuffixoutput + S (pftrim_value_unique_secondsuffix) = S ((S (pftrim_index_unique_secondsuffix)) * g)) /\ exists ff_q_pfp_unique_secondsuffixoutput. f = ff_q_pfp_unique_secondsuffixoutput * S ((S (pftrim_index_unique_secondsuffix)) * g) + (pftrim_value_unique_secondsuffix)))) /\ (((N)=0 \/ (exists pftrim_leading_unique_secondnormal. ((((exists ff_h_pfp_unique_secondnormalentry. ff_h_pfp_unique_secondnormalentry + S (pftrim_leading_unique_secondnormal) = S ((S (0)) * g)) /\ exists ff_q_pfp_unique_secondnormalentry. f = ff_q_pfp_unique_secondnormalentry * S ((S (0)) * g) + (pftrim_leading_unique_secondnormal))) /\ ((~(pftrim_leading_unique_secondnormal=0))))))))))))))) -> t=u

Complete tactic proof in conservative notation

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

47 script commands · 6 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 (1)
prime field polynomial trim removed le
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 u
  10. L10
    intro f
02Fix variables and assumptionsL11–14

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

  1. L11
    intro g
  2. L12
    intro N
  3. L13
    intro h
  4. L14
    intro hk
03Use earlier factsL15–24

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

  1. L15
    specialize le_antisymm (t)
  2. L16
    specialize le_antisymm (u)
  3. L17
    apply le_antisymm
  4. L18
    specialize prime_field_polynomial_trim_removed_le (p)
  5. L19
    specialize prime_field_polynomial_trim_removed_le (b)
  6. L20
    specialize prime_field_polynomial_trim_removed_le (c)
  7. L21
    specialize prime_field_polynomial_trim_removed_le (L)
  8. L22
    specialize prime_field_polynomial_trim_removed_le (t)
  9. L23
    specialize prime_field_polynomial_trim_removed_le (d)
  10. L24
    specialize prime_field_polynomial_trim_removed_le (e)
04Use earlier factsL25–34

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

  1. L25
    specialize prime_field_polynomial_trim_removed_le (M)
  2. L26
    specialize prime_field_polynomial_trim_removed_le (u)
  3. L27
    specialize prime_field_polynomial_trim_removed_le (f)
  4. L28
    specialize prime_field_polynomial_trim_removed_le (g)
  5. L29
    specialize prime_field_polynomial_trim_removed_le (N)
  6. L30
    apply prime_field_polynomial_trim_removed_le
  7. L31
    exact h
  8. L32
    exact hk
  9. L33
    specialize prime_field_polynomial_trim_removed_le (p)
  10. L34
    specialize prime_field_polynomial_trim_removed_le (b)
05Use earlier factsL35–44

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

  1. L35
    specialize prime_field_polynomial_trim_removed_le (c)
  2. L36
    specialize prime_field_polynomial_trim_removed_le (L)
  3. L37
    specialize prime_field_polynomial_trim_removed_le (u)
  4. L38
    specialize prime_field_polynomial_trim_removed_le (f)
  5. L39
    specialize prime_field_polynomial_trim_removed_le (g)
  6. L40
    specialize prime_field_polynomial_trim_removed_le (N)
  7. L41
    specialize prime_field_polynomial_trim_removed_le (t)
  8. L42
    specialize prime_field_polynomial_trim_removed_le (d)
  9. L43
    specialize prime_field_polynomial_trim_removed_le (e)
  10. L44
    specialize prime_field_polynomial_trim_removed_le (M)
06Use earlier factsL45–47

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

  1. L45
    apply prime_field_polynomial_trim_removed_le
  2. L46
    exact hk
  3. L47
    exact h

Library-wide reading audit

Original defined command ledger · 47 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 u
  10. 0010intro f
  11. 0011intro g
  12. 0012intro N
  13. 0013intro h
  14. 0014intro hk
  15. 0015specialize le_antisymm (t)
  16. 0016specialize le_antisymm (u)
  17. 0017apply le_antisymm
  18. 0018specialize prime_field_polynomial_trim_removed_le (p)
  19. 0019specialize prime_field_polynomial_trim_removed_le (b)
  20. 0020specialize prime_field_polynomial_trim_removed_le (c)
  21. 0021specialize prime_field_polynomial_trim_removed_le (L)
  22. 0022specialize prime_field_polynomial_trim_removed_le (t)
  23. 0023specialize prime_field_polynomial_trim_removed_le (d)
  24. 0024specialize prime_field_polynomial_trim_removed_le (e)
  25. 0025specialize prime_field_polynomial_trim_removed_le (M)
  26. 0026specialize prime_field_polynomial_trim_removed_le (u)
  27. 0027specialize prime_field_polynomial_trim_removed_le (f)
  28. 0028specialize prime_field_polynomial_trim_removed_le (g)
  29. 0029specialize prime_field_polynomial_trim_removed_le (N)
  30. 0030apply prime_field_polynomial_trim_removed_le
  31. 0031exact h
  32. 0032exact hk
  33. 0033specialize prime_field_polynomial_trim_removed_le (p)
  34. 0034specialize prime_field_polynomial_trim_removed_le (b)
  35. 0035specialize prime_field_polynomial_trim_removed_le (c)
  36. 0036specialize prime_field_polynomial_trim_removed_le (L)
  37. 0037specialize prime_field_polynomial_trim_removed_le (u)
  38. 0038specialize prime_field_polynomial_trim_removed_le (f)
  39. 0039specialize prime_field_polynomial_trim_removed_le (g)
  40. 0040specialize prime_field_polynomial_trim_removed_le (N)
  41. 0041specialize prime_field_polynomial_trim_removed_le (t)
  42. 0042specialize prime_field_polynomial_trim_removed_le (d)
  43. 0043specialize prime_field_polynomial_trim_removed_le (e)
  44. 0044specialize prime_field_polynomial_trim_removed_le (M)
  45. 0045apply prime_field_polynomial_trim_removed_le
  46. 0046exact hk
  47. 0047exact h