PX0025

prime_field_polynomial_scale_to_constant_product

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

Recover a genuine convolution from scalar action by constructing every antidiagonal sum and identifying its residue, including the empty product case.

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

Exact expanded first-order arithmetic statement

forall p k ab ac bb bc cb cc L. (~((p) = 1) /\ forall pfa_factor_left_constant_recover_prime pfa_factor_right_constant_recover_prime. (p) = pfa_factor_left_constant_recover_prime * pfa_factor_right_constant_recover_prime -> pfa_factor_left_constant_recover_prime = 1 \/ pfa_factor_right_constant_recover_prime = 1) -> (forall fom_index_pfp_constant_recover_constant. (exists fom_gap_pfp_constant_recover_constant_index_bound. fom_gap_pfp_constant_recover_constant_index_bound + S (fom_index_pfp_constant_recover_constant) = 1) -> exists fom_value_pfp_constant_recover_constant. ((((exists fom_beta_height_pfp_constant_recover_constant_entry. fom_beta_height_pfp_constant_recover_constant_entry + S (fom_value_pfp_constant_recover_constant) = S ((S (fom_index_pfp_constant_recover_constant)) * bc)) /\ exists fom_beta_quotient_pfp_constant_recover_constant_entry. bb = fom_beta_quotient_pfp_constant_recover_constant_entry * S ((S (fom_index_pfp_constant_recover_constant)) * bc) + (fom_value_pfp_constant_recover_constant))) /\ (exists fom_gap_pfp_constant_recover_constant_value_bound. fom_gap_pfp_constant_recover_constant_value_bound + S (fom_value_pfp_constant_recover_constant) = p))) -> (((exists ff_h_pfp_constant_recover_value. ff_h_pfp_constant_recover_value + S (k) = S ((S (0)) * bc)) /\ exists ff_q_pfp_constant_recover_value. bb = ff_q_pfp_constant_recover_value * S ((S (0)) * bc) + (k))) -> (((exists pfa_gap_constant_recover_scalescalar. pfa_gap_constant_recover_scalescalar + S (k) = (p)) /\ ((forall pfp_index_constant_recover_scale. (exists pfa_gap_constant_recover_scaleindex. pfa_gap_constant_recover_scaleindex + S (pfp_index_constant_recover_scale) = (L)) -> exists pfp_source_constant_recover_scale pfp_value_constant_recover_scale. ((((exists ff_h_pfp_constant_recover_scalesource. ff_h_pfp_constant_recover_scalesource + S (pfp_source_constant_recover_scale) = S ((S (pfp_index_constant_recover_scale)) * ac)) /\ exists ff_q_pfp_constant_recover_scalesource. ab = ff_q_pfp_constant_recover_scalesource * S ((S (pfp_index_constant_recover_scale)) * ac) + (pfp_source_constant_recover_scale))) /\ (((((exists ff_h_pfp_constant_recover_scaletarget. ff_h_pfp_constant_recover_scaletarget + S (pfp_value_constant_recover_scale) = S ((S (pfp_index_constant_recover_scale)) * cc)) /\ exists ff_q_pfp_constant_recover_scaletarget. cb = ff_q_pfp_constant_recover_scaletarget * S ((S (pfp_index_constant_recover_scale)) * cc) + (pfp_value_constant_recover_scale))) /\ ((((exists pfa_gap_constant_recover_scaleoperationleft. pfa_gap_constant_recover_scaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_constant_recover_scaleoperationright. pfa_gap_constant_recover_scaleoperationright + S (pfp_source_constant_recover_scale) = (p)) /\ ((((exists pfa_gap_constant_recover_scaleoperationresultbound. pfa_gap_constant_recover_scaleoperationresultbound + S (pfp_value_constant_recover_scale) = (p)) /\ ((exists pfa_offset_left_constant_recover_scaleoperationresultcongruence pfa_offset_right_constant_recover_scaleoperationresultcongruence. ((k) * (pfp_source_constant_recover_scale)) + (p) * pfa_offset_left_constant_recover_scaleoperationresultcongruence = (pfp_value_constant_recover_scale) + (p) * pfa_offset_right_constant_recover_scaleoperationresultcongruence))))))))))))))))) -> (((forall fom_index_pfp_constant_recover_productleft. (exists fom_gap_pfp_constant_recover_productleft_index_bound. fom_gap_pfp_constant_recover_productleft_index_bound + S (fom_index_pfp_constant_recover_productleft) = L) -> exists fom_value_pfp_constant_recover_productleft. ((((exists fom_beta_height_pfp_constant_recover_productleft_entry. fom_beta_height_pfp_constant_recover_productleft_entry + S (fom_value_pfp_constant_recover_productleft) = S ((S (fom_index_pfp_constant_recover_productleft)) * ac)) /\ exists fom_beta_quotient_pfp_constant_recover_productleft_entry. ab = fom_beta_quotient_pfp_constant_recover_productleft_entry * S ((S (fom_index_pfp_constant_recover_productleft)) * ac) + (fom_value_pfp_constant_recover_productleft))) /\ (exists fom_gap_pfp_constant_recover_productleft_value_bound. fom_gap_pfp_constant_recover_productleft_value_bound + S (fom_value_pfp_constant_recover_productleft) = p))) /\ (((forall fom_index_pfp_constant_recover_productright. (exists fom_gap_pfp_constant_recover_productright_index_bound. fom_gap_pfp_constant_recover_productright_index_bound + S (fom_index_pfp_constant_recover_productright) = 1) -> exists fom_value_pfp_constant_recover_productright. ((((exists fom_beta_height_pfp_constant_recover_productright_entry. fom_beta_height_pfp_constant_recover_productright_entry + S (fom_value_pfp_constant_recover_productright) = S ((S (fom_index_pfp_constant_recover_productright)) * bc)) /\ exists fom_beta_quotient_pfp_constant_recover_productright_entry. bb = fom_beta_quotient_pfp_constant_recover_productright_entry * S ((S (fom_index_pfp_constant_recover_productright)) * bc) + (fom_value_pfp_constant_recover_productright))) /\ (exists fom_gap_pfp_constant_recover_productright_value_bound. fom_gap_pfp_constant_recover_productright_value_bound + S (fom_value_pfp_constant_recover_productright) = p))) /\ (((((((L)=0 \/ (1)=0) /\ (((L)=0)))) \/ (((~((L)=0)) /\ (((~((1)=0)) /\ (((L)+(1)=S (L)))))))) /\ ((forall pfc_index_constant_recover_productcoefficients. (exists pfa_gap_constant_recover_productcoefficientsbound. pfa_gap_constant_recover_productcoefficientsbound + S (pfc_index_constant_recover_productcoefficients) = (L)) -> exists pfc_value_constant_recover_productcoefficients. ((((exists ff_h_pfp_constant_recover_productcoefficientsentry. ff_h_pfp_constant_recover_productcoefficientsentry + S (pfc_value_constant_recover_productcoefficients) = S ((S (pfc_index_constant_recover_productcoefficients)) * cc)) /\ exists ff_q_pfp_constant_recover_productcoefficientsentry. cb = ff_q_pfp_constant_recover_productcoefficientsentry * S ((S (pfc_index_constant_recover_productcoefficients)) * cc) + (pfc_value_constant_recover_productcoefficients))) /\ ((exists pfc_terms_code_constant_recover_productcoefficientscoefficient pfc_terms_scale_constant_recover_productcoefficientscoefficient pfc_natural_sum_constant_recover_productcoefficientscoefficient. ((forall pfc_index_constant_recover_productcoefficientscoefficientdiagonal. (exists pfa_gap_constant_recover_productcoefficientscoefficientdiagonalbound. pfa_gap_constant_recover_productcoefficientscoefficientdiagonalbound + S (pfc_index_constant_recover_productcoefficientscoefficientdiagonal) = (S (pfc_index_constant_recover_productcoefficients))) -> exists pfc_value_constant_recover_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_constant_recover_productcoefficientscoefficientdiagonalentry. ff_h_pfp_constant_recover_productcoefficientscoefficientdiagonalentry + S (pfc_value_constant_recover_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_constant_recover_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_constant_recover_productcoefficientscoefficient)) /\ exists ff_q_pfp_constant_recover_productcoefficientscoefficientdiagonalentry. pfc_terms_code_constant_recover_productcoefficientscoefficient = ff_q_pfp_constant_recover_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_constant_recover_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_constant_recover_productcoefficientscoefficient) + (pfc_value_constant_recover_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_constant_recover_productcoefficientscoefficientdiagonalterm pfc_left_constant_recover_productcoefficientscoefficientdiagonalterm pfc_right_constant_recover_productcoefficientscoefficientdiagonalterm. (((pfc_index_constant_recover_productcoefficientscoefficientdiagonal)+pfc_complement_constant_recover_productcoefficientscoefficientdiagonalterm=(pfc_index_constant_recover_productcoefficients)) /\ ((((((exists pfa_gap_constant_recover_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_constant_recover_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_constant_recover_productcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_constant_recover_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_constant_recover_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_constant_recover_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_constant_recover_productcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_constant_recover_productcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_constant_recover_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_constant_recover_productcoefficientscoefficientdiagonal)) * ac) + (pfc_left_constant_recover_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_constant_recover_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_constant_recover_productcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_constant_recover_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_constant_recover_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_constant_recover_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_constant_recover_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_constant_recover_productcoefficientscoefficientdiagonalterm) = (1)) /\ ((((exists ff_h_pfp_constant_recover_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_constant_recover_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_constant_recover_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_constant_recover_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_constant_recover_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_constant_recover_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_constant_recover_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_constant_recover_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_constant_recover_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_constant_recover_productcoefficientscoefficientdiagonaltermrightoutside+(1)=(pfc_complement_constant_recover_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_constant_recover_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_constant_recover_productcoefficientscoefficientdiagonal)=pfc_left_constant_recover_productcoefficientscoefficientdiagonalterm*pfc_right_constant_recover_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_constant_recover_productcoefficientscoefficientsum fs_v_pfc_constant_recover_productcoefficientscoefficientsum. ((((exists fs_h_pfc_constant_recover_productcoefficientscoefficientsum_body_start. fs_h_pfc_constant_recover_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_constant_recover_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_constant_recover_productcoefficientscoefficientsum_body_start. fs_u_pfc_constant_recover_productcoefficientscoefficientsum = fs_q_pfc_constant_recover_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_constant_recover_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_constant_recover_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_constant_recover_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_constant_recover_productcoefficientscoefficient) = S ((S (S (pfc_index_constant_recover_productcoefficients))) * fs_v_pfc_constant_recover_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_constant_recover_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_constant_recover_productcoefficientscoefficientsum = fs_q_pfc_constant_recover_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_constant_recover_productcoefficients))) * fs_v_pfc_constant_recover_productcoefficientscoefficientsum) + (pfc_natural_sum_constant_recover_productcoefficientscoefficient))) /\ forall fs_i_pfc_constant_recover_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_constant_recover_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_constant_recover_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_constant_recover_productcoefficientscoefficientsum_body_steps = S (pfc_index_constant_recover_productcoefficients)) -> exists fs_a_pfc_constant_recover_productcoefficientscoefficientsum_body_steps fs_r_pfc_constant_recover_productcoefficientscoefficientsum_body_steps fs_s_pfc_constant_recover_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_constant_recover_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_constant_recover_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_constant_recover_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_constant_recover_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_constant_recover_productcoefficientscoefficient)) /\ exists fs_q_pfc_constant_recover_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_constant_recover_productcoefficientscoefficient = fs_q_pfc_constant_recover_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_constant_recover_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_constant_recover_productcoefficientscoefficient) + (fs_a_pfc_constant_recover_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_constant_recover_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_constant_recover_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_constant_recover_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_constant_recover_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_constant_recover_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_constant_recover_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_constant_recover_productcoefficientscoefficientsum = fs_q_pfc_constant_recover_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_constant_recover_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_constant_recover_productcoefficientscoefficientsum) + (fs_r_pfc_constant_recover_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_constant_recover_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_constant_recover_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_constant_recover_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_constant_recover_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_constant_recover_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_constant_recover_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_constant_recover_productcoefficientscoefficientsum = fs_q_pfc_constant_recover_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_constant_recover_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_constant_recover_productcoefficientscoefficientsum) + (fs_s_pfc_constant_recover_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_constant_recover_productcoefficientscoefficientsum_body_steps = fs_r_pfc_constant_recover_productcoefficientscoefficientsum_body_steps + fs_a_pfc_constant_recover_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_constant_recover_productcoefficientscoefficientresiduebound. pfa_gap_constant_recover_productcoefficientscoefficientresiduebound + S (pfc_value_constant_recover_productcoefficients) = (p)) /\ ((exists pfa_offset_left_constant_recover_productcoefficientscoefficientresiduecongruence pfa_offset_right_constant_recover_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_constant_recover_productcoefficientscoefficient) + (p) * pfa_offset_left_constant_recover_productcoefficientscoefficientresiduecongruence = (pfc_value_constant_recover_productcoefficients) + (p) * pfa_offset_right_constant_recover_productcoefficientscoefficientresiduecongruence)))))))))))))))))))

Constructive proof overview

Generated structural guide

Recover a genuine convolution from scalar action by constructing every antidiagonal sum and identifying its residue, including the empty product case.

The unchanged tactic script uses 7 declared prerequisites and contains 107 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_field_polynomial_scale_bounded Alpha theorem; checked-use authorized eq_decidable Alpha theorem; checked-use authorized succ_ne_zero Alpha theorem; checked-use authorized prime_field_convolution_coefficient_exists Alpha theorem; checked-use authorized prime_nonzero Alpha theorem; checked-use authorized prime_field_multiply_functional Alpha theorem; checked-use authorized PX0023 prime_field_polynomial_constant_right_coefficient

Direct dependents

none

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

107 script commands · 34 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 constant right coefficient

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro 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–13

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

  1. L11
    intro hB
  2. L12
    intro hk
  3. L13
    intro hs
03Establish hbL14–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 hb : BetaPrefixInto(ab,ac,L,p) ∧ BetaPrefixInto(cb,cc,L,p)Definitions: BetaPrefixInto
  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 (cb)
  7. L20
    specialize prime_field_polynomial_scale_bounded (cc)
  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 hb
  2. L25
    split
05Use earlier factsL26–26

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

  1. L26
    exact hb_left
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 hB
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
    left
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
13Use earlier factsL42–42

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

  1. L42
    exact hz_right
14Separate the logical casesL43–43

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

  1. L43
    split
15Fix variables and assumptionsL44–44

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

  1. L44
    intro hbad
16Use earlier factsL45–47

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

  1. L45
    specialize succ_ne_zero (0)
  2. L46
    apply succ_ne_zero
  3. L47
    exact hbad
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
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(cb,cc,i,r) ∧ FpMul(p,k,a,r))Definitions: FpMulBetaAt
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 hcL60–69

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

  1. L60
    have hc : ∃ r. FpConvolutionCoefficient(p,ab,ac,L,bb,bc,1,i,r)Definitions: FpConvolutionCoefficient
  2. L61
    specialize prime_field_convolution_coefficient_exists (p)
  3. L62
    specialize prime_field_convolution_coefficient_exists (ab)
  4. L63
    specialize prime_field_convolution_coefficient_exists (ac)
  5. L64
    specialize prime_field_convolution_coefficient_exists (L)
  6. L65
    specialize prime_field_convolution_coefficient_exists (bb)
  7. L66
    specialize prime_field_convolution_coefficient_exists (bc)
  8. L67
    specialize prime_field_convolution_coefficient_exists (1)
  9. L68
    specialize prime_field_convolution_coefficient_exists (i)
  10. L69
    apply prime_field_convolution_coefficient_exists
24Fix variables and assumptionsL70–70

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

  1. L70
    intro hpzero
25Use earlier factsL71–74

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

  1. L71
    specialize prime_nonzero (p)
  2. L72
    apply prime_nonzero
  3. L73
    exact hp
  4. L74
    exact hpzero
26Separate the logical casesL75–75

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

  1. L75
    cases hc
27Establish heqL76–85

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

  1. L76
    have heq : x2=x1
  2. L77
    specialize prime_field_multiply_functional (p)
  3. L78
    specialize prime_field_multiply_functional (k)
  4. L79
    specialize prime_field_multiply_functional (x)
  5. L80
    specialize prime_field_multiply_functional (x2)
  6. L81
    specialize prime_field_multiply_functional (x1)
  7. L82
    apply prime_field_multiply_functional
  8. L83
    specialize prime_field_polynomial_constant_right_coefficient (p)
  9. L84
    specialize prime_field_polynomial_constant_right_coefficient (ab)
  10. L85
    specialize prime_field_polynomial_constant_right_coefficient (ac)
28Use earlier factsL86–95

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

  1. L86
    specialize prime_field_polynomial_constant_right_coefficient (L)
  2. L87
    specialize prime_field_polynomial_constant_right_coefficient (bb)
  3. L88
    specialize prime_field_polynomial_constant_right_coefficient (bc)
  4. L89
    specialize prime_field_polynomial_constant_right_coefficient (k)
  5. L90
    specialize prime_field_polynomial_constant_right_coefficient (i)
  6. L91
    specialize prime_field_polynomial_constant_right_coefficient (x)
  7. L92
    specialize prime_field_polynomial_constant_right_coefficient (x2)
  8. L93
    apply prime_field_polynomial_constant_right_coefficient
  9. L94
    exact hp
  10. L95
    exact hb_left
29Use earlier factsL96–101

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

  1. L96
    exact hB
  2. L97
    exact hk
  3. L98
    exact hi
  4. L99
    exact hv_witness_witness_left
  5. L100
    exact hc_witness
  6. L101
    exact hv_witness_witness_right_right
30Construct an explicit witnessL102–102

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

  1. L102
    exists x1
31Separate the logical casesL103–103

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

  1. L103
    split
32Use earlier factsL104–104

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

  1. L104
    exact hv_witness_witness_right_left
33Calculate and transport equalitiesL105–106

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

  1. L105
    rewrite heq at hc_witness
  2. L106
    rewrite heq at hc_witness
34Use earlier factsL107–107

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

  1. L107
    exact hc_witness

Library-wide reading audit

Original exact command ledger · 107 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 hB
  12. 0012intro hk
  13. 0013intro hs
  14. 0014have hb : ((forall fom_index_pfp_constant_recover_A. (exists fom_gap_pfp_constant_recover_A_index_bound. fom_gap_pfp_constant_recover_A_index_bound + S (fom_index_pfp_constant_recover_A) = L) -> exists fom_value_pfp_constant_recover_A. ((((exists fom_beta_height_pfp_constant_recover_A_entry. fom_beta_height_pfp_constant_recover_A_entry + S (fom_value_pfp_constant_recover_A) = S ((S (fom_index_pfp_constant_recover_A)) * ac)) /\ exists fom_beta_quotient_pfp_constant_recover_A_entry. ab = fom_beta_quotient_pfp_constant_recover_A_entry * S ((S (fom_index_pfp_constant_recover_A)) * ac) + (fom_value_pfp_constant_recover_A))) /\ (exists fom_gap_pfp_constant_recover_A_value_bound. fom_gap_pfp_constant_recover_A_value_bound + S (fom_value_pfp_constant_recover_A) = p))) /\ ((forall fom_index_pfp_constant_recover_C. (exists fom_gap_pfp_constant_recover_C_index_bound. fom_gap_pfp_constant_recover_C_index_bound + S (fom_index_pfp_constant_recover_C) = L) -> exists fom_value_pfp_constant_recover_C. ((((exists fom_beta_height_pfp_constant_recover_C_entry. fom_beta_height_pfp_constant_recover_C_entry + S (fom_value_pfp_constant_recover_C) = S ((S (fom_index_pfp_constant_recover_C)) * cc)) /\ exists fom_beta_quotient_pfp_constant_recover_C_entry. cb = fom_beta_quotient_pfp_constant_recover_C_entry * S ((S (fom_index_pfp_constant_recover_C)) * cc) + (fom_value_pfp_constant_recover_C))) /\ (exists fom_gap_pfp_constant_recover_C_value_bound. fom_gap_pfp_constant_recover_C_value_bound + S (fom_value_pfp_constant_recover_C) = 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 (cb)
  20. 0020specialize prime_field_polynomial_scale_bounded (cc)
  21. 0021specialize prime_field_polynomial_scale_bounded (L)
  22. 0022apply prime_field_polynomial_scale_bounded
  23. 0023exact hs
  24. 0024cases hb
  25. 0025split
  26. 0026exact hb_left
  27. 0027split
  28. 0028exact hB
  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. 0037left
  38. 0038exact hz_left
  39. 0039exact hz_left
  40. 0040right
  41. 0041split
  42. 0042exact hz_right
  43. 0043split
  44. 0044intro hbad
  45. 0045specialize succ_ne_zero (0)
  46. 0046apply succ_ne_zero
  47. 0047exact hbad
  48. 0048simp
  49. 0049intro i
  50. 0050intro hi
  51. 0051have hv : exists a r. (((((exists ff_h_pfp_constant_recover_source. ff_h_pfp_constant_recover_source + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_constant_recover_source. ab = ff_q_pfp_constant_recover_source * S ((S (i)) * ac) + (a))) /\ (((((exists ff_h_pfp_constant_recover_target. ff_h_pfp_constant_recover_target + S (r) = S ((S (i)) * cc)) /\ exists ff_q_pfp_constant_recover_target. cb = ff_q_pfp_constant_recover_target * S ((S (i)) * cc) + (r))) /\ ((((exists pfa_gap_constant_recover_mulleft. pfa_gap_constant_recover_mulleft + S (k) = (p)) /\ (((exists pfa_gap_constant_recover_mulright. pfa_gap_constant_recover_mulright + S (a) = (p)) /\ ((((exists pfa_gap_constant_recover_mulresultbound. pfa_gap_constant_recover_mulresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_constant_recover_mulresultcongruence pfa_offset_right_constant_recover_mulresultcongruence. ((k) * (a)) + (p) * pfa_offset_left_constant_recover_mulresultcongruence = (r) + (p) * pfa_offset_right_constant_recover_mulresultcongruence))))))))))))))
  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 hc : exists r. (exists pfc_terms_code_constant_recover_actual pfc_terms_scale_constant_recover_actual pfc_natural_sum_constant_recover_actual. ((forall pfc_index_constant_recover_actualdiagonal. (exists pfa_gap_constant_recover_actualdiagonalbound. pfa_gap_constant_recover_actualdiagonalbound + S (pfc_index_constant_recover_actualdiagonal) = (S (i))) -> exists pfc_value_constant_recover_actualdiagonal. ((((exists ff_h_pfp_constant_recover_actualdiagonalentry. ff_h_pfp_constant_recover_actualdiagonalentry + S (pfc_value_constant_recover_actualdiagonal) = S ((S (pfc_index_constant_recover_actualdiagonal)) * pfc_terms_scale_constant_recover_actual)) /\ exists ff_q_pfp_constant_recover_actualdiagonalentry. pfc_terms_code_constant_recover_actual = ff_q_pfp_constant_recover_actualdiagonalentry * S ((S (pfc_index_constant_recover_actualdiagonal)) * pfc_terms_scale_constant_recover_actual) + (pfc_value_constant_recover_actualdiagonal))) /\ ((exists pfc_complement_constant_recover_actualdiagonalterm pfc_left_constant_recover_actualdiagonalterm pfc_right_constant_recover_actualdiagonalterm. (((pfc_index_constant_recover_actualdiagonal)+pfc_complement_constant_recover_actualdiagonalterm=(i)) /\ ((((((exists pfa_gap_constant_recover_actualdiagonaltermleftinside. pfa_gap_constant_recover_actualdiagonaltermleftinside + S (pfc_index_constant_recover_actualdiagonal) = (L)) /\ ((((exists ff_h_pfp_constant_recover_actualdiagonaltermleftentry. ff_h_pfp_constant_recover_actualdiagonaltermleftentry + S (pfc_left_constant_recover_actualdiagonalterm) = S ((S (pfc_index_constant_recover_actualdiagonal)) * ac)) /\ exists ff_q_pfp_constant_recover_actualdiagonaltermleftentry. ab = ff_q_pfp_constant_recover_actualdiagonaltermleftentry * S ((S (pfc_index_constant_recover_actualdiagonal)) * ac) + (pfc_left_constant_recover_actualdiagonalterm)))))) \/ (((exists pfc_gap_constant_recover_actualdiagonaltermleftoutside. pfc_gap_constant_recover_actualdiagonaltermleftoutside+(L)=(pfc_index_constant_recover_actualdiagonal)) /\ (((pfc_left_constant_recover_actualdiagonalterm)=0))))) /\ ((((((exists pfa_gap_constant_recover_actualdiagonaltermrightinside. pfa_gap_constant_recover_actualdiagonaltermrightinside + S (pfc_complement_constant_recover_actualdiagonalterm) = (1)) /\ ((((exists ff_h_pfp_constant_recover_actualdiagonaltermrightentry. ff_h_pfp_constant_recover_actualdiagonaltermrightentry + S (pfc_right_constant_recover_actualdiagonalterm) = S ((S (pfc_complement_constant_recover_actualdiagonalterm)) * bc)) /\ exists ff_q_pfp_constant_recover_actualdiagonaltermrightentry. bb = ff_q_pfp_constant_recover_actualdiagonaltermrightentry * S ((S (pfc_complement_constant_recover_actualdiagonalterm)) * bc) + (pfc_right_constant_recover_actualdiagonalterm)))))) \/ (((exists pfc_gap_constant_recover_actualdiagonaltermrightoutside. pfc_gap_constant_recover_actualdiagonaltermrightoutside+(1)=(pfc_complement_constant_recover_actualdiagonalterm)) /\ (((pfc_right_constant_recover_actualdiagonalterm)=0))))) /\ (((pfc_value_constant_recover_actualdiagonal)=pfc_left_constant_recover_actualdiagonalterm*pfc_right_constant_recover_actualdiagonalterm))))))))))) /\ (((exists fs_u_pfc_constant_recover_actualsum fs_v_pfc_constant_recover_actualsum. ((((exists fs_h_pfc_constant_recover_actualsum_body_start. fs_h_pfc_constant_recover_actualsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_constant_recover_actualsum)) /\ exists fs_q_pfc_constant_recover_actualsum_body_start. fs_u_pfc_constant_recover_actualsum = fs_q_pfc_constant_recover_actualsum_body_start * S ((S (0)) * fs_v_pfc_constant_recover_actualsum) + (0))) /\ ((((exists fs_h_pfc_constant_recover_actualsum_body_terminal. fs_h_pfc_constant_recover_actualsum_body_terminal + S (pfc_natural_sum_constant_recover_actual) = S ((S (S (i))) * fs_v_pfc_constant_recover_actualsum)) /\ exists fs_q_pfc_constant_recover_actualsum_body_terminal. fs_u_pfc_constant_recover_actualsum = fs_q_pfc_constant_recover_actualsum_body_terminal * S ((S (S (i))) * fs_v_pfc_constant_recover_actualsum) + (pfc_natural_sum_constant_recover_actual))) /\ forall fs_i_pfc_constant_recover_actualsum_body_steps. (exists fs_lt_pfc_constant_recover_actualsum_body_steps_bound. fs_lt_pfc_constant_recover_actualsum_body_steps_bound + S fs_i_pfc_constant_recover_actualsum_body_steps = S (i)) -> exists fs_a_pfc_constant_recover_actualsum_body_steps fs_r_pfc_constant_recover_actualsum_body_steps fs_s_pfc_constant_recover_actualsum_body_steps. ((((exists fs_h_pfc_constant_recover_actualsum_body_steps_summand. fs_h_pfc_constant_recover_actualsum_body_steps_summand + S (fs_a_pfc_constant_recover_actualsum_body_steps) = S ((S (fs_i_pfc_constant_recover_actualsum_body_steps)) * pfc_terms_scale_constant_recover_actual)) /\ exists fs_q_pfc_constant_recover_actualsum_body_steps_summand. pfc_terms_code_constant_recover_actual = fs_q_pfc_constant_recover_actualsum_body_steps_summand * S ((S (fs_i_pfc_constant_recover_actualsum_body_steps)) * pfc_terms_scale_constant_recover_actual) + (fs_a_pfc_constant_recover_actualsum_body_steps))) /\ ((((exists fs_h_pfc_constant_recover_actualsum_body_steps_partial. fs_h_pfc_constant_recover_actualsum_body_steps_partial + S (fs_r_pfc_constant_recover_actualsum_body_steps) = S ((S (fs_i_pfc_constant_recover_actualsum_body_steps)) * fs_v_pfc_constant_recover_actualsum)) /\ exists fs_q_pfc_constant_recover_actualsum_body_steps_partial. fs_u_pfc_constant_recover_actualsum = fs_q_pfc_constant_recover_actualsum_body_steps_partial * S ((S (fs_i_pfc_constant_recover_actualsum_body_steps)) * fs_v_pfc_constant_recover_actualsum) + (fs_r_pfc_constant_recover_actualsum_body_steps))) /\ ((((exists fs_h_pfc_constant_recover_actualsum_body_steps_successor. fs_h_pfc_constant_recover_actualsum_body_steps_successor + S (fs_s_pfc_constant_recover_actualsum_body_steps) = S ((S (S fs_i_pfc_constant_recover_actualsum_body_steps)) * fs_v_pfc_constant_recover_actualsum)) /\ exists fs_q_pfc_constant_recover_actualsum_body_steps_successor. fs_u_pfc_constant_recover_actualsum = fs_q_pfc_constant_recover_actualsum_body_steps_successor * S ((S (S fs_i_pfc_constant_recover_actualsum_body_steps)) * fs_v_pfc_constant_recover_actualsum) + (fs_s_pfc_constant_recover_actualsum_body_steps))) /\ fs_s_pfc_constant_recover_actualsum_body_steps = fs_r_pfc_constant_recover_actualsum_body_steps + fs_a_pfc_constant_recover_actualsum_body_steps)))))) /\ ((((exists pfa_gap_constant_recover_actualresiduebound. pfa_gap_constant_recover_actualresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_constant_recover_actualresiduecongruence pfa_offset_right_constant_recover_actualresiduecongruence. (pfc_natural_sum_constant_recover_actual) + (p) * pfa_offset_left_constant_recover_actualresiduecongruence = (r) + (p) * pfa_offset_right_constant_recover_actualresiduecongruence)))))))))
  61. 0061specialize prime_field_convolution_coefficient_exists (p)
  62. 0062specialize prime_field_convolution_coefficient_exists (ab)
  63. 0063specialize prime_field_convolution_coefficient_exists (ac)
  64. 0064specialize prime_field_convolution_coefficient_exists (L)
  65. 0065specialize prime_field_convolution_coefficient_exists (bb)
  66. 0066specialize prime_field_convolution_coefficient_exists (bc)
  67. 0067specialize prime_field_convolution_coefficient_exists (1)
  68. 0068specialize prime_field_convolution_coefficient_exists (i)
  69. 0069apply prime_field_convolution_coefficient_exists
  70. 0070intro hpzero
  71. 0071specialize prime_nonzero (p)
  72. 0072apply prime_nonzero
  73. 0073exact hp
  74. 0074exact hpzero
  75. 0075cases hc
  76. 0076have heq : x2=x1
  77. 0077specialize prime_field_multiply_functional (p)
  78. 0078specialize prime_field_multiply_functional (k)
  79. 0079specialize prime_field_multiply_functional (x)
  80. 0080specialize prime_field_multiply_functional (x2)
  81. 0081specialize prime_field_multiply_functional (x1)
  82. 0082apply prime_field_multiply_functional
  83. 0083specialize prime_field_polynomial_constant_right_coefficient (p)
  84. 0084specialize prime_field_polynomial_constant_right_coefficient (ab)
  85. 0085specialize prime_field_polynomial_constant_right_coefficient (ac)
  86. 0086specialize prime_field_polynomial_constant_right_coefficient (L)
  87. 0087specialize prime_field_polynomial_constant_right_coefficient (bb)
  88. 0088specialize prime_field_polynomial_constant_right_coefficient (bc)
  89. 0089specialize prime_field_polynomial_constant_right_coefficient (k)
  90. 0090specialize prime_field_polynomial_constant_right_coefficient (i)
  91. 0091specialize prime_field_polynomial_constant_right_coefficient (x)
  92. 0092specialize prime_field_polynomial_constant_right_coefficient (x2)
  93. 0093apply prime_field_polynomial_constant_right_coefficient
  94. 0094exact hp
  95. 0095exact hb_left
  96. 0096exact hB
  97. 0097exact hk
  98. 0098exact hi
  99. 0099exact hv_witness_witness_left
  100. 0100exact hc_witness
  101. 0101exact hv_witness_witness_right_right
  102. 0102exists x1
  103. 0103split
  104. 0104exact hv_witness_witness_right_left
  105. 0105rewrite heq at hc_witness
  106. 0106rewrite heq at hc_witness
  107. 0107exact hc_witness