PG0065

prime_field_polynomial_reduced_representative_exists

Construct a formally equivalent canonical representative of no greater retained length, either empty or with an actual nonzero leading coefficient and represented degree. This trims stored leading zeros without requiring a prime modulus.

Alpha v34 checked-use · first admitted v34 · 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 products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ L. BetaPrefixInto(ab,ac,L,p) → ∃ x. ∃ y. ∃ z. BetaPrefixInto(x,y,z,p) ∧ (PolynomialEquivalent(x,y,z,ab,ac,L) ∧ (Le(z,L) ∧ (z = 0 ∨ (∃ n. FpRepresentedDegree(p,x,y,z,n)))))

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 2FpRepresentedDegree(p,b,c,L,d) · 1FpPolynomialTrim(p,b,c,L,t,d,e,M) · 1PolynomialEquivalent(b,c,L,d,e,M) · 1Le(a,b) · 3

Actual proof prerequisites

prime_field_polynomial_trim_exists · checked external prerequisiteprime_field_polynomial_trim_output_coefficients · checked external prerequisiteprime_field_polynomial_equivalent_symmetric · checked external prerequisiteprime_field_polynomial_trim_equivalent · checked external prerequisiteprime_field_polynomial_trim_length_bounds · checked external prerequisiteeq_decidable · checked external prerequisiteprime_field_polynomial_trim_nonempty_degree_exists · checked external prerequisite
Original expanded first-order statement 
forall p ab ac L. (forall fom_index_pfp_gcd_reduced_input. (exists fom_gap_pfp_gcd_reduced_input_index_bound. fom_gap_pfp_gcd_reduced_input_index_bound + S (fom_index_pfp_gcd_reduced_input) = L) -> exists fom_value_pfp_gcd_reduced_input. ((((exists fom_beta_height_pfp_gcd_reduced_input_entry. fom_beta_height_pfp_gcd_reduced_input_entry + S (fom_value_pfp_gcd_reduced_input) = S ((S (fom_index_pfp_gcd_reduced_input)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_reduced_input_entry. ab = fom_beta_quotient_pfp_gcd_reduced_input_entry * S ((S (fom_index_pfp_gcd_reduced_input)) * ac) + (fom_value_pfp_gcd_reduced_input))) /\ (exists fom_gap_pfp_gcd_reduced_input_value_bound. fom_gap_pfp_gcd_reduced_input_value_bound + S (fom_value_pfp_gcd_reduced_input) = p))) -> (exists tb tc K. ((forall fom_index_pfp_gcd_reduced_result_bounded. (exists fom_gap_pfp_gcd_reduced_result_bounded_index_bound. fom_gap_pfp_gcd_reduced_result_bounded_index_bound + S (fom_index_pfp_gcd_reduced_result_bounded) = K) -> exists fom_value_pfp_gcd_reduced_result_bounded. ((((exists fom_beta_height_pfp_gcd_reduced_result_bounded_entry. fom_beta_height_pfp_gcd_reduced_result_bounded_entry + S (fom_value_pfp_gcd_reduced_result_bounded) = S ((S (fom_index_pfp_gcd_reduced_result_bounded)) * tc)) /\ exists fom_beta_quotient_pfp_gcd_reduced_result_bounded_entry. tb = fom_beta_quotient_pfp_gcd_reduced_result_bounded_entry * S ((S (fom_index_pfp_gcd_reduced_result_bounded)) * tc) + (fom_value_pfp_gcd_reduced_result_bounded))) /\ (exists fom_gap_pfp_gcd_reduced_result_bounded_value_bound. fom_gap_pfp_gcd_reduced_result_bounded_value_bound + S (fom_value_pfp_gcd_reduced_result_bounded) = p))) /\ (((forall pfrep_power_gcd_reduced_result_equivalent pfrep_left_gcd_reduced_result_equivalent pfrep_right_gcd_reduced_result_equivalent. ((exists pfrep_position_gcd_reduced_result_equivalentfirst. ((pfrep_position_gcd_reduced_result_equivalentfirst+S (pfrep_power_gcd_reduced_result_equivalent)=(K)) /\ ((((exists ff_h_pfp_gcd_reduced_result_equivalentfirstentry. ff_h_pfp_gcd_reduced_result_equivalentfirstentry + S (pfrep_left_gcd_reduced_result_equivalent) = S ((S (pfrep_position_gcd_reduced_result_equivalentfirst)) * tc)) /\ exists ff_q_pfp_gcd_reduced_result_equivalentfirstentry. tb = ff_q_pfp_gcd_reduced_result_equivalentfirstentry * S ((S (pfrep_position_gcd_reduced_result_equivalentfirst)) * tc) + (pfrep_left_gcd_reduced_result_equivalent)))))) \/ (((exists pfrep_gap_gcd_reduced_result_equivalentfirstoutside. pfrep_gap_gcd_reduced_result_equivalentfirstoutside+(K)=(pfrep_power_gcd_reduced_result_equivalent)) /\ (((pfrep_left_gcd_reduced_result_equivalent)=0))))) -> ((exists pfrep_position_gcd_reduced_result_equivalentsecond. ((pfrep_position_gcd_reduced_result_equivalentsecond+S (pfrep_power_gcd_reduced_result_equivalent)=(L)) /\ ((((exists ff_h_pfp_gcd_reduced_result_equivalentsecondentry. ff_h_pfp_gcd_reduced_result_equivalentsecondentry + S (pfrep_right_gcd_reduced_result_equivalent) = S ((S (pfrep_position_gcd_reduced_result_equivalentsecond)) * ac)) /\ exists ff_q_pfp_gcd_reduced_result_equivalentsecondentry. ab = ff_q_pfp_gcd_reduced_result_equivalentsecondentry * S ((S (pfrep_position_gcd_reduced_result_equivalentsecond)) * ac) + (pfrep_right_gcd_reduced_result_equivalent)))))) \/ (((exists pfrep_gap_gcd_reduced_result_equivalentsecondoutside. pfrep_gap_gcd_reduced_result_equivalentsecondoutside+(L)=(pfrep_power_gcd_reduced_result_equivalent)) /\ (((pfrep_right_gcd_reduced_result_equivalent)=0))))) -> pfrep_left_gcd_reduced_result_equivalent=pfrep_right_gcd_reduced_result_equivalent) /\ (((exists pfc_gap_gcd_reduced_result_length. pfc_gap_gcd_reduced_result_length+(K)=(L)) /\ (((K)=0 \/ (exists pfg_degree_gcd_reduced_result. (((K)=S (pfg_degree_gcd_reduced_result)) /\ (((forall fom_index_pfp_gcd_reduced_result_degreecoefficients. (exists fom_gap_pfp_gcd_reduced_result_degreecoefficients_index_bound. fom_gap_pfp_gcd_reduced_result_degreecoefficients_index_bound + S (fom_index_pfp_gcd_reduced_result_degreecoefficients) = K) -> exists fom_value_pfp_gcd_reduced_result_degreecoefficients. ((((exists fom_beta_height_pfp_gcd_reduced_result_degreecoefficients_entry. fom_beta_height_pfp_gcd_reduced_result_degreecoefficients_entry + S (fom_value_pfp_gcd_reduced_result_degreecoefficients) = S ((S (fom_index_pfp_gcd_reduced_result_degreecoefficients)) * tc)) /\ exists fom_beta_quotient_pfp_gcd_reduced_result_degreecoefficients_entry. tb = fom_beta_quotient_pfp_gcd_reduced_result_degreecoefficients_entry * S ((S (fom_index_pfp_gcd_reduced_result_degreecoefficients)) * tc) + (fom_value_pfp_gcd_reduced_result_degreecoefficients))) /\ (exists fom_gap_pfp_gcd_reduced_result_degreecoefficients_value_bound. fom_gap_pfp_gcd_reduced_result_degreecoefficients_value_bound + S (fom_value_pfp_gcd_reduced_result_degreecoefficients) = p))) /\ ((exists pfd_leading_gcd_reduced_result_degree. ((((exists ff_h_pfp_gcd_reduced_result_degreeentry. ff_h_pfp_gcd_reduced_result_degreeentry + S (pfd_leading_gcd_reduced_result_degree) = S ((S (0)) * tc)) /\ exists ff_q_pfp_gcd_reduced_result_degreeentry. tb = ff_q_pfp_gcd_reduced_result_degreeentry * S ((S (0)) * tc) + (pfd_leading_gcd_reduced_result_degree))) /\ ((~(pfd_leading_gcd_reduced_result_degree=0))))))))))))))))))

Complete tactic proof in conservative notation

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

81 script commands · 20 reading checkpoints · 3 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 ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro hA
02Establish htL6–12

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

  1. L6
    have ht : ∃ t. ∃ tb. ∃ tc. ∃ K. FpPolynomialTrim(p,ab,ac,L,t,tb,tc,K)Definitions: FpPolynomialTrim(p,ab,ac,L,t,tb,tc,K)Original native command in the exact edition
  2. L7
    specialize prime_field_polynomial_trim_exists (p)
  3. L8
    specialize prime_field_polynomial_trim_exists (ab)
  4. L9
    specialize prime_field_polynomial_trim_exists (ac)
  5. L10
    specialize prime_field_polynomial_trim_exists (L)
  6. L11
    apply prime_field_polynomial_trim_exists
  7. L12
    exact hA
03Separate the logical casesL13–16

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

  1. L13
    cases ht
  2. L14
    cases ht_witness
  3. L15
    cases ht_witness_witness
  4. L16
    cases ht_witness_witness_witness
04Construct an explicit witnessL17–19

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

  1. L17
    exists x1
  2. L18
    exists x2
  3. L19
    exists x3
05Separate the logical casesL20–20

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

  1. L20
    split
06Use earlier factsL21–30

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

  1. L21
    specialize prime_field_polynomial_trim_output_coefficients (p)
  2. L22
    specialize prime_field_polynomial_trim_output_coefficients (ab)
  3. L23
    specialize prime_field_polynomial_trim_output_coefficients (ac)
  4. L24
    specialize prime_field_polynomial_trim_output_coefficients (L)
  5. L25
    specialize prime_field_polynomial_trim_output_coefficients (x)
  6. L26
    specialize prime_field_polynomial_trim_output_coefficients (x1)
  7. L27
    specialize prime_field_polynomial_trim_output_coefficients (x2)
  8. L28
    specialize prime_field_polynomial_trim_output_coefficients (x3)
  9. L29
    apply prime_field_polynomial_trim_output_coefficients
  10. L30
    exact ht_witness_witness_witness_witness
07Separate the logical casesL31–31

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

  1. L31
    split
08Use earlier factsL32–41

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

  1. L32
    specialize prime_field_polynomial_equivalent_symmetric (ab)
  2. L33
    specialize prime_field_polynomial_equivalent_symmetric (ac)
  3. L34
    specialize prime_field_polynomial_equivalent_symmetric (L)
  4. L35
    specialize prime_field_polynomial_equivalent_symmetric (x1)
  5. L36
    specialize prime_field_polynomial_equivalent_symmetric (x2)
  6. L37
    specialize prime_field_polynomial_equivalent_symmetric (x3)
  7. L38
    apply prime_field_polynomial_equivalent_symmetric
  8. L39
    specialize prime_field_polynomial_trim_equivalent (p)
  9. L40
    specialize prime_field_polynomial_trim_equivalent (ab)
  10. L41
    specialize prime_field_polynomial_trim_equivalent (ac)
09Use earlier factsL42–48

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

  1. L42
    specialize prime_field_polynomial_trim_equivalent (L)
  2. L43
    specialize prime_field_polynomial_trim_equivalent (x)
  3. L44
    specialize prime_field_polynomial_trim_equivalent (x1)
  4. L45
    specialize prime_field_polynomial_trim_equivalent (x2)
  5. L46
    specialize prime_field_polynomial_trim_equivalent (x3)
  6. L47
    apply prime_field_polynomial_trim_equivalent
  7. L48
    exact ht_witness_witness_witness_witness
10Separate the logical casesL49–49

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

  1. L49
    split
11Establish hbL50–59

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

  1. L50
    have hb : Le(x,L) ∧ Le(x3,L)Definitions: Le(x,L)Le(x3,L)Original native command in the exact edition
  2. L51
    specialize prime_field_polynomial_trim_length_bounds (p)
  3. L52
    specialize prime_field_polynomial_trim_length_bounds (ab)
  4. L53
    specialize prime_field_polynomial_trim_length_bounds (ac)
  5. L54
    specialize prime_field_polynomial_trim_length_bounds (L)
  6. L55
    specialize prime_field_polynomial_trim_length_bounds (x)
  7. L56
    specialize prime_field_polynomial_trim_length_bounds (x1)
  8. L57
    specialize prime_field_polynomial_trim_length_bounds (x2)
  9. L58
    specialize prime_field_polynomial_trim_length_bounds (x3)
  10. L59
    apply prime_field_polynomial_trim_length_bounds
12Use earlier factsL60–60

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

  1. L60
    exact ht_witness_witness_witness_witness
13Separate the logical casesL61–61

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

  1. L61
    cases hb
14Use earlier factsL62–62

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

  1. L62
    exact hb_right
15Establish hzL63–66

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eq decidable.

  1. L63
    have hz : x3=0 \/ ~(x3=0)
  2. L64
    specialize eq_decidable (x3)
  3. L65
    specialize eq_decidable (0)
  4. L66
    apply eq_decidable
16Separate the logical casesL67–68

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

  1. L67
    cases hz
  2. L68
    left
17Use earlier factsL69–69

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

  1. L69
    exact hz_left
18Separate the logical casesL70–70

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

  1. L70
    right
19Use earlier factsL71–80

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

  1. L71
    specialize prime_field_polynomial_trim_nonempty_degree_exists (p)
  2. L72
    specialize prime_field_polynomial_trim_nonempty_degree_exists (ab)
  3. L73
    specialize prime_field_polynomial_trim_nonempty_degree_exists (ac)
  4. L74
    specialize prime_field_polynomial_trim_nonempty_degree_exists (L)
  5. L75
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x)
  6. L76
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x1)
  7. L77
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x2)
  8. L78
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x3)
  9. L79
    apply prime_field_polynomial_trim_nonempty_degree_exists
  10. L80
    exact ht_witness_witness_witness_witness
20Use earlier factsL81–81

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

  1. L81
    exact hz_right

Library-wide reading audit

Original defined command ledger · 81 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro hA
  6. 0006have ht : ∃ t. ∃ tb. ∃ tc. ∃ K. FpPolynomialTrim(p,ab,ac,L,t,tb,tc,K)
  7. 0007specialize prime_field_polynomial_trim_exists (p)
  8. 0008specialize prime_field_polynomial_trim_exists (ab)
  9. 0009specialize prime_field_polynomial_trim_exists (ac)
  10. 0010specialize prime_field_polynomial_trim_exists (L)
  11. 0011apply prime_field_polynomial_trim_exists
  12. 0012exact hA
  13. 0013cases ht
  14. 0014cases ht_witness
  15. 0015cases ht_witness_witness
  16. 0016cases ht_witness_witness_witness
  17. 0017exists x1
  18. 0018exists x2
  19. 0019exists x3
  20. 0020split
  21. 0021specialize prime_field_polynomial_trim_output_coefficients (p)
  22. 0022specialize prime_field_polynomial_trim_output_coefficients (ab)
  23. 0023specialize prime_field_polynomial_trim_output_coefficients (ac)
  24. 0024specialize prime_field_polynomial_trim_output_coefficients (L)
  25. 0025specialize prime_field_polynomial_trim_output_coefficients (x)
  26. 0026specialize prime_field_polynomial_trim_output_coefficients (x1)
  27. 0027specialize prime_field_polynomial_trim_output_coefficients (x2)
  28. 0028specialize prime_field_polynomial_trim_output_coefficients (x3)
  29. 0029apply prime_field_polynomial_trim_output_coefficients
  30. 0030exact ht_witness_witness_witness_witness
  31. 0031split
  32. 0032specialize prime_field_polynomial_equivalent_symmetric (ab)
  33. 0033specialize prime_field_polynomial_equivalent_symmetric (ac)
  34. 0034specialize prime_field_polynomial_equivalent_symmetric (L)
  35. 0035specialize prime_field_polynomial_equivalent_symmetric (x1)
  36. 0036specialize prime_field_polynomial_equivalent_symmetric (x2)
  37. 0037specialize prime_field_polynomial_equivalent_symmetric (x3)
  38. 0038apply prime_field_polynomial_equivalent_symmetric
  39. 0039specialize prime_field_polynomial_trim_equivalent (p)
  40. 0040specialize prime_field_polynomial_trim_equivalent (ab)
  41. 0041specialize prime_field_polynomial_trim_equivalent (ac)
  42. 0042specialize prime_field_polynomial_trim_equivalent (L)
  43. 0043specialize prime_field_polynomial_trim_equivalent (x)
  44. 0044specialize prime_field_polynomial_trim_equivalent (x1)
  45. 0045specialize prime_field_polynomial_trim_equivalent (x2)
  46. 0046specialize prime_field_polynomial_trim_equivalent (x3)
  47. 0047apply prime_field_polynomial_trim_equivalent
  48. 0048exact ht_witness_witness_witness_witness
  49. 0049split
  50. 0050have hb : Le(x,L) ∧ Le(x3,L)
  51. 0051specialize prime_field_polynomial_trim_length_bounds (p)
  52. 0052specialize prime_field_polynomial_trim_length_bounds (ab)
  53. 0053specialize prime_field_polynomial_trim_length_bounds (ac)
  54. 0054specialize prime_field_polynomial_trim_length_bounds (L)
  55. 0055specialize prime_field_polynomial_trim_length_bounds (x)
  56. 0056specialize prime_field_polynomial_trim_length_bounds (x1)
  57. 0057specialize prime_field_polynomial_trim_length_bounds (x2)
  58. 0058specialize prime_field_polynomial_trim_length_bounds (x3)
  59. 0059apply prime_field_polynomial_trim_length_bounds
  60. 0060exact ht_witness_witness_witness_witness
  61. 0061cases hb
  62. 0062exact hb_right
  63. 0063have hz : x3=0 \/ ~(x3=0)
  64. 0064specialize eq_decidable (x3)
  65. 0065specialize eq_decidable (0)
  66. 0066apply eq_decidable
  67. 0067cases hz
  68. 0068left
  69. 0069exact hz_left
  70. 0070right
  71. 0071specialize prime_field_polynomial_trim_nonempty_degree_exists (p)
  72. 0072specialize prime_field_polynomial_trim_nonempty_degree_exists (ab)
  73. 0073specialize prime_field_polynomial_trim_nonempty_degree_exists (ac)
  74. 0074specialize prime_field_polynomial_trim_nonempty_degree_exists (L)
  75. 0075specialize prime_field_polynomial_trim_nonempty_degree_exists (x)
  76. 0076specialize prime_field_polynomial_trim_nonempty_degree_exists (x1)
  77. 0077specialize prime_field_polynomial_trim_nonempty_degree_exists (x2)
  78. 0078specialize prime_field_polynomial_trim_nonempty_degree_exists (x3)
  79. 0079apply prime_field_polynomial_trim_nonempty_degree_exists
  80. 0080exact ht_witness_witness_witness_witness
  81. 0081exact hz_right