PQ0027

prime_field_polynomial_trim_empty_of_zero

A genuinely all-zero input cannot have a nonempty normalized trim, proved using actual input and output beta values.

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. FpPolynomialTrim(p,b,c,L,t,d,e,M) → Repeat(b,c,0,L) → M = 0

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) · 1Repeat(b,c,a,l) · 1

Actual proof prerequisites

eq_decidable · checked external prerequisitematrix_recursive_lt_add_left · checked external prerequisiteone_le_of_ne_zero · checked external prerequisiteprime_field_polynomial_trim_leading_source_nonzero
Original expanded first-order statement 
forall p b c L t d e M. ((((L)=(t)+(M)) /\ (((forall fom_index_pfp_trim_all_zeroinput. (exists fom_gap_pfp_trim_all_zeroinput_index_bound. fom_gap_pfp_trim_all_zeroinput_index_bound + S (fom_index_pfp_trim_all_zeroinput) = L) -> exists fom_value_pfp_trim_all_zeroinput. ((((exists fom_beta_height_pfp_trim_all_zeroinput_entry. fom_beta_height_pfp_trim_all_zeroinput_entry + S (fom_value_pfp_trim_all_zeroinput) = S ((S (fom_index_pfp_trim_all_zeroinput)) * c)) /\ exists fom_beta_quotient_pfp_trim_all_zeroinput_entry. b = fom_beta_quotient_pfp_trim_all_zeroinput_entry * S ((S (fom_index_pfp_trim_all_zeroinput)) * c) + (fom_value_pfp_trim_all_zeroinput))) /\ (exists fom_gap_pfp_trim_all_zeroinput_value_bound. fom_gap_pfp_trim_all_zeroinput_value_bound + S (fom_value_pfp_trim_all_zeroinput) = p))) /\ (((forall pfp_repeat_index_trim_all_zeroremoved. (exists pfa_gap_trim_all_zeroremovedindex. pfa_gap_trim_all_zeroremovedindex + S (pfp_repeat_index_trim_all_zeroremoved) = (t)) -> (((exists ff_h_pfp_trim_all_zeroremovedentry. ff_h_pfp_trim_all_zeroremovedentry + S (0) = S ((S (pfp_repeat_index_trim_all_zeroremoved)) * c)) /\ exists ff_q_pfp_trim_all_zeroremovedentry. b = ff_q_pfp_trim_all_zeroremovedentry * S ((S (pfp_repeat_index_trim_all_zeroremoved)) * c) + (0)))) /\ (((forall pftrim_index_trim_all_zerosuffix pftrim_value_trim_all_zerosuffix. (exists pfa_gap_trim_all_zerosuffixbound. pfa_gap_trim_all_zerosuffixbound + S (pftrim_index_trim_all_zerosuffix) = (M)) -> (((exists ff_h_pfp_trim_all_zerosuffixsource. ff_h_pfp_trim_all_zerosuffixsource + S (pftrim_value_trim_all_zerosuffix) = S ((S ((t)+pftrim_index_trim_all_zerosuffix)) * c)) /\ exists ff_q_pfp_trim_all_zerosuffixsource. b = ff_q_pfp_trim_all_zerosuffixsource * S ((S ((t)+pftrim_index_trim_all_zerosuffix)) * c) + (pftrim_value_trim_all_zerosuffix))) -> (((exists ff_h_pfp_trim_all_zerosuffixoutput. ff_h_pfp_trim_all_zerosuffixoutput + S (pftrim_value_trim_all_zerosuffix) = S ((S (pftrim_index_trim_all_zerosuffix)) * e)) /\ exists ff_q_pfp_trim_all_zerosuffixoutput. d = ff_q_pfp_trim_all_zerosuffixoutput * S ((S (pftrim_index_trim_all_zerosuffix)) * e) + (pftrim_value_trim_all_zerosuffix)))) /\ (((M)=0 \/ (exists pftrim_leading_trim_all_zeronormal. ((((exists ff_h_pfp_trim_all_zeronormalentry. ff_h_pfp_trim_all_zeronormalentry + S (pftrim_leading_trim_all_zeronormal) = S ((S (0)) * e)) /\ exists ff_q_pfp_trim_all_zeronormalentry. d = ff_q_pfp_trim_all_zeronormalentry * S ((S (0)) * e) + (pftrim_leading_trim_all_zeronormal))) /\ ((~(pftrim_leading_trim_all_zeronormal=0))))))))))))))) -> (forall pfp_repeat_index_trim_all_zero_input. (exists pfa_gap_trim_all_zero_inputindex. pfa_gap_trim_all_zero_inputindex + S (pfp_repeat_index_trim_all_zero_input) = (L)) -> (((exists ff_h_pfp_trim_all_zero_inputentry. ff_h_pfp_trim_all_zero_inputentry + S (0) = S ((S (pfp_repeat_index_trim_all_zero_input)) * c)) /\ exists ff_q_pfp_trim_all_zero_inputentry. b = ff_q_pfp_trim_all_zero_inputentry * S ((S (pfp_repeat_index_trim_all_zero_input)) * c) + (0)))) -> M=0

Complete tactic proof in conservative notation

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

53 script commands · 13 reading checkpoints · 5 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 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 h
  10. L10
    intro hz
02Establish hML11–14

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

  1. L11
    have hM : M=0 \/ ~(M=0)
  2. L12
    specialize eq_decidable (M)
  3. L13
    specialize eq_decidable (0)
  4. L14
    apply eq_decidable
03Separate the logical casesL15–15

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

  1. L15
    cases hM
04Use earlier factsL16–16

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

  1. L16
    exact hM_left
05Establish hcopyL17–18

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

  1. L17
    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. L18
    exact h
06Separate the logical casesL19–22

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

  1. L19
    cases hcopy
  2. L20
    cases hcopy_right
  3. L21
    cases hcopy_right_right
  4. L22
    cases hcopy_right_right_right
07Establish htL23–31

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

  1. L23
  2. L24
    rewrite hcopy_left
  3. L25
    specialize matrix_recursive_lt_add_left (0)
  4. L26
    specialize matrix_recursive_lt_add_left (M)
  5. L27
    specialize matrix_recursive_lt_add_left (t)
  6. L28
    apply matrix_recursive_lt_add_left
  7. L29
    specialize one_le_of_ne_zero (M)
  8. L30
    apply one_le_of_ne_zero
  9. L31
    exact hM_right
08Establish hindexL32–34

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

  1. L32
    have hindex : t+0=t
  2. L33
    simp
  3. L34
    rewrite hindex at ht
09Establish hatL35–38

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

  1. L35
  2. L36
    specialize hz (t)
  3. L37
    apply hz
  4. L38
    exact ht
10Separate the logical casesL39–39

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

  1. L39
    exfalso
11Use earlier factsL40–49

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

  1. L40
    specialize prime_field_polynomial_trim_leading_source_nonzero (p)
  2. L41
    specialize prime_field_polynomial_trim_leading_source_nonzero (b)
  3. L42
    specialize prime_field_polynomial_trim_leading_source_nonzero (c)
  4. L43
    specialize prime_field_polynomial_trim_leading_source_nonzero (L)
  5. L44
    specialize prime_field_polynomial_trim_leading_source_nonzero (t)
  6. L45
    specialize prime_field_polynomial_trim_leading_source_nonzero (d)
  7. L46
    specialize prime_field_polynomial_trim_leading_source_nonzero (e)
  8. L47
    specialize prime_field_polynomial_trim_leading_source_nonzero (M)
  9. L48
    specialize prime_field_polynomial_trim_leading_source_nonzero (0)
  10. L49
    apply prime_field_polynomial_trim_leading_source_nonzero
12Use earlier factsL50–52

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

  1. L50
    exact h
  2. L51
    exact hM_right
  3. L52
    exact hat
13Calculate and transport equalitiesL53–53

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

  1. L53
    refl

Library-wide reading audit

Original defined command ledger · 53 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 h
  10. 0010intro hz
  11. 0011have hM : M=0 \/ ~(M=0)
  12. 0012specialize eq_decidable (M)
  13. 0013specialize eq_decidable (0)
  14. 0014apply eq_decidable
  15. 0015cases hM
  16. 0016exact hM_left
  17. 0017have hcopy : FpPolynomialTrim(p,b,c,L,t,d,e,M)
  18. 0018exact h
  19. 0019cases hcopy
  20. 0020cases hcopy_right
  21. 0021cases hcopy_right_right
  22. 0022cases hcopy_right_right_right
  23. 0023have ht : Lt(t + 0,L)
  24. 0024rewrite hcopy_left
  25. 0025specialize matrix_recursive_lt_add_left (0)
  26. 0026specialize matrix_recursive_lt_add_left (M)
  27. 0027specialize matrix_recursive_lt_add_left (t)
  28. 0028apply matrix_recursive_lt_add_left
  29. 0029specialize one_le_of_ne_zero (M)
  30. 0030apply one_le_of_ne_zero
  31. 0031exact hM_right
  32. 0032have hindex : t+0=t
  33. 0033simp
  34. 0034rewrite hindex at ht
  35. 0035have hat : BetaAt(b,c,t,0)
  36. 0036specialize hz (t)
  37. 0037apply hz
  38. 0038exact ht
  39. 0039exfalso
  40. 0040specialize prime_field_polynomial_trim_leading_source_nonzero (p)
  41. 0041specialize prime_field_polynomial_trim_leading_source_nonzero (b)
  42. 0042specialize prime_field_polynomial_trim_leading_source_nonzero (c)
  43. 0043specialize prime_field_polynomial_trim_leading_source_nonzero (L)
  44. 0044specialize prime_field_polynomial_trim_leading_source_nonzero (t)
  45. 0045specialize prime_field_polynomial_trim_leading_source_nonzero (d)
  46. 0046specialize prime_field_polynomial_trim_leading_source_nonzero (e)
  47. 0047specialize prime_field_polynomial_trim_leading_source_nonzero (M)
  48. 0048specialize prime_field_polynomial_trim_leading_source_nonzero (0)
  49. 0049apply prime_field_polynomial_trim_leading_source_nonzero
  50. 0050exact h
  51. 0051exact hM_right
  52. 0052exact hat
  53. 0053refl