PQ0021

prime_field_polynomial_trim_exists

Every actual canonical input has a genuinely beta-coded leading-zero trim, for all moduli and all finite lengths including zero.

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. ∀ L. BetaPrefixInto(b,c,L,p) → ∃ x. ∃ y. ∃ z. ∃ n. FpPolynomialTrim(p,b,c,L,x,y,z,n)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 1PolynomialSuffix(b,c,t,d,e,M) · 1FpPolynomialTrim(p,b,c,L,t,d,e,M) · 1BetaAt(b,c,i,x) · 1Repeat(b,c,a,l) · 1

Actual proof prerequisites

prime_field_polynomial_leading_zero_cut_existsprime_field_polynomial_suffix_existsprime_field_polynomial_trim_from_cut
Original expanded first-order statement 
forall p b c L. (forall fom_index_pfp_trim_exists_source. (exists fom_gap_pfp_trim_exists_source_index_bound. fom_gap_pfp_trim_exists_source_index_bound + S (fom_index_pfp_trim_exists_source) = L) -> exists fom_value_pfp_trim_exists_source. ((((exists fom_beta_height_pfp_trim_exists_source_entry. fom_beta_height_pfp_trim_exists_source_entry + S (fom_value_pfp_trim_exists_source) = S ((S (fom_index_pfp_trim_exists_source)) * c)) /\ exists fom_beta_quotient_pfp_trim_exists_source_entry. b = fom_beta_quotient_pfp_trim_exists_source_entry * S ((S (fom_index_pfp_trim_exists_source)) * c) + (fom_value_pfp_trim_exists_source))) /\ (exists fom_gap_pfp_trim_exists_source_value_bound. fom_gap_pfp_trim_exists_source_value_bound + S (fom_value_pfp_trim_exists_source) = p))) -> exists t d e M. ((((L)=(t)+(M)) /\ (((forall fom_index_pfp_trim_exists_resultinput. (exists fom_gap_pfp_trim_exists_resultinput_index_bound. fom_gap_pfp_trim_exists_resultinput_index_bound + S (fom_index_pfp_trim_exists_resultinput) = L) -> exists fom_value_pfp_trim_exists_resultinput. ((((exists fom_beta_height_pfp_trim_exists_resultinput_entry. fom_beta_height_pfp_trim_exists_resultinput_entry + S (fom_value_pfp_trim_exists_resultinput) = S ((S (fom_index_pfp_trim_exists_resultinput)) * c)) /\ exists fom_beta_quotient_pfp_trim_exists_resultinput_entry. b = fom_beta_quotient_pfp_trim_exists_resultinput_entry * S ((S (fom_index_pfp_trim_exists_resultinput)) * c) + (fom_value_pfp_trim_exists_resultinput))) /\ (exists fom_gap_pfp_trim_exists_resultinput_value_bound. fom_gap_pfp_trim_exists_resultinput_value_bound + S (fom_value_pfp_trim_exists_resultinput) = p))) /\ (((forall pfp_repeat_index_trim_exists_resultremoved. (exists pfa_gap_trim_exists_resultremovedindex. pfa_gap_trim_exists_resultremovedindex + S (pfp_repeat_index_trim_exists_resultremoved) = (t)) -> (((exists ff_h_pfp_trim_exists_resultremovedentry. ff_h_pfp_trim_exists_resultremovedentry + S (0) = S ((S (pfp_repeat_index_trim_exists_resultremoved)) * c)) /\ exists ff_q_pfp_trim_exists_resultremovedentry. b = ff_q_pfp_trim_exists_resultremovedentry * S ((S (pfp_repeat_index_trim_exists_resultremoved)) * c) + (0)))) /\ (((forall pftrim_index_trim_exists_resultsuffix pftrim_value_trim_exists_resultsuffix. (exists pfa_gap_trim_exists_resultsuffixbound. pfa_gap_trim_exists_resultsuffixbound + S (pftrim_index_trim_exists_resultsuffix) = (M)) -> (((exists ff_h_pfp_trim_exists_resultsuffixsource. ff_h_pfp_trim_exists_resultsuffixsource + S (pftrim_value_trim_exists_resultsuffix) = S ((S ((t)+pftrim_index_trim_exists_resultsuffix)) * c)) /\ exists ff_q_pfp_trim_exists_resultsuffixsource. b = ff_q_pfp_trim_exists_resultsuffixsource * S ((S ((t)+pftrim_index_trim_exists_resultsuffix)) * c) + (pftrim_value_trim_exists_resultsuffix))) -> (((exists ff_h_pfp_trim_exists_resultsuffixoutput. ff_h_pfp_trim_exists_resultsuffixoutput + S (pftrim_value_trim_exists_resultsuffix) = S ((S (pftrim_index_trim_exists_resultsuffix)) * e)) /\ exists ff_q_pfp_trim_exists_resultsuffixoutput. d = ff_q_pfp_trim_exists_resultsuffixoutput * S ((S (pftrim_index_trim_exists_resultsuffix)) * e) + (pftrim_value_trim_exists_resultsuffix)))) /\ (((M)=0 \/ (exists pftrim_leading_trim_exists_resultnormal. ((((exists ff_h_pfp_trim_exists_resultnormalentry. ff_h_pfp_trim_exists_resultnormalentry + S (pftrim_leading_trim_exists_resultnormal) = S ((S (0)) * e)) /\ exists ff_q_pfp_trim_exists_resultnormalentry. d = ff_q_pfp_trim_exists_resultnormalentry * S ((S (0)) * e) + (pftrim_leading_trim_exists_resultnormal))) /\ ((~(pftrim_leading_trim_exists_resultnormal=0)))))))))))))))

Complete tactic proof in conservative notation

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

36 script commands · 8 reading checkpoints · 2 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.

Named ingredients (3)
prime field polynomial leading zero cut existsprime field polynomial suffix existsprime field polynomial trim from cut
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 L
  5. L5
    intro hc
02Establish hcutL6–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial leading zero cut exists.

  1. L6
    have hcut : ∃ t. ∃ M. L = t + M ∧ (Repeat(b,c,0,t) ∧ (M = 0 ∨ ¬M = 0 ∧ (∃ x. BetaAt(b,c,t,x) ∧ ¬x = 0)))Definitions: Repeat(b,c,0,t)BetaAt(b,c,t,x)Original native command in the exact edition
  2. L7
    specialize prime_field_polynomial_leading_zero_cut_exists (b)
  3. L8
    specialize prime_field_polynomial_leading_zero_cut_exists (c)
  4. L9
    specialize prime_field_polynomial_leading_zero_cut_exists (L)
  5. L10
    apply prime_field_polynomial_leading_zero_cut_exists
03Separate the logical casesL11–12

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

  1. L11
    cases hcut
  2. L12
    cases hcut_witness
04Establish hsL13–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial suffix exists.

  1. L13
    have hs : ∃ d. ∃ e. PolynomialSuffix(b,c,x,d,e,x1)Definitions: PolynomialSuffix(b,c,x,d,e,x1)Original native command in the exact edition
  2. L14
    specialize prime_field_polynomial_suffix_exists (b)
  3. L15
    specialize prime_field_polynomial_suffix_exists (c)
  4. L16
    specialize prime_field_polynomial_suffix_exists (x)
  5. L17
    specialize prime_field_polynomial_suffix_exists (x1)
  6. L18
    apply prime_field_polynomial_suffix_exists
05Separate the logical casesL19–20

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

  1. L19
    cases hs
  2. L20
    cases hs_witness
06Construct an explicit witnessL21–24

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

  1. L21
    exists x
  2. L22
    exists x2
  3. L23
    exists x3
  4. L24
    exists x1
07Use earlier factsL25–34

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

  1. L25
    specialize prime_field_polynomial_trim_from_cut (p)
  2. L26
    specialize prime_field_polynomial_trim_from_cut (b)
  3. L27
    specialize prime_field_polynomial_trim_from_cut (c)
  4. L28
    specialize prime_field_polynomial_trim_from_cut (L)
  5. L29
    specialize prime_field_polynomial_trim_from_cut (x)
  6. L30
    specialize prime_field_polynomial_trim_from_cut (x2)
  7. L31
    specialize prime_field_polynomial_trim_from_cut (x3)
  8. L32
    specialize prime_field_polynomial_trim_from_cut (x1)
  9. L33
    apply prime_field_polynomial_trim_from_cut
  10. L34
    exact hc
08Use earlier factsL35–36

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

  1. L35
    exact hcut_witness_witness
  2. L36
    exact hs_witness_witness

Library-wide reading audit

Original defined command ledger · 36 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro L
  5. 0005intro hc
  6. 0006have hcut : ∃ t. ∃ M. L = t + M ∧ (Repeat(b,c,0,t) ∧ (M = 0 ∨ ¬M = 0 ∧ (∃ x. BetaAt(b,c,t,x) ∧ ¬x = 0)))
  7. 0007specialize prime_field_polynomial_leading_zero_cut_exists (b)
  8. 0008specialize prime_field_polynomial_leading_zero_cut_exists (c)
  9. 0009specialize prime_field_polynomial_leading_zero_cut_exists (L)
  10. 0010apply prime_field_polynomial_leading_zero_cut_exists
  11. 0011cases hcut
  12. 0012cases hcut_witness
  13. 0013have hs : ∃ d. ∃ e. PolynomialSuffix(b,c,x,d,e,x1)
  14. 0014specialize prime_field_polynomial_suffix_exists (b)
  15. 0015specialize prime_field_polynomial_suffix_exists (c)
  16. 0016specialize prime_field_polynomial_suffix_exists (x)
  17. 0017specialize prime_field_polynomial_suffix_exists (x1)
  18. 0018apply prime_field_polynomial_suffix_exists
  19. 0019cases hs
  20. 0020cases hs_witness
  21. 0021exists x
  22. 0022exists x2
  23. 0023exists x3
  24. 0024exists x1
  25. 0025specialize prime_field_polynomial_trim_from_cut (p)
  26. 0026specialize prime_field_polynomial_trim_from_cut (b)
  27. 0027specialize prime_field_polynomial_trim_from_cut (c)
  28. 0028specialize prime_field_polynomial_trim_from_cut (L)
  29. 0029specialize prime_field_polynomial_trim_from_cut (x)
  30. 0030specialize prime_field_polynomial_trim_from_cut (x2)
  31. 0031specialize prime_field_polynomial_trim_from_cut (x3)
  32. 0032specialize prime_field_polynomial_trim_from_cut (x1)
  33. 0033apply prime_field_polynomial_trim_from_cut
  34. 0034exact hc
  35. 0035exact hcut_witness_witness
  36. 0036exact hs_witness_witness