PG0032

prime_field_polynomial_convolution_left_unit_equivalent

Actual left multiplication by a length-one unit preserves formal coefficients, not just evaluations or a selected encoding.

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. ∀ ub. ∀ uc. ∀ ab. ∀ ac. ∀ L. ∀ cb. ∀ cc. BetaAt(ub,uc,0,1) → FpPolyProduct(p,ub,uc,1,ab,ac,L,cb,cc,L) → PolynomialEquivalent(cb,cc,L,ab,ac,L)

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

Definition DAG

FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 1PolynomialEquivalent(b,c,L,d,e,M) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

prime_field_polynomial_equal_implies_equivalent · checked external prerequisiteprime_field_polynomial_convolution_left_unit_equal
Original expanded first-order statement 
forall p ub uc ab ac L cb cc. (((exists ff_h_pfp_unit_equal_unit. ff_h_pfp_unit_equal_unit + S (1) = S ((S (0)) * uc)) /\ exists ff_q_pfp_unit_equal_unit. ub = ff_q_pfp_unit_equal_unit * S ((S (0)) * uc) + (1))) -> (((forall fom_index_pfp_unit_equal_actualleft. (exists fom_gap_pfp_unit_equal_actualleft_index_bound. fom_gap_pfp_unit_equal_actualleft_index_bound + S (fom_index_pfp_unit_equal_actualleft) = 1) -> exists fom_value_pfp_unit_equal_actualleft. ((((exists fom_beta_height_pfp_unit_equal_actualleft_entry. fom_beta_height_pfp_unit_equal_actualleft_entry + S (fom_value_pfp_unit_equal_actualleft) = S ((S (fom_index_pfp_unit_equal_actualleft)) * uc)) /\ exists fom_beta_quotient_pfp_unit_equal_actualleft_entry. ub = fom_beta_quotient_pfp_unit_equal_actualleft_entry * S ((S (fom_index_pfp_unit_equal_actualleft)) * uc) + (fom_value_pfp_unit_equal_actualleft))) /\ (exists fom_gap_pfp_unit_equal_actualleft_value_bound. fom_gap_pfp_unit_equal_actualleft_value_bound + S (fom_value_pfp_unit_equal_actualleft) = p))) /\ (((forall fom_index_pfp_unit_equal_actualright. (exists fom_gap_pfp_unit_equal_actualright_index_bound. fom_gap_pfp_unit_equal_actualright_index_bound + S (fom_index_pfp_unit_equal_actualright) = L) -> exists fom_value_pfp_unit_equal_actualright. ((((exists fom_beta_height_pfp_unit_equal_actualright_entry. fom_beta_height_pfp_unit_equal_actualright_entry + S (fom_value_pfp_unit_equal_actualright) = S ((S (fom_index_pfp_unit_equal_actualright)) * ac)) /\ exists fom_beta_quotient_pfp_unit_equal_actualright_entry. ab = fom_beta_quotient_pfp_unit_equal_actualright_entry * S ((S (fom_index_pfp_unit_equal_actualright)) * ac) + (fom_value_pfp_unit_equal_actualright))) /\ (exists fom_gap_pfp_unit_equal_actualright_value_bound. fom_gap_pfp_unit_equal_actualright_value_bound + S (fom_value_pfp_unit_equal_actualright) = p))) /\ (((((((1)=0 \/ (L)=0) /\ (((L)=0)))) \/ (((~((1)=0)) /\ (((~((L)=0)) /\ (((1)+(L)=S (L)))))))) /\ ((forall pfc_index_unit_equal_actualcoefficients. (exists pfa_gap_unit_equal_actualcoefficientsbound. pfa_gap_unit_equal_actualcoefficientsbound + S (pfc_index_unit_equal_actualcoefficients) = (L)) -> exists pfc_value_unit_equal_actualcoefficients. ((((exists ff_h_pfp_unit_equal_actualcoefficientsentry. ff_h_pfp_unit_equal_actualcoefficientsentry + S (pfc_value_unit_equal_actualcoefficients) = S ((S (pfc_index_unit_equal_actualcoefficients)) * cc)) /\ exists ff_q_pfp_unit_equal_actualcoefficientsentry. cb = ff_q_pfp_unit_equal_actualcoefficientsentry * S ((S (pfc_index_unit_equal_actualcoefficients)) * cc) + (pfc_value_unit_equal_actualcoefficients))) /\ ((exists pfc_terms_code_unit_equal_actualcoefficientscoefficient pfc_terms_scale_unit_equal_actualcoefficientscoefficient pfc_natural_sum_unit_equal_actualcoefficientscoefficient. ((forall pfc_index_unit_equal_actualcoefficientscoefficientdiagonal. (exists pfa_gap_unit_equal_actualcoefficientscoefficientdiagonalbound. pfa_gap_unit_equal_actualcoefficientscoefficientdiagonalbound + S (pfc_index_unit_equal_actualcoefficientscoefficientdiagonal) = (S (pfc_index_unit_equal_actualcoefficients))) -> exists pfc_value_unit_equal_actualcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_unit_equal_actualcoefficientscoefficientdiagonalentry. ff_h_pfp_unit_equal_actualcoefficientscoefficientdiagonalentry + S (pfc_value_unit_equal_actualcoefficientscoefficientdiagonal) = S ((S (pfc_index_unit_equal_actualcoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_equal_actualcoefficientscoefficient)) /\ exists ff_q_pfp_unit_equal_actualcoefficientscoefficientdiagonalentry. pfc_terms_code_unit_equal_actualcoefficientscoefficient = ff_q_pfp_unit_equal_actualcoefficientscoefficientdiagonalentry * S ((S (pfc_index_unit_equal_actualcoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_equal_actualcoefficientscoefficient) + (pfc_value_unit_equal_actualcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_unit_equal_actualcoefficientscoefficientdiagonalterm pfc_left_unit_equal_actualcoefficientscoefficientdiagonalterm pfc_right_unit_equal_actualcoefficientscoefficientdiagonalterm. (((pfc_index_unit_equal_actualcoefficientscoefficientdiagonal)+pfc_complement_unit_equal_actualcoefficientscoefficientdiagonalterm=(pfc_index_unit_equal_actualcoefficients)) /\ ((((((exists pfa_gap_unit_equal_actualcoefficientscoefficientdiagonaltermleftinside. pfa_gap_unit_equal_actualcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_unit_equal_actualcoefficientscoefficientdiagonal) = (1)) /\ ((((exists ff_h_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_unit_equal_actualcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_unit_equal_actualcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_unit_equal_actualcoefficientscoefficientdiagonal)) * uc) + (pfc_left_unit_equal_actualcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_equal_actualcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_unit_equal_actualcoefficientscoefficientdiagonaltermleftoutside+(1)=(pfc_index_unit_equal_actualcoefficientscoefficientdiagonal)) /\ (((pfc_left_unit_equal_actualcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_unit_equal_actualcoefficientscoefficientdiagonaltermrightinside. pfa_gap_unit_equal_actualcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_unit_equal_actualcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_unit_equal_actualcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_unit_equal_actualcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_unit_equal_actualcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_unit_equal_actualcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_equal_actualcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_unit_equal_actualcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_unit_equal_actualcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_unit_equal_actualcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_unit_equal_actualcoefficientscoefficientdiagonal)=pfc_left_unit_equal_actualcoefficientscoefficientdiagonalterm*pfc_right_unit_equal_actualcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_unit_equal_actualcoefficientscoefficientsum fs_v_pfc_unit_equal_actualcoefficientscoefficientsum. ((((exists fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_start. fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_start. fs_u_pfc_unit_equal_actualcoefficientscoefficientsum = fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_terminal. fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_unit_equal_actualcoefficientscoefficient) = S ((S (S (pfc_index_unit_equal_actualcoefficients))) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_terminal. fs_u_pfc_unit_equal_actualcoefficientscoefficientsum = fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_unit_equal_actualcoefficients))) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum) + (pfc_natural_sum_unit_equal_actualcoefficientscoefficient))) /\ forall fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps = S (pfc_index_unit_equal_actualcoefficients)) -> exists fs_a_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps fs_r_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps fs_s_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_equal_actualcoefficientscoefficient)) /\ exists fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_unit_equal_actualcoefficientscoefficient = fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_equal_actualcoefficientscoefficient) + (fs_a_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_unit_equal_actualcoefficientscoefficientsum = fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum) + (fs_r_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_unit_equal_actualcoefficientscoefficientsum = fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum) + (fs_s_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps = fs_r_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps + fs_a_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_unit_equal_actualcoefficientscoefficientresiduebound. pfa_gap_unit_equal_actualcoefficientscoefficientresiduebound + S (pfc_value_unit_equal_actualcoefficients) = (p)) /\ ((exists pfa_offset_left_unit_equal_actualcoefficientscoefficientresiduecongruence pfa_offset_right_unit_equal_actualcoefficientscoefficientresiduecongruence. (pfc_natural_sum_unit_equal_actualcoefficientscoefficient) + (p) * pfa_offset_left_unit_equal_actualcoefficientscoefficientresiduecongruence = (pfc_value_unit_equal_actualcoefficients) + (p) * pfa_offset_right_unit_equal_actualcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_unit_equivalent_result pfrep_left_unit_equivalent_result pfrep_right_unit_equivalent_result. ((exists pfrep_position_unit_equivalent_resultfirst. ((pfrep_position_unit_equivalent_resultfirst+S (pfrep_power_unit_equivalent_result)=(L)) /\ ((((exists ff_h_pfp_unit_equivalent_resultfirstentry. ff_h_pfp_unit_equivalent_resultfirstentry + S (pfrep_left_unit_equivalent_result) = S ((S (pfrep_position_unit_equivalent_resultfirst)) * cc)) /\ exists ff_q_pfp_unit_equivalent_resultfirstentry. cb = ff_q_pfp_unit_equivalent_resultfirstentry * S ((S (pfrep_position_unit_equivalent_resultfirst)) * cc) + (pfrep_left_unit_equivalent_result)))))) \/ (((exists pfrep_gap_unit_equivalent_resultfirstoutside. pfrep_gap_unit_equivalent_resultfirstoutside+(L)=(pfrep_power_unit_equivalent_result)) /\ (((pfrep_left_unit_equivalent_result)=0))))) -> ((exists pfrep_position_unit_equivalent_resultsecond. ((pfrep_position_unit_equivalent_resultsecond+S (pfrep_power_unit_equivalent_result)=(L)) /\ ((((exists ff_h_pfp_unit_equivalent_resultsecondentry. ff_h_pfp_unit_equivalent_resultsecondentry + S (pfrep_right_unit_equivalent_result) = S ((S (pfrep_position_unit_equivalent_resultsecond)) * ac)) /\ exists ff_q_pfp_unit_equivalent_resultsecondentry. ab = ff_q_pfp_unit_equivalent_resultsecondentry * S ((S (pfrep_position_unit_equivalent_resultsecond)) * ac) + (pfrep_right_unit_equivalent_result)))))) \/ (((exists pfrep_gap_unit_equivalent_resultsecondoutside. pfrep_gap_unit_equivalent_resultsecondoutside+(L)=(pfrep_power_unit_equivalent_result)) /\ (((pfrep_right_unit_equivalent_result)=0))))) -> pfrep_left_unit_equivalent_result=pfrep_right_unit_equivalent_result)

Complete tactic proof in conservative notation

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

27 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.

Named ingredients (1)
prime field polynomial convolution left unit equal
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro ub
  3. L3
    intro uc
  4. L4
    intro ab
  5. L5
    intro ac
  6. L6
    intro L
  7. L7
    intro cb
  8. L8
    intro cc
  9. L9
    intro hu
  10. L10
    intro hc
02Use earlier factsL11–20

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

  1. L11
    specialize prime_field_polynomial_equal_implies_equivalent (cb)
  2. L12
    specialize prime_field_polynomial_equal_implies_equivalent (cc)
  3. L13
    specialize prime_field_polynomial_equal_implies_equivalent (ab)
  4. L14
    specialize prime_field_polynomial_equal_implies_equivalent (ac)
  5. L15
    specialize prime_field_polynomial_equal_implies_equivalent (L)
  6. L16
    apply prime_field_polynomial_equal_implies_equivalent
  7. L17
    specialize prime_field_polynomial_convolution_left_unit_equal (p)
  8. L18
    specialize prime_field_polynomial_convolution_left_unit_equal (ub)
  9. L19
    specialize prime_field_polynomial_convolution_left_unit_equal (uc)
  10. L20
    specialize prime_field_polynomial_convolution_left_unit_equal (ab)
03Use earlier factsL21–27

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

  1. L21
    specialize prime_field_polynomial_convolution_left_unit_equal (ac)
  2. L22
    specialize prime_field_polynomial_convolution_left_unit_equal (L)
  3. L23
    specialize prime_field_polynomial_convolution_left_unit_equal (cb)
  4. L24
    specialize prime_field_polynomial_convolution_left_unit_equal (cc)
  5. L25
    apply prime_field_polynomial_convolution_left_unit_equal
  6. L26
    exact hu
  7. L27
    exact hc

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro p
  2. 0002intro ub
  3. 0003intro uc
  4. 0004intro ab
  5. 0005intro ac
  6. 0006intro L
  7. 0007intro cb
  8. 0008intro cc
  9. 0009intro hu
  10. 0010intro hc
  11. 0011specialize prime_field_polynomial_equal_implies_equivalent (cb)
  12. 0012specialize prime_field_polynomial_equal_implies_equivalent (cc)
  13. 0013specialize prime_field_polynomial_equal_implies_equivalent (ab)
  14. 0014specialize prime_field_polynomial_equal_implies_equivalent (ac)
  15. 0015specialize prime_field_polynomial_equal_implies_equivalent (L)
  16. 0016apply prime_field_polynomial_equal_implies_equivalent
  17. 0017specialize prime_field_polynomial_convolution_left_unit_equal (p)
  18. 0018specialize prime_field_polynomial_convolution_left_unit_equal (ub)
  19. 0019specialize prime_field_polynomial_convolution_left_unit_equal (uc)
  20. 0020specialize prime_field_polynomial_convolution_left_unit_equal (ab)
  21. 0021specialize prime_field_polynomial_convolution_left_unit_equal (ac)
  22. 0022specialize prime_field_polynomial_convolution_left_unit_equal (L)
  23. 0023specialize prime_field_polynomial_convolution_left_unit_equal (cb)
  24. 0024specialize prime_field_polynomial_convolution_left_unit_equal (cc)
  25. 0025apply prime_field_polynomial_convolution_left_unit_equal
  26. 0026exact hu
  27. 0027exact hc