PG0033

prime_field_polynomial_convolution_left_unit_exists

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

Construct an actual canonical length-one unit and its actual length-L left product, formally equal to A. The proper length is zero when A is empty.

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. (~((p) = 1) /\ forall pfa_factor_left_unit_exists_prime pfa_factor_right_unit_exists_prime. (p) = pfa_factor_left_unit_exists_prime * pfa_factor_right_unit_exists_prime -> pfa_factor_left_unit_exists_prime = 1 \/ pfa_factor_right_unit_exists_prime = 1) -> (forall fom_index_pfp_unit_exists_A. (exists fom_gap_pfp_unit_exists_A_index_bound. fom_gap_pfp_unit_exists_A_index_bound + S (fom_index_pfp_unit_exists_A) = L) -> exists fom_value_pfp_unit_exists_A. ((((exists fom_beta_height_pfp_unit_exists_A_entry. fom_beta_height_pfp_unit_exists_A_entry + S (fom_value_pfp_unit_exists_A) = S ((S (fom_index_pfp_unit_exists_A)) * ac)) /\ exists fom_beta_quotient_pfp_unit_exists_A_entry. ab = fom_beta_quotient_pfp_unit_exists_A_entry * S ((S (fom_index_pfp_unit_exists_A)) * ac) + (fom_value_pfp_unit_exists_A))) /\ (exists fom_gap_pfp_unit_exists_A_value_bound. fom_gap_pfp_unit_exists_A_value_bound + S (fom_value_pfp_unit_exists_A) = p))) -> (exists ub uc cb cc. ((forall fom_index_pfp_unit_exists_result_unit_bound. (exists fom_gap_pfp_unit_exists_result_unit_bound_index_bound. fom_gap_pfp_unit_exists_result_unit_bound_index_bound + S (fom_index_pfp_unit_exists_result_unit_bound) = 1) -> exists fom_value_pfp_unit_exists_result_unit_bound. ((((exists fom_beta_height_pfp_unit_exists_result_unit_bound_entry. fom_beta_height_pfp_unit_exists_result_unit_bound_entry + S (fom_value_pfp_unit_exists_result_unit_bound) = S ((S (fom_index_pfp_unit_exists_result_unit_bound)) * uc)) /\ exists fom_beta_quotient_pfp_unit_exists_result_unit_bound_entry. ub = fom_beta_quotient_pfp_unit_exists_result_unit_bound_entry * S ((S (fom_index_pfp_unit_exists_result_unit_bound)) * uc) + (fom_value_pfp_unit_exists_result_unit_bound))) /\ (exists fom_gap_pfp_unit_exists_result_unit_bound_value_bound. fom_gap_pfp_unit_exists_result_unit_bound_value_bound + S (fom_value_pfp_unit_exists_result_unit_bound) = p))) /\ (((((exists ff_h_pfp_unit_exists_result_unit_value. ff_h_pfp_unit_exists_result_unit_value + S (1) = S ((S (0)) * uc)) /\ exists ff_q_pfp_unit_exists_result_unit_value. ub = ff_q_pfp_unit_exists_result_unit_value * S ((S (0)) * uc) + (1))) /\ (((((forall fom_index_pfp_unit_exists_result_productleft. (exists fom_gap_pfp_unit_exists_result_productleft_index_bound. fom_gap_pfp_unit_exists_result_productleft_index_bound + S (fom_index_pfp_unit_exists_result_productleft) = 1) -> exists fom_value_pfp_unit_exists_result_productleft. ((((exists fom_beta_height_pfp_unit_exists_result_productleft_entry. fom_beta_height_pfp_unit_exists_result_productleft_entry + S (fom_value_pfp_unit_exists_result_productleft) = S ((S (fom_index_pfp_unit_exists_result_productleft)) * uc)) /\ exists fom_beta_quotient_pfp_unit_exists_result_productleft_entry. ub = fom_beta_quotient_pfp_unit_exists_result_productleft_entry * S ((S (fom_index_pfp_unit_exists_result_productleft)) * uc) + (fom_value_pfp_unit_exists_result_productleft))) /\ (exists fom_gap_pfp_unit_exists_result_productleft_value_bound. fom_gap_pfp_unit_exists_result_productleft_value_bound + S (fom_value_pfp_unit_exists_result_productleft) = p))) /\ (((forall fom_index_pfp_unit_exists_result_productright. (exists fom_gap_pfp_unit_exists_result_productright_index_bound. fom_gap_pfp_unit_exists_result_productright_index_bound + S (fom_index_pfp_unit_exists_result_productright) = L) -> exists fom_value_pfp_unit_exists_result_productright. ((((exists fom_beta_height_pfp_unit_exists_result_productright_entry. fom_beta_height_pfp_unit_exists_result_productright_entry + S (fom_value_pfp_unit_exists_result_productright) = S ((S (fom_index_pfp_unit_exists_result_productright)) * ac)) /\ exists fom_beta_quotient_pfp_unit_exists_result_productright_entry. ab = fom_beta_quotient_pfp_unit_exists_result_productright_entry * S ((S (fom_index_pfp_unit_exists_result_productright)) * ac) + (fom_value_pfp_unit_exists_result_productright))) /\ (exists fom_gap_pfp_unit_exists_result_productright_value_bound. fom_gap_pfp_unit_exists_result_productright_value_bound + S (fom_value_pfp_unit_exists_result_productright) = p))) /\ (((((((1)=0 \/ (L)=0) /\ (((L)=0)))) \/ (((~((1)=0)) /\ (((~((L)=0)) /\ (((1)+(L)=S (L)))))))) /\ ((forall pfc_index_unit_exists_result_productcoefficients. (exists pfa_gap_unit_exists_result_productcoefficientsbound. pfa_gap_unit_exists_result_productcoefficientsbound + S (pfc_index_unit_exists_result_productcoefficients) = (L)) -> exists pfc_value_unit_exists_result_productcoefficients. ((((exists ff_h_pfp_unit_exists_result_productcoefficientsentry. ff_h_pfp_unit_exists_result_productcoefficientsentry + S (pfc_value_unit_exists_result_productcoefficients) = S ((S (pfc_index_unit_exists_result_productcoefficients)) * cc)) /\ exists ff_q_pfp_unit_exists_result_productcoefficientsentry. cb = ff_q_pfp_unit_exists_result_productcoefficientsentry * S ((S (pfc_index_unit_exists_result_productcoefficients)) * cc) + (pfc_value_unit_exists_result_productcoefficients))) /\ ((exists pfc_terms_code_unit_exists_result_productcoefficientscoefficient pfc_terms_scale_unit_exists_result_productcoefficientscoefficient pfc_natural_sum_unit_exists_result_productcoefficientscoefficient. ((forall pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal. (exists pfa_gap_unit_exists_result_productcoefficientscoefficientdiagonalbound. pfa_gap_unit_exists_result_productcoefficientscoefficientdiagonalbound + S (pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal) = (S (pfc_index_unit_exists_result_productcoefficients))) -> exists pfc_value_unit_exists_result_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_unit_exists_result_productcoefficientscoefficientdiagonalentry. ff_h_pfp_unit_exists_result_productcoefficientscoefficientdiagonalentry + S (pfc_value_unit_exists_result_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_exists_result_productcoefficientscoefficient)) /\ exists ff_q_pfp_unit_exists_result_productcoefficientscoefficientdiagonalentry. pfc_terms_code_unit_exists_result_productcoefficientscoefficient = ff_q_pfp_unit_exists_result_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_exists_result_productcoefficientscoefficient) + (pfc_value_unit_exists_result_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_unit_exists_result_productcoefficientscoefficientdiagonalterm pfc_left_unit_exists_result_productcoefficientscoefficientdiagonalterm pfc_right_unit_exists_result_productcoefficientscoefficientdiagonalterm. (((pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal)+pfc_complement_unit_exists_result_productcoefficientscoefficientdiagonalterm=(pfc_index_unit_exists_result_productcoefficients)) /\ ((((((exists pfa_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal) = (1)) /\ ((((exists ff_h_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_unit_exists_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal)) * uc) + (pfc_left_unit_exists_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermleftoutside+(1)=(pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_unit_exists_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_unit_exists_result_productcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_unit_exists_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_unit_exists_result_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_unit_exists_result_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_unit_exists_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_unit_exists_result_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_unit_exists_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_unit_exists_result_productcoefficientscoefficientdiagonal)=pfc_left_unit_exists_result_productcoefficientscoefficientdiagonalterm*pfc_right_unit_exists_result_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_unit_exists_result_productcoefficientscoefficientsum fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum. ((((exists fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_start. fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_start. fs_u_pfc_unit_exists_result_productcoefficientscoefficientsum = fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_unit_exists_result_productcoefficientscoefficient) = S ((S (S (pfc_index_unit_exists_result_productcoefficients))) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_unit_exists_result_productcoefficientscoefficientsum = fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_unit_exists_result_productcoefficients))) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum) + (pfc_natural_sum_unit_exists_result_productcoefficientscoefficient))) /\ forall fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps = S (pfc_index_unit_exists_result_productcoefficients)) -> exists fs_a_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps fs_r_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps fs_s_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_exists_result_productcoefficientscoefficient)) /\ exists fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_unit_exists_result_productcoefficientscoefficient = fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_exists_result_productcoefficientscoefficient) + (fs_a_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_unit_exists_result_productcoefficientscoefficientsum = fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum) + (fs_r_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_unit_exists_result_productcoefficientscoefficientsum = fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum) + (fs_s_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps = fs_r_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps + fs_a_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_unit_exists_result_productcoefficientscoefficientresiduebound. pfa_gap_unit_exists_result_productcoefficientscoefficientresiduebound + S (pfc_value_unit_exists_result_productcoefficients) = (p)) /\ ((exists pfa_offset_left_unit_exists_result_productcoefficientscoefficientresiduecongruence pfa_offset_right_unit_exists_result_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_unit_exists_result_productcoefficientscoefficient) + (p) * pfa_offset_left_unit_exists_result_productcoefficientscoefficientresiduecongruence = (pfc_value_unit_exists_result_productcoefficients) + (p) * pfa_offset_right_unit_exists_result_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_unit_exists_result_equivalent pfrep_left_unit_exists_result_equivalent pfrep_right_unit_exists_result_equivalent. ((exists pfrep_position_unit_exists_result_equivalentfirst. ((pfrep_position_unit_exists_result_equivalentfirst+S (pfrep_power_unit_exists_result_equivalent)=(L)) /\ ((((exists ff_h_pfp_unit_exists_result_equivalentfirstentry. ff_h_pfp_unit_exists_result_equivalentfirstentry + S (pfrep_left_unit_exists_result_equivalent) = S ((S (pfrep_position_unit_exists_result_equivalentfirst)) * cc)) /\ exists ff_q_pfp_unit_exists_result_equivalentfirstentry. cb = ff_q_pfp_unit_exists_result_equivalentfirstentry * S ((S (pfrep_position_unit_exists_result_equivalentfirst)) * cc) + (pfrep_left_unit_exists_result_equivalent)))))) \/ (((exists pfrep_gap_unit_exists_result_equivalentfirstoutside. pfrep_gap_unit_exists_result_equivalentfirstoutside+(L)=(pfrep_power_unit_exists_result_equivalent)) /\ (((pfrep_left_unit_exists_result_equivalent)=0))))) -> ((exists pfrep_position_unit_exists_result_equivalentsecond. ((pfrep_position_unit_exists_result_equivalentsecond+S (pfrep_power_unit_exists_result_equivalent)=(L)) /\ ((((exists ff_h_pfp_unit_exists_result_equivalentsecondentry. ff_h_pfp_unit_exists_result_equivalentsecondentry + S (pfrep_right_unit_exists_result_equivalent) = S ((S (pfrep_position_unit_exists_result_equivalentsecond)) * ac)) /\ exists ff_q_pfp_unit_exists_result_equivalentsecondentry. ab = ff_q_pfp_unit_exists_result_equivalentsecondentry * S ((S (pfrep_position_unit_exists_result_equivalentsecond)) * ac) + (pfrep_right_unit_exists_result_equivalent)))))) \/ (((exists pfrep_gap_unit_exists_result_equivalentsecondoutside. pfrep_gap_unit_exists_result_equivalentsecondoutside+(L)=(pfrep_power_unit_exists_result_equivalent)) /\ (((pfrep_right_unit_exists_result_equivalent)=0))))) -> pfrep_left_unit_exists_result_equivalent=pfrep_right_unit_exists_result_equivalent))))))))

Constructive proof overview

Generated structural guide

Construct an actual canonical length-one unit and its actual length-L left product, formally equal to A. The proper length is zero when A is empty.

The unchanged tactic script uses 9 declared prerequisites and contains 81 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_nonzero Alpha theorem; checked-use authorized prime_field_polynomial_repeat_exists Alpha theorem; checked-use authorized prime_two_le Alpha theorem; checked-use authorized zero_add Alpha theorem; checked-use authorized prime_field_polynomial_convolution_at_length_exists Alpha theorem; checked-use authorized eq_decidable Alpha theorem; checked-use authorized succ_ne_zero Alpha theorem; checked-use authorized add_succ_left Alpha theorem; checked-use authorized PG0032 prime_field_polynomial_convolution_left_unit_equivalent

Direct dependents

PG0034 prime_field_polynomial_right_divides_reflexive

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

81 script commands · 26 reading checkpoints · 5 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 convolution left unit equivalent

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–6

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 hp
  6. L6
    intro hA
02Establish hp0L7–12

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

  1. L7
    have hp0 : ~(p=0)
  2. L8
    intro hz
  3. L9
    specialize prime_nonzero (p)
  4. L10
    apply prime_nonzero
  5. L11
    exact hp
  6. L12
    exact hz
03Establish huL13–20

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

  1. L13
    have hu : ∃ ub. ∃ uc. BetaPrefixInto(ub,uc,1,p) ∧ Repeat(ub,uc,1,1)Definitions: BetaPrefixIntoRepeat
  2. L14
    specialize prime_field_polynomial_repeat_exists (p)
  3. L15
    specialize prime_field_polynomial_repeat_exists (1)
  4. L16
    specialize prime_field_polynomial_repeat_exists (1)
  5. L17
    apply prime_field_polynomial_repeat_exists
  6. L18
    specialize prime_two_le (p)
  7. L19
    apply prime_two_le
  8. L20
    exact hp
04Separate the logical casesL21–23

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

  1. L21
    cases hu
  2. L22
    cases hu_witness
  3. L23
    cases hu_witness_witness
05Establish honeL24–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hu witness witness right.

  1. L24
    have hone : ((exists ff_h_pfp_unit_exists_value. ff_h_pfp_unit_exists_value + S (1) = S ((S (0)) * x1)) /\ exists ff_q_pfp_unit_exists_value. x = ff_q_pfp_unit_exists_value * S ((S (0)) * x1) + (1))
  2. L25
    specialize hu_witness_witness_right (0)
  3. L26
    apply hu_witness_witness_right
06Construct an explicit witnessL27–27

Supply the displayed value, then prove that it has the required property.

  1. L27
    exists 0
07Use earlier factsL28–28

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

  1. L28
    apply zero_add
08Establish hcL29–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial convolution at length exists.

  1. L29
    have hc : ∃ cb. ∃ cc. FpPolyProduct(p,x,x1,1,ab,ac,L,cb,cc,L)Definitions: FpPolyProduct
  2. L30
    specialize prime_field_polynomial_convolution_at_length_exists (p)
  3. L31
    specialize prime_field_polynomial_convolution_at_length_exists (x)
  4. L32
    specialize prime_field_polynomial_convolution_at_length_exists (x1)
  5. L33
    specialize prime_field_polynomial_convolution_at_length_exists (1)
  6. L34
    specialize prime_field_polynomial_convolution_at_length_exists (ab)
  7. L35
    specialize prime_field_polynomial_convolution_at_length_exists (ac)
  8. L36
    specialize prime_field_polynomial_convolution_at_length_exists (L)
  9. L37
    specialize prime_field_polynomial_convolution_at_length_exists (L)
  10. L38
    apply prime_field_polynomial_convolution_at_length_exists
09Use earlier factsL39–41

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

  1. L39
    exact hp0
  2. L40
    exact hu_witness_witness_left
  3. L41
    exact hA
10Establish hzeroL42–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eq decidable.

  1. L42
    have hzero : L=0 \/ ~(L=0)
  2. L43
    specialize eq_decidable (L)
  3. L44
    specialize eq_decidable (0)
  4. L45
    apply eq_decidable
11Separate the logical casesL46–49

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

  1. L46
    cases hzero
  2. L47
    left
  3. L48
    split
  4. L49
    right
12Use earlier factsL50–51

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

  1. L50
    exact hzero_left
  2. L51
    exact hzero_left
13Separate the logical casesL52–53

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

  1. L52
    right
  2. L53
    split
14Use earlier factsL54–55

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

  1. L54
    specialize succ_ne_zero (0)
  2. L55
    apply succ_ne_zero
15Separate the logical casesL56–56

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

  1. L56
    split
16Use earlier factsL57–57

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

  1. L57
    exact hzero_right
17Calculate and transport equalitiesL58–58

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

  1. L58
    simp [add_succ_left,zero_add]
18Separate the logical casesL59–60

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

  1. L59
    cases hc
  2. L60
    cases hc_witness
19Construct an explicit witnessL61–64

Supply the displayed value, then prove that it has the required property.

  1. L61
    exists x
  2. L62
    exists x1
  3. L63
    exists x2
  4. L64
    exists x3
20Separate the logical casesL65–65

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

  1. L65
    split
21Use earlier factsL66–66

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

  1. L66
    exact hu_witness_witness_left
22Separate the logical casesL67–67

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

  1. L67
    split
23Use earlier factsL68–68

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

  1. L68
    exact hone
24Separate the logical casesL69–69

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

  1. L69
    split
25Use earlier factsL70–79

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

  1. L70
    exact hc_witness_witness
  2. L71
    specialize prime_field_polynomial_convolution_left_unit_equivalent (p)
  3. L72
    specialize prime_field_polynomial_convolution_left_unit_equivalent (x)
  4. L73
    specialize prime_field_polynomial_convolution_left_unit_equivalent (x1)
  5. L74
    specialize prime_field_polynomial_convolution_left_unit_equivalent (ab)
  6. L75
    specialize prime_field_polynomial_convolution_left_unit_equivalent (ac)
  7. L76
    specialize prime_field_polynomial_convolution_left_unit_equivalent (L)
  8. L77
    specialize prime_field_polynomial_convolution_left_unit_equivalent (x2)
  9. L78
    specialize prime_field_polynomial_convolution_left_unit_equivalent (x3)
  10. L79
    apply prime_field_polynomial_convolution_left_unit_equivalent
26Use earlier factsL80–81

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

  1. L80
    exact hone
  2. L81
    exact hc_witness_witness

Library-wide reading audit

Original exact command ledger · 81 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro hp
  6. 0006intro hA
  7. 0007have hp0 : ~(p=0)
  8. 0008intro hz
  9. 0009specialize prime_nonzero (p)
  10. 0010apply prime_nonzero
  11. 0011exact hp
  12. 0012exact hz
  13. 0013have hu : exists ub uc. ((forall fom_index_pfp_unit_exists_bound. (exists fom_gap_pfp_unit_exists_bound_index_bound. fom_gap_pfp_unit_exists_bound_index_bound + S (fom_index_pfp_unit_exists_bound) = 1) -> exists fom_value_pfp_unit_exists_bound. ((((exists fom_beta_height_pfp_unit_exists_bound_entry. fom_beta_height_pfp_unit_exists_bound_entry + S (fom_value_pfp_unit_exists_bound) = S ((S (fom_index_pfp_unit_exists_bound)) * uc)) /\ exists fom_beta_quotient_pfp_unit_exists_bound_entry. ub = fom_beta_quotient_pfp_unit_exists_bound_entry * S ((S (fom_index_pfp_unit_exists_bound)) * uc) + (fom_value_pfp_unit_exists_bound))) /\ (exists fom_gap_pfp_unit_exists_bound_value_bound. fom_gap_pfp_unit_exists_bound_value_bound + S (fom_value_pfp_unit_exists_bound) = p))) /\ ((forall pfp_repeat_index_unit_exists_repeat. (exists pfa_gap_unit_exists_repeatindex. pfa_gap_unit_exists_repeatindex + S (pfp_repeat_index_unit_exists_repeat) = (1)) -> (((exists ff_h_pfp_unit_exists_repeatentry. ff_h_pfp_unit_exists_repeatentry + S (1) = S ((S (pfp_repeat_index_unit_exists_repeat)) * uc)) /\ exists ff_q_pfp_unit_exists_repeatentry. ub = ff_q_pfp_unit_exists_repeatentry * S ((S (pfp_repeat_index_unit_exists_repeat)) * uc) + (1))))))
  14. 0014specialize prime_field_polynomial_repeat_exists (p)
  15. 0015specialize prime_field_polynomial_repeat_exists (1)
  16. 0016specialize prime_field_polynomial_repeat_exists (1)
  17. 0017apply prime_field_polynomial_repeat_exists
  18. 0018specialize prime_two_le (p)
  19. 0019apply prime_two_le
  20. 0020exact hp
  21. 0021cases hu
  22. 0022cases hu_witness
  23. 0023cases hu_witness_witness
  24. 0024have hone : ((exists ff_h_pfp_unit_exists_value. ff_h_pfp_unit_exists_value + S (1) = S ((S (0)) * x1)) /\ exists ff_q_pfp_unit_exists_value. x = ff_q_pfp_unit_exists_value * S ((S (0)) * x1) + (1))
  25. 0025specialize hu_witness_witness_right (0)
  26. 0026apply hu_witness_witness_right
  27. 0027exists 0
  28. 0028apply zero_add
  29. 0029have hc : exists cb cc. (((forall fom_index_pfp_unit_exists_chosenleft. (exists fom_gap_pfp_unit_exists_chosenleft_index_bound. fom_gap_pfp_unit_exists_chosenleft_index_bound + S (fom_index_pfp_unit_exists_chosenleft) = 1) -> exists fom_value_pfp_unit_exists_chosenleft. ((((exists fom_beta_height_pfp_unit_exists_chosenleft_entry. fom_beta_height_pfp_unit_exists_chosenleft_entry + S (fom_value_pfp_unit_exists_chosenleft) = S ((S (fom_index_pfp_unit_exists_chosenleft)) * x1)) /\ exists fom_beta_quotient_pfp_unit_exists_chosenleft_entry. x = fom_beta_quotient_pfp_unit_exists_chosenleft_entry * S ((S (fom_index_pfp_unit_exists_chosenleft)) * x1) + (fom_value_pfp_unit_exists_chosenleft))) /\ (exists fom_gap_pfp_unit_exists_chosenleft_value_bound. fom_gap_pfp_unit_exists_chosenleft_value_bound + S (fom_value_pfp_unit_exists_chosenleft) = p))) /\ (((forall fom_index_pfp_unit_exists_chosenright. (exists fom_gap_pfp_unit_exists_chosenright_index_bound. fom_gap_pfp_unit_exists_chosenright_index_bound + S (fom_index_pfp_unit_exists_chosenright) = L) -> exists fom_value_pfp_unit_exists_chosenright. ((((exists fom_beta_height_pfp_unit_exists_chosenright_entry. fom_beta_height_pfp_unit_exists_chosenright_entry + S (fom_value_pfp_unit_exists_chosenright) = S ((S (fom_index_pfp_unit_exists_chosenright)) * ac)) /\ exists fom_beta_quotient_pfp_unit_exists_chosenright_entry. ab = fom_beta_quotient_pfp_unit_exists_chosenright_entry * S ((S (fom_index_pfp_unit_exists_chosenright)) * ac) + (fom_value_pfp_unit_exists_chosenright))) /\ (exists fom_gap_pfp_unit_exists_chosenright_value_bound. fom_gap_pfp_unit_exists_chosenright_value_bound + S (fom_value_pfp_unit_exists_chosenright) = p))) /\ (((((((1)=0 \/ (L)=0) /\ (((L)=0)))) \/ (((~((1)=0)) /\ (((~((L)=0)) /\ (((1)+(L)=S (L)))))))) /\ ((forall pfc_index_unit_exists_chosencoefficients. (exists pfa_gap_unit_exists_chosencoefficientsbound. pfa_gap_unit_exists_chosencoefficientsbound + S (pfc_index_unit_exists_chosencoefficients) = (L)) -> exists pfc_value_unit_exists_chosencoefficients. ((((exists ff_h_pfp_unit_exists_chosencoefficientsentry. ff_h_pfp_unit_exists_chosencoefficientsentry + S (pfc_value_unit_exists_chosencoefficients) = S ((S (pfc_index_unit_exists_chosencoefficients)) * cc)) /\ exists ff_q_pfp_unit_exists_chosencoefficientsentry. cb = ff_q_pfp_unit_exists_chosencoefficientsentry * S ((S (pfc_index_unit_exists_chosencoefficients)) * cc) + (pfc_value_unit_exists_chosencoefficients))) /\ ((exists pfc_terms_code_unit_exists_chosencoefficientscoefficient pfc_terms_scale_unit_exists_chosencoefficientscoefficient pfc_natural_sum_unit_exists_chosencoefficientscoefficient. ((forall pfc_index_unit_exists_chosencoefficientscoefficientdiagonal. (exists pfa_gap_unit_exists_chosencoefficientscoefficientdiagonalbound. pfa_gap_unit_exists_chosencoefficientscoefficientdiagonalbound + S (pfc_index_unit_exists_chosencoefficientscoefficientdiagonal) = (S (pfc_index_unit_exists_chosencoefficients))) -> exists pfc_value_unit_exists_chosencoefficientscoefficientdiagonal. ((((exists ff_h_pfp_unit_exists_chosencoefficientscoefficientdiagonalentry. ff_h_pfp_unit_exists_chosencoefficientscoefficientdiagonalentry + S (pfc_value_unit_exists_chosencoefficientscoefficientdiagonal) = S ((S (pfc_index_unit_exists_chosencoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_exists_chosencoefficientscoefficient)) /\ exists ff_q_pfp_unit_exists_chosencoefficientscoefficientdiagonalentry. pfc_terms_code_unit_exists_chosencoefficientscoefficient = ff_q_pfp_unit_exists_chosencoefficientscoefficientdiagonalentry * S ((S (pfc_index_unit_exists_chosencoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_exists_chosencoefficientscoefficient) + (pfc_value_unit_exists_chosencoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_unit_exists_chosencoefficientscoefficientdiagonalterm pfc_left_unit_exists_chosencoefficientscoefficientdiagonalterm pfc_right_unit_exists_chosencoefficientscoefficientdiagonalterm. (((pfc_index_unit_exists_chosencoefficientscoefficientdiagonal)+pfc_complement_unit_exists_chosencoefficientscoefficientdiagonalterm=(pfc_index_unit_exists_chosencoefficients)) /\ ((((((exists pfa_gap_unit_exists_chosencoefficientscoefficientdiagonaltermleftinside. pfa_gap_unit_exists_chosencoefficientscoefficientdiagonaltermleftinside + S (pfc_index_unit_exists_chosencoefficientscoefficientdiagonal) = (1)) /\ ((((exists ff_h_pfp_unit_exists_chosencoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_unit_exists_chosencoefficientscoefficientdiagonaltermleftentry + S (pfc_left_unit_exists_chosencoefficientscoefficientdiagonalterm) = S ((S (pfc_index_unit_exists_chosencoefficientscoefficientdiagonal)) * x1)) /\ exists ff_q_pfp_unit_exists_chosencoefficientscoefficientdiagonaltermleftentry. x = ff_q_pfp_unit_exists_chosencoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_unit_exists_chosencoefficientscoefficientdiagonal)) * x1) + (pfc_left_unit_exists_chosencoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_exists_chosencoefficientscoefficientdiagonaltermleftoutside. pfc_gap_unit_exists_chosencoefficientscoefficientdiagonaltermleftoutside+(1)=(pfc_index_unit_exists_chosencoefficientscoefficientdiagonal)) /\ (((pfc_left_unit_exists_chosencoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_unit_exists_chosencoefficientscoefficientdiagonaltermrightinside. pfa_gap_unit_exists_chosencoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_unit_exists_chosencoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_unit_exists_chosencoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_unit_exists_chosencoefficientscoefficientdiagonaltermrightentry + S (pfc_right_unit_exists_chosencoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_unit_exists_chosencoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_unit_exists_chosencoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_unit_exists_chosencoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_unit_exists_chosencoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_unit_exists_chosencoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_exists_chosencoefficientscoefficientdiagonaltermrightoutside. pfc_gap_unit_exists_chosencoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_unit_exists_chosencoefficientscoefficientdiagonalterm)) /\ (((pfc_right_unit_exists_chosencoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_unit_exists_chosencoefficientscoefficientdiagonal)=pfc_left_unit_exists_chosencoefficientscoefficientdiagonalterm*pfc_right_unit_exists_chosencoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_unit_exists_chosencoefficientscoefficientsum fs_v_pfc_unit_exists_chosencoefficientscoefficientsum. ((((exists fs_h_pfc_unit_exists_chosencoefficientscoefficientsum_body_start. fs_h_pfc_unit_exists_chosencoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_unit_exists_chosencoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_exists_chosencoefficientscoefficientsum_body_start. fs_u_pfc_unit_exists_chosencoefficientscoefficientsum = fs_q_pfc_unit_exists_chosencoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_unit_exists_chosencoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_unit_exists_chosencoefficientscoefficientsum_body_terminal. fs_h_pfc_unit_exists_chosencoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_unit_exists_chosencoefficientscoefficient) = S ((S (S (pfc_index_unit_exists_chosencoefficients))) * fs_v_pfc_unit_exists_chosencoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_exists_chosencoefficientscoefficientsum_body_terminal. fs_u_pfc_unit_exists_chosencoefficientscoefficientsum = fs_q_pfc_unit_exists_chosencoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_unit_exists_chosencoefficients))) * fs_v_pfc_unit_exists_chosencoefficientscoefficientsum) + (pfc_natural_sum_unit_exists_chosencoefficientscoefficient))) /\ forall fs_i_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps = S (pfc_index_unit_exists_chosencoefficients)) -> exists fs_a_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps fs_r_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps fs_s_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps_summand. fs_h_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_exists_chosencoefficientscoefficient)) /\ exists fs_q_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps_summand. pfc_terms_code_unit_exists_chosencoefficientscoefficient = fs_q_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_exists_chosencoefficientscoefficient) + (fs_a_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps_partial. fs_h_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_exists_chosencoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps_partial. fs_u_pfc_unit_exists_chosencoefficientscoefficientsum = fs_q_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_exists_chosencoefficientscoefficientsum) + (fs_r_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps_successor. fs_h_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_exists_chosencoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps_successor. fs_u_pfc_unit_exists_chosencoefficientscoefficientsum = fs_q_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_exists_chosencoefficientscoefficientsum) + (fs_s_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps = fs_r_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps + fs_a_pfc_unit_exists_chosencoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_unit_exists_chosencoefficientscoefficientresiduebound. pfa_gap_unit_exists_chosencoefficientscoefficientresiduebound + S (pfc_value_unit_exists_chosencoefficients) = (p)) /\ ((exists pfa_offset_left_unit_exists_chosencoefficientscoefficientresiduecongruence pfa_offset_right_unit_exists_chosencoefficientscoefficientresiduecongruence. (pfc_natural_sum_unit_exists_chosencoefficientscoefficient) + (p) * pfa_offset_left_unit_exists_chosencoefficientscoefficientresiduecongruence = (pfc_value_unit_exists_chosencoefficients) + (p) * pfa_offset_right_unit_exists_chosencoefficientscoefficientresiduecongruence)))))))))))))))))))
  30. 0030specialize prime_field_polynomial_convolution_at_length_exists (p)
  31. 0031specialize prime_field_polynomial_convolution_at_length_exists (x)
  32. 0032specialize prime_field_polynomial_convolution_at_length_exists (x1)
  33. 0033specialize prime_field_polynomial_convolution_at_length_exists (1)
  34. 0034specialize prime_field_polynomial_convolution_at_length_exists (ab)
  35. 0035specialize prime_field_polynomial_convolution_at_length_exists (ac)
  36. 0036specialize prime_field_polynomial_convolution_at_length_exists (L)
  37. 0037specialize prime_field_polynomial_convolution_at_length_exists (L)
  38. 0038apply prime_field_polynomial_convolution_at_length_exists
  39. 0039exact hp0
  40. 0040exact hu_witness_witness_left
  41. 0041exact hA
  42. 0042have hzero : L=0 \/ ~(L=0)
  43. 0043specialize eq_decidable (L)
  44. 0044specialize eq_decidable (0)
  45. 0045apply eq_decidable
  46. 0046cases hzero
  47. 0047left
  48. 0048split
  49. 0049right
  50. 0050exact hzero_left
  51. 0051exact hzero_left
  52. 0052right
  53. 0053split
  54. 0054specialize succ_ne_zero (0)
  55. 0055apply succ_ne_zero
  56. 0056split
  57. 0057exact hzero_right
  58. 0058simp [add_succ_left,zero_add]
  59. 0059cases hc
  60. 0060cases hc_witness
  61. 0061exists x
  62. 0062exists x1
  63. 0063exists x2
  64. 0064exists x3
  65. 0065split
  66. 0066exact hu_witness_witness_left
  67. 0067split
  68. 0068exact hone
  69. 0069split
  70. 0070exact hc_witness_witness
  71. 0071specialize prime_field_polynomial_convolution_left_unit_equivalent (p)
  72. 0072specialize prime_field_polynomial_convolution_left_unit_equivalent (x)
  73. 0073specialize prime_field_polynomial_convolution_left_unit_equivalent (x1)
  74. 0074specialize prime_field_polynomial_convolution_left_unit_equivalent (ab)
  75. 0075specialize prime_field_polynomial_convolution_left_unit_equivalent (ac)
  76. 0076specialize prime_field_polynomial_convolution_left_unit_equivalent (L)
  77. 0077specialize prime_field_polynomial_convolution_left_unit_equivalent (x2)
  78. 0078specialize prime_field_polynomial_convolution_left_unit_equivalent (x3)
  79. 0079apply prime_field_polynomial_convolution_left_unit_equivalent
  80. 0080exact hone
  81. 0081exact hc_witness_witness