PX0036

prime_field_polynomial_trim_bounded_degree

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

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

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 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))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 35 exact native proof lines.

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

Proof neighborhood

Direct dependencies

zero_or_succ Alpha theorem; checked-use authorized prime_field_polynomial_trim_represented_degree Alpha theorem; checked-use authorized

Direct dependents

PX003A prime_field_polynomial_division_remainder_degree

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

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.

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 exact 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