PG006E

prime_field_polynomial_equivalent_represented_degrees_equal

Formal equivalence preserves genuine represented degree across independently encoded and independently length-annotated nonzero-leading prefixes.

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. ∀ d. ∀ bb. ∀ bc. ∀ M. ∀ e. FpRepresentedDegree(p,ab,ac,L,d) → FpRepresentedDegree(p,bb,bc,M,e) → PolynomialEquivalent(ab,ac,L,bb,bc,M) → d = e

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

Definition DAG

FpRepresentedDegree(p,b,c,L,d) · 2PolynomialEquivalent(b,c,L,d,e,M) · 3

Actual proof prerequisites

prime_field_polynomial_nonzero_leading_equivalent_length_boundle_antisymm · checked external prerequisiteprime_field_polynomial_equivalent_symmetric · checked external prerequisitesucc_injective · checked external prerequisite
Original expanded first-order statement 
forall p ab ac L d bb bc M e. ((((L)=S (d)) /\ (((forall fom_index_pfp_degree_leftcoefficients. (exists fom_gap_pfp_degree_leftcoefficients_index_bound. fom_gap_pfp_degree_leftcoefficients_index_bound + S (fom_index_pfp_degree_leftcoefficients) = L) -> exists fom_value_pfp_degree_leftcoefficients. ((((exists fom_beta_height_pfp_degree_leftcoefficients_entry. fom_beta_height_pfp_degree_leftcoefficients_entry + S (fom_value_pfp_degree_leftcoefficients) = S ((S (fom_index_pfp_degree_leftcoefficients)) * ac)) /\ exists fom_beta_quotient_pfp_degree_leftcoefficients_entry. ab = fom_beta_quotient_pfp_degree_leftcoefficients_entry * S ((S (fom_index_pfp_degree_leftcoefficients)) * ac) + (fom_value_pfp_degree_leftcoefficients))) /\ (exists fom_gap_pfp_degree_leftcoefficients_value_bound. fom_gap_pfp_degree_leftcoefficients_value_bound + S (fom_value_pfp_degree_leftcoefficients) = p))) /\ ((exists pfd_leading_degree_left. ((((exists ff_h_pfp_degree_leftentry. ff_h_pfp_degree_leftentry + S (pfd_leading_degree_left) = S ((S (0)) * ac)) /\ exists ff_q_pfp_degree_leftentry. ab = ff_q_pfp_degree_leftentry * S ((S (0)) * ac) + (pfd_leading_degree_left))) /\ ((~(pfd_leading_degree_left=0)))))))))) -> ((((M)=S (e)) /\ (((forall fom_index_pfp_degree_rightcoefficients. (exists fom_gap_pfp_degree_rightcoefficients_index_bound. fom_gap_pfp_degree_rightcoefficients_index_bound + S (fom_index_pfp_degree_rightcoefficients) = M) -> exists fom_value_pfp_degree_rightcoefficients. ((((exists fom_beta_height_pfp_degree_rightcoefficients_entry. fom_beta_height_pfp_degree_rightcoefficients_entry + S (fom_value_pfp_degree_rightcoefficients) = S ((S (fom_index_pfp_degree_rightcoefficients)) * bc)) /\ exists fom_beta_quotient_pfp_degree_rightcoefficients_entry. bb = fom_beta_quotient_pfp_degree_rightcoefficients_entry * S ((S (fom_index_pfp_degree_rightcoefficients)) * bc) + (fom_value_pfp_degree_rightcoefficients))) /\ (exists fom_gap_pfp_degree_rightcoefficients_value_bound. fom_gap_pfp_degree_rightcoefficients_value_bound + S (fom_value_pfp_degree_rightcoefficients) = p))) /\ ((exists pfd_leading_degree_right. ((((exists ff_h_pfp_degree_rightentry. ff_h_pfp_degree_rightentry + S (pfd_leading_degree_right) = S ((S (0)) * bc)) /\ exists ff_q_pfp_degree_rightentry. bb = ff_q_pfp_degree_rightentry * S ((S (0)) * bc) + (pfd_leading_degree_right))) /\ ((~(pfd_leading_degree_right=0)))))))))) -> (forall pfrep_power_degree_equivalent pfrep_left_degree_equivalent pfrep_right_degree_equivalent. ((exists pfrep_position_degree_equivalentfirst. ((pfrep_position_degree_equivalentfirst+S (pfrep_power_degree_equivalent)=(L)) /\ ((((exists ff_h_pfp_degree_equivalentfirstentry. ff_h_pfp_degree_equivalentfirstentry + S (pfrep_left_degree_equivalent) = S ((S (pfrep_position_degree_equivalentfirst)) * ac)) /\ exists ff_q_pfp_degree_equivalentfirstentry. ab = ff_q_pfp_degree_equivalentfirstentry * S ((S (pfrep_position_degree_equivalentfirst)) * ac) + (pfrep_left_degree_equivalent)))))) \/ (((exists pfrep_gap_degree_equivalentfirstoutside. pfrep_gap_degree_equivalentfirstoutside+(L)=(pfrep_power_degree_equivalent)) /\ (((pfrep_left_degree_equivalent)=0))))) -> ((exists pfrep_position_degree_equivalentsecond. ((pfrep_position_degree_equivalentsecond+S (pfrep_power_degree_equivalent)=(M)) /\ ((((exists ff_h_pfp_degree_equivalentsecondentry. ff_h_pfp_degree_equivalentsecondentry + S (pfrep_right_degree_equivalent) = S ((S (pfrep_position_degree_equivalentsecond)) * bc)) /\ exists ff_q_pfp_degree_equivalentsecondentry. bb = ff_q_pfp_degree_equivalentsecondentry * S ((S (pfrep_position_degree_equivalentsecond)) * bc) + (pfrep_right_degree_equivalent)))))) \/ (((exists pfrep_gap_degree_equivalentsecondoutside. pfrep_gap_degree_equivalentsecondoutside+(M)=(pfrep_power_degree_equivalent)) /\ (((pfrep_right_degree_equivalent)=0))))) -> pfrep_left_degree_equivalent=pfrep_right_degree_equivalent) -> (d=e)

Complete tactic proof in conservative notation

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

65 script commands · 10 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.

Named ingredients (1)
prime field polynomial nonzero leading equivalent length bound
01Fix variables and assumptionsL1–10

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 d
  6. L6
    intro bb
  7. L7
    intro bc
  8. L8
    intro M
  9. L9
    intro e
  10. L10
    intro ha
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hb
  2. L12
    intro he
03Separate the logical casesL13–16

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

  1. L13
    cases ha
  2. L14
    cases ha_right
  3. L15
    cases hb
  4. L16
    cases hb_right
04Establish hsameL17–17

Establish this local claim before using it. It is not an additional assumption.

  1. L17
    have hsame : PolynomialEquivalent(ab,ac,S d,bb,bc,S e)Definitions: PolynomialEquivalent(ab,ac,S d,bb,bc,S e)Original native command in the exact edition
05Establish hcopyL18–24

Establish this local claim before using it. It is not an additional assumption.

  1. L18
    have hcopy : PolynomialEquivalent(ab,ac,L,bb,bc,M)Definitions: PolynomialEquivalent(ab,ac,L,bb,bc,M)Original native command in the exact edition
  2. L19
    exact he
  3. L20
    rewrite ha_left at hcopy
  4. L21
    rewrite ha_left at hcopy
  5. L22
    rewrite hb_left at hcopy
  6. L23
    rewrite hb_left at hcopy
  7. L24
    exact hcopy
06Separate the logical casesL25–28

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

  1. L25
    cases ha_right_right
  2. L26
    cases ha_right_right_witness
  3. L27
    cases hb_right_right
  4. L28
    cases hb_right_right_witness
07Establish hlengthL29–38

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

  1. L29
    have hlength : S d=S e
  2. L30
    specialize le_antisymm (S d)
  3. L31
    specialize le_antisymm (S e)
  4. L32
    apply le_antisymm
  5. L33
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (ab)
  6. L34
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (ac)
  7. L35
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (d)
  8. L36
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (bb)
  9. L37
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (bc)
  10. L38
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (S e)
08Use earlier factsL39–48

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

  1. L39
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (x)
  2. L40
    apply prime_field_polynomial_nonzero_leading_equivalent_length_bound
  3. L41
    exact ha_right_right_witness_left
  4. L42
    exact ha_right_right_witness_right
  5. L43
    exact hsame
  6. L44
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (bb)
  7. L45
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (bc)
  8. L46
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (e)
  9. L47
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (ab)
  10. L48
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (ac)
09Use earlier factsL49–58

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

  1. L49
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (S d)
  2. L50
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (x1)
  3. L51
    apply prime_field_polynomial_nonzero_leading_equivalent_length_bound
  4. L52
    exact hb_right_right_witness_left
  5. L53
    exact hb_right_right_witness_right
  6. L54
    specialize prime_field_polynomial_equivalent_symmetric (ab)
  7. L55
    specialize prime_field_polynomial_equivalent_symmetric (ac)
  8. L56
    specialize prime_field_polynomial_equivalent_symmetric (S d)
  9. L57
    specialize prime_field_polynomial_equivalent_symmetric (bb)
  10. L58
    specialize prime_field_polynomial_equivalent_symmetric (bc)
10Use earlier factsL59–65

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

  1. L59
    specialize prime_field_polynomial_equivalent_symmetric (S e)
  2. L60
    apply prime_field_polynomial_equivalent_symmetric
  3. L61
    exact hsame
  4. L62
    specialize succ_injective (d)
  5. L63
    specialize succ_injective (e)
  6. L64
    apply succ_injective
  7. L65
    exact hlength

Library-wide reading audit

Original defined command ledger · 65 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro d
  6. 0006intro bb
  7. 0007intro bc
  8. 0008intro M
  9. 0009intro e
  10. 0010intro ha
  11. 0011intro hb
  12. 0012intro he
  13. 0013cases ha
  14. 0014cases ha_right
  15. 0015cases hb
  16. 0016cases hb_right
  17. 0017have hsame : PolynomialEquivalent(ab,ac,S d,bb,bc,S e)
  18. 0018have hcopy : PolynomialEquivalent(ab,ac,L,bb,bc,M)
  19. 0019exact he
  20. 0020rewrite ha_left at hcopy
  21. 0021rewrite ha_left at hcopy
  22. 0022rewrite hb_left at hcopy
  23. 0023rewrite hb_left at hcopy
  24. 0024exact hcopy
  25. 0025cases ha_right_right
  26. 0026cases ha_right_right_witness
  27. 0027cases hb_right_right
  28. 0028cases hb_right_right_witness
  29. 0029have hlength : S d=S e
  30. 0030specialize le_antisymm (S d)
  31. 0031specialize le_antisymm (S e)
  32. 0032apply le_antisymm
  33. 0033specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (ab)
  34. 0034specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (ac)
  35. 0035specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (d)
  36. 0036specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (bb)
  37. 0037specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (bc)
  38. 0038specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (S e)
  39. 0039specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (x)
  40. 0040apply prime_field_polynomial_nonzero_leading_equivalent_length_bound
  41. 0041exact ha_right_right_witness_left
  42. 0042exact ha_right_right_witness_right
  43. 0043exact hsame
  44. 0044specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (bb)
  45. 0045specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (bc)
  46. 0046specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (e)
  47. 0047specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (ab)
  48. 0048specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (ac)
  49. 0049specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (S d)
  50. 0050specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (x1)
  51. 0051apply prime_field_polynomial_nonzero_leading_equivalent_length_bound
  52. 0052exact hb_right_right_witness_left
  53. 0053exact hb_right_right_witness_right
  54. 0054specialize prime_field_polynomial_equivalent_symmetric (ab)
  55. 0055specialize prime_field_polynomial_equivalent_symmetric (ac)
  56. 0056specialize prime_field_polynomial_equivalent_symmetric (S d)
  57. 0057specialize prime_field_polynomial_equivalent_symmetric (bb)
  58. 0058specialize prime_field_polynomial_equivalent_symmetric (bc)
  59. 0059specialize prime_field_polynomial_equivalent_symmetric (S e)
  60. 0060apply prime_field_polynomial_equivalent_symmetric
  61. 0061exact hsame
  62. 0062specialize succ_injective (d)
  63. 0063specialize succ_injective (e)
  64. 0064apply succ_injective
  65. 0065exact hlength