PG006E

prime_field_polynomial_equivalent_represented_degrees_equal

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 65 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PG006D prime_field_polynomial_nonzero_leading_equivalent_length_bound le_antisymm Alpha theorem; checked-use authorized prime_field_polynomial_equivalent_symmetric Alpha theorem; checked-use authorized succ_injective Alpha theorem; checked-use authorized

Direct dependents

PG0070 prime_field_polynomial_right_divides_represented_factorization

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

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.

Named ingredients (1)
prime field polynomial nonzero leading equivalent length bound

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 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
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
  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 exact 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 : forall pfrep_power_degree_lengths pfrep_left_degree_lengths pfrep_right_degree_lengths. ((exists pfrep_position_degree_lengthsfirst. ((pfrep_position_degree_lengthsfirst+S (pfrep_power_degree_lengths)=(S d)) /\ ((((exists ff_h_pfp_degree_lengthsfirstentry. ff_h_pfp_degree_lengthsfirstentry + S (pfrep_left_degree_lengths) = S ((S (pfrep_position_degree_lengthsfirst)) * ac)) /\ exists ff_q_pfp_degree_lengthsfirstentry. ab = ff_q_pfp_degree_lengthsfirstentry * S ((S (pfrep_position_degree_lengthsfirst)) * ac) + (pfrep_left_degree_lengths)))))) \/ (((exists pfrep_gap_degree_lengthsfirstoutside. pfrep_gap_degree_lengthsfirstoutside+(S d)=(pfrep_power_degree_lengths)) /\ (((pfrep_left_degree_lengths)=0))))) -> ((exists pfrep_position_degree_lengthssecond. ((pfrep_position_degree_lengthssecond+S (pfrep_power_degree_lengths)=(S e)) /\ ((((exists ff_h_pfp_degree_lengthssecondentry. ff_h_pfp_degree_lengthssecondentry + S (pfrep_right_degree_lengths) = S ((S (pfrep_position_degree_lengthssecond)) * bc)) /\ exists ff_q_pfp_degree_lengthssecondentry. bb = ff_q_pfp_degree_lengthssecondentry * S ((S (pfrep_position_degree_lengthssecond)) * bc) + (pfrep_right_degree_lengths)))))) \/ (((exists pfrep_gap_degree_lengthssecondoutside. pfrep_gap_degree_lengthssecondoutside+(S e)=(pfrep_power_degree_lengths)) /\ (((pfrep_right_degree_lengths)=0))))) -> pfrep_left_degree_lengths=pfrep_right_degree_lengths
  18. 0018have hcopy : 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
  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