PG0051

prime_field_polynomial_scale_to_left_constant_product

Recover the genuine LEFT-constant convolution on the supplied scalar-output codes. Every needed antidiagonal sum is actually constructed and its residue identified; the empty proper-length branch is separate, including scalar zero and characteristic two.

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. Prime(p) → BetaPrefixInto(kb,kc,1,p) → BetaAt(kb,kc,0,k) → FpPolyScale(p,k,ab,ac,hb,hc,L) → FpPolyProduct(p,kb,kc,1,ab,ac,L,hb,hc,L)

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

Definition DAG

FpMul(p,a,b,c) · 2BetaPrefixInto(b,c,l,B) · 3FpPolyScale(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) · 1Prime(p) · 1BetaAt(b,c,i,x) · 3

Actual proof prerequisites

prime_field_polynomial_scale_bounded · checked external prerequisiteeq_decidable · checked external prerequisitesucc_ne_zero · checked external prerequisiteadd_succ_left · checked external prerequisitezero_add · checked external prerequisiteprime_field_convolution_coefficient_exists · checked external prerequisiteprime_nonzero · checked external prerequisiteprime_field_multiply_functional · checked external prerequisiteprime_field_convolution_coefficient_left_constant
Original expanded first-order statement 
forall p k kb kc ab ac hb hc L. (~((p) = 1) /\ forall pfa_factor_left_left_constant_recover_prime pfa_factor_right_left_constant_recover_prime. (p) = pfa_factor_left_left_constant_recover_prime * pfa_factor_right_left_constant_recover_prime -> pfa_factor_left_left_constant_recover_prime = 1 \/ pfa_factor_right_left_constant_recover_prime = 1) -> (forall fom_index_pfp_left_constant_recover_K. (exists fom_gap_pfp_left_constant_recover_K_index_bound. fom_gap_pfp_left_constant_recover_K_index_bound + S (fom_index_pfp_left_constant_recover_K) = 1) -> exists fom_value_pfp_left_constant_recover_K. ((((exists fom_beta_height_pfp_left_constant_recover_K_entry. fom_beta_height_pfp_left_constant_recover_K_entry + S (fom_value_pfp_left_constant_recover_K) = S ((S (fom_index_pfp_left_constant_recover_K)) * kc)) /\ exists fom_beta_quotient_pfp_left_constant_recover_K_entry. kb = fom_beta_quotient_pfp_left_constant_recover_K_entry * S ((S (fom_index_pfp_left_constant_recover_K)) * kc) + (fom_value_pfp_left_constant_recover_K))) /\ (exists fom_gap_pfp_left_constant_recover_K_value_bound. fom_gap_pfp_left_constant_recover_K_value_bound + S (fom_value_pfp_left_constant_recover_K) = p))) -> (((exists ff_h_pfp_left_constant_recover_value. ff_h_pfp_left_constant_recover_value + S (k) = S ((S (0)) * kc)) /\ exists ff_q_pfp_left_constant_recover_value. kb = ff_q_pfp_left_constant_recover_value * S ((S (0)) * kc) + (k))) -> (((exists pfa_gap_left_constant_recover_scalescalar. pfa_gap_left_constant_recover_scalescalar + S (k) = (p)) /\ ((forall pfp_index_left_constant_recover_scale. (exists pfa_gap_left_constant_recover_scaleindex. pfa_gap_left_constant_recover_scaleindex + S (pfp_index_left_constant_recover_scale) = (L)) -> exists pfp_source_left_constant_recover_scale pfp_value_left_constant_recover_scale. ((((exists ff_h_pfp_left_constant_recover_scalesource. ff_h_pfp_left_constant_recover_scalesource + S (pfp_source_left_constant_recover_scale) = S ((S (pfp_index_left_constant_recover_scale)) * ac)) /\ exists ff_q_pfp_left_constant_recover_scalesource. ab = ff_q_pfp_left_constant_recover_scalesource * S ((S (pfp_index_left_constant_recover_scale)) * ac) + (pfp_source_left_constant_recover_scale))) /\ (((((exists ff_h_pfp_left_constant_recover_scaletarget. ff_h_pfp_left_constant_recover_scaletarget + S (pfp_value_left_constant_recover_scale) = S ((S (pfp_index_left_constant_recover_scale)) * hc)) /\ exists ff_q_pfp_left_constant_recover_scaletarget. hb = ff_q_pfp_left_constant_recover_scaletarget * S ((S (pfp_index_left_constant_recover_scale)) * hc) + (pfp_value_left_constant_recover_scale))) /\ ((((exists pfa_gap_left_constant_recover_scaleoperationleft. pfa_gap_left_constant_recover_scaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_left_constant_recover_scaleoperationright. pfa_gap_left_constant_recover_scaleoperationright + S (pfp_source_left_constant_recover_scale) = (p)) /\ ((((exists pfa_gap_left_constant_recover_scaleoperationresultbound. pfa_gap_left_constant_recover_scaleoperationresultbound + S (pfp_value_left_constant_recover_scale) = (p)) /\ ((exists pfa_offset_left_left_constant_recover_scaleoperationresultcongruence pfa_offset_right_left_constant_recover_scaleoperationresultcongruence. ((k) * (pfp_source_left_constant_recover_scale)) + (p) * pfa_offset_left_left_constant_recover_scaleoperationresultcongruence = (pfp_value_left_constant_recover_scale) + (p) * pfa_offset_right_left_constant_recover_scaleoperationresultcongruence))))))))))))))))) -> (((forall fom_index_pfp_left_constant_recover_productleft. (exists fom_gap_pfp_left_constant_recover_productleft_index_bound. fom_gap_pfp_left_constant_recover_productleft_index_bound + S (fom_index_pfp_left_constant_recover_productleft) = 1) -> exists fom_value_pfp_left_constant_recover_productleft. ((((exists fom_beta_height_pfp_left_constant_recover_productleft_entry. fom_beta_height_pfp_left_constant_recover_productleft_entry + S (fom_value_pfp_left_constant_recover_productleft) = S ((S (fom_index_pfp_left_constant_recover_productleft)) * kc)) /\ exists fom_beta_quotient_pfp_left_constant_recover_productleft_entry. kb = fom_beta_quotient_pfp_left_constant_recover_productleft_entry * S ((S (fom_index_pfp_left_constant_recover_productleft)) * kc) + (fom_value_pfp_left_constant_recover_productleft))) /\ (exists fom_gap_pfp_left_constant_recover_productleft_value_bound. fom_gap_pfp_left_constant_recover_productleft_value_bound + S (fom_value_pfp_left_constant_recover_productleft) = p))) /\ (((forall fom_index_pfp_left_constant_recover_productright. (exists fom_gap_pfp_left_constant_recover_productright_index_bound. fom_gap_pfp_left_constant_recover_productright_index_bound + S (fom_index_pfp_left_constant_recover_productright) = L) -> exists fom_value_pfp_left_constant_recover_productright. ((((exists fom_beta_height_pfp_left_constant_recover_productright_entry. fom_beta_height_pfp_left_constant_recover_productright_entry + S (fom_value_pfp_left_constant_recover_productright) = S ((S (fom_index_pfp_left_constant_recover_productright)) * ac)) /\ exists fom_beta_quotient_pfp_left_constant_recover_productright_entry. ab = fom_beta_quotient_pfp_left_constant_recover_productright_entry * S ((S (fom_index_pfp_left_constant_recover_productright)) * ac) + (fom_value_pfp_left_constant_recover_productright))) /\ (exists fom_gap_pfp_left_constant_recover_productright_value_bound. fom_gap_pfp_left_constant_recover_productright_value_bound + S (fom_value_pfp_left_constant_recover_productright) = p))) /\ (((((((1)=0 \/ (L)=0) /\ (((L)=0)))) \/ (((~((1)=0)) /\ (((~((L)=0)) /\ (((1)+(L)=S (L)))))))) /\ ((forall pfc_index_left_constant_recover_productcoefficients. (exists pfa_gap_left_constant_recover_productcoefficientsbound. pfa_gap_left_constant_recover_productcoefficientsbound + S (pfc_index_left_constant_recover_productcoefficients) = (L)) -> exists pfc_value_left_constant_recover_productcoefficients. ((((exists ff_h_pfp_left_constant_recover_productcoefficientsentry. ff_h_pfp_left_constant_recover_productcoefficientsentry + S (pfc_value_left_constant_recover_productcoefficients) = S ((S (pfc_index_left_constant_recover_productcoefficients)) * hc)) /\ exists ff_q_pfp_left_constant_recover_productcoefficientsentry. hb = ff_q_pfp_left_constant_recover_productcoefficientsentry * S ((S (pfc_index_left_constant_recover_productcoefficients)) * hc) + (pfc_value_left_constant_recover_productcoefficients))) /\ ((exists pfc_terms_code_left_constant_recover_productcoefficientscoefficient pfc_terms_scale_left_constant_recover_productcoefficientscoefficient pfc_natural_sum_left_constant_recover_productcoefficientscoefficient. ((forall pfc_index_left_constant_recover_productcoefficientscoefficientdiagonal. (exists pfa_gap_left_constant_recover_productcoefficientscoefficientdiagonalbound. pfa_gap_left_constant_recover_productcoefficientscoefficientdiagonalbound + S (pfc_index_left_constant_recover_productcoefficientscoefficientdiagonal) = (S (pfc_index_left_constant_recover_productcoefficients))) -> exists pfc_value_left_constant_recover_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_left_constant_recover_productcoefficientscoefficientdiagonalentry. ff_h_pfp_left_constant_recover_productcoefficientscoefficientdiagonalentry + S (pfc_value_left_constant_recover_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_left_constant_recover_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_left_constant_recover_productcoefficientscoefficient)) /\ exists ff_q_pfp_left_constant_recover_productcoefficientscoefficientdiagonalentry. pfc_terms_code_left_constant_recover_productcoefficientscoefficient = ff_q_pfp_left_constant_recover_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_left_constant_recover_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_left_constant_recover_productcoefficientscoefficient) + (pfc_value_left_constant_recover_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_left_constant_recover_productcoefficientscoefficientdiagonalterm pfc_left_left_constant_recover_productcoefficientscoefficientdiagonalterm pfc_right_left_constant_recover_productcoefficientscoefficientdiagonalterm. (((pfc_index_left_constant_recover_productcoefficientscoefficientdiagonal)+pfc_complement_left_constant_recover_productcoefficientscoefficientdiagonalterm=(pfc_index_left_constant_recover_productcoefficients)) /\ ((((((exists pfa_gap_left_constant_recover_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_left_constant_recover_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_left_constant_recover_productcoefficientscoefficientdiagonal) = (1)) /\ ((((exists ff_h_pfp_left_constant_recover_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_left_constant_recover_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_left_constant_recover_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_left_constant_recover_productcoefficientscoefficientdiagonal)) * kc)) /\ exists ff_q_pfp_left_constant_recover_productcoefficientscoefficientdiagonaltermleftentry. kb = ff_q_pfp_left_constant_recover_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_left_constant_recover_productcoefficientscoefficientdiagonal)) * kc) + (pfc_left_left_constant_recover_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_left_constant_recover_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_left_constant_recover_productcoefficientscoefficientdiagonaltermleftoutside+(1)=(pfc_index_left_constant_recover_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_left_constant_recover_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_left_constant_recover_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_left_constant_recover_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_left_constant_recover_productcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_left_constant_recover_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_left_constant_recover_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_left_constant_recover_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_left_constant_recover_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_left_constant_recover_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_left_constant_recover_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_left_constant_recover_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_left_constant_recover_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_left_constant_recover_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_left_constant_recover_productcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_left_constant_recover_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_left_constant_recover_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_left_constant_recover_productcoefficientscoefficientdiagonal)=pfc_left_left_constant_recover_productcoefficientscoefficientdiagonalterm*pfc_right_left_constant_recover_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_left_constant_recover_productcoefficientscoefficientsum fs_v_pfc_left_constant_recover_productcoefficientscoefficientsum. ((((exists fs_h_pfc_left_constant_recover_productcoefficientscoefficientsum_body_start. fs_h_pfc_left_constant_recover_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_left_constant_recover_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_constant_recover_productcoefficientscoefficientsum_body_start. fs_u_pfc_left_constant_recover_productcoefficientscoefficientsum = fs_q_pfc_left_constant_recover_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_left_constant_recover_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_left_constant_recover_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_left_constant_recover_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_left_constant_recover_productcoefficientscoefficient) = S ((S (S (pfc_index_left_constant_recover_productcoefficients))) * fs_v_pfc_left_constant_recover_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_constant_recover_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_left_constant_recover_productcoefficientscoefficientsum = fs_q_pfc_left_constant_recover_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_left_constant_recover_productcoefficients))) * fs_v_pfc_left_constant_recover_productcoefficientscoefficientsum) + (pfc_natural_sum_left_constant_recover_productcoefficientscoefficient))) /\ forall fs_i_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps = S (pfc_index_left_constant_recover_productcoefficients)) -> exists fs_a_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps fs_r_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps fs_s_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_left_constant_recover_productcoefficientscoefficient)) /\ exists fs_q_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_left_constant_recover_productcoefficientscoefficient = fs_q_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_left_constant_recover_productcoefficientscoefficient) + (fs_a_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_constant_recover_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_left_constant_recover_productcoefficientscoefficientsum = fs_q_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_constant_recover_productcoefficientscoefficientsum) + (fs_r_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_constant_recover_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_left_constant_recover_productcoefficientscoefficientsum = fs_q_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_constant_recover_productcoefficientscoefficientsum) + (fs_s_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps = fs_r_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps + fs_a_pfc_left_constant_recover_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_left_constant_recover_productcoefficientscoefficientresiduebound. pfa_gap_left_constant_recover_productcoefficientscoefficientresiduebound + S (pfc_value_left_constant_recover_productcoefficients) = (p)) /\ ((exists pfa_offset_left_left_constant_recover_productcoefficientscoefficientresiduecongruence pfa_offset_right_left_constant_recover_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_left_constant_recover_productcoefficientscoefficient) + (p) * pfa_offset_left_left_constant_recover_productcoefficientscoefficientresiduecongruence = (pfc_value_left_constant_recover_productcoefficients) + (p) * pfa_offset_right_left_constant_recover_productcoefficientscoefficientresiduecongruence)))))))))))))))))))

Complete tactic proof in conservative notation

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

110 script commands · 36 reading checkpoints · 6 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 hp
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hK
  2. L12
    intro hk
  3. L13
    intro hs
03Establish hboundsL14–23

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

  1. L14
    have hbounds : BetaPrefixInto(ab,ac,L,p) ∧ BetaPrefixInto(hb,hc,L,p)Definitions: BetaPrefixInto(ab,ac,L,p)BetaPrefixInto(hb,hc,L,p)Original native command in the exact edition
  2. L15
    specialize prime_field_polynomial_scale_bounded (p)
  3. L16
    specialize prime_field_polynomial_scale_bounded (k)
  4. L17
    specialize prime_field_polynomial_scale_bounded (ab)
  5. L18
    specialize prime_field_polynomial_scale_bounded (ac)
  6. L19
    specialize prime_field_polynomial_scale_bounded (hb)
  7. L20
    specialize prime_field_polynomial_scale_bounded (hc)
  8. L21
    specialize prime_field_polynomial_scale_bounded (L)
  9. L22
    apply prime_field_polynomial_scale_bounded
  10. L23
    exact hs
04Separate the logical casesL24–25

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

  1. L24
    cases hbounds
  2. L25
    split
05Use earlier factsL26–26

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

  1. L26
    exact hK
06Separate the logical casesL27–27

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

  1. L27
    split
07Use earlier factsL28–28

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

  1. L28
    exact hbounds_left
08Separate the logical casesL29–29

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

  1. L29
    split
09Establish hzL30–33

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

  1. L30
    have hz : L=0 \/ ~(L=0)
  2. L31
    specialize eq_decidable (L)
  3. L32
    specialize eq_decidable (0)
  4. L33
    apply eq_decidable
10Separate the logical casesL34–37

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

  1. L34
    cases hz
  2. L35
    left
  3. L36
    split
  4. L37
    right
11Use earlier factsL38–39

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

  1. L38
    exact hz_left
  2. L39
    exact hz_left
12Separate the logical casesL40–41

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

  1. L40
    right
  2. L41
    split
13Fix variables and assumptionsL42–42

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

  1. L42
    intro hbad
14Use earlier factsL43–45

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

  1. L43
    specialize succ_ne_zero (0)
  2. L44
    apply succ_ne_zero
  3. L45
    exact hbad
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 hz_right
17Calculate and transport equalitiesL48–48

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

  1. L48
    simp [add_succ_left,zero_add]
18Fix variables and assumptionsL49–50

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

  1. L49
    intro i
  2. L50
    intro hi
19Establish hvL51–51

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

  1. L51
    have hv : ∃ a. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(hb,hc,i,r) ∧ FpMul(p,k,a,r))Definitions: BetaAt(ab,ac,i,a)BetaAt(hb,hc,i,r)FpMul(p,k,a,r)Original native command in the exact edition
20Separate the logical casesL52–52

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

  1. L52
    cases hs
21Use earlier factsL53–55

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

  1. L53
    specialize hs_right (i)
  2. L54
    apply hs_right
  3. L55
    exact hi
22Separate the logical casesL56–59

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

  1. L56
    cases hv
  2. L57
    cases hv_witness
  3. L58
    cases hv_witness_witness
  4. L59
    cases hv_witness_witness_right
23Establish hmL60–61

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

  1. L60
  2. L61
    exact hv_witness_witness_right_right
24Separate the logical casesL62–63

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

  1. L62
    cases hm
  2. L63
    cases hm_right
25Establish hcoefficientL64–73

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

  1. L64
    have hcoefficient : ∃ r. FpConvolutionCoefficient(p,kb,kc,1,ab,ac,L,i,r)Definitions: FpConvolutionCoefficient(p,kb,kc,1,ab,ac,L,i,r)Original native command in the exact edition
  2. L65
    specialize prime_field_convolution_coefficient_exists (p)
  3. L66
    specialize prime_field_convolution_coefficient_exists (kb)
  4. L67
    specialize prime_field_convolution_coefficient_exists (kc)
  5. L68
    specialize prime_field_convolution_coefficient_exists (1)
  6. L69
    specialize prime_field_convolution_coefficient_exists (ab)
  7. L70
    specialize prime_field_convolution_coefficient_exists (ac)
  8. L71
    specialize prime_field_convolution_coefficient_exists (L)
  9. L72
    specialize prime_field_convolution_coefficient_exists (i)
  10. L73
    apply prime_field_convolution_coefficient_exists
26Fix variables and assumptionsL74–74

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

  1. L74
    intro hpzero
27Use earlier factsL75–78

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

  1. L75
    specialize prime_nonzero (p)
  2. L76
    apply prime_nonzero
  3. L77
    exact hp
  4. L78
    exact hpzero
28Separate the logical casesL79–79

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

  1. L79
    cases hcoefficient
29Establish heqL80–89

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

  1. L80
    have heq : x2=x1
  2. L81
    specialize prime_field_multiply_functional (p)
  3. L82
    specialize prime_field_multiply_functional (k)
  4. L83
    specialize prime_field_multiply_functional (x)
  5. L84
    specialize prime_field_multiply_functional (x2)
  6. L85
    specialize prime_field_multiply_functional (x1)
  7. L86
    apply prime_field_multiply_functional
  8. L87
    specialize prime_field_convolution_coefficient_left_constant (p)
  9. L88
    specialize prime_field_convolution_coefficient_left_constant (k)
  10. L89
    specialize prime_field_convolution_coefficient_left_constant (kb)
30Use earlier factsL90–99

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

  1. L90
    specialize prime_field_convolution_coefficient_left_constant (kc)
  2. L91
    specialize prime_field_convolution_coefficient_left_constant (ab)
  3. L92
    specialize prime_field_convolution_coefficient_left_constant (ac)
  4. L93
    specialize prime_field_convolution_coefficient_left_constant (L)
  5. L94
    specialize prime_field_convolution_coefficient_left_constant (i)
  6. L95
    specialize prime_field_convolution_coefficient_left_constant (x)
  7. L96
    specialize prime_field_convolution_coefficient_left_constant (x2)
  8. L97
    apply prime_field_convolution_coefficient_left_constant
  9. L98
    exact hk
  10. L99
    exact hi
31Use earlier factsL100–104

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

  1. L100
    exact hv_witness_witness_left
  2. L101
    exact hm_left
  3. L102
    exact hm_right_left
  4. L103
    exact hcoefficient_witness
  5. L104
    exact hv_witness_witness_right_right
32Construct an explicit witnessL105–105

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

  1. L105
    exists x1
33Separate the logical casesL106–106

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

  1. L106
    split
34Use earlier factsL107–107

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

  1. L107
    exact hv_witness_witness_right_left
35Calculate and transport equalitiesL108–109

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

  1. L108
    rewrite heq at hcoefficient_witness
  2. L109
    rewrite heq at hcoefficient_witness
36Use earlier factsL110–110

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

  1. L110
    exact hcoefficient_witness

Library-wide reading audit

Original defined command ledger · 110 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 hp
  11. 0011intro hK
  12. 0012intro hk
  13. 0013intro hs
  14. 0014have hbounds : BetaPrefixInto(ab,ac,L,p) ∧ BetaPrefixInto(hb,hc,L,p)
  15. 0015specialize prime_field_polynomial_scale_bounded (p)
  16. 0016specialize prime_field_polynomial_scale_bounded (k)
  17. 0017specialize prime_field_polynomial_scale_bounded (ab)
  18. 0018specialize prime_field_polynomial_scale_bounded (ac)
  19. 0019specialize prime_field_polynomial_scale_bounded (hb)
  20. 0020specialize prime_field_polynomial_scale_bounded (hc)
  21. 0021specialize prime_field_polynomial_scale_bounded (L)
  22. 0022apply prime_field_polynomial_scale_bounded
  23. 0023exact hs
  24. 0024cases hbounds
  25. 0025split
  26. 0026exact hK
  27. 0027split
  28. 0028exact hbounds_left
  29. 0029split
  30. 0030have hz : L=0 \/ ~(L=0)
  31. 0031specialize eq_decidable (L)
  32. 0032specialize eq_decidable (0)
  33. 0033apply eq_decidable
  34. 0034cases hz
  35. 0035left
  36. 0036split
  37. 0037right
  38. 0038exact hz_left
  39. 0039exact hz_left
  40. 0040right
  41. 0041split
  42. 0042intro hbad
  43. 0043specialize succ_ne_zero (0)
  44. 0044apply succ_ne_zero
  45. 0045exact hbad
  46. 0046split
  47. 0047exact hz_right
  48. 0048simp [add_succ_left,zero_add]
  49. 0049intro i
  50. 0050intro hi
  51. 0051have hv : ∃ a. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(hb,hc,i,r) ∧ FpMul(p,k,a,r))
  52. 0052cases hs
  53. 0053specialize hs_right (i)
  54. 0054apply hs_right
  55. 0055exact hi
  56. 0056cases hv
  57. 0057cases hv_witness
  58. 0058cases hv_witness_witness
  59. 0059cases hv_witness_witness_right
  60. 0060have hm : FpMul(p,k,x,x1)
  61. 0061exact hv_witness_witness_right_right
  62. 0062cases hm
  63. 0063cases hm_right
  64. 0064have hcoefficient : ∃ r. FpConvolutionCoefficient(p,kb,kc,1,ab,ac,L,i,r)
  65. 0065specialize prime_field_convolution_coefficient_exists (p)
  66. 0066specialize prime_field_convolution_coefficient_exists (kb)
  67. 0067specialize prime_field_convolution_coefficient_exists (kc)
  68. 0068specialize prime_field_convolution_coefficient_exists (1)
  69. 0069specialize prime_field_convolution_coefficient_exists (ab)
  70. 0070specialize prime_field_convolution_coefficient_exists (ac)
  71. 0071specialize prime_field_convolution_coefficient_exists (L)
  72. 0072specialize prime_field_convolution_coefficient_exists (i)
  73. 0073apply prime_field_convolution_coefficient_exists
  74. 0074intro hpzero
  75. 0075specialize prime_nonzero (p)
  76. 0076apply prime_nonzero
  77. 0077exact hp
  78. 0078exact hpzero
  79. 0079cases hcoefficient
  80. 0080have heq : x2=x1
  81. 0081specialize prime_field_multiply_functional (p)
  82. 0082specialize prime_field_multiply_functional (k)
  83. 0083specialize prime_field_multiply_functional (x)
  84. 0084specialize prime_field_multiply_functional (x2)
  85. 0085specialize prime_field_multiply_functional (x1)
  86. 0086apply prime_field_multiply_functional
  87. 0087specialize prime_field_convolution_coefficient_left_constant (p)
  88. 0088specialize prime_field_convolution_coefficient_left_constant (k)
  89. 0089specialize prime_field_convolution_coefficient_left_constant (kb)
  90. 0090specialize prime_field_convolution_coefficient_left_constant (kc)
  91. 0091specialize prime_field_convolution_coefficient_left_constant (ab)
  92. 0092specialize prime_field_convolution_coefficient_left_constant (ac)
  93. 0093specialize prime_field_convolution_coefficient_left_constant (L)
  94. 0094specialize prime_field_convolution_coefficient_left_constant (i)
  95. 0095specialize prime_field_convolution_coefficient_left_constant (x)
  96. 0096specialize prime_field_convolution_coefficient_left_constant (x2)
  97. 0097apply prime_field_convolution_coefficient_left_constant
  98. 0098exact hk
  99. 0099exact hi
  100. 0100exact hv_witness_witness_left
  101. 0101exact hm_left
  102. 0102exact hm_right_left
  103. 0103exact hcoefficient_witness
  104. 0104exact hv_witness_witness_right_right
  105. 0105exists x1
  106. 0106split
  107. 0107exact hv_witness_witness_right_left
  108. 0108rewrite heq at hcoefficient_witness
  109. 0109rewrite heq at hcoefficient_witness
  110. 0110exact hcoefficient_witness