PQ002B

prime_field_polynomial_trim_retained_length_unique

The retained representation length is unique by the actual length split and additive cancellation.

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) → M = N

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

prime_field_polynomial_trim_removed_count_uniqueadd_left_cancel · checked external prerequisite
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))))))))))))))) -> M=N

Complete tactic proof in conservative notation

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

51 script commands · 13 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 removed count unique
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
03Establish htL15–24

Establish this local claim before using it. It is not an additional assumption.

  1. L15
    have ht : t=u
  2. L16
    specialize prime_field_polynomial_trim_removed_count_unique (p)
  3. L17
    specialize prime_field_polynomial_trim_removed_count_unique (b)
  4. L18
    specialize prime_field_polynomial_trim_removed_count_unique (c)
  5. L19
    specialize prime_field_polynomial_trim_removed_count_unique (L)
  6. L20
    specialize prime_field_polynomial_trim_removed_count_unique (t)
  7. L21
    specialize prime_field_polynomial_trim_removed_count_unique (d)
  8. L22
    specialize prime_field_polynomial_trim_removed_count_unique (e)
  9. L23
    specialize prime_field_polynomial_trim_removed_count_unique (M)
  10. L24
    specialize prime_field_polynomial_trim_removed_count_unique (u)
04Use earlier factsL25–30

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

  1. L25
    specialize prime_field_polynomial_trim_removed_count_unique (f)
  2. L26
    specialize prime_field_polynomial_trim_removed_count_unique (g)
  3. L27
    specialize prime_field_polynomial_trim_removed_count_unique (N)
  4. L28
    apply prime_field_polynomial_trim_removed_count_unique
  5. L29
    exact h
  6. L30
    exact hk
05Separate the logical casesL31–38

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

  1. L31
    cases h
  2. L32
    cases h_right
  3. L33
    cases h_right_right
  4. L34
    cases h_right_right_right
  5. L35
    cases hk
  6. L36
    cases hk_right
  7. L37
    cases hk_right_right
  8. L38
    cases hk_right_right_right
06Use earlier factsL39–42

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

  1. L39
    specialize add_left_cancel (t)
  2. L40
    specialize add_left_cancel (M)
  3. L41
    specialize add_left_cancel (N)
  4. L42
    apply add_left_cancel
07Calculate and transport equalitiesL43–44

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L43
    trans L
  2. L44
    symm
08Use earlier factsL45–45

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

  1. L45
    exact h_left
09Calculate and transport equalitiesL46–46

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L46
    trans u+N
10Use earlier factsL47–47

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

  1. L47
    exact hk_left
11Calculate and transport equalitiesL48–49

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L48
    congr
  2. L49
    symm
12Use earlier factsL50–50

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

  1. L50
    exact ht
13Calculate and transport equalitiesL51–51

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L51
    refl

Library-wide reading audit

Original defined command ledger · 51 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. 0015have ht : t=u
  16. 0016specialize prime_field_polynomial_trim_removed_count_unique (p)
  17. 0017specialize prime_field_polynomial_trim_removed_count_unique (b)
  18. 0018specialize prime_field_polynomial_trim_removed_count_unique (c)
  19. 0019specialize prime_field_polynomial_trim_removed_count_unique (L)
  20. 0020specialize prime_field_polynomial_trim_removed_count_unique (t)
  21. 0021specialize prime_field_polynomial_trim_removed_count_unique (d)
  22. 0022specialize prime_field_polynomial_trim_removed_count_unique (e)
  23. 0023specialize prime_field_polynomial_trim_removed_count_unique (M)
  24. 0024specialize prime_field_polynomial_trim_removed_count_unique (u)
  25. 0025specialize prime_field_polynomial_trim_removed_count_unique (f)
  26. 0026specialize prime_field_polynomial_trim_removed_count_unique (g)
  27. 0027specialize prime_field_polynomial_trim_removed_count_unique (N)
  28. 0028apply prime_field_polynomial_trim_removed_count_unique
  29. 0029exact h
  30. 0030exact hk
  31. 0031cases h
  32. 0032cases h_right
  33. 0033cases h_right_right
  34. 0034cases h_right_right_right
  35. 0035cases hk
  36. 0036cases hk_right
  37. 0037cases hk_right_right
  38. 0038cases hk_right_right_right
  39. 0039specialize add_left_cancel (t)
  40. 0040specialize add_left_cancel (M)
  41. 0041specialize add_left_cancel (N)
  42. 0042apply add_left_cancel
  43. 0043trans L
  44. 0044symm
  45. 0045exact h_left
  46. 0046trans u+N
  47. 0047exact hk_left
  48. 0048congr
  49. 0049symm
  50. 0050exact ht
  51. 0051refl