PX0036

prime_field_polynomial_trim_bounded_degree

An actual normalized remainder of length at most d is empty or has an actual represented degree strictly below d, even when d=0.

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. ∀ d. FpPolynomialTrim(p,ub,uc,L,t,rb,rc,R) → Le(R,d) → R = 0 ∨ (∃ x. FpRepresentedDegree(p,rb,rc,R,x) ∧ Lt(x,d))

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

Definition DAG

FpRepresentedDegree(p,b,c,L,d) · 1FpPolynomialTrim(p,b,c,L,t,d,e,M) · 1Le(a,b) · 1Lt(a,b) · 1

Actual proof prerequisites

zero_or_succ · checked external prerequisiteprime_field_polynomial_trim_represented_degree · checked external prerequisite
Original expanded first-order statement 
forall p ub uc L t rb rc R d. ((((L)=(t)+(R)) /\ (((forall fom_index_pfp_division_remainder_degree_triminput. (exists fom_gap_pfp_division_remainder_degree_triminput_index_bound. fom_gap_pfp_division_remainder_degree_triminput_index_bound + S (fom_index_pfp_division_remainder_degree_triminput) = L) -> exists fom_value_pfp_division_remainder_degree_triminput. ((((exists fom_beta_height_pfp_division_remainder_degree_triminput_entry. fom_beta_height_pfp_division_remainder_degree_triminput_entry + S (fom_value_pfp_division_remainder_degree_triminput) = S ((S (fom_index_pfp_division_remainder_degree_triminput)) * uc)) /\ exists fom_beta_quotient_pfp_division_remainder_degree_triminput_entry. ub = fom_beta_quotient_pfp_division_remainder_degree_triminput_entry * S ((S (fom_index_pfp_division_remainder_degree_triminput)) * uc) + (fom_value_pfp_division_remainder_degree_triminput))) /\ (exists fom_gap_pfp_division_remainder_degree_triminput_value_bound. fom_gap_pfp_division_remainder_degree_triminput_value_bound + S (fom_value_pfp_division_remainder_degree_triminput) = p))) /\ (((forall pfp_repeat_index_division_remainder_degree_trimremoved. (exists pfa_gap_division_remainder_degree_trimremovedindex. pfa_gap_division_remainder_degree_trimremovedindex + S (pfp_repeat_index_division_remainder_degree_trimremoved) = (t)) -> (((exists ff_h_pfp_division_remainder_degree_trimremovedentry. ff_h_pfp_division_remainder_degree_trimremovedentry + S (0) = S ((S (pfp_repeat_index_division_remainder_degree_trimremoved)) * uc)) /\ exists ff_q_pfp_division_remainder_degree_trimremovedentry. ub = ff_q_pfp_division_remainder_degree_trimremovedentry * S ((S (pfp_repeat_index_division_remainder_degree_trimremoved)) * uc) + (0)))) /\ (((forall pftrim_index_division_remainder_degree_trimsuffix pftrim_value_division_remainder_degree_trimsuffix. (exists pfa_gap_division_remainder_degree_trimsuffixbound. pfa_gap_division_remainder_degree_trimsuffixbound + S (pftrim_index_division_remainder_degree_trimsuffix) = (R)) -> (((exists ff_h_pfp_division_remainder_degree_trimsuffixsource. ff_h_pfp_division_remainder_degree_trimsuffixsource + S (pftrim_value_division_remainder_degree_trimsuffix) = S ((S ((t)+pftrim_index_division_remainder_degree_trimsuffix)) * uc)) /\ exists ff_q_pfp_division_remainder_degree_trimsuffixsource. ub = ff_q_pfp_division_remainder_degree_trimsuffixsource * S ((S ((t)+pftrim_index_division_remainder_degree_trimsuffix)) * uc) + (pftrim_value_division_remainder_degree_trimsuffix))) -> (((exists ff_h_pfp_division_remainder_degree_trimsuffixoutput. ff_h_pfp_division_remainder_degree_trimsuffixoutput + S (pftrim_value_division_remainder_degree_trimsuffix) = S ((S (pftrim_index_division_remainder_degree_trimsuffix)) * rc)) /\ exists ff_q_pfp_division_remainder_degree_trimsuffixoutput. rb = ff_q_pfp_division_remainder_degree_trimsuffixoutput * S ((S (pftrim_index_division_remainder_degree_trimsuffix)) * rc) + (pftrim_value_division_remainder_degree_trimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_division_remainder_degree_trimnormal. ((((exists ff_h_pfp_division_remainder_degree_trimnormalentry. ff_h_pfp_division_remainder_degree_trimnormalentry + S (pftrim_leading_division_remainder_degree_trimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_remainder_degree_trimnormalentry. rb = ff_q_pfp_division_remainder_degree_trimnormalentry * S ((S (0)) * rc) + (pftrim_leading_division_remainder_degree_trimnormal))) /\ ((~(pftrim_leading_division_remainder_degree_trimnormal=0))))))))))))))) -> (exists pfc_gap_division_remainder_degree_bound. pfc_gap_division_remainder_degree_bound+(R)=(d)) -> ((R)=0 \/ (exists pfd_remainder_degree_division_remainder_degree. (((((R)=S (pfd_remainder_degree_division_remainder_degree)) /\ (((forall fom_index_pfp_division_remainder_degreerepresentedcoefficients. (exists fom_gap_pfp_division_remainder_degreerepresentedcoefficients_index_bound. fom_gap_pfp_division_remainder_degreerepresentedcoefficients_index_bound + S (fom_index_pfp_division_remainder_degreerepresentedcoefficients) = R) -> exists fom_value_pfp_division_remainder_degreerepresentedcoefficients. ((((exists fom_beta_height_pfp_division_remainder_degreerepresentedcoefficients_entry. fom_beta_height_pfp_division_remainder_degreerepresentedcoefficients_entry + S (fom_value_pfp_division_remainder_degreerepresentedcoefficients) = S ((S (fom_index_pfp_division_remainder_degreerepresentedcoefficients)) * rc)) /\ exists fom_beta_quotient_pfp_division_remainder_degreerepresentedcoefficients_entry. rb = fom_beta_quotient_pfp_division_remainder_degreerepresentedcoefficients_entry * S ((S (fom_index_pfp_division_remainder_degreerepresentedcoefficients)) * rc) + (fom_value_pfp_division_remainder_degreerepresentedcoefficients))) /\ (exists fom_gap_pfp_division_remainder_degreerepresentedcoefficients_value_bound. fom_gap_pfp_division_remainder_degreerepresentedcoefficients_value_bound + S (fom_value_pfp_division_remainder_degreerepresentedcoefficients) = p))) /\ ((exists pfd_leading_division_remainder_degreerepresented. ((((exists ff_h_pfp_division_remainder_degreerepresentedentry. ff_h_pfp_division_remainder_degreerepresentedentry + S (pfd_leading_division_remainder_degreerepresented) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_remainder_degreerepresentedentry. rb = ff_q_pfp_division_remainder_degreerepresentedentry * S ((S (0)) * rc) + (pfd_leading_division_remainder_degreerepresented))) /\ ((~(pfd_leading_division_remainder_degreerepresented=0)))))))))) /\ ((exists pfa_gap_division_remainder_degreestrict. pfa_gap_division_remainder_degreestrict + S (pfd_remainder_degree_division_remainder_degree) = (d))))))

Complete tactic proof in conservative notation

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

35 script commands · 12 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 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 d
  10. L10
    intro ht
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hbound
03Establish hRL12–14

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

  1. L12
    have hR : R=0 \/ exists e. R=S e
  2. L13
    specialize zero_or_succ (R)
  3. L14
    apply zero_or_succ
04Separate the logical casesL15–16

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

  1. L15
    cases hR
  2. L16
    left
05Use earlier factsL17–17

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

  1. L17
    exact hR_left
06Separate the logical casesL18–19

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

  1. L18
    cases hR_right
  2. L19
    right
07Construct an explicit witnessL20–20

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

  1. L20
    exists x
08Separate the logical casesL21–21

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

  1. L21
    split
09Use earlier factsL22–31

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

  1. L22
    specialize prime_field_polynomial_trim_represented_degree (p)
  2. L23
    specialize prime_field_polynomial_trim_represented_degree (ub)
  3. L24
    specialize prime_field_polynomial_trim_represented_degree (uc)
  4. L25
    specialize prime_field_polynomial_trim_represented_degree (L)
  5. L26
    specialize prime_field_polynomial_trim_represented_degree (t)
  6. L27
    specialize prime_field_polynomial_trim_represented_degree (rb)
  7. L28
    specialize prime_field_polynomial_trim_represented_degree (rc)
  8. L29
    specialize prime_field_polynomial_trim_represented_degree (R)
  9. L30
    specialize prime_field_polynomial_trim_represented_degree (x)
  10. L31
    apply prime_field_polynomial_trim_represented_degree
10Use earlier factsL32–33

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

  1. L32
    exact ht
  2. L33
    exact hR_right_witness
11Calculate and transport equalitiesL34–34

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

  1. L34
    rewrite hR_right_witness at hbound
12Use earlier factsL35–35

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

  1. L35
    exact hbound

Library-wide reading audit

Original defined command ledger · 35 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 d
  10. 0010intro ht
  11. 0011intro hbound
  12. 0012have hR : R=0 \/ exists e. R=S e
  13. 0013specialize zero_or_succ (R)
  14. 0014apply zero_or_succ
  15. 0015cases hR
  16. 0016left
  17. 0017exact hR_left
  18. 0018cases hR_right
  19. 0019right
  20. 0020exists x
  21. 0021split
  22. 0022specialize prime_field_polynomial_trim_represented_degree (p)
  23. 0023specialize prime_field_polynomial_trim_represented_degree (ub)
  24. 0024specialize prime_field_polynomial_trim_represented_degree (uc)
  25. 0025specialize prime_field_polynomial_trim_represented_degree (L)
  26. 0026specialize prime_field_polynomial_trim_represented_degree (t)
  27. 0027specialize prime_field_polynomial_trim_represented_degree (rb)
  28. 0028specialize prime_field_polynomial_trim_represented_degree (rc)
  29. 0029specialize prime_field_polynomial_trim_represented_degree (R)
  30. 0030specialize prime_field_polynomial_trim_represented_degree (x)
  31. 0031apply prime_field_polynomial_trim_represented_degree
  32. 0032exact ht
  33. 0033exact hR_right_witness
  34. 0034rewrite hR_right_witness at hbound
  35. 0035exact hbound