PX0034

prime_field_polynomial_trim_zero_prefix_cut_bound

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

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

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

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

le_or_lt Alpha theorem; checked-use authorized eq_decidable Alpha theorem; checked-use authorized prime_field_polynomial_trim_leading_source_nonzero Alpha theorem; checked-use authorized

Direct dependents

PX0035 prime_field_polynomial_trim_zero_prefix_remainder_bound

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

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 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 : (exists pfc_gap_division_cut_before. pfc_gap_division_cut_before+(q)=(t)) \/ (exists pfa_gap_division_cut_inside. pfa_gap_division_cut_inside + S (t) = (q))
  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
  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 exact 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 : (exists pfc_gap_division_cut_before. pfc_gap_division_cut_before+(q)=(t)) \/ (exists pfa_gap_division_cut_inside. pfa_gap_division_cut_inside + S (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 : (((L)=(t)+(R)) /\ (((forall fom_index_pfp_division_cut_copyinput. (exists fom_gap_pfp_division_cut_copyinput_index_bound. fom_gap_pfp_division_cut_copyinput_index_bound + S (fom_index_pfp_division_cut_copyinput) = L) -> exists fom_value_pfp_division_cut_copyinput. ((((exists fom_beta_height_pfp_division_cut_copyinput_entry. fom_beta_height_pfp_division_cut_copyinput_entry + S (fom_value_pfp_division_cut_copyinput) = S ((S (fom_index_pfp_division_cut_copyinput)) * uc)) /\ exists fom_beta_quotient_pfp_division_cut_copyinput_entry. ub = fom_beta_quotient_pfp_division_cut_copyinput_entry * S ((S (fom_index_pfp_division_cut_copyinput)) * uc) + (fom_value_pfp_division_cut_copyinput))) /\ (exists fom_gap_pfp_division_cut_copyinput_value_bound. fom_gap_pfp_division_cut_copyinput_value_bound + S (fom_value_pfp_division_cut_copyinput) = p))) /\ (((forall pfp_repeat_index_division_cut_copyremoved. (exists pfa_gap_division_cut_copyremovedindex. pfa_gap_division_cut_copyremovedindex + S (pfp_repeat_index_division_cut_copyremoved) = (t)) -> (((exists ff_h_pfp_division_cut_copyremovedentry. ff_h_pfp_division_cut_copyremovedentry + S (0) = S ((S (pfp_repeat_index_division_cut_copyremoved)) * uc)) /\ exists ff_q_pfp_division_cut_copyremovedentry. ub = ff_q_pfp_division_cut_copyremovedentry * S ((S (pfp_repeat_index_division_cut_copyremoved)) * uc) + (0)))) /\ (((forall pftrim_index_division_cut_copysuffix pftrim_value_division_cut_copysuffix. (exists pfa_gap_division_cut_copysuffixbound. pfa_gap_division_cut_copysuffixbound + S (pftrim_index_division_cut_copysuffix) = (R)) -> (((exists ff_h_pfp_division_cut_copysuffixsource. ff_h_pfp_division_cut_copysuffixsource + S (pftrim_value_division_cut_copysuffix) = S ((S ((t)+pftrim_index_division_cut_copysuffix)) * uc)) /\ exists ff_q_pfp_division_cut_copysuffixsource. ub = ff_q_pfp_division_cut_copysuffixsource * S ((S ((t)+pftrim_index_division_cut_copysuffix)) * uc) + (pftrim_value_division_cut_copysuffix))) -> (((exists ff_h_pfp_division_cut_copysuffixoutput. ff_h_pfp_division_cut_copysuffixoutput + S (pftrim_value_division_cut_copysuffix) = S ((S (pftrim_index_division_cut_copysuffix)) * rc)) /\ exists ff_q_pfp_division_cut_copysuffixoutput. rb = ff_q_pfp_division_cut_copysuffixoutput * S ((S (pftrim_index_division_cut_copysuffix)) * rc) + (pftrim_value_division_cut_copysuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_division_cut_copynormal. ((((exists ff_h_pfp_division_cut_copynormalentry. ff_h_pfp_division_cut_copynormalentry + S (pftrim_leading_division_cut_copynormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_cut_copynormalentry. rb = ff_q_pfp_division_cut_copynormalentry * S ((S (0)) * rc) + (pftrim_leading_division_cut_copynormal))) /\ ((~(pftrim_leading_division_cut_copynormal=0))))))))))))))
  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