PQ002A

prime_field_polynomial_trim_removed_count_unique

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

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

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

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

le_antisymm Stable theorem; checked-use authorized PQ0029 prime_field_polynomial_trim_removed_le

Direct dependents

PQ002B prime_field_polynomial_trim_retained_length_unique PQ002C prime_field_polynomial_trim_output_equal PQ002D prime_field_polynomial_trim_exists_unique

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

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.

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