PQ002B

prime_field_polynomial_trim_retained_length_unique

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

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

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

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

PQ002A prime_field_polynomial_trim_removed_count_unique add_left_cancel Stable theorem; checked-use authorized

Direct dependents

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

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.

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