PQ002C

prime_field_polynomial_trim_output_equal

All actual trims of the same input agree coefficientwise on the unique retained prefix; no beta-code identity follows.

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) → ∀ x. ∀ y. Lt(x,M) → BetaAt(d,e,x,y) → BetaAt(f,g,x,y)

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

Definition DAG

FpPolynomialTrim(p,b,c,L,t,d,e,M) · 2Lt(a,b) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

prime_field_polynomial_trim_removed_count_uniqueprime_field_polynomial_trim_retained_length_uniqueprime_field_polynomial_suffix_equal
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))))))))))))))) -> (forall mdr_i_pfp_unique_coefficients mdr_a_pfp_unique_coefficients. (exists mdr_gap_pfp_unique_coefficientsb. mdr_gap_pfp_unique_coefficientsb + S (mdr_i_pfp_unique_coefficients) = (M)) -> (((exists ff_h_mdr_pfp_unique_coefficientso. ff_h_mdr_pfp_unique_coefficientso + S (mdr_a_pfp_unique_coefficients) = S ((S (mdr_i_pfp_unique_coefficients)) * e)) /\ exists ff_q_mdr_pfp_unique_coefficientso. d = ff_q_mdr_pfp_unique_coefficientso * S ((S (mdr_i_pfp_unique_coefficients)) * e) + (mdr_a_pfp_unique_coefficients))) -> (((exists ff_h_mdr_pfp_unique_coefficientsn. ff_h_mdr_pfp_unique_coefficientsn + S (mdr_a_pfp_unique_coefficients) = S ((S (mdr_i_pfp_unique_coefficients)) * g)) /\ exists ff_q_mdr_pfp_unique_coefficientsn. f = ff_q_mdr_pfp_unique_coefficientsn * S ((S (mdr_i_pfp_unique_coefficients)) * g) + (mdr_a_pfp_unique_coefficients))))

Complete tactic proof in conservative notation

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

69 script commands · 10 reading checkpoints · 2 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 (3)
prime field polynomial trim removed count uniqueprime field polynomial trim retained length uniqueprime field polynomial suffix equal
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
05Establish hML31–40

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

  1. L31
    have hM : M=N
  2. L32
    specialize prime_field_polynomial_trim_retained_length_unique (p)
  3. L33
    specialize prime_field_polynomial_trim_retained_length_unique (b)
  4. L34
    specialize prime_field_polynomial_trim_retained_length_unique (c)
  5. L35
    specialize prime_field_polynomial_trim_retained_length_unique (L)
  6. L36
    specialize prime_field_polynomial_trim_retained_length_unique (t)
  7. L37
    specialize prime_field_polynomial_trim_retained_length_unique (d)
  8. L38
    specialize prime_field_polynomial_trim_retained_length_unique (e)
  9. L39
    specialize prime_field_polynomial_trim_retained_length_unique (M)
  10. L40
    specialize prime_field_polynomial_trim_retained_length_unique (u)
06Use earlier factsL41–46

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

  1. L41
    specialize prime_field_polynomial_trim_retained_length_unique (f)
  2. L42
    specialize prime_field_polynomial_trim_retained_length_unique (g)
  3. L43
    specialize prime_field_polynomial_trim_retained_length_unique (N)
  4. L44
    apply prime_field_polynomial_trim_retained_length_unique
  5. L45
    exact h
  6. L46
    exact hk
07Separate the logical casesL47–54

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

  1. L47
    cases h
  2. L48
    cases h_right
  3. L49
    cases h_right_right
  4. L50
    cases h_right_right_right
  5. L51
    cases hk
  6. L52
    cases hk_right
  7. L53
    cases hk_right_right
  8. L54
    cases hk_right_right_right
08Calculate and transport equalitiesL55–58

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

  1. L55
    rewrite ht at h_right_right_right_left
  2. L56
    rewrite ht at h_right_right_right_left
  3. L57
    rewrite hM at h_right_right_right_left
  4. L58
    rewrite hM
09Use earlier factsL59–68

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

  1. L59
    specialize prime_field_polynomial_suffix_equal (b)
  2. L60
    specialize prime_field_polynomial_suffix_equal (c)
  3. L61
    specialize prime_field_polynomial_suffix_equal (u)
  4. L62
    specialize prime_field_polynomial_suffix_equal (d)
  5. L63
    specialize prime_field_polynomial_suffix_equal (e)
  6. L64
    specialize prime_field_polynomial_suffix_equal (f)
  7. L65
    specialize prime_field_polynomial_suffix_equal (g)
  8. L66
    specialize prime_field_polynomial_suffix_equal (N)
  9. L67
    apply prime_field_polynomial_suffix_equal
  10. L68
    exact h_right_right_right_left
10Use earlier factsL69–69

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

  1. L69
    exact hk_right_right_right_left

Library-wide reading audit

Original defined command ledger · 69 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. 0031have hM : M=N
  32. 0032specialize prime_field_polynomial_trim_retained_length_unique (p)
  33. 0033specialize prime_field_polynomial_trim_retained_length_unique (b)
  34. 0034specialize prime_field_polynomial_trim_retained_length_unique (c)
  35. 0035specialize prime_field_polynomial_trim_retained_length_unique (L)
  36. 0036specialize prime_field_polynomial_trim_retained_length_unique (t)
  37. 0037specialize prime_field_polynomial_trim_retained_length_unique (d)
  38. 0038specialize prime_field_polynomial_trim_retained_length_unique (e)
  39. 0039specialize prime_field_polynomial_trim_retained_length_unique (M)
  40. 0040specialize prime_field_polynomial_trim_retained_length_unique (u)
  41. 0041specialize prime_field_polynomial_trim_retained_length_unique (f)
  42. 0042specialize prime_field_polynomial_trim_retained_length_unique (g)
  43. 0043specialize prime_field_polynomial_trim_retained_length_unique (N)
  44. 0044apply prime_field_polynomial_trim_retained_length_unique
  45. 0045exact h
  46. 0046exact hk
  47. 0047cases h
  48. 0048cases h_right
  49. 0049cases h_right_right
  50. 0050cases h_right_right_right
  51. 0051cases hk
  52. 0052cases hk_right
  53. 0053cases hk_right_right
  54. 0054cases hk_right_right_right
  55. 0055rewrite ht at h_right_right_right_left
  56. 0056rewrite ht at h_right_right_right_left
  57. 0057rewrite hM at h_right_right_right_left
  58. 0058rewrite hM
  59. 0059specialize prime_field_polynomial_suffix_equal (b)
  60. 0060specialize prime_field_polynomial_suffix_equal (c)
  61. 0061specialize prime_field_polynomial_suffix_equal (u)
  62. 0062specialize prime_field_polynomial_suffix_equal (d)
  63. 0063specialize prime_field_polynomial_suffix_equal (e)
  64. 0064specialize prime_field_polynomial_suffix_equal (f)
  65. 0065specialize prime_field_polynomial_suffix_equal (g)
  66. 0066specialize prime_field_polynomial_suffix_equal (N)
  67. 0067apply prime_field_polynomial_suffix_equal
  68. 0068exact h_right_right_right_left
  69. 0069exact hk_right_right_right_left