PG0031

prime_field_polynomial_convolution_left_unit_equal

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

Every coefficient of an actual length-L product U*A agrees with A when U is a length-one unit, including the vacuous L=0 case.

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 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 mdr_i_pfp_unit_equal_result mdr_a_pfp_unit_equal_result. (exists mdr_gap_pfp_unit_equal_resultb. mdr_gap_pfp_unit_equal_resultb + S (mdr_i_pfp_unit_equal_result) = (L)) -> (((exists ff_h_mdr_pfp_unit_equal_resulto. ff_h_mdr_pfp_unit_equal_resulto + S (mdr_a_pfp_unit_equal_result) = S ((S (mdr_i_pfp_unit_equal_result)) * cc)) /\ exists ff_q_mdr_pfp_unit_equal_resulto. cb = ff_q_mdr_pfp_unit_equal_resulto * S ((S (mdr_i_pfp_unit_equal_result)) * cc) + (mdr_a_pfp_unit_equal_result))) -> (((exists ff_h_mdr_pfp_unit_equal_resultn. ff_h_mdr_pfp_unit_equal_resultn + S (mdr_a_pfp_unit_equal_result) = S ((S (mdr_i_pfp_unit_equal_result)) * ac)) /\ exists ff_q_mdr_pfp_unit_equal_resultn. ab = ff_q_mdr_pfp_unit_equal_resultn * S ((S (mdr_i_pfp_unit_equal_result)) * ac) + (mdr_a_pfp_unit_equal_result))))

Constructive proof overview

Generated structural guide

Every coefficient of an actual length-L product U*A agrees with A when U is a length-one unit, including the vacuous L=0 case.

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

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

Proof neighborhood

Direct dependencies

beta_at_exists Alpha theorem; checked-use authorized PG0030 prime_field_convolution_coefficient_left_unit matrix_rank_bounded_prefix_value Alpha theorem; checked-use authorized prime_field_polynomial_convolution_entry Alpha theorem; checked-use authorized

Direct dependents

PG0032 prime_field_polynomial_convolution_left_unit_equivalent

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

67 script commands · 13 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 convolution coefficient left unit

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 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
02Establish hAL11–11

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

  1. L11
    have hA : BetaPrefixInto(ab,ac,L,p)Definitions: BetaPrefixInto
03Separate the logical casesL12–13

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

  1. L12
    cases hc
  2. L13
    cases hc_right
04Use earlier factsL14–14

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

  1. L14
    exact hc_right_left
05Fix variables and assumptionsL15–18

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

  1. L15
    intro i
  2. L16
    intro r
  3. L17
    intro hi
  4. L18
    intro hr
06Establish haL19–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at exists.

  1. L19
    have ha : exists a. (((exists ff_h_pfp_unit_equal_entry. ff_h_pfp_unit_equal_entry + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_unit_equal_entry. ab = ff_q_pfp_unit_equal_entry * S ((S (i)) * ac) + (a)))
  2. L20
    specialize beta_at_exists (ab)
  3. L21
    specialize beta_at_exists (ac)
  4. L22
    specialize beta_at_exists (i)
  5. L23
    apply beta_at_exists
07Separate the logical casesL24–24

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

  1. L24
    cases ha
08Establish heqL25–34

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

  1. L25
    have heq : r=x
  2. L26
    specialize prime_field_convolution_coefficient_left_unit (p)
  3. L27
    specialize prime_field_convolution_coefficient_left_unit (ub)
  4. L28
    specialize prime_field_convolution_coefficient_left_unit (uc)
  5. L29
    specialize prime_field_convolution_coefficient_left_unit (ab)
  6. L30
    specialize prime_field_convolution_coefficient_left_unit (ac)
  7. L31
    specialize prime_field_convolution_coefficient_left_unit (L)
  8. L32
    specialize prime_field_convolution_coefficient_left_unit (i)
  9. L33
    specialize prime_field_convolution_coefficient_left_unit (x)
  10. L34
    specialize prime_field_convolution_coefficient_left_unit (r)
09Use earlier factsL35–44

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

  1. L35
    apply prime_field_convolution_coefficient_left_unit
  2. L36
    exact hu
  3. L37
    exact hi
  4. L38
    exact ha_witness
  5. L39
    specialize matrix_rank_bounded_prefix_value (ab)
  6. L40
    specialize matrix_rank_bounded_prefix_value (ac)
  7. L41
    specialize matrix_rank_bounded_prefix_value (L)
  8. L42
    specialize matrix_rank_bounded_prefix_value (p)
  9. L43
    specialize matrix_rank_bounded_prefix_value (i)
  10. L44
    specialize matrix_rank_bounded_prefix_value (x)
10Use earlier factsL45–54

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

  1. L45
    apply matrix_rank_bounded_prefix_value
  2. L46
    exact hA
  3. L47
    exact hi
  4. L48
    exact ha_witness
  5. L49
    specialize prime_field_polynomial_convolution_entry (p)
  6. L50
    specialize prime_field_polynomial_convolution_entry (ub)
  7. L51
    specialize prime_field_polynomial_convolution_entry (uc)
  8. L52
    specialize prime_field_polynomial_convolution_entry (1)
  9. L53
    specialize prime_field_polynomial_convolution_entry (ab)
  10. L54
    specialize prime_field_polynomial_convolution_entry (ac)
11Use earlier factsL55–64

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

  1. L55
    specialize prime_field_polynomial_convolution_entry (L)
  2. L56
    specialize prime_field_polynomial_convolution_entry (cb)
  3. L57
    specialize prime_field_polynomial_convolution_entry (cc)
  4. L58
    specialize prime_field_polynomial_convolution_entry (L)
  5. L59
    specialize prime_field_polynomial_convolution_entry (i)
  6. L60
    specialize prime_field_polynomial_convolution_entry (r)
  7. L61
    apply prime_field_polynomial_convolution_entry
  8. L62
    exact hc
  9. L63
    exact hi
  10. L64
    exact hr
12Calculate and transport equalitiesL65–66

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L65
    rewrite heq
  2. L66
    rewrite heq
13Use earlier factsL67–67

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

  1. L67
    exact ha_witness

Library-wide reading audit

Original exact command ledger · 67 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. 0011have hA : forall fom_index_pfp_unit_equal_A. (exists fom_gap_pfp_unit_equal_A_index_bound. fom_gap_pfp_unit_equal_A_index_bound + S (fom_index_pfp_unit_equal_A) = L) -> exists fom_value_pfp_unit_equal_A. ((((exists fom_beta_height_pfp_unit_equal_A_entry. fom_beta_height_pfp_unit_equal_A_entry + S (fom_value_pfp_unit_equal_A) = S ((S (fom_index_pfp_unit_equal_A)) * ac)) /\ exists fom_beta_quotient_pfp_unit_equal_A_entry. ab = fom_beta_quotient_pfp_unit_equal_A_entry * S ((S (fom_index_pfp_unit_equal_A)) * ac) + (fom_value_pfp_unit_equal_A))) /\ (exists fom_gap_pfp_unit_equal_A_value_bound. fom_gap_pfp_unit_equal_A_value_bound + S (fom_value_pfp_unit_equal_A) = p))
  12. 0012cases hc
  13. 0013cases hc_right
  14. 0014exact hc_right_left
  15. 0015intro i
  16. 0016intro r
  17. 0017intro hi
  18. 0018intro hr
  19. 0019have ha : exists a. (((exists ff_h_pfp_unit_equal_entry. ff_h_pfp_unit_equal_entry + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_unit_equal_entry. ab = ff_q_pfp_unit_equal_entry * S ((S (i)) * ac) + (a)))
  20. 0020specialize beta_at_exists (ab)
  21. 0021specialize beta_at_exists (ac)
  22. 0022specialize beta_at_exists (i)
  23. 0023apply beta_at_exists
  24. 0024cases ha
  25. 0025have heq : r=x
  26. 0026specialize prime_field_convolution_coefficient_left_unit (p)
  27. 0027specialize prime_field_convolution_coefficient_left_unit (ub)
  28. 0028specialize prime_field_convolution_coefficient_left_unit (uc)
  29. 0029specialize prime_field_convolution_coefficient_left_unit (ab)
  30. 0030specialize prime_field_convolution_coefficient_left_unit (ac)
  31. 0031specialize prime_field_convolution_coefficient_left_unit (L)
  32. 0032specialize prime_field_convolution_coefficient_left_unit (i)
  33. 0033specialize prime_field_convolution_coefficient_left_unit (x)
  34. 0034specialize prime_field_convolution_coefficient_left_unit (r)
  35. 0035apply prime_field_convolution_coefficient_left_unit
  36. 0036exact hu
  37. 0037exact hi
  38. 0038exact ha_witness
  39. 0039specialize matrix_rank_bounded_prefix_value (ab)
  40. 0040specialize matrix_rank_bounded_prefix_value (ac)
  41. 0041specialize matrix_rank_bounded_prefix_value (L)
  42. 0042specialize matrix_rank_bounded_prefix_value (p)
  43. 0043specialize matrix_rank_bounded_prefix_value (i)
  44. 0044specialize matrix_rank_bounded_prefix_value (x)
  45. 0045apply matrix_rank_bounded_prefix_value
  46. 0046exact hA
  47. 0047exact hi
  48. 0048exact ha_witness
  49. 0049specialize prime_field_polynomial_convolution_entry (p)
  50. 0050specialize prime_field_polynomial_convolution_entry (ub)
  51. 0051specialize prime_field_polynomial_convolution_entry (uc)
  52. 0052specialize prime_field_polynomial_convolution_entry (1)
  53. 0053specialize prime_field_polynomial_convolution_entry (ab)
  54. 0054specialize prime_field_polynomial_convolution_entry (ac)
  55. 0055specialize prime_field_polynomial_convolution_entry (L)
  56. 0056specialize prime_field_polynomial_convolution_entry (cb)
  57. 0057specialize prime_field_polynomial_convolution_entry (cc)
  58. 0058specialize prime_field_polynomial_convolution_entry (L)
  59. 0059specialize prime_field_polynomial_convolution_entry (i)
  60. 0060specialize prime_field_polynomial_convolution_entry (r)
  61. 0061apply prime_field_polynomial_convolution_entry
  62. 0062exact hc
  63. 0063exact hi
  64. 0064exact hr
  65. 0065rewrite heq
  66. 0066rewrite heq
  67. 0067exact ha_witness