PG0050

prime_field_polynomial_left_constant_product_to_scale

An actual length-L product of a canonical left singleton and a length-L prefix yields the existing scalar graph, even when L=0. The scalar bound follows from the singleton rather than from vacuous output entries.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ p. ∀ k. ∀ kb. ∀ kc. ∀ ab. ∀ ac. ∀ hb. ∀ hc. ∀ L. BetaAt(kb,kc,0,k) → FpPolyProduct(p,kb,kc,1,ab,ac,L,hb,hc,L) → FpPolyScale(p,k,ab,ac,hb,hc,L)

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

Definition DAG

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

Actual proof prerequisites

matrix_rank_bounded_prefix_value · checked external prerequisitezero_add · checked external prerequisitebeta_at_exists · checked external prerequisiteprime_field_convolution_coefficient_left_constant
Original expanded first-order statement 
forall p k kb kc ab ac hb hc L. (((exists ff_h_pfp_left_constant_product_K. ff_h_pfp_left_constant_product_K + S (k) = S ((S (0)) * kc)) /\ exists ff_q_pfp_left_constant_product_K. kb = ff_q_pfp_left_constant_product_K * S ((S (0)) * kc) + (k))) -> (((forall fom_index_pfp_left_constant_product_sourceleft. (exists fom_gap_pfp_left_constant_product_sourceleft_index_bound. fom_gap_pfp_left_constant_product_sourceleft_index_bound + S (fom_index_pfp_left_constant_product_sourceleft) = 1) -> exists fom_value_pfp_left_constant_product_sourceleft. ((((exists fom_beta_height_pfp_left_constant_product_sourceleft_entry. fom_beta_height_pfp_left_constant_product_sourceleft_entry + S (fom_value_pfp_left_constant_product_sourceleft) = S ((S (fom_index_pfp_left_constant_product_sourceleft)) * kc)) /\ exists fom_beta_quotient_pfp_left_constant_product_sourceleft_entry. kb = fom_beta_quotient_pfp_left_constant_product_sourceleft_entry * S ((S (fom_index_pfp_left_constant_product_sourceleft)) * kc) + (fom_value_pfp_left_constant_product_sourceleft))) /\ (exists fom_gap_pfp_left_constant_product_sourceleft_value_bound. fom_gap_pfp_left_constant_product_sourceleft_value_bound + S (fom_value_pfp_left_constant_product_sourceleft) = p))) /\ (((forall fom_index_pfp_left_constant_product_sourceright. (exists fom_gap_pfp_left_constant_product_sourceright_index_bound. fom_gap_pfp_left_constant_product_sourceright_index_bound + S (fom_index_pfp_left_constant_product_sourceright) = L) -> exists fom_value_pfp_left_constant_product_sourceright. ((((exists fom_beta_height_pfp_left_constant_product_sourceright_entry. fom_beta_height_pfp_left_constant_product_sourceright_entry + S (fom_value_pfp_left_constant_product_sourceright) = S ((S (fom_index_pfp_left_constant_product_sourceright)) * ac)) /\ exists fom_beta_quotient_pfp_left_constant_product_sourceright_entry. ab = fom_beta_quotient_pfp_left_constant_product_sourceright_entry * S ((S (fom_index_pfp_left_constant_product_sourceright)) * ac) + (fom_value_pfp_left_constant_product_sourceright))) /\ (exists fom_gap_pfp_left_constant_product_sourceright_value_bound. fom_gap_pfp_left_constant_product_sourceright_value_bound + S (fom_value_pfp_left_constant_product_sourceright) = p))) /\ (((((((1)=0 \/ (L)=0) /\ (((L)=0)))) \/ (((~((1)=0)) /\ (((~((L)=0)) /\ (((1)+(L)=S (L)))))))) /\ ((forall pfc_index_left_constant_product_sourcecoefficients. (exists pfa_gap_left_constant_product_sourcecoefficientsbound. pfa_gap_left_constant_product_sourcecoefficientsbound + S (pfc_index_left_constant_product_sourcecoefficients) = (L)) -> exists pfc_value_left_constant_product_sourcecoefficients. ((((exists ff_h_pfp_left_constant_product_sourcecoefficientsentry. ff_h_pfp_left_constant_product_sourcecoefficientsentry + S (pfc_value_left_constant_product_sourcecoefficients) = S ((S (pfc_index_left_constant_product_sourcecoefficients)) * hc)) /\ exists ff_q_pfp_left_constant_product_sourcecoefficientsentry. hb = ff_q_pfp_left_constant_product_sourcecoefficientsentry * S ((S (pfc_index_left_constant_product_sourcecoefficients)) * hc) + (pfc_value_left_constant_product_sourcecoefficients))) /\ ((exists pfc_terms_code_left_constant_product_sourcecoefficientscoefficient pfc_terms_scale_left_constant_product_sourcecoefficientscoefficient pfc_natural_sum_left_constant_product_sourcecoefficientscoefficient. ((forall pfc_index_left_constant_product_sourcecoefficientscoefficientdiagonal. (exists pfa_gap_left_constant_product_sourcecoefficientscoefficientdiagonalbound. pfa_gap_left_constant_product_sourcecoefficientscoefficientdiagonalbound + S (pfc_index_left_constant_product_sourcecoefficientscoefficientdiagonal) = (S (pfc_index_left_constant_product_sourcecoefficients))) -> exists pfc_value_left_constant_product_sourcecoefficientscoefficientdiagonal. ((((exists ff_h_pfp_left_constant_product_sourcecoefficientscoefficientdiagonalentry. ff_h_pfp_left_constant_product_sourcecoefficientscoefficientdiagonalentry + S (pfc_value_left_constant_product_sourcecoefficientscoefficientdiagonal) = S ((S (pfc_index_left_constant_product_sourcecoefficientscoefficientdiagonal)) * pfc_terms_scale_left_constant_product_sourcecoefficientscoefficient)) /\ exists ff_q_pfp_left_constant_product_sourcecoefficientscoefficientdiagonalentry. pfc_terms_code_left_constant_product_sourcecoefficientscoefficient = ff_q_pfp_left_constant_product_sourcecoefficientscoefficientdiagonalentry * S ((S (pfc_index_left_constant_product_sourcecoefficientscoefficientdiagonal)) * pfc_terms_scale_left_constant_product_sourcecoefficientscoefficient) + (pfc_value_left_constant_product_sourcecoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_left_constant_product_sourcecoefficientscoefficientdiagonalterm pfc_left_left_constant_product_sourcecoefficientscoefficientdiagonalterm pfc_right_left_constant_product_sourcecoefficientscoefficientdiagonalterm. (((pfc_index_left_constant_product_sourcecoefficientscoefficientdiagonal)+pfc_complement_left_constant_product_sourcecoefficientscoefficientdiagonalterm=(pfc_index_left_constant_product_sourcecoefficients)) /\ ((((((exists pfa_gap_left_constant_product_sourcecoefficientscoefficientdiagonaltermleftinside. pfa_gap_left_constant_product_sourcecoefficientscoefficientdiagonaltermleftinside + S (pfc_index_left_constant_product_sourcecoefficientscoefficientdiagonal) = (1)) /\ ((((exists ff_h_pfp_left_constant_product_sourcecoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_left_constant_product_sourcecoefficientscoefficientdiagonaltermleftentry + S (pfc_left_left_constant_product_sourcecoefficientscoefficientdiagonalterm) = S ((S (pfc_index_left_constant_product_sourcecoefficientscoefficientdiagonal)) * kc)) /\ exists ff_q_pfp_left_constant_product_sourcecoefficientscoefficientdiagonaltermleftentry. kb = ff_q_pfp_left_constant_product_sourcecoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_left_constant_product_sourcecoefficientscoefficientdiagonal)) * kc) + (pfc_left_left_constant_product_sourcecoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_left_constant_product_sourcecoefficientscoefficientdiagonaltermleftoutside. pfc_gap_left_constant_product_sourcecoefficientscoefficientdiagonaltermleftoutside+(1)=(pfc_index_left_constant_product_sourcecoefficientscoefficientdiagonal)) /\ (((pfc_left_left_constant_product_sourcecoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_left_constant_product_sourcecoefficientscoefficientdiagonaltermrightinside. pfa_gap_left_constant_product_sourcecoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_left_constant_product_sourcecoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_left_constant_product_sourcecoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_left_constant_product_sourcecoefficientscoefficientdiagonaltermrightentry + S (pfc_right_left_constant_product_sourcecoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_left_constant_product_sourcecoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_left_constant_product_sourcecoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_left_constant_product_sourcecoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_left_constant_product_sourcecoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_left_constant_product_sourcecoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_left_constant_product_sourcecoefficientscoefficientdiagonaltermrightoutside. pfc_gap_left_constant_product_sourcecoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_left_constant_product_sourcecoefficientscoefficientdiagonalterm)) /\ (((pfc_right_left_constant_product_sourcecoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_left_constant_product_sourcecoefficientscoefficientdiagonal)=pfc_left_left_constant_product_sourcecoefficientscoefficientdiagonalterm*pfc_right_left_constant_product_sourcecoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_left_constant_product_sourcecoefficientscoefficientsum fs_v_pfc_left_constant_product_sourcecoefficientscoefficientsum. ((((exists fs_h_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_start. fs_h_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_left_constant_product_sourcecoefficientscoefficientsum)) /\ exists fs_q_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_start. fs_u_pfc_left_constant_product_sourcecoefficientscoefficientsum = fs_q_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_left_constant_product_sourcecoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_terminal. fs_h_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_left_constant_product_sourcecoefficientscoefficient) = S ((S (S (pfc_index_left_constant_product_sourcecoefficients))) * fs_v_pfc_left_constant_product_sourcecoefficientscoefficientsum)) /\ exists fs_q_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_terminal. fs_u_pfc_left_constant_product_sourcecoefficientscoefficientsum = fs_q_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_left_constant_product_sourcecoefficients))) * fs_v_pfc_left_constant_product_sourcecoefficientscoefficientsum) + (pfc_natural_sum_left_constant_product_sourcecoefficientscoefficient))) /\ forall fs_i_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps = S (pfc_index_left_constant_product_sourcecoefficients)) -> exists fs_a_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps fs_r_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps fs_s_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps_summand. fs_h_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps)) * pfc_terms_scale_left_constant_product_sourcecoefficientscoefficient)) /\ exists fs_q_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps_summand. pfc_terms_code_left_constant_product_sourcecoefficientscoefficient = fs_q_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps)) * pfc_terms_scale_left_constant_product_sourcecoefficientscoefficient) + (fs_a_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps_partial. fs_h_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_constant_product_sourcecoefficientscoefficientsum)) /\ exists fs_q_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps_partial. fs_u_pfc_left_constant_product_sourcecoefficientscoefficientsum = fs_q_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_constant_product_sourcecoefficientscoefficientsum) + (fs_r_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps_successor. fs_h_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_constant_product_sourcecoefficientscoefficientsum)) /\ exists fs_q_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps_successor. fs_u_pfc_left_constant_product_sourcecoefficientscoefficientsum = fs_q_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_constant_product_sourcecoefficientscoefficientsum) + (fs_s_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps = fs_r_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps + fs_a_pfc_left_constant_product_sourcecoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_left_constant_product_sourcecoefficientscoefficientresiduebound. pfa_gap_left_constant_product_sourcecoefficientscoefficientresiduebound + S (pfc_value_left_constant_product_sourcecoefficients) = (p)) /\ ((exists pfa_offset_left_left_constant_product_sourcecoefficientscoefficientresiduecongruence pfa_offset_right_left_constant_product_sourcecoefficientscoefficientresiduecongruence. (pfc_natural_sum_left_constant_product_sourcecoefficientscoefficient) + (p) * pfa_offset_left_left_constant_product_sourcecoefficientscoefficientresiduecongruence = (pfc_value_left_constant_product_sourcecoefficients) + (p) * pfa_offset_right_left_constant_product_sourcecoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((exists pfa_gap_left_constant_product_scalescalar. pfa_gap_left_constant_product_scalescalar + S (k) = (p)) /\ ((forall pfp_index_left_constant_product_scale. (exists pfa_gap_left_constant_product_scaleindex. pfa_gap_left_constant_product_scaleindex + S (pfp_index_left_constant_product_scale) = (L)) -> exists pfp_source_left_constant_product_scale pfp_value_left_constant_product_scale. ((((exists ff_h_pfp_left_constant_product_scalesource. ff_h_pfp_left_constant_product_scalesource + S (pfp_source_left_constant_product_scale) = S ((S (pfp_index_left_constant_product_scale)) * ac)) /\ exists ff_q_pfp_left_constant_product_scalesource. ab = ff_q_pfp_left_constant_product_scalesource * S ((S (pfp_index_left_constant_product_scale)) * ac) + (pfp_source_left_constant_product_scale))) /\ (((((exists ff_h_pfp_left_constant_product_scaletarget. ff_h_pfp_left_constant_product_scaletarget + S (pfp_value_left_constant_product_scale) = S ((S (pfp_index_left_constant_product_scale)) * hc)) /\ exists ff_q_pfp_left_constant_product_scaletarget. hb = ff_q_pfp_left_constant_product_scaletarget * S ((S (pfp_index_left_constant_product_scale)) * hc) + (pfp_value_left_constant_product_scale))) /\ ((((exists pfa_gap_left_constant_product_scaleoperationleft. pfa_gap_left_constant_product_scaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_left_constant_product_scaleoperationright. pfa_gap_left_constant_product_scaleoperationright + S (pfp_source_left_constant_product_scale) = (p)) /\ ((((exists pfa_gap_left_constant_product_scaleoperationresultbound. pfa_gap_left_constant_product_scaleoperationresultbound + S (pfp_value_left_constant_product_scale) = (p)) /\ ((exists pfa_offset_left_left_constant_product_scaleoperationresultcongruence pfa_offset_right_left_constant_product_scaleoperationresultcongruence. ((k) * (pfp_source_left_constant_product_scale)) + (p) * pfa_offset_left_left_constant_product_scaleoperationresultcongruence = (pfp_value_left_constant_product_scale) + (p) * pfa_offset_right_left_constant_product_scaleoperationresultcongruence)))))))))))))))))

Complete tactic proof in conservative notation

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

74 script commands · 20 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 convolution coefficient left constant
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 kb
  4. L4
    intro kc
  5. L5
    intro ab
  6. L6
    intro ac
  7. L7
    intro hb
  8. L8
    intro hc
  9. L9
    intro L
  10. L10
    intro hk
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hproduct
03Separate the logical casesL12–14

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

  1. L12
    cases hproduct
  2. L13
    cases hproduct_right
  3. L14
    cases hproduct_right_right
04Establish hkbL15–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix rank bounded prefix value.

  1. L15
  2. L16
    specialize matrix_rank_bounded_prefix_value (kb)
  3. L17
    specialize matrix_rank_bounded_prefix_value (kc)
  4. L18
    specialize matrix_rank_bounded_prefix_value (1)
  5. L19
    specialize matrix_rank_bounded_prefix_value (p)
  6. L20
    specialize matrix_rank_bounded_prefix_value (0)
  7. L21
    specialize matrix_rank_bounded_prefix_value (k)
  8. L22
    apply matrix_rank_bounded_prefix_value
  9. L23
    exact hproduct_left
05Construct an explicit witnessL24–24

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

  1. L24
    exists 0
06Use earlier factsL25–26

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

  1. L25
    apply zero_add
  2. L26
    exact hk
07Separate the logical casesL27–27

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

  1. L27
    split
08Use earlier factsL28–28

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

  1. L28
    exact hkb
09Fix variables and assumptionsL29–30

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

  1. L29
    intro i
  2. L30
    intro hi
10Establish haL31–35

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

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

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

  1. L36
    cases ha
12Establish hrL37–40

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

  1. L37
    have hr : ∃ r. BetaAt(hb,hc,i,r) ∧ FpConvolutionCoefficient(p,kb,kc,1,ab,ac,L,i,r)Definitions: BetaAt(hb,hc,i,r)FpConvolutionCoefficient(p,kb,kc,1,ab,ac,L,i,r)Original native command in the exact edition
  2. L38
    specialize hproduct_right_right_right (i)
  3. L39
    apply hproduct_right_right_right
  4. L40
    exact hi
13Separate the logical casesL41–42

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

  1. L41
    cases hr
  2. L42
    cases hr_witness
14Construct an explicit witnessL43–44

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

  1. L43
    exists x
  2. L44
    exists x1
15Separate the logical casesL45–45

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

  1. L45
    split
16Use earlier factsL46–46

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

  1. L46
    exact ha_witness
17Separate the logical casesL47–47

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

  1. L47
    split
18Use earlier factsL48–57

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

  1. L48
    exact hr_witness_left
  2. L49
    specialize prime_field_convolution_coefficient_left_constant (p)
  3. L50
    specialize prime_field_convolution_coefficient_left_constant (k)
  4. L51
    specialize prime_field_convolution_coefficient_left_constant (kb)
  5. L52
    specialize prime_field_convolution_coefficient_left_constant (kc)
  6. L53
    specialize prime_field_convolution_coefficient_left_constant (ab)
  7. L54
    specialize prime_field_convolution_coefficient_left_constant (ac)
  8. L55
    specialize prime_field_convolution_coefficient_left_constant (L)
  9. L56
    specialize prime_field_convolution_coefficient_left_constant (i)
  10. L57
    specialize prime_field_convolution_coefficient_left_constant (x)
19Use earlier factsL58–67

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

  1. L58
    specialize prime_field_convolution_coefficient_left_constant (x1)
  2. L59
    apply prime_field_convolution_coefficient_left_constant
  3. L60
    exact hk
  4. L61
    exact hi
  5. L62
    exact ha_witness
  6. L63
    exact hkb
  7. L64
    specialize matrix_rank_bounded_prefix_value (ab)
  8. L65
    specialize matrix_rank_bounded_prefix_value (ac)
  9. L66
    specialize matrix_rank_bounded_prefix_value (L)
  10. L67
    specialize matrix_rank_bounded_prefix_value (p)
20Use earlier factsL68–74

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

  1. L68
    specialize matrix_rank_bounded_prefix_value (i)
  2. L69
    specialize matrix_rank_bounded_prefix_value (x)
  3. L70
    apply matrix_rank_bounded_prefix_value
  4. L71
    exact hproduct_right_left
  5. L72
    exact hi
  6. L73
    exact ha_witness
  7. L74
    exact hr_witness_right

Library-wide reading audit

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