PX0024

prime_field_polynomial_constant_product_to_scale

An actual proper-length constant-right polynomial product is the existing actual coefficient scalar action.

Alpha v34 checked-use · first admitted v33 · 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.

Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.

Exact theorem in conservative defined notation

∀ p. ∀ k. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ cb. ∀ cc. ∀ L. Prime(p) → BetaAt(bb,bc,0,k) → FpPolyProduct(p,ab,ac,L,bb,bc,1,cb,cc,L) → FpPolyScale(p,k,ab,ac,cb,cc,L)

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

Definition DAG

FpPolyScale(p,k,ab,ac,bb,bc,l) · 1FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 2Prime(p) · 1BetaAt(b,c,i,x) · 3

Actual proof prerequisites

matrix_rank_bounded_prefix_value · checked external prerequisitebeta_at_exists · checked external prerequisiteprime_field_polynomial_constant_right_coefficientprime_field_polynomial_convolution_entry · checked external prerequisite
Original expanded first-order statement 
forall p k ab ac bb bc cb cc L. (~((p) = 1) /\ forall pfa_factor_left_constant_scale_prime pfa_factor_right_constant_scale_prime. (p) = pfa_factor_left_constant_scale_prime * pfa_factor_right_constant_scale_prime -> pfa_factor_left_constant_scale_prime = 1 \/ pfa_factor_right_constant_scale_prime = 1) -> (((exists ff_h_pfp_constant_scale_value. ff_h_pfp_constant_scale_value + S (k) = S ((S (0)) * bc)) /\ exists ff_q_pfp_constant_scale_value. bb = ff_q_pfp_constant_scale_value * S ((S (0)) * bc) + (k))) -> (((forall fom_index_pfp_constant_scale_convolutionleft. (exists fom_gap_pfp_constant_scale_convolutionleft_index_bound. fom_gap_pfp_constant_scale_convolutionleft_index_bound + S (fom_index_pfp_constant_scale_convolutionleft) = L) -> exists fom_value_pfp_constant_scale_convolutionleft. ((((exists fom_beta_height_pfp_constant_scale_convolutionleft_entry. fom_beta_height_pfp_constant_scale_convolutionleft_entry + S (fom_value_pfp_constant_scale_convolutionleft) = S ((S (fom_index_pfp_constant_scale_convolutionleft)) * ac)) /\ exists fom_beta_quotient_pfp_constant_scale_convolutionleft_entry. ab = fom_beta_quotient_pfp_constant_scale_convolutionleft_entry * S ((S (fom_index_pfp_constant_scale_convolutionleft)) * ac) + (fom_value_pfp_constant_scale_convolutionleft))) /\ (exists fom_gap_pfp_constant_scale_convolutionleft_value_bound. fom_gap_pfp_constant_scale_convolutionleft_value_bound + S (fom_value_pfp_constant_scale_convolutionleft) = p))) /\ (((forall fom_index_pfp_constant_scale_convolutionright. (exists fom_gap_pfp_constant_scale_convolutionright_index_bound. fom_gap_pfp_constant_scale_convolutionright_index_bound + S (fom_index_pfp_constant_scale_convolutionright) = 1) -> exists fom_value_pfp_constant_scale_convolutionright. ((((exists fom_beta_height_pfp_constant_scale_convolutionright_entry. fom_beta_height_pfp_constant_scale_convolutionright_entry + S (fom_value_pfp_constant_scale_convolutionright) = S ((S (fom_index_pfp_constant_scale_convolutionright)) * bc)) /\ exists fom_beta_quotient_pfp_constant_scale_convolutionright_entry. bb = fom_beta_quotient_pfp_constant_scale_convolutionright_entry * S ((S (fom_index_pfp_constant_scale_convolutionright)) * bc) + (fom_value_pfp_constant_scale_convolutionright))) /\ (exists fom_gap_pfp_constant_scale_convolutionright_value_bound. fom_gap_pfp_constant_scale_convolutionright_value_bound + S (fom_value_pfp_constant_scale_convolutionright) = p))) /\ (((((((L)=0 \/ (1)=0) /\ (((L)=0)))) \/ (((~((L)=0)) /\ (((~((1)=0)) /\ (((L)+(1)=S (L)))))))) /\ ((forall pfc_index_constant_scale_convolutioncoefficients. (exists pfa_gap_constant_scale_convolutioncoefficientsbound. pfa_gap_constant_scale_convolutioncoefficientsbound + S (pfc_index_constant_scale_convolutioncoefficients) = (L)) -> exists pfc_value_constant_scale_convolutioncoefficients. ((((exists ff_h_pfp_constant_scale_convolutioncoefficientsentry. ff_h_pfp_constant_scale_convolutioncoefficientsentry + S (pfc_value_constant_scale_convolutioncoefficients) = S ((S (pfc_index_constant_scale_convolutioncoefficients)) * cc)) /\ exists ff_q_pfp_constant_scale_convolutioncoefficientsentry. cb = ff_q_pfp_constant_scale_convolutioncoefficientsentry * S ((S (pfc_index_constant_scale_convolutioncoefficients)) * cc) + (pfc_value_constant_scale_convolutioncoefficients))) /\ ((exists pfc_terms_code_constant_scale_convolutioncoefficientscoefficient pfc_terms_scale_constant_scale_convolutioncoefficientscoefficient pfc_natural_sum_constant_scale_convolutioncoefficientscoefficient. ((forall pfc_index_constant_scale_convolutioncoefficientscoefficientdiagonal. (exists pfa_gap_constant_scale_convolutioncoefficientscoefficientdiagonalbound. pfa_gap_constant_scale_convolutioncoefficientscoefficientdiagonalbound + S (pfc_index_constant_scale_convolutioncoefficientscoefficientdiagonal) = (S (pfc_index_constant_scale_convolutioncoefficients))) -> exists pfc_value_constant_scale_convolutioncoefficientscoefficientdiagonal. ((((exists ff_h_pfp_constant_scale_convolutioncoefficientscoefficientdiagonalentry. ff_h_pfp_constant_scale_convolutioncoefficientscoefficientdiagonalentry + S (pfc_value_constant_scale_convolutioncoefficientscoefficientdiagonal) = S ((S (pfc_index_constant_scale_convolutioncoefficientscoefficientdiagonal)) * pfc_terms_scale_constant_scale_convolutioncoefficientscoefficient)) /\ exists ff_q_pfp_constant_scale_convolutioncoefficientscoefficientdiagonalentry. pfc_terms_code_constant_scale_convolutioncoefficientscoefficient = ff_q_pfp_constant_scale_convolutioncoefficientscoefficientdiagonalentry * S ((S (pfc_index_constant_scale_convolutioncoefficientscoefficientdiagonal)) * pfc_terms_scale_constant_scale_convolutioncoefficientscoefficient) + (pfc_value_constant_scale_convolutioncoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_constant_scale_convolutioncoefficientscoefficientdiagonalterm pfc_left_constant_scale_convolutioncoefficientscoefficientdiagonalterm pfc_right_constant_scale_convolutioncoefficientscoefficientdiagonalterm. (((pfc_index_constant_scale_convolutioncoefficientscoefficientdiagonal)+pfc_complement_constant_scale_convolutioncoefficientscoefficientdiagonalterm=(pfc_index_constant_scale_convolutioncoefficients)) /\ ((((((exists pfa_gap_constant_scale_convolutioncoefficientscoefficientdiagonaltermleftinside. pfa_gap_constant_scale_convolutioncoefficientscoefficientdiagonaltermleftinside + S (pfc_index_constant_scale_convolutioncoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_constant_scale_convolutioncoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_constant_scale_convolutioncoefficientscoefficientdiagonaltermleftentry + S (pfc_left_constant_scale_convolutioncoefficientscoefficientdiagonalterm) = S ((S (pfc_index_constant_scale_convolutioncoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_constant_scale_convolutioncoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_constant_scale_convolutioncoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_constant_scale_convolutioncoefficientscoefficientdiagonal)) * ac) + (pfc_left_constant_scale_convolutioncoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_constant_scale_convolutioncoefficientscoefficientdiagonaltermleftoutside. pfc_gap_constant_scale_convolutioncoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_constant_scale_convolutioncoefficientscoefficientdiagonal)) /\ (((pfc_left_constant_scale_convolutioncoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_constant_scale_convolutioncoefficientscoefficientdiagonaltermrightinside. pfa_gap_constant_scale_convolutioncoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_constant_scale_convolutioncoefficientscoefficientdiagonalterm) = (1)) /\ ((((exists ff_h_pfp_constant_scale_convolutioncoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_constant_scale_convolutioncoefficientscoefficientdiagonaltermrightentry + S (pfc_right_constant_scale_convolutioncoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_constant_scale_convolutioncoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_constant_scale_convolutioncoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_constant_scale_convolutioncoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_constant_scale_convolutioncoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_constant_scale_convolutioncoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_constant_scale_convolutioncoefficientscoefficientdiagonaltermrightoutside. pfc_gap_constant_scale_convolutioncoefficientscoefficientdiagonaltermrightoutside+(1)=(pfc_complement_constant_scale_convolutioncoefficientscoefficientdiagonalterm)) /\ (((pfc_right_constant_scale_convolutioncoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_constant_scale_convolutioncoefficientscoefficientdiagonal)=pfc_left_constant_scale_convolutioncoefficientscoefficientdiagonalterm*pfc_right_constant_scale_convolutioncoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_constant_scale_convolutioncoefficientscoefficientsum fs_v_pfc_constant_scale_convolutioncoefficientscoefficientsum. ((((exists fs_h_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_start. fs_h_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_constant_scale_convolutioncoefficientscoefficientsum)) /\ exists fs_q_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_start. fs_u_pfc_constant_scale_convolutioncoefficientscoefficientsum = fs_q_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_constant_scale_convolutioncoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_terminal. fs_h_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_constant_scale_convolutioncoefficientscoefficient) = S ((S (S (pfc_index_constant_scale_convolutioncoefficients))) * fs_v_pfc_constant_scale_convolutioncoefficientscoefficientsum)) /\ exists fs_q_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_terminal. fs_u_pfc_constant_scale_convolutioncoefficientscoefficientsum = fs_q_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_constant_scale_convolutioncoefficients))) * fs_v_pfc_constant_scale_convolutioncoefficientscoefficientsum) + (pfc_natural_sum_constant_scale_convolutioncoefficientscoefficient))) /\ forall fs_i_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps = S (pfc_index_constant_scale_convolutioncoefficients)) -> exists fs_a_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps fs_r_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps fs_s_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps_summand. fs_h_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps)) * pfc_terms_scale_constant_scale_convolutioncoefficientscoefficient)) /\ exists fs_q_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps_summand. pfc_terms_code_constant_scale_convolutioncoefficientscoefficient = fs_q_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps)) * pfc_terms_scale_constant_scale_convolutioncoefficientscoefficient) + (fs_a_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps_partial. fs_h_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps)) * fs_v_pfc_constant_scale_convolutioncoefficientscoefficientsum)) /\ exists fs_q_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps_partial. fs_u_pfc_constant_scale_convolutioncoefficientscoefficientsum = fs_q_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps)) * fs_v_pfc_constant_scale_convolutioncoefficientscoefficientsum) + (fs_r_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps_successor. fs_h_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps)) * fs_v_pfc_constant_scale_convolutioncoefficientscoefficientsum)) /\ exists fs_q_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps_successor. fs_u_pfc_constant_scale_convolutioncoefficientscoefficientsum = fs_q_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps)) * fs_v_pfc_constant_scale_convolutioncoefficientscoefficientsum) + (fs_s_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps = fs_r_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps + fs_a_pfc_constant_scale_convolutioncoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_constant_scale_convolutioncoefficientscoefficientresiduebound. pfa_gap_constant_scale_convolutioncoefficientscoefficientresiduebound + S (pfc_value_constant_scale_convolutioncoefficients) = (p)) /\ ((exists pfa_offset_left_constant_scale_convolutioncoefficientscoefficientresiduecongruence pfa_offset_right_constant_scale_convolutioncoefficientscoefficientresiduecongruence. (pfc_natural_sum_constant_scale_convolutioncoefficientscoefficient) + (p) * pfa_offset_left_constant_scale_convolutioncoefficientscoefficientresiduecongruence = (pfc_value_constant_scale_convolutioncoefficients) + (p) * pfa_offset_right_constant_scale_convolutioncoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((exists pfa_gap_constant_scale_resultscalar. pfa_gap_constant_scale_resultscalar + S (k) = (p)) /\ ((forall pfp_index_constant_scale_result. (exists pfa_gap_constant_scale_resultindex. pfa_gap_constant_scale_resultindex + S (pfp_index_constant_scale_result) = (L)) -> exists pfp_source_constant_scale_result pfp_value_constant_scale_result. ((((exists ff_h_pfp_constant_scale_resultsource. ff_h_pfp_constant_scale_resultsource + S (pfp_source_constant_scale_result) = S ((S (pfp_index_constant_scale_result)) * ac)) /\ exists ff_q_pfp_constant_scale_resultsource. ab = ff_q_pfp_constant_scale_resultsource * S ((S (pfp_index_constant_scale_result)) * ac) + (pfp_source_constant_scale_result))) /\ (((((exists ff_h_pfp_constant_scale_resulttarget. ff_h_pfp_constant_scale_resulttarget + S (pfp_value_constant_scale_result) = S ((S (pfp_index_constant_scale_result)) * cc)) /\ exists ff_q_pfp_constant_scale_resulttarget. cb = ff_q_pfp_constant_scale_resulttarget * S ((S (pfp_index_constant_scale_result)) * cc) + (pfp_value_constant_scale_result))) /\ ((((exists pfa_gap_constant_scale_resultoperationleft. pfa_gap_constant_scale_resultoperationleft + S (k) = (p)) /\ (((exists pfa_gap_constant_scale_resultoperationright. pfa_gap_constant_scale_resultoperationright + S (pfp_source_constant_scale_result) = (p)) /\ ((((exists pfa_gap_constant_scale_resultoperationresultbound. pfa_gap_constant_scale_resultoperationresultbound + S (pfp_value_constant_scale_result) = (p)) /\ ((exists pfa_offset_left_constant_scale_resultoperationresultcongruence pfa_offset_right_constant_scale_resultoperationresultcongruence. ((k) * (pfp_source_constant_scale_result)) + (p) * pfa_offset_left_constant_scale_resultoperationresultcongruence = (pfp_value_constant_scale_result) + (p) * pfa_offset_right_constant_scale_resultoperationresultcongruence)))))))))))))))))

Complete tactic proof in conservative notation

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

82 script commands · 21 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.

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 constant right coefficient
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro cb
  8. L8
    intro cc
  9. L9
    intro L
  10. L10
    intro hp
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hk
  2. L12
    intro hc
03Establish hcopyL13–14

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

  1. L13
    have hcopy : FpPolyProduct(p,ab,ac,L,bb,bc,1,cb,cc,L)Definitions: FpPolyProduct(p,ab,ac,L,bb,bc,1,cb,cc,L)Original native command in the exact edition
  2. L14
    exact hc
04Separate the logical casesL15–18

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

  1. L15
    cases hcopy
  2. L16
    cases hcopy_right
  3. L17
    cases hcopy_right_right
  4. L18
    split
05Use earlier factsL19–26

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

  1. L19
    specialize matrix_rank_bounded_prefix_value (bb)
  2. L20
    specialize matrix_rank_bounded_prefix_value (bc)
  3. L21
    specialize matrix_rank_bounded_prefix_value (1)
  4. L22
    specialize matrix_rank_bounded_prefix_value (p)
  5. L23
    specialize matrix_rank_bounded_prefix_value (0)
  6. L24
    specialize matrix_rank_bounded_prefix_value (k)
  7. L25
    apply matrix_rank_bounded_prefix_value
  8. L26
    exact hcopy_right_left
06Construct an explicit witnessL27–27

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

  1. L27
    exists 0
07Calculate and transport equalitiesL28–28

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

  1. L28
    simp
08Use earlier factsL29–29

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

  1. L29
    exact hk
09Fix variables and assumptionsL30–31

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

  1. L30
    intro i
  2. L31
    intro hi
10Establish haL32–36

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

  1. L32
    have ha : ∃ a. BetaAt(ab,ac,i,a)Definitions: BetaAt(ab,ac,i,a)Original native command in the exact edition
  2. L33
    specialize beta_at_exists (ab)
  3. L34
    specialize beta_at_exists (ac)
  4. L35
    specialize beta_at_exists (i)
  5. L36
    apply beta_at_exists
11Separate the logical casesL37–37

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

  1. L37
    cases ha
12Establish hrL38–42

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

  1. L38
    have hr : ∃ r. BetaAt(cb,cc,i,r)Definitions: BetaAt(cb,cc,i,r)Original native command in the exact edition
  2. L39
    specialize beta_at_exists (cb)
  3. L40
    specialize beta_at_exists (cc)
  4. L41
    specialize beta_at_exists (i)
  5. L42
    apply beta_at_exists
13Separate the logical casesL43–43

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

  1. L43
    cases hr
14Construct an explicit witnessL44–45

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

  1. L44
    exists x
  2. L45
    exists x1
15Separate the logical casesL46–46

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

  1. L46
    split
16Use earlier factsL47–47

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

  1. L47
    exact ha_witness
17Separate the logical casesL48–48

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

  1. L48
    split
18Use earlier factsL49–58

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

  1. L49
    exact hr_witness
  2. L50
    specialize prime_field_polynomial_constant_right_coefficient (p)
  3. L51
    specialize prime_field_polynomial_constant_right_coefficient (ab)
  4. L52
    specialize prime_field_polynomial_constant_right_coefficient (ac)
  5. L53
    specialize prime_field_polynomial_constant_right_coefficient (L)
  6. L54
    specialize prime_field_polynomial_constant_right_coefficient (bb)
  7. L55
    specialize prime_field_polynomial_constant_right_coefficient (bc)
  8. L56
    specialize prime_field_polynomial_constant_right_coefficient (k)
  9. L57
    specialize prime_field_polynomial_constant_right_coefficient (i)
  10. L58
    specialize prime_field_polynomial_constant_right_coefficient (x)
19Use earlier factsL59–68

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

  1. L59
    specialize prime_field_polynomial_constant_right_coefficient (x1)
  2. L60
    apply prime_field_polynomial_constant_right_coefficient
  3. L61
    exact hp
  4. L62
    exact hcopy_left
  5. L63
    exact hcopy_right_left
  6. L64
    exact hk
  7. L65
    exact hi
  8. L66
    exact ha_witness
  9. L67
    specialize prime_field_polynomial_convolution_entry (p)
  10. L68
    specialize prime_field_polynomial_convolution_entry (ab)
20Use earlier factsL69–78

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

  1. L69
    specialize prime_field_polynomial_convolution_entry (ac)
  2. L70
    specialize prime_field_polynomial_convolution_entry (L)
  3. L71
    specialize prime_field_polynomial_convolution_entry (bb)
  4. L72
    specialize prime_field_polynomial_convolution_entry (bc)
  5. L73
    specialize prime_field_polynomial_convolution_entry (1)
  6. L74
    specialize prime_field_polynomial_convolution_entry (cb)
  7. L75
    specialize prime_field_polynomial_convolution_entry (cc)
  8. L76
    specialize prime_field_polynomial_convolution_entry (L)
  9. L77
    specialize prime_field_polynomial_convolution_entry (i)
  10. L78
    specialize prime_field_polynomial_convolution_entry (x1)
21Use earlier factsL79–82

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

  1. L79
    apply prime_field_polynomial_convolution_entry
  2. L80
    exact hc
  3. L81
    exact hi
  4. L82
    exact hr_witness

Library-wide reading audit

Original defined command ledger · 82 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro cb
  8. 0008intro cc
  9. 0009intro L
  10. 0010intro hp
  11. 0011intro hk
  12. 0012intro hc
  13. 0013have hcopy : FpPolyProduct(p,ab,ac,L,bb,bc,1,cb,cc,L)
  14. 0014exact hc
  15. 0015cases hcopy
  16. 0016cases hcopy_right
  17. 0017cases hcopy_right_right
  18. 0018split
  19. 0019specialize matrix_rank_bounded_prefix_value (bb)
  20. 0020specialize matrix_rank_bounded_prefix_value (bc)
  21. 0021specialize matrix_rank_bounded_prefix_value (1)
  22. 0022specialize matrix_rank_bounded_prefix_value (p)
  23. 0023specialize matrix_rank_bounded_prefix_value (0)
  24. 0024specialize matrix_rank_bounded_prefix_value (k)
  25. 0025apply matrix_rank_bounded_prefix_value
  26. 0026exact hcopy_right_left
  27. 0027exists 0
  28. 0028simp
  29. 0029exact hk
  30. 0030intro i
  31. 0031intro hi
  32. 0032have ha : ∃ a. BetaAt(ab,ac,i,a)
  33. 0033specialize beta_at_exists (ab)
  34. 0034specialize beta_at_exists (ac)
  35. 0035specialize beta_at_exists (i)
  36. 0036apply beta_at_exists
  37. 0037cases ha
  38. 0038have hr : ∃ r. BetaAt(cb,cc,i,r)
  39. 0039specialize beta_at_exists (cb)
  40. 0040specialize beta_at_exists (cc)
  41. 0041specialize beta_at_exists (i)
  42. 0042apply beta_at_exists
  43. 0043cases hr
  44. 0044exists x
  45. 0045exists x1
  46. 0046split
  47. 0047exact ha_witness
  48. 0048split
  49. 0049exact hr_witness
  50. 0050specialize prime_field_polynomial_constant_right_coefficient (p)
  51. 0051specialize prime_field_polynomial_constant_right_coefficient (ab)
  52. 0052specialize prime_field_polynomial_constant_right_coefficient (ac)
  53. 0053specialize prime_field_polynomial_constant_right_coefficient (L)
  54. 0054specialize prime_field_polynomial_constant_right_coefficient (bb)
  55. 0055specialize prime_field_polynomial_constant_right_coefficient (bc)
  56. 0056specialize prime_field_polynomial_constant_right_coefficient (k)
  57. 0057specialize prime_field_polynomial_constant_right_coefficient (i)
  58. 0058specialize prime_field_polynomial_constant_right_coefficient (x)
  59. 0059specialize prime_field_polynomial_constant_right_coefficient (x1)
  60. 0060apply prime_field_polynomial_constant_right_coefficient
  61. 0061exact hp
  62. 0062exact hcopy_left
  63. 0063exact hcopy_right_left
  64. 0064exact hk
  65. 0065exact hi
  66. 0066exact ha_witness
  67. 0067specialize prime_field_polynomial_convolution_entry (p)
  68. 0068specialize prime_field_polynomial_convolution_entry (ab)
  69. 0069specialize prime_field_polynomial_convolution_entry (ac)
  70. 0070specialize prime_field_polynomial_convolution_entry (L)
  71. 0071specialize prime_field_polynomial_convolution_entry (bb)
  72. 0072specialize prime_field_polynomial_convolution_entry (bc)
  73. 0073specialize prime_field_polynomial_convolution_entry (1)
  74. 0074specialize prime_field_polynomial_convolution_entry (cb)
  75. 0075specialize prime_field_polynomial_convolution_entry (cc)
  76. 0076specialize prime_field_polynomial_convolution_entry (L)
  77. 0077specialize prime_field_polynomial_convolution_entry (i)
  78. 0078specialize prime_field_polynomial_convolution_entry (x1)
  79. 0079apply prime_field_polynomial_convolution_entry
  80. 0080exact hc
  81. 0081exact hi
  82. 0082exact hr_witness