PQ0029

prime_field_polynomial_trim_removed_le

One normalized cut cannot lie after another: otherwise a supposedly leading nonzero coefficient belongs to the other removed zero 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) → Le(t,u)

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

Definition DAG

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

Actual proof prerequisites

prime_field_polynomial_trim_length_boundsle_or_lt · checked external prerequisiteeq_decidable · checked external prerequisitelt_not_le · checked external prerequisiteprime_field_polynomial_trim_leading_source_nonzero
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))))))))))))))) -> (exists pftrim_gap_unique_removed_le. pftrim_gap_unique_removed_le+(t)=(u))

Complete tactic proof in conservative notation

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

79 script commands · 20 reading checkpoints · 7 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 (2)
prime field polynomial trim length boundsprime field polynomial trim leading source nonzero
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 hboundL15–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial trim length bounds.

  1. L15
    have hbound : Le(t,L) ∧ Le(M,L)Definitions: Le(t,L)Le(M,L)Original native command in the exact edition
  2. L16
    specialize prime_field_polynomial_trim_length_bounds (p)
  3. L17
    specialize prime_field_polynomial_trim_length_bounds (b)
  4. L18
    specialize prime_field_polynomial_trim_length_bounds (c)
  5. L19
    specialize prime_field_polynomial_trim_length_bounds (L)
  6. L20
    specialize prime_field_polynomial_trim_length_bounds (t)
  7. L21
    specialize prime_field_polynomial_trim_length_bounds (d)
  8. L22
    specialize prime_field_polynomial_trim_length_bounds (e)
  9. L23
    specialize prime_field_polynomial_trim_length_bounds (M)
  10. L24
    apply prime_field_polynomial_trim_length_bounds
04Use earlier factsL25–25

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

  1. L25
    exact h
05Separate the logical casesL26–26

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

  1. L26
    cases hbound
06Establish horderL27–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le or lt.

  1. L27
    have horder : Le(t,u) ∨ Lt(u,t)Definitions: Le(t,u)Lt(u,t)Original native command in the exact edition
  2. L28
    specialize le_or_lt (t)
  3. L29
    specialize le_or_lt (u)
  4. L30
    apply le_or_lt
07Separate the logical casesL31–31

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

  1. L31
    cases horder
08Use earlier factsL32–32

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

  1. L32
    exact horder_left
09Separate the logical casesL33–33

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

  1. L33
    exfalso
10Establish hNL34–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eq decidable.

  1. L34
    have hN : N=0 \/ ~(N=0)
  2. L35
    specialize eq_decidable (N)
  3. L36
    specialize eq_decidable (0)
  4. L37
    apply eq_decidable
11Separate the logical casesL38–38

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

  1. L38
    cases hN
12Establish hkcopyL39–40

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

  1. L39
    have hkcopy : FpPolynomialTrim(p,b,c,L,u,f,g,N)Definitions: FpPolynomialTrim(p,b,c,L,u,f,g,N)Original native command in the exact edition
  2. L40
    exact hk
13Separate the logical casesL41–44

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

  1. L41
    cases hkcopy
  2. L42
    cases hkcopy_right
  3. L43
    cases hkcopy_right_right
  4. L44
    cases hkcopy_right_right_right
14Establish hlenL45–54

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt not le.

  1. L45
    have hlen : L=u
  2. L46
    trans u+N
  3. L47
    exact hkcopy_left
  4. L48
    rewrite hN_left
  5. L49
    simp
  6. L50
    rewrite hlen at hbound_left
  7. L51
    specialize lt_not_le (u)
  8. L52
    specialize lt_not_le (t)
  9. L53
    apply lt_not_le
  10. L54
    exact horder_right
15Use earlier factsL55–55

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

  1. L55
    exact hbound_left
16Establish hcopyL56–57

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

  1. L56
    have hcopy : FpPolynomialTrim(p,b,c,L,t,d,e,M)Definitions: FpPolynomialTrim(p,b,c,L,t,d,e,M)Original native command in the exact edition
  2. L57
    exact h
17Separate the logical casesL58–61

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

  1. L58
    cases hcopy
  2. L59
    cases hcopy_right
  3. L60
    cases hcopy_right_right
  4. L61
    cases hcopy_right_right_right
18Establish hzL62–71

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hcopy right right left.

  1. L62
  2. L63
    specialize hcopy_right_right_left (u)
  3. L64
    apply hcopy_right_right_left
  4. L65
    exact horder_right
  5. L66
    specialize prime_field_polynomial_trim_leading_source_nonzero (p)
  6. L67
    specialize prime_field_polynomial_trim_leading_source_nonzero (b)
  7. L68
    specialize prime_field_polynomial_trim_leading_source_nonzero (c)
  8. L69
    specialize prime_field_polynomial_trim_leading_source_nonzero (L)
  9. L70
    specialize prime_field_polynomial_trim_leading_source_nonzero (u)
  10. L71
    specialize prime_field_polynomial_trim_leading_source_nonzero (f)
19Use earlier factsL72–78

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

  1. L72
    specialize prime_field_polynomial_trim_leading_source_nonzero (g)
  2. L73
    specialize prime_field_polynomial_trim_leading_source_nonzero (N)
  3. L74
    specialize prime_field_polynomial_trim_leading_source_nonzero (0)
  4. L75
    apply prime_field_polynomial_trim_leading_source_nonzero
  5. L76
    exact hk
  6. L77
    exact hN_right
  7. L78
    exact hz
20Calculate and transport equalitiesL79–79

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

  1. L79
    refl

Library-wide reading audit

Original defined command ledger · 79 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 hbound : Le(t,L) ∧ Le(M,L)
  16. 0016specialize prime_field_polynomial_trim_length_bounds (p)
  17. 0017specialize prime_field_polynomial_trim_length_bounds (b)
  18. 0018specialize prime_field_polynomial_trim_length_bounds (c)
  19. 0019specialize prime_field_polynomial_trim_length_bounds (L)
  20. 0020specialize prime_field_polynomial_trim_length_bounds (t)
  21. 0021specialize prime_field_polynomial_trim_length_bounds (d)
  22. 0022specialize prime_field_polynomial_trim_length_bounds (e)
  23. 0023specialize prime_field_polynomial_trim_length_bounds (M)
  24. 0024apply prime_field_polynomial_trim_length_bounds
  25. 0025exact h
  26. 0026cases hbound
  27. 0027have horder : Le(t,u) ∨ Lt(u,t)
  28. 0028specialize le_or_lt (t)
  29. 0029specialize le_or_lt (u)
  30. 0030apply le_or_lt
  31. 0031cases horder
  32. 0032exact horder_left
  33. 0033exfalso
  34. 0034have hN : N=0 \/ ~(N=0)
  35. 0035specialize eq_decidable (N)
  36. 0036specialize eq_decidable (0)
  37. 0037apply eq_decidable
  38. 0038cases hN
  39. 0039have hkcopy : FpPolynomialTrim(p,b,c,L,u,f,g,N)
  40. 0040exact hk
  41. 0041cases hkcopy
  42. 0042cases hkcopy_right
  43. 0043cases hkcopy_right_right
  44. 0044cases hkcopy_right_right_right
  45. 0045have hlen : L=u
  46. 0046trans u+N
  47. 0047exact hkcopy_left
  48. 0048rewrite hN_left
  49. 0049simp
  50. 0050rewrite hlen at hbound_left
  51. 0051specialize lt_not_le (u)
  52. 0052specialize lt_not_le (t)
  53. 0053apply lt_not_le
  54. 0054exact horder_right
  55. 0055exact hbound_left
  56. 0056have hcopy : FpPolynomialTrim(p,b,c,L,t,d,e,M)
  57. 0057exact h
  58. 0058cases hcopy
  59. 0059cases hcopy_right
  60. 0060cases hcopy_right_right
  61. 0061cases hcopy_right_right_right
  62. 0062have hz : BetaAt(b,c,u,0)
  63. 0063specialize hcopy_right_right_left (u)
  64. 0064apply hcopy_right_right_left
  65. 0065exact horder_right
  66. 0066specialize prime_field_polynomial_trim_leading_source_nonzero (p)
  67. 0067specialize prime_field_polynomial_trim_leading_source_nonzero (b)
  68. 0068specialize prime_field_polynomial_trim_leading_source_nonzero (c)
  69. 0069specialize prime_field_polynomial_trim_leading_source_nonzero (L)
  70. 0070specialize prime_field_polynomial_trim_leading_source_nonzero (u)
  71. 0071specialize prime_field_polynomial_trim_leading_source_nonzero (f)
  72. 0072specialize prime_field_polynomial_trim_leading_source_nonzero (g)
  73. 0073specialize prime_field_polynomial_trim_leading_source_nonzero (N)
  74. 0074specialize prime_field_polynomial_trim_leading_source_nonzero (0)
  75. 0075apply prime_field_polynomial_trim_leading_source_nonzero
  76. 0076exact hk
  77. 0077exact hN_right
  78. 0078exact hz
  79. 0079refl