PG0036

prime_field_polynomial_common_representatives_same_length

Two prefixes already at one length serve as their actual common representatives; no new beta encoding or prime premise is needed.

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. ∀ bb. ∀ bc. ∀ K. CommonRepresentatives(ab,ac,K,bb,bc,K,ab,ac,bb,bc,K)

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

Definition DAG

CommonRepresentatives(ab,ac,L,bb,bc,M,ub,uc,vb,vc,K) · 1

Actual proof prerequisites

prime_field_polynomial_power_coefficient_functional · checked external prerequisite
Original expanded first-order statement 
forall ab ac bb bc K. (((forall pfrep_power_common_self_left pfrep_left_common_self_left pfrep_right_common_self_left. ((exists pfrep_position_common_self_leftfirst. ((pfrep_position_common_self_leftfirst+S (pfrep_power_common_self_left)=(K)) /\ ((((exists ff_h_pfp_common_self_leftfirstentry. ff_h_pfp_common_self_leftfirstentry + S (pfrep_left_common_self_left) = S ((S (pfrep_position_common_self_leftfirst)) * ac)) /\ exists ff_q_pfp_common_self_leftfirstentry. ab = ff_q_pfp_common_self_leftfirstentry * S ((S (pfrep_position_common_self_leftfirst)) * ac) + (pfrep_left_common_self_left)))))) \/ (((exists pfrep_gap_common_self_leftfirstoutside. pfrep_gap_common_self_leftfirstoutside+(K)=(pfrep_power_common_self_left)) /\ (((pfrep_left_common_self_left)=0))))) -> ((exists pfrep_position_common_self_leftsecond. ((pfrep_position_common_self_leftsecond+S (pfrep_power_common_self_left)=(K)) /\ ((((exists ff_h_pfp_common_self_leftsecondentry. ff_h_pfp_common_self_leftsecondentry + S (pfrep_right_common_self_left) = S ((S (pfrep_position_common_self_leftsecond)) * ac)) /\ exists ff_q_pfp_common_self_leftsecondentry. ab = ff_q_pfp_common_self_leftsecondentry * S ((S (pfrep_position_common_self_leftsecond)) * ac) + (pfrep_right_common_self_left)))))) \/ (((exists pfrep_gap_common_self_leftsecondoutside. pfrep_gap_common_self_leftsecondoutside+(K)=(pfrep_power_common_self_left)) /\ (((pfrep_right_common_self_left)=0))))) -> pfrep_left_common_self_left=pfrep_right_common_self_left) /\ ((forall pfrep_power_common_self_right pfrep_left_common_self_right pfrep_right_common_self_right. ((exists pfrep_position_common_self_rightfirst. ((pfrep_position_common_self_rightfirst+S (pfrep_power_common_self_right)=(K)) /\ ((((exists ff_h_pfp_common_self_rightfirstentry. ff_h_pfp_common_self_rightfirstentry + S (pfrep_left_common_self_right) = S ((S (pfrep_position_common_self_rightfirst)) * bc)) /\ exists ff_q_pfp_common_self_rightfirstentry. bb = ff_q_pfp_common_self_rightfirstentry * S ((S (pfrep_position_common_self_rightfirst)) * bc) + (pfrep_left_common_self_right)))))) \/ (((exists pfrep_gap_common_self_rightfirstoutside. pfrep_gap_common_self_rightfirstoutside+(K)=(pfrep_power_common_self_right)) /\ (((pfrep_left_common_self_right)=0))))) -> ((exists pfrep_position_common_self_rightsecond. ((pfrep_position_common_self_rightsecond+S (pfrep_power_common_self_right)=(K)) /\ ((((exists ff_h_pfp_common_self_rightsecondentry. ff_h_pfp_common_self_rightsecondentry + S (pfrep_right_common_self_right) = S ((S (pfrep_position_common_self_rightsecond)) * bc)) /\ exists ff_q_pfp_common_self_rightsecondentry. bb = ff_q_pfp_common_self_rightsecondentry * S ((S (pfrep_position_common_self_rightsecond)) * bc) + (pfrep_right_common_self_right)))))) \/ (((exists pfrep_gap_common_self_rightsecondoutside. pfrep_gap_common_self_rightsecondoutside+(K)=(pfrep_power_common_self_right)) /\ (((pfrep_right_common_self_right)=0))))) -> pfrep_left_common_self_right=pfrep_right_common_self_right))))

Complete tactic proof in conservative notation

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

14 script commands · 3 reading checkpoints · 0 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 ab
  2. L2
    intro ac
  3. L3
    intro bb
  4. L4
    intro bc
  5. L5
    intro K
02Separate the logical casesL6–6

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

  1. L6
    split
03Use earlier factsL7–14

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

  1. L7
    specialize prime_field_polynomial_power_coefficient_functional (ab)
  2. L8
    specialize prime_field_polynomial_power_coefficient_functional (ac)
  3. L9
    specialize prime_field_polynomial_power_coefficient_functional (K)
  4. L10
    apply prime_field_polynomial_power_coefficient_functional
  5. L11
    specialize prime_field_polynomial_power_coefficient_functional (bb)
  6. L12
    specialize prime_field_polynomial_power_coefficient_functional (bc)
  7. L13
    specialize prime_field_polynomial_power_coefficient_functional (K)
  8. L14
    apply prime_field_polynomial_power_coefficient_functional

Library-wide reading audit

Original defined command ledger · 14 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro bb
  4. 0004intro bc
  5. 0005intro K
  6. 0006split
  7. 0007specialize prime_field_polynomial_power_coefficient_functional (ab)
  8. 0008specialize prime_field_polynomial_power_coefficient_functional (ac)
  9. 0009specialize prime_field_polynomial_power_coefficient_functional (K)
  10. 0010apply prime_field_polynomial_power_coefficient_functional
  11. 0011specialize prime_field_polynomial_power_coefficient_functional (bb)
  12. 0012specialize prime_field_polynomial_power_coefficient_functional (bc)
  13. 0013specialize prime_field_polynomial_power_coefficient_functional (K)
  14. 0014apply prime_field_polynomial_power_coefficient_functional