PQ0027

prime_field_polynomial_trim_empty_of_zero

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

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

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. ((((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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 53 exact native proof lines.

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

Proof neighborhood

Direct dependencies

eq_decidable Stable theorem; checked-use authorized matrix_recursive_lt_add_left Alpha theorem; checked-use authorized one_le_of_ne_zero Stable theorem; checked-use authorized PQ0025 prime_field_polynomial_trim_leading_source_nonzero

Direct dependents

PQ0028 prime_field_polynomial_trim_zero_iff

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

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.

Named ingredients (1)
prime field polynomial trim leading source nonzero

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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
  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
    have ht : exists pfa_gap_trim_zero_cut_bound. pfa_gap_trim_zero_cut_bound + S (t+0) = (L)
  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
    have hat : ((exists ff_h_pfp_trim_zero_cut_entry. ff_h_pfp_trim_zero_cut_entry + S (0) = S ((S (t)) * c)) /\ exists ff_q_pfp_trim_zero_cut_entry. b = ff_q_pfp_trim_zero_cut_entry * S ((S (t)) * c) + (0))
  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 exact 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 : (((L)=(t)+(M)) /\ (((forall fom_index_pfp_trim_zero_copyinput. (exists fom_gap_pfp_trim_zero_copyinput_index_bound. fom_gap_pfp_trim_zero_copyinput_index_bound + S (fom_index_pfp_trim_zero_copyinput) = L) -> exists fom_value_pfp_trim_zero_copyinput. ((((exists fom_beta_height_pfp_trim_zero_copyinput_entry. fom_beta_height_pfp_trim_zero_copyinput_entry + S (fom_value_pfp_trim_zero_copyinput) = S ((S (fom_index_pfp_trim_zero_copyinput)) * c)) /\ exists fom_beta_quotient_pfp_trim_zero_copyinput_entry. b = fom_beta_quotient_pfp_trim_zero_copyinput_entry * S ((S (fom_index_pfp_trim_zero_copyinput)) * c) + (fom_value_pfp_trim_zero_copyinput))) /\ (exists fom_gap_pfp_trim_zero_copyinput_value_bound. fom_gap_pfp_trim_zero_copyinput_value_bound + S (fom_value_pfp_trim_zero_copyinput) = p))) /\ (((forall pfp_repeat_index_trim_zero_copyremoved. (exists pfa_gap_trim_zero_copyremovedindex. pfa_gap_trim_zero_copyremovedindex + S (pfp_repeat_index_trim_zero_copyremoved) = (t)) -> (((exists ff_h_pfp_trim_zero_copyremovedentry. ff_h_pfp_trim_zero_copyremovedentry + S (0) = S ((S (pfp_repeat_index_trim_zero_copyremoved)) * c)) /\ exists ff_q_pfp_trim_zero_copyremovedentry. b = ff_q_pfp_trim_zero_copyremovedentry * S ((S (pfp_repeat_index_trim_zero_copyremoved)) * c) + (0)))) /\ (((forall pftrim_index_trim_zero_copysuffix pftrim_value_trim_zero_copysuffix. (exists pfa_gap_trim_zero_copysuffixbound. pfa_gap_trim_zero_copysuffixbound + S (pftrim_index_trim_zero_copysuffix) = (M)) -> (((exists ff_h_pfp_trim_zero_copysuffixsource. ff_h_pfp_trim_zero_copysuffixsource + S (pftrim_value_trim_zero_copysuffix) = S ((S ((t)+pftrim_index_trim_zero_copysuffix)) * c)) /\ exists ff_q_pfp_trim_zero_copysuffixsource. b = ff_q_pfp_trim_zero_copysuffixsource * S ((S ((t)+pftrim_index_trim_zero_copysuffix)) * c) + (pftrim_value_trim_zero_copysuffix))) -> (((exists ff_h_pfp_trim_zero_copysuffixoutput. ff_h_pfp_trim_zero_copysuffixoutput + S (pftrim_value_trim_zero_copysuffix) = S ((S (pftrim_index_trim_zero_copysuffix)) * e)) /\ exists ff_q_pfp_trim_zero_copysuffixoutput. d = ff_q_pfp_trim_zero_copysuffixoutput * S ((S (pftrim_index_trim_zero_copysuffix)) * e) + (pftrim_value_trim_zero_copysuffix)))) /\ (((M)=0 \/ (exists pftrim_leading_trim_zero_copynormal. ((((exists ff_h_pfp_trim_zero_copynormalentry. ff_h_pfp_trim_zero_copynormalentry + S (pftrim_leading_trim_zero_copynormal) = S ((S (0)) * e)) /\ exists ff_q_pfp_trim_zero_copynormalentry. d = ff_q_pfp_trim_zero_copynormalentry * S ((S (0)) * e) + (pftrim_leading_trim_zero_copynormal))) /\ ((~(pftrim_leading_trim_zero_copynormal=0))))))))))))))
  18. 0018exact h
  19. 0019cases hcopy
  20. 0020cases hcopy_right
  21. 0021cases hcopy_right_right
  22. 0022cases hcopy_right_right_right
  23. 0023have ht : exists pfa_gap_trim_zero_cut_bound. pfa_gap_trim_zero_cut_bound + S (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 : ((exists ff_h_pfp_trim_zero_cut_entry. ff_h_pfp_trim_zero_cut_entry + S (0) = S ((S (t)) * c)) /\ exists ff_q_pfp_trim_zero_cut_entry. b = ff_q_pfp_trim_zero_cut_entry * S ((S (t)) * c) + (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