PX0034

prime_field_polynomial_trim_zero_prefix_cut_bound

A normalized trim cannot stop inside a proved all-zero leading prefix; empty output is treated separately.

Alpha v34 checked-use · first admitted v33 · 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.

Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.

Exact theorem in conservative defined notation

∀ p. ∀ ub. ∀ uc. ∀ L. ∀ t. ∀ rb. ∀ rc. ∀ R. ∀ q. Le(q,L) → Repeat(ub,uc,0,q) → FpPolynomialTrim(p,ub,uc,L,t,rb,rc,R) → Le(q,t)

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

Definition DAG

FpPolynomialTrim(p,b,c,L,t,d,e,M) · 2Le(a,b) · 3Lt(a,b) · 1Repeat(b,c,a,l) · 1

Actual proof prerequisites

le_or_lt · checked external prerequisiteeq_decidable · checked external prerequisiteprime_field_polynomial_trim_leading_source_nonzero · checked external prerequisite
Original expanded first-order statement 
forall p ub uc L t rb rc R q. (exists pfc_gap_division_cut_length. pfc_gap_division_cut_length+(q)=(L)) -> (forall pfp_repeat_index_division_cut_zero. (exists pfa_gap_division_cut_zeroindex. pfa_gap_division_cut_zeroindex + S (pfp_repeat_index_division_cut_zero) = (q)) -> (((exists ff_h_pfp_division_cut_zeroentry. ff_h_pfp_division_cut_zeroentry + S (0) = S ((S (pfp_repeat_index_division_cut_zero)) * uc)) /\ exists ff_q_pfp_division_cut_zeroentry. ub = ff_q_pfp_division_cut_zeroentry * S ((S (pfp_repeat_index_division_cut_zero)) * uc) + (0)))) -> ((((L)=(t)+(R)) /\ (((forall fom_index_pfp_division_cut_triminput. (exists fom_gap_pfp_division_cut_triminput_index_bound. fom_gap_pfp_division_cut_triminput_index_bound + S (fom_index_pfp_division_cut_triminput) = L) -> exists fom_value_pfp_division_cut_triminput. ((((exists fom_beta_height_pfp_division_cut_triminput_entry. fom_beta_height_pfp_division_cut_triminput_entry + S (fom_value_pfp_division_cut_triminput) = S ((S (fom_index_pfp_division_cut_triminput)) * uc)) /\ exists fom_beta_quotient_pfp_division_cut_triminput_entry. ub = fom_beta_quotient_pfp_division_cut_triminput_entry * S ((S (fom_index_pfp_division_cut_triminput)) * uc) + (fom_value_pfp_division_cut_triminput))) /\ (exists fom_gap_pfp_division_cut_triminput_value_bound. fom_gap_pfp_division_cut_triminput_value_bound + S (fom_value_pfp_division_cut_triminput) = p))) /\ (((forall pfp_repeat_index_division_cut_trimremoved. (exists pfa_gap_division_cut_trimremovedindex. pfa_gap_division_cut_trimremovedindex + S (pfp_repeat_index_division_cut_trimremoved) = (t)) -> (((exists ff_h_pfp_division_cut_trimremovedentry. ff_h_pfp_division_cut_trimremovedentry + S (0) = S ((S (pfp_repeat_index_division_cut_trimremoved)) * uc)) /\ exists ff_q_pfp_division_cut_trimremovedentry. ub = ff_q_pfp_division_cut_trimremovedentry * S ((S (pfp_repeat_index_division_cut_trimremoved)) * uc) + (0)))) /\ (((forall pftrim_index_division_cut_trimsuffix pftrim_value_division_cut_trimsuffix. (exists pfa_gap_division_cut_trimsuffixbound. pfa_gap_division_cut_trimsuffixbound + S (pftrim_index_division_cut_trimsuffix) = (R)) -> (((exists ff_h_pfp_division_cut_trimsuffixsource. ff_h_pfp_division_cut_trimsuffixsource + S (pftrim_value_division_cut_trimsuffix) = S ((S ((t)+pftrim_index_division_cut_trimsuffix)) * uc)) /\ exists ff_q_pfp_division_cut_trimsuffixsource. ub = ff_q_pfp_division_cut_trimsuffixsource * S ((S ((t)+pftrim_index_division_cut_trimsuffix)) * uc) + (pftrim_value_division_cut_trimsuffix))) -> (((exists ff_h_pfp_division_cut_trimsuffixoutput. ff_h_pfp_division_cut_trimsuffixoutput + S (pftrim_value_division_cut_trimsuffix) = S ((S (pftrim_index_division_cut_trimsuffix)) * rc)) /\ exists ff_q_pfp_division_cut_trimsuffixoutput. rb = ff_q_pfp_division_cut_trimsuffixoutput * S ((S (pftrim_index_division_cut_trimsuffix)) * rc) + (pftrim_value_division_cut_trimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_division_cut_trimnormal. ((((exists ff_h_pfp_division_cut_trimnormalentry. ff_h_pfp_division_cut_trimnormalentry + S (pftrim_leading_division_cut_trimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_cut_trimnormalentry. rb = ff_q_pfp_division_cut_trimnormalentry * S ((S (0)) * rc) + (pftrim_leading_division_cut_trimnormal))) /\ ((~(pftrim_leading_division_cut_trimnormal=0))))))))))))))) -> (exists pfc_gap_division_cut_result. pfc_gap_division_cut_result+(q)=(t))

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 · 14 reading checkpoints · 4 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 ub
  3. L3
    intro uc
  4. L4
    intro L
  5. L5
    intro t
  6. L6
    intro rb
  7. L7
    intro rc
  8. L8
    intro R
  9. L9
    intro q
  10. L10
    intro hlen
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hz
  2. L12
    intro ht
03Establish horderL13–16

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

  1. L13
    have horder : Le(q,t) ∨ Lt(t,q)Definitions: Le(q,t)Lt(t,q)Original native command in the exact edition
  2. L14
    specialize le_or_lt (q)
  3. L15
    specialize le_or_lt (t)
  4. L16
    apply le_or_lt
04Separate the logical casesL17–17

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

  1. L17
    cases horder
05Use earlier factsL18–18

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

  1. L18
    exact horder_left
06Establish hRL19–22

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

  1. L19
    have hR : R=0 \/ ~(R=0)
  2. L20
    specialize eq_decidable (R)
  3. L21
    specialize eq_decidable (0)
  4. L22
    apply eq_decidable
07Separate the logical casesL23–23

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

  1. L23
    cases hR
08Establish hcopyL24–25

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

  1. L24
    have hcopy : FpPolynomialTrim(p,ub,uc,L,t,rb,rc,R)Definitions: FpPolynomialTrim(p,ub,uc,L,t,rb,rc,R)Original native command in the exact edition
  2. L25
    exact ht
09Separate the logical casesL26–29

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

  1. L26
    cases hcopy
  2. L27
    cases hcopy_right
  3. L28
    cases hcopy_right_right
  4. L29
    cases hcopy_right_right_right
10Establish hLtL30–36

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

  1. L30
    have hLt : L=t
  2. L31
    trans t+R
  3. L32
    exact hcopy_left
  4. L33
    rewrite hR_left
  5. L34
    simp
  6. L35
    rewrite hLt at hlen
  7. L36
    exact hlen
11Separate the logical casesL37–37

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

  1. L37
    exfalso
12Use earlier factsL38–47

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

  1. L38
    specialize prime_field_polynomial_trim_leading_source_nonzero (p)
  2. L39
    specialize prime_field_polynomial_trim_leading_source_nonzero (ub)
  3. L40
    specialize prime_field_polynomial_trim_leading_source_nonzero (uc)
  4. L41
    specialize prime_field_polynomial_trim_leading_source_nonzero (L)
  5. L42
    specialize prime_field_polynomial_trim_leading_source_nonzero (t)
  6. L43
    specialize prime_field_polynomial_trim_leading_source_nonzero (rb)
  7. L44
    specialize prime_field_polynomial_trim_leading_source_nonzero (rc)
  8. L45
    specialize prime_field_polynomial_trim_leading_source_nonzero (R)
  9. L46
    specialize prime_field_polynomial_trim_leading_source_nonzero (0)
  10. L47
    apply prime_field_polynomial_trim_leading_source_nonzero
13Use earlier factsL48–52

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

  1. L48
    exact ht
  2. L49
    exact hR_right
  3. L50
    specialize hz (t)
  4. L51
    apply hz
  5. L52
    exact horder_right
14Calculate 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 ub
  3. 0003intro uc
  4. 0004intro L
  5. 0005intro t
  6. 0006intro rb
  7. 0007intro rc
  8. 0008intro R
  9. 0009intro q
  10. 0010intro hlen
  11. 0011intro hz
  12. 0012intro ht
  13. 0013have horder : Le(q,t) ∨ Lt(t,q)
  14. 0014specialize le_or_lt (q)
  15. 0015specialize le_or_lt (t)
  16. 0016apply le_or_lt
  17. 0017cases horder
  18. 0018exact horder_left
  19. 0019have hR : R=0 \/ ~(R=0)
  20. 0020specialize eq_decidable (R)
  21. 0021specialize eq_decidable (0)
  22. 0022apply eq_decidable
  23. 0023cases hR
  24. 0024have hcopy : FpPolynomialTrim(p,ub,uc,L,t,rb,rc,R)
  25. 0025exact ht
  26. 0026cases hcopy
  27. 0027cases hcopy_right
  28. 0028cases hcopy_right_right
  29. 0029cases hcopy_right_right_right
  30. 0030have hLt : L=t
  31. 0031trans t+R
  32. 0032exact hcopy_left
  33. 0033rewrite hR_left
  34. 0034simp
  35. 0035rewrite hLt at hlen
  36. 0036exact hlen
  37. 0037exfalso
  38. 0038specialize prime_field_polynomial_trim_leading_source_nonzero (p)
  39. 0039specialize prime_field_polynomial_trim_leading_source_nonzero (ub)
  40. 0040specialize prime_field_polynomial_trim_leading_source_nonzero (uc)
  41. 0041specialize prime_field_polynomial_trim_leading_source_nonzero (L)
  42. 0042specialize prime_field_polynomial_trim_leading_source_nonzero (t)
  43. 0043specialize prime_field_polynomial_trim_leading_source_nonzero (rb)
  44. 0044specialize prime_field_polynomial_trim_leading_source_nonzero (rc)
  45. 0045specialize prime_field_polynomial_trim_leading_source_nonzero (R)
  46. 0046specialize prime_field_polynomial_trim_leading_source_nonzero (0)
  47. 0047apply prime_field_polynomial_trim_leading_source_nonzero
  48. 0048exact ht
  49. 0049exact hR_right
  50. 0050specialize hz (t)
  51. 0051apply hz
  52. 0052exact horder_right
  53. 0053refl