PQ0020

prime_field_polynomial_trim_from_cut

An actually constructed first-nonzero cut and actual suffix supply the normalized output head; no output-bound or algebra-law premise is assumed.

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. BetaPrefixInto(b,c,L,p) → L = t + M ∧ (Repeat(b,c,0,t) ∧ (M = 0 ∨ ¬M = 0 ∧ (∃ x. BetaAt(b,c,t,x) ∧ ¬x = 0))) → PolynomialSuffix(b,c,t,d,e,M) → FpPolynomialTrim(p,b,c,L,t,d,e,M)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 1PolynomialSuffix(b,c,t,d,e,M) · 1FpPolynomialTrim(p,b,c,L,t,d,e,M) · 1BetaAt(b,c,i,x) · 1Repeat(b,c,a,l) · 1

Actual proof prerequisites

one_le_of_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall p b c L t d e M. (forall fom_index_pfp_cut_to_trim_coefficients. (exists fom_gap_pfp_cut_to_trim_coefficients_index_bound. fom_gap_pfp_cut_to_trim_coefficients_index_bound + S (fom_index_pfp_cut_to_trim_coefficients) = L) -> exists fom_value_pfp_cut_to_trim_coefficients. ((((exists fom_beta_height_pfp_cut_to_trim_coefficients_entry. fom_beta_height_pfp_cut_to_trim_coefficients_entry + S (fom_value_pfp_cut_to_trim_coefficients) = S ((S (fom_index_pfp_cut_to_trim_coefficients)) * c)) /\ exists fom_beta_quotient_pfp_cut_to_trim_coefficients_entry. b = fom_beta_quotient_pfp_cut_to_trim_coefficients_entry * S ((S (fom_index_pfp_cut_to_trim_coefficients)) * c) + (fom_value_pfp_cut_to_trim_coefficients))) /\ (exists fom_gap_pfp_cut_to_trim_coefficients_value_bound. fom_gap_pfp_cut_to_trim_coefficients_value_bound + S (fom_value_pfp_cut_to_trim_coefficients) = p))) -> ((((L)=(t)+(M)) /\ (((forall pfp_repeat_index_cut_to_trim_sourcezero. (exists pfa_gap_cut_to_trim_sourcezeroindex. pfa_gap_cut_to_trim_sourcezeroindex + S (pfp_repeat_index_cut_to_trim_sourcezero) = (t)) -> (((exists ff_h_pfp_cut_to_trim_sourcezeroentry. ff_h_pfp_cut_to_trim_sourcezeroentry + S (0) = S ((S (pfp_repeat_index_cut_to_trim_sourcezero)) * c)) /\ exists ff_q_pfp_cut_to_trim_sourcezeroentry. b = ff_q_pfp_cut_to_trim_sourcezeroentry * S ((S (pfp_repeat_index_cut_to_trim_sourcezero)) * c) + (0)))) /\ (((M)=0 \/ (((~((M)=0)) /\ ((exists pftrim_leading_cut_to_trim_sourcehead. ((((exists ff_h_pfp_cut_to_trim_sourceheadentry. ff_h_pfp_cut_to_trim_sourceheadentry + S (pftrim_leading_cut_to_trim_sourcehead) = S ((S (t)) * c)) /\ exists ff_q_pfp_cut_to_trim_sourceheadentry. b = ff_q_pfp_cut_to_trim_sourceheadentry * S ((S (t)) * c) + (pftrim_leading_cut_to_trim_sourcehead))) /\ ((~(pftrim_leading_cut_to_trim_sourcehead=0)))))))))))))) -> (forall pftrim_index_cut_to_trim_suffix pftrim_value_cut_to_trim_suffix. (exists pfa_gap_cut_to_trim_suffixbound. pfa_gap_cut_to_trim_suffixbound + S (pftrim_index_cut_to_trim_suffix) = (M)) -> (((exists ff_h_pfp_cut_to_trim_suffixsource. ff_h_pfp_cut_to_trim_suffixsource + S (pftrim_value_cut_to_trim_suffix) = S ((S ((t)+pftrim_index_cut_to_trim_suffix)) * c)) /\ exists ff_q_pfp_cut_to_trim_suffixsource. b = ff_q_pfp_cut_to_trim_suffixsource * S ((S ((t)+pftrim_index_cut_to_trim_suffix)) * c) + (pftrim_value_cut_to_trim_suffix))) -> (((exists ff_h_pfp_cut_to_trim_suffixoutput. ff_h_pfp_cut_to_trim_suffixoutput + S (pftrim_value_cut_to_trim_suffix) = S ((S (pftrim_index_cut_to_trim_suffix)) * e)) /\ exists ff_q_pfp_cut_to_trim_suffixoutput. d = ff_q_pfp_cut_to_trim_suffixoutput * S ((S (pftrim_index_cut_to_trim_suffix)) * e) + (pftrim_value_cut_to_trim_suffix)))) -> ((((L)=(t)+(M)) /\ (((forall fom_index_pfp_cut_to_trim_resultinput. (exists fom_gap_pfp_cut_to_trim_resultinput_index_bound. fom_gap_pfp_cut_to_trim_resultinput_index_bound + S (fom_index_pfp_cut_to_trim_resultinput) = L) -> exists fom_value_pfp_cut_to_trim_resultinput. ((((exists fom_beta_height_pfp_cut_to_trim_resultinput_entry. fom_beta_height_pfp_cut_to_trim_resultinput_entry + S (fom_value_pfp_cut_to_trim_resultinput) = S ((S (fom_index_pfp_cut_to_trim_resultinput)) * c)) /\ exists fom_beta_quotient_pfp_cut_to_trim_resultinput_entry. b = fom_beta_quotient_pfp_cut_to_trim_resultinput_entry * S ((S (fom_index_pfp_cut_to_trim_resultinput)) * c) + (fom_value_pfp_cut_to_trim_resultinput))) /\ (exists fom_gap_pfp_cut_to_trim_resultinput_value_bound. fom_gap_pfp_cut_to_trim_resultinput_value_bound + S (fom_value_pfp_cut_to_trim_resultinput) = p))) /\ (((forall pfp_repeat_index_cut_to_trim_resultremoved. (exists pfa_gap_cut_to_trim_resultremovedindex. pfa_gap_cut_to_trim_resultremovedindex + S (pfp_repeat_index_cut_to_trim_resultremoved) = (t)) -> (((exists ff_h_pfp_cut_to_trim_resultremovedentry. ff_h_pfp_cut_to_trim_resultremovedentry + S (0) = S ((S (pfp_repeat_index_cut_to_trim_resultremoved)) * c)) /\ exists ff_q_pfp_cut_to_trim_resultremovedentry. b = ff_q_pfp_cut_to_trim_resultremovedentry * S ((S (pfp_repeat_index_cut_to_trim_resultremoved)) * c) + (0)))) /\ (((forall pftrim_index_cut_to_trim_resultsuffix pftrim_value_cut_to_trim_resultsuffix. (exists pfa_gap_cut_to_trim_resultsuffixbound. pfa_gap_cut_to_trim_resultsuffixbound + S (pftrim_index_cut_to_trim_resultsuffix) = (M)) -> (((exists ff_h_pfp_cut_to_trim_resultsuffixsource. ff_h_pfp_cut_to_trim_resultsuffixsource + S (pftrim_value_cut_to_trim_resultsuffix) = S ((S ((t)+pftrim_index_cut_to_trim_resultsuffix)) * c)) /\ exists ff_q_pfp_cut_to_trim_resultsuffixsource. b = ff_q_pfp_cut_to_trim_resultsuffixsource * S ((S ((t)+pftrim_index_cut_to_trim_resultsuffix)) * c) + (pftrim_value_cut_to_trim_resultsuffix))) -> (((exists ff_h_pfp_cut_to_trim_resultsuffixoutput. ff_h_pfp_cut_to_trim_resultsuffixoutput + S (pftrim_value_cut_to_trim_resultsuffix) = S ((S (pftrim_index_cut_to_trim_resultsuffix)) * e)) /\ exists ff_q_pfp_cut_to_trim_resultsuffixoutput. d = ff_q_pfp_cut_to_trim_resultsuffixoutput * S ((S (pftrim_index_cut_to_trim_resultsuffix)) * e) + (pftrim_value_cut_to_trim_resultsuffix)))) /\ (((M)=0 \/ (exists pftrim_leading_cut_to_trim_resultnormal. ((((exists ff_h_pfp_cut_to_trim_resultnormalentry. ff_h_pfp_cut_to_trim_resultnormalentry + S (pftrim_leading_cut_to_trim_resultnormal) = S ((S (0)) * e)) /\ exists ff_q_pfp_cut_to_trim_resultnormalentry. d = ff_q_pfp_cut_to_trim_resultnormalentry * S ((S (0)) * e) + (pftrim_leading_cut_to_trim_resultnormal))) /\ ((~(pftrim_leading_cut_to_trim_resultnormal=0)))))))))))))))

Complete tactic proof in conservative notation

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

42 script commands · 17 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 hc
  10. L10
    intro hcut
02Fix variables and assumptionsL11–11

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hs
03Separate the logical casesL12–14

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

  1. L12
    cases hcut
  2. L13
    cases hcut_right
  3. L14
    split
04Use earlier factsL15–15

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

  1. L15
    exact hcut_left
05Separate the logical casesL16–16

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

  1. L16
    split
06Use earlier factsL17–17

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

  1. L17
    exact hc
07Separate the logical casesL18–18

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

  1. L18
    split
08Use earlier factsL19–19

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

  1. L19
    exact hcut_right_left
09Separate the logical casesL20–20

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

  1. L20
    split
10Use earlier factsL21–21

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

  1. L21
    exact hs
11Separate the logical casesL22–23

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

  1. L22
    cases hcut_right_right
  2. L23
    left
12Use earlier factsL24–24

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

  1. L24
    exact hcut_right_right_left
13Separate the logical casesL25–28

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

  1. L25
    right
  2. L26
    cases hcut_right_right_right
  3. L27
    cases hcut_right_right_right_right
  4. L28
    cases hcut_right_right_right_right_witness
14Construct an explicit witnessL29–29

Supply the displayed value, then prove that it has the required property.

  1. L29
    exists x
15Separate the logical casesL30–30

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

  1. L30
    split
16Use earlier factsL31–36

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

  1. L31
    specialize hs (0)
  2. L32
    specialize hs (x)
  3. L33
    apply hs
  4. L34
    specialize one_le_of_ne_zero (M)
  5. L35
    apply one_le_of_ne_zero
  6. L36
    exact hcut_right_right_right_left
17Establish hindexL37–42

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

  1. L37
    have hindex : t+0=t
  2. L38
    simp
  3. L39
    rewrite hindex
  4. L40
    rewrite hindex
  5. L41
    exact hcut_right_right_right_right_witness_left
  6. L42
    exact hcut_right_right_right_right_witness_right

Library-wide reading audit

Original defined command ledger · 42 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 hc
  10. 0010intro hcut
  11. 0011intro hs
  12. 0012cases hcut
  13. 0013cases hcut_right
  14. 0014split
  15. 0015exact hcut_left
  16. 0016split
  17. 0017exact hc
  18. 0018split
  19. 0019exact hcut_right_left
  20. 0020split
  21. 0021exact hs
  22. 0022cases hcut_right_right
  23. 0023left
  24. 0024exact hcut_right_right_left
  25. 0025right
  26. 0026cases hcut_right_right_right
  27. 0027cases hcut_right_right_right_right
  28. 0028cases hcut_right_right_right_right_witness
  29. 0029exists x
  30. 0030split
  31. 0031specialize hs (0)
  32. 0032specialize hs (x)
  33. 0033apply hs
  34. 0034specialize one_le_of_ne_zero (M)
  35. 0035apply one_le_of_ne_zero
  36. 0036exact hcut_right_right_right_left
  37. 0037have hindex : t+0=t
  38. 0038simp
  39. 0039rewrite hindex
  40. 0040rewrite hindex
  41. 0041exact hcut_right_right_right_right_witness_left
  42. 0042exact hcut_right_right_right_right_witness_right