PQ0022

prime_field_polynomial_trim_empty_input

Every pair of output beta codes is a valid empty trim of every empty input, including modulus zero; raw encodings are deliberately unconstrained.

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. ∀ d. ∀ e. FpPolynomialTrim(p,b,c,0,0,d,e,0)

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

Definition DAG

FpPolynomialTrim(p,b,c,L,t,d,e,M) · 1

Actual proof prerequisites

matrix_rank_bounded_prefix_empty · checked external prerequisitebeta_repeat_empty · checked external prerequisitematrix_rank_no_index_below_zero · checked external prerequisite
Original expanded first-order statement 
forall p b c d e. ((((0)=(0)+(0)) /\ (((forall fom_index_pfp_empty_triminput. (exists fom_gap_pfp_empty_triminput_index_bound. fom_gap_pfp_empty_triminput_index_bound + S (fom_index_pfp_empty_triminput) = 0) -> exists fom_value_pfp_empty_triminput. ((((exists fom_beta_height_pfp_empty_triminput_entry. fom_beta_height_pfp_empty_triminput_entry + S (fom_value_pfp_empty_triminput) = S ((S (fom_index_pfp_empty_triminput)) * c)) /\ exists fom_beta_quotient_pfp_empty_triminput_entry. b = fom_beta_quotient_pfp_empty_triminput_entry * S ((S (fom_index_pfp_empty_triminput)) * c) + (fom_value_pfp_empty_triminput))) /\ (exists fom_gap_pfp_empty_triminput_value_bound. fom_gap_pfp_empty_triminput_value_bound + S (fom_value_pfp_empty_triminput) = p))) /\ (((forall pfp_repeat_index_empty_trimremoved. (exists pfa_gap_empty_trimremovedindex. pfa_gap_empty_trimremovedindex + S (pfp_repeat_index_empty_trimremoved) = (0)) -> (((exists ff_h_pfp_empty_trimremovedentry. ff_h_pfp_empty_trimremovedentry + S (0) = S ((S (pfp_repeat_index_empty_trimremoved)) * c)) /\ exists ff_q_pfp_empty_trimremovedentry. b = ff_q_pfp_empty_trimremovedentry * S ((S (pfp_repeat_index_empty_trimremoved)) * c) + (0)))) /\ (((forall pftrim_index_empty_trimsuffix pftrim_value_empty_trimsuffix. (exists pfa_gap_empty_trimsuffixbound. pfa_gap_empty_trimsuffixbound + S (pftrim_index_empty_trimsuffix) = (0)) -> (((exists ff_h_pfp_empty_trimsuffixsource. ff_h_pfp_empty_trimsuffixsource + S (pftrim_value_empty_trimsuffix) = S ((S ((0)+pftrim_index_empty_trimsuffix)) * c)) /\ exists ff_q_pfp_empty_trimsuffixsource. b = ff_q_pfp_empty_trimsuffixsource * S ((S ((0)+pftrim_index_empty_trimsuffix)) * c) + (pftrim_value_empty_trimsuffix))) -> (((exists ff_h_pfp_empty_trimsuffixoutput. ff_h_pfp_empty_trimsuffixoutput + S (pftrim_value_empty_trimsuffix) = S ((S (pftrim_index_empty_trimsuffix)) * e)) /\ exists ff_q_pfp_empty_trimsuffixoutput. d = ff_q_pfp_empty_trimsuffixoutput * S ((S (pftrim_index_empty_trimsuffix)) * e) + (pftrim_value_empty_trimsuffix)))) /\ (((0)=0 \/ (exists pftrim_leading_empty_trimnormal. ((((exists ff_h_pfp_empty_trimnormalentry. ff_h_pfp_empty_trimnormalentry + S (pftrim_leading_empty_trimnormal) = S ((S (0)) * e)) /\ exists ff_q_pfp_empty_trimnormalentry. d = ff_q_pfp_empty_trimnormalentry * S ((S (0)) * e) + (pftrim_leading_empty_trimnormal))) /\ ((~(pftrim_leading_empty_trimnormal=0)))))))))))))))

Complete tactic proof in conservative notation

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

30 script commands · 14 reading checkpoints · 0 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–5

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 d
  5. L5
    intro e
02Separate the logical casesL6–6

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

  1. L6
    split
03Calculate and transport equalitiesL7–7

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

  1. L7
    simp
04Separate the logical casesL8–8

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

  1. L8
    split
05Use earlier factsL9–12

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

  1. L9
    specialize matrix_rank_bounded_prefix_empty (b)
  2. L10
    specialize matrix_rank_bounded_prefix_empty (c)
  3. L11
    specialize matrix_rank_bounded_prefix_empty (p)
  4. L12
    apply matrix_rank_bounded_prefix_empty
06Separate the logical casesL13–13

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

  1. L13
    split
07Use earlier factsL14–18

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

  1. L14
    specialize beta_repeat_empty (b)
  2. L15
    specialize beta_repeat_empty (c)
  3. L16
    specialize beta_repeat_empty (0)
  4. L17
    specialize beta_repeat_empty (0)
  5. L18
    apply beta_repeat_empty
08Calculate and transport equalitiesL19–19

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

  1. L19
    refl
09Separate the logical casesL20–20

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

  1. L20
    split
10Fix variables and assumptionsL21–24

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

  1. L21
    intro i
  2. L22
    intro a
  3. L23
    intro hi
  4. L24
    intro ha
11Separate the logical casesL25–25

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

  1. L25
    exfalso
12Use earlier factsL26–28

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

  1. L26
    specialize matrix_rank_no_index_below_zero (i)
  2. L27
    apply matrix_rank_no_index_below_zero
  3. L28
    exact hi
13Separate the logical casesL29–29

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

  1. L29
    left
14Calculate and transport equalitiesL30–30

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

  1. L30
    refl

Library-wide reading audit

Original defined command ledger · 30 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006split
  7. 0007simp
  8. 0008split
  9. 0009specialize matrix_rank_bounded_prefix_empty (b)
  10. 0010specialize matrix_rank_bounded_prefix_empty (c)
  11. 0011specialize matrix_rank_bounded_prefix_empty (p)
  12. 0012apply matrix_rank_bounded_prefix_empty
  13. 0013split
  14. 0014specialize beta_repeat_empty (b)
  15. 0015specialize beta_repeat_empty (c)
  16. 0016specialize beta_repeat_empty (0)
  17. 0017specialize beta_repeat_empty (0)
  18. 0018apply beta_repeat_empty
  19. 0019refl
  20. 0020split
  21. 0021intro i
  22. 0022intro a
  23. 0023intro hi
  24. 0024intro ha
  25. 0025exfalso
  26. 0026specialize matrix_rank_no_index_below_zero (i)
  27. 0027apply matrix_rank_no_index_below_zero
  28. 0028exact hi
  29. 0029left
  30. 0030refl