PG003A

prime_field_polynomial_common_representatives_functional

Any two choices of common representatives are pairwise formally equivalent, even at different common lengths; no raw-code or length uniqueness is asserted.

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

∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ M. ∀ ub. ∀ uc. ∀ vb. ∀ vc. ∀ K. ∀ db. ∀ dc. ∀ eb. ∀ ec. ∀ J. CommonRepresentatives(ab,ac,L,bb,bc,M,ub,uc,vb,vc,K) → CommonRepresentatives(ab,ac,L,bb,bc,M,db,dc,eb,ec,J) → CommonRepresentatives(ub,uc,K,vb,vc,K,db,dc,eb,ec,J)

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

Definition DAG

PolynomialEquivalent(b,c,L,d,e,M) · 2CommonRepresentatives(ab,ac,L,bb,bc,M,ub,uc,vb,vc,K) · 3

Actual proof prerequisites

prime_field_polynomial_equivalent_symmetric · checked external prerequisiteprime_field_polynomial_equivalent_transitive · checked external prerequisite
Original expanded first-order statement 
forall ab ac L bb bc M ub uc vb vc K db dc eb ec J. (((forall pfrep_power_common_function_first_left pfrep_left_common_function_first_left pfrep_right_common_function_first_left. ((exists pfrep_position_common_function_first_leftfirst. ((pfrep_position_common_function_first_leftfirst+S (pfrep_power_common_function_first_left)=(L)) /\ ((((exists ff_h_pfp_common_function_first_leftfirstentry. ff_h_pfp_common_function_first_leftfirstentry + S (pfrep_left_common_function_first_left) = S ((S (pfrep_position_common_function_first_leftfirst)) * ac)) /\ exists ff_q_pfp_common_function_first_leftfirstentry. ab = ff_q_pfp_common_function_first_leftfirstentry * S ((S (pfrep_position_common_function_first_leftfirst)) * ac) + (pfrep_left_common_function_first_left)))))) \/ (((exists pfrep_gap_common_function_first_leftfirstoutside. pfrep_gap_common_function_first_leftfirstoutside+(L)=(pfrep_power_common_function_first_left)) /\ (((pfrep_left_common_function_first_left)=0))))) -> ((exists pfrep_position_common_function_first_leftsecond. ((pfrep_position_common_function_first_leftsecond+S (pfrep_power_common_function_first_left)=(K)) /\ ((((exists ff_h_pfp_common_function_first_leftsecondentry. ff_h_pfp_common_function_first_leftsecondentry + S (pfrep_right_common_function_first_left) = S ((S (pfrep_position_common_function_first_leftsecond)) * uc)) /\ exists ff_q_pfp_common_function_first_leftsecondentry. ub = ff_q_pfp_common_function_first_leftsecondentry * S ((S (pfrep_position_common_function_first_leftsecond)) * uc) + (pfrep_right_common_function_first_left)))))) \/ (((exists pfrep_gap_common_function_first_leftsecondoutside. pfrep_gap_common_function_first_leftsecondoutside+(K)=(pfrep_power_common_function_first_left)) /\ (((pfrep_right_common_function_first_left)=0))))) -> pfrep_left_common_function_first_left=pfrep_right_common_function_first_left) /\ ((forall pfrep_power_common_function_first_right pfrep_left_common_function_first_right pfrep_right_common_function_first_right. ((exists pfrep_position_common_function_first_rightfirst. ((pfrep_position_common_function_first_rightfirst+S (pfrep_power_common_function_first_right)=(M)) /\ ((((exists ff_h_pfp_common_function_first_rightfirstentry. ff_h_pfp_common_function_first_rightfirstentry + S (pfrep_left_common_function_first_right) = S ((S (pfrep_position_common_function_first_rightfirst)) * bc)) /\ exists ff_q_pfp_common_function_first_rightfirstentry. bb = ff_q_pfp_common_function_first_rightfirstentry * S ((S (pfrep_position_common_function_first_rightfirst)) * bc) + (pfrep_left_common_function_first_right)))))) \/ (((exists pfrep_gap_common_function_first_rightfirstoutside. pfrep_gap_common_function_first_rightfirstoutside+(M)=(pfrep_power_common_function_first_right)) /\ (((pfrep_left_common_function_first_right)=0))))) -> ((exists pfrep_position_common_function_first_rightsecond. ((pfrep_position_common_function_first_rightsecond+S (pfrep_power_common_function_first_right)=(K)) /\ ((((exists ff_h_pfp_common_function_first_rightsecondentry. ff_h_pfp_common_function_first_rightsecondentry + S (pfrep_right_common_function_first_right) = S ((S (pfrep_position_common_function_first_rightsecond)) * vc)) /\ exists ff_q_pfp_common_function_first_rightsecondentry. vb = ff_q_pfp_common_function_first_rightsecondentry * S ((S (pfrep_position_common_function_first_rightsecond)) * vc) + (pfrep_right_common_function_first_right)))))) \/ (((exists pfrep_gap_common_function_first_rightsecondoutside. pfrep_gap_common_function_first_rightsecondoutside+(K)=(pfrep_power_common_function_first_right)) /\ (((pfrep_right_common_function_first_right)=0))))) -> pfrep_left_common_function_first_right=pfrep_right_common_function_first_right)))) -> (((forall pfrep_power_common_function_second_left pfrep_left_common_function_second_left pfrep_right_common_function_second_left. ((exists pfrep_position_common_function_second_leftfirst. ((pfrep_position_common_function_second_leftfirst+S (pfrep_power_common_function_second_left)=(L)) /\ ((((exists ff_h_pfp_common_function_second_leftfirstentry. ff_h_pfp_common_function_second_leftfirstentry + S (pfrep_left_common_function_second_left) = S ((S (pfrep_position_common_function_second_leftfirst)) * ac)) /\ exists ff_q_pfp_common_function_second_leftfirstentry. ab = ff_q_pfp_common_function_second_leftfirstentry * S ((S (pfrep_position_common_function_second_leftfirst)) * ac) + (pfrep_left_common_function_second_left)))))) \/ (((exists pfrep_gap_common_function_second_leftfirstoutside. pfrep_gap_common_function_second_leftfirstoutside+(L)=(pfrep_power_common_function_second_left)) /\ (((pfrep_left_common_function_second_left)=0))))) -> ((exists pfrep_position_common_function_second_leftsecond. ((pfrep_position_common_function_second_leftsecond+S (pfrep_power_common_function_second_left)=(J)) /\ ((((exists ff_h_pfp_common_function_second_leftsecondentry. ff_h_pfp_common_function_second_leftsecondentry + S (pfrep_right_common_function_second_left) = S ((S (pfrep_position_common_function_second_leftsecond)) * dc)) /\ exists ff_q_pfp_common_function_second_leftsecondentry. db = ff_q_pfp_common_function_second_leftsecondentry * S ((S (pfrep_position_common_function_second_leftsecond)) * dc) + (pfrep_right_common_function_second_left)))))) \/ (((exists pfrep_gap_common_function_second_leftsecondoutside. pfrep_gap_common_function_second_leftsecondoutside+(J)=(pfrep_power_common_function_second_left)) /\ (((pfrep_right_common_function_second_left)=0))))) -> pfrep_left_common_function_second_left=pfrep_right_common_function_second_left) /\ ((forall pfrep_power_common_function_second_right pfrep_left_common_function_second_right pfrep_right_common_function_second_right. ((exists pfrep_position_common_function_second_rightfirst. ((pfrep_position_common_function_second_rightfirst+S (pfrep_power_common_function_second_right)=(M)) /\ ((((exists ff_h_pfp_common_function_second_rightfirstentry. ff_h_pfp_common_function_second_rightfirstentry + S (pfrep_left_common_function_second_right) = S ((S (pfrep_position_common_function_second_rightfirst)) * bc)) /\ exists ff_q_pfp_common_function_second_rightfirstentry. bb = ff_q_pfp_common_function_second_rightfirstentry * S ((S (pfrep_position_common_function_second_rightfirst)) * bc) + (pfrep_left_common_function_second_right)))))) \/ (((exists pfrep_gap_common_function_second_rightfirstoutside. pfrep_gap_common_function_second_rightfirstoutside+(M)=(pfrep_power_common_function_second_right)) /\ (((pfrep_left_common_function_second_right)=0))))) -> ((exists pfrep_position_common_function_second_rightsecond. ((pfrep_position_common_function_second_rightsecond+S (pfrep_power_common_function_second_right)=(J)) /\ ((((exists ff_h_pfp_common_function_second_rightsecondentry. ff_h_pfp_common_function_second_rightsecondentry + S (pfrep_right_common_function_second_right) = S ((S (pfrep_position_common_function_second_rightsecond)) * ec)) /\ exists ff_q_pfp_common_function_second_rightsecondentry. eb = ff_q_pfp_common_function_second_rightsecondentry * S ((S (pfrep_position_common_function_second_rightsecond)) * ec) + (pfrep_right_common_function_second_right)))))) \/ (((exists pfrep_gap_common_function_second_rightsecondoutside. pfrep_gap_common_function_second_rightsecondoutside+(J)=(pfrep_power_common_function_second_right)) /\ (((pfrep_right_common_function_second_right)=0))))) -> pfrep_left_common_function_second_right=pfrep_right_common_function_second_right)))) -> (((forall pfrep_power_common_function_result_left pfrep_left_common_function_result_left pfrep_right_common_function_result_left. ((exists pfrep_position_common_function_result_leftfirst. ((pfrep_position_common_function_result_leftfirst+S (pfrep_power_common_function_result_left)=(K)) /\ ((((exists ff_h_pfp_common_function_result_leftfirstentry. ff_h_pfp_common_function_result_leftfirstentry + S (pfrep_left_common_function_result_left) = S ((S (pfrep_position_common_function_result_leftfirst)) * uc)) /\ exists ff_q_pfp_common_function_result_leftfirstentry. ub = ff_q_pfp_common_function_result_leftfirstentry * S ((S (pfrep_position_common_function_result_leftfirst)) * uc) + (pfrep_left_common_function_result_left)))))) \/ (((exists pfrep_gap_common_function_result_leftfirstoutside. pfrep_gap_common_function_result_leftfirstoutside+(K)=(pfrep_power_common_function_result_left)) /\ (((pfrep_left_common_function_result_left)=0))))) -> ((exists pfrep_position_common_function_result_leftsecond. ((pfrep_position_common_function_result_leftsecond+S (pfrep_power_common_function_result_left)=(J)) /\ ((((exists ff_h_pfp_common_function_result_leftsecondentry. ff_h_pfp_common_function_result_leftsecondentry + S (pfrep_right_common_function_result_left) = S ((S (pfrep_position_common_function_result_leftsecond)) * dc)) /\ exists ff_q_pfp_common_function_result_leftsecondentry. db = ff_q_pfp_common_function_result_leftsecondentry * S ((S (pfrep_position_common_function_result_leftsecond)) * dc) + (pfrep_right_common_function_result_left)))))) \/ (((exists pfrep_gap_common_function_result_leftsecondoutside. pfrep_gap_common_function_result_leftsecondoutside+(J)=(pfrep_power_common_function_result_left)) /\ (((pfrep_right_common_function_result_left)=0))))) -> pfrep_left_common_function_result_left=pfrep_right_common_function_result_left) /\ ((forall pfrep_power_common_function_result_right pfrep_left_common_function_result_right pfrep_right_common_function_result_right. ((exists pfrep_position_common_function_result_rightfirst. ((pfrep_position_common_function_result_rightfirst+S (pfrep_power_common_function_result_right)=(K)) /\ ((((exists ff_h_pfp_common_function_result_rightfirstentry. ff_h_pfp_common_function_result_rightfirstentry + S (pfrep_left_common_function_result_right) = S ((S (pfrep_position_common_function_result_rightfirst)) * vc)) /\ exists ff_q_pfp_common_function_result_rightfirstentry. vb = ff_q_pfp_common_function_result_rightfirstentry * S ((S (pfrep_position_common_function_result_rightfirst)) * vc) + (pfrep_left_common_function_result_right)))))) \/ (((exists pfrep_gap_common_function_result_rightfirstoutside. pfrep_gap_common_function_result_rightfirstoutside+(K)=(pfrep_power_common_function_result_right)) /\ (((pfrep_left_common_function_result_right)=0))))) -> ((exists pfrep_position_common_function_result_rightsecond. ((pfrep_position_common_function_result_rightsecond+S (pfrep_power_common_function_result_right)=(J)) /\ ((((exists ff_h_pfp_common_function_result_rightsecondentry. ff_h_pfp_common_function_result_rightsecondentry + S (pfrep_right_common_function_result_right) = S ((S (pfrep_position_common_function_result_rightsecond)) * ec)) /\ exists ff_q_pfp_common_function_result_rightsecondentry. eb = ff_q_pfp_common_function_result_rightsecondentry * S ((S (pfrep_position_common_function_result_rightsecond)) * ec) + (pfrep_right_common_function_result_right)))))) \/ (((exists pfrep_gap_common_function_result_rightsecondoutside. pfrep_gap_common_function_result_rightsecondoutside+(J)=(pfrep_power_common_function_result_right)) /\ (((pfrep_right_common_function_result_right)=0))))) -> pfrep_left_common_function_result_right=pfrep_right_common_function_result_right))))

Complete tactic proof in conservative notation

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

63 script commands · 9 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro ab
  2. L2
    intro ac
  3. L3
    intro L
  4. L4
    intro bb
  5. L5
    intro bc
  6. L6
    intro M
  7. L7
    intro ub
  8. L8
    intro uc
  9. L9
    intro vb
  10. L10
    intro vc
02Fix variables and assumptionsL11–18

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

  1. L11
    intro K
  2. L12
    intro db
  3. L13
    intro dc
  4. L14
    intro eb
  5. L15
    intro ec
  6. L16
    intro J
  7. L17
    intro h
  8. L18
    intro hnew
03Separate the logical casesL19–21

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

  1. L19
    cases h
  2. L20
    cases hnew
  3. L21
    split
04Establish hrL22–31

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

  1. L22
    have hr : PolynomialEquivalent(ub,uc,K,ab,ac,L)Definitions: PolynomialEquivalent(ub,uc,K,ab,ac,L)Original native command in the exact edition
  2. L23
    specialize prime_field_polynomial_equivalent_symmetric (ab)
  3. L24
    specialize prime_field_polynomial_equivalent_symmetric (ac)
  4. L25
    specialize prime_field_polynomial_equivalent_symmetric (L)
  5. L26
    specialize prime_field_polynomial_equivalent_symmetric (ub)
  6. L27
    specialize prime_field_polynomial_equivalent_symmetric (uc)
  7. L28
    specialize prime_field_polynomial_equivalent_symmetric (K)
  8. L29
    apply prime_field_polynomial_equivalent_symmetric
  9. L30
    exact h_left
  10. L31
    specialize prime_field_polynomial_equivalent_transitive (ub)
05Use earlier factsL32–41

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

  1. L32
    specialize prime_field_polynomial_equivalent_transitive (uc)
  2. L33
    specialize prime_field_polynomial_equivalent_transitive (K)
  3. L34
    specialize prime_field_polynomial_equivalent_transitive (ab)
  4. L35
    specialize prime_field_polynomial_equivalent_transitive (ac)
  5. L36
    specialize prime_field_polynomial_equivalent_transitive (L)
  6. L37
    specialize prime_field_polynomial_equivalent_transitive (db)
  7. L38
    specialize prime_field_polynomial_equivalent_transitive (dc)
  8. L39
    specialize prime_field_polynomial_equivalent_transitive (J)
  9. L40
    apply prime_field_polynomial_equivalent_transitive
  10. L41
    exact hr
06Use earlier factsL42–42

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

  1. L42
    exact hnew_left
07Establish hrL43–52

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

  1. L43
    have hr : PolynomialEquivalent(vb,vc,K,bb,bc,M)Definitions: PolynomialEquivalent(vb,vc,K,bb,bc,M)Original native command in the exact edition
  2. L44
    specialize prime_field_polynomial_equivalent_symmetric (bb)
  3. L45
    specialize prime_field_polynomial_equivalent_symmetric (bc)
  4. L46
    specialize prime_field_polynomial_equivalent_symmetric (M)
  5. L47
    specialize prime_field_polynomial_equivalent_symmetric (vb)
  6. L48
    specialize prime_field_polynomial_equivalent_symmetric (vc)
  7. L49
    specialize prime_field_polynomial_equivalent_symmetric (K)
  8. L50
    apply prime_field_polynomial_equivalent_symmetric
  9. L51
    exact h_right
  10. L52
    specialize prime_field_polynomial_equivalent_transitive (vb)
08Use earlier factsL53–62

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

  1. L53
    specialize prime_field_polynomial_equivalent_transitive (vc)
  2. L54
    specialize prime_field_polynomial_equivalent_transitive (K)
  3. L55
    specialize prime_field_polynomial_equivalent_transitive (bb)
  4. L56
    specialize prime_field_polynomial_equivalent_transitive (bc)
  5. L57
    specialize prime_field_polynomial_equivalent_transitive (M)
  6. L58
    specialize prime_field_polynomial_equivalent_transitive (eb)
  7. L59
    specialize prime_field_polynomial_equivalent_transitive (ec)
  8. L60
    specialize prime_field_polynomial_equivalent_transitive (J)
  9. L61
    apply prime_field_polynomial_equivalent_transitive
  10. L62
    exact hr
09Use earlier factsL63–63

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

  1. L63
    exact hnew_right

Library-wide reading audit

Original defined command ledger · 63 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro L
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro M
  7. 0007intro ub
  8. 0008intro uc
  9. 0009intro vb
  10. 0010intro vc
  11. 0011intro K
  12. 0012intro db
  13. 0013intro dc
  14. 0014intro eb
  15. 0015intro ec
  16. 0016intro J
  17. 0017intro h
  18. 0018intro hnew
  19. 0019cases h
  20. 0020cases hnew
  21. 0021split
  22. 0022have hr : PolynomialEquivalent(ub,uc,K,ab,ac,L)
  23. 0023specialize prime_field_polynomial_equivalent_symmetric (ab)
  24. 0024specialize prime_field_polynomial_equivalent_symmetric (ac)
  25. 0025specialize prime_field_polynomial_equivalent_symmetric (L)
  26. 0026specialize prime_field_polynomial_equivalent_symmetric (ub)
  27. 0027specialize prime_field_polynomial_equivalent_symmetric (uc)
  28. 0028specialize prime_field_polynomial_equivalent_symmetric (K)
  29. 0029apply prime_field_polynomial_equivalent_symmetric
  30. 0030exact h_left
  31. 0031specialize prime_field_polynomial_equivalent_transitive (ub)
  32. 0032specialize prime_field_polynomial_equivalent_transitive (uc)
  33. 0033specialize prime_field_polynomial_equivalent_transitive (K)
  34. 0034specialize prime_field_polynomial_equivalent_transitive (ab)
  35. 0035specialize prime_field_polynomial_equivalent_transitive (ac)
  36. 0036specialize prime_field_polynomial_equivalent_transitive (L)
  37. 0037specialize prime_field_polynomial_equivalent_transitive (db)
  38. 0038specialize prime_field_polynomial_equivalent_transitive (dc)
  39. 0039specialize prime_field_polynomial_equivalent_transitive (J)
  40. 0040apply prime_field_polynomial_equivalent_transitive
  41. 0041exact hr
  42. 0042exact hnew_left
  43. 0043have hr : PolynomialEquivalent(vb,vc,K,bb,bc,M)
  44. 0044specialize prime_field_polynomial_equivalent_symmetric (bb)
  45. 0045specialize prime_field_polynomial_equivalent_symmetric (bc)
  46. 0046specialize prime_field_polynomial_equivalent_symmetric (M)
  47. 0047specialize prime_field_polynomial_equivalent_symmetric (vb)
  48. 0048specialize prime_field_polynomial_equivalent_symmetric (vc)
  49. 0049specialize prime_field_polynomial_equivalent_symmetric (K)
  50. 0050apply prime_field_polynomial_equivalent_symmetric
  51. 0051exact h_right
  52. 0052specialize prime_field_polynomial_equivalent_transitive (vb)
  53. 0053specialize prime_field_polynomial_equivalent_transitive (vc)
  54. 0054specialize prime_field_polynomial_equivalent_transitive (K)
  55. 0055specialize prime_field_polynomial_equivalent_transitive (bb)
  56. 0056specialize prime_field_polynomial_equivalent_transitive (bc)
  57. 0057specialize prime_field_polynomial_equivalent_transitive (M)
  58. 0058specialize prime_field_polynomial_equivalent_transitive (eb)
  59. 0059specialize prime_field_polynomial_equivalent_transitive (ec)
  60. 0060specialize prime_field_polynomial_equivalent_transitive (J)
  61. 0061apply prime_field_polynomial_equivalent_transitive
  62. 0062exact hr
  63. 0063exact hnew_right