PX0023

prime_field_polynomial_constant_right_coefficient

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

The actual antidiagonal coefficient with a length-one right factor is its actual scalar product, by triangular append and proved vanished prior support.

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

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc k i a r. (~((p) = 1) /\ forall pfa_factor_left_constant_coefficient_prime pfa_factor_right_constant_coefficient_prime. (p) = pfa_factor_left_constant_coefficient_prime * pfa_factor_right_constant_coefficient_prime -> pfa_factor_left_constant_coefficient_prime = 1 \/ pfa_factor_right_constant_coefficient_prime = 1) -> (forall fom_index_pfp_constant_coefficient_A. (exists fom_gap_pfp_constant_coefficient_A_index_bound. fom_gap_pfp_constant_coefficient_A_index_bound + S (fom_index_pfp_constant_coefficient_A) = L) -> exists fom_value_pfp_constant_coefficient_A. ((((exists fom_beta_height_pfp_constant_coefficient_A_entry. fom_beta_height_pfp_constant_coefficient_A_entry + S (fom_value_pfp_constant_coefficient_A) = S ((S (fom_index_pfp_constant_coefficient_A)) * ac)) /\ exists fom_beta_quotient_pfp_constant_coefficient_A_entry. ab = fom_beta_quotient_pfp_constant_coefficient_A_entry * S ((S (fom_index_pfp_constant_coefficient_A)) * ac) + (fom_value_pfp_constant_coefficient_A))) /\ (exists fom_gap_pfp_constant_coefficient_A_value_bound. fom_gap_pfp_constant_coefficient_A_value_bound + S (fom_value_pfp_constant_coefficient_A) = p))) -> (forall fom_index_pfp_constant_coefficient_B. (exists fom_gap_pfp_constant_coefficient_B_index_bound. fom_gap_pfp_constant_coefficient_B_index_bound + S (fom_index_pfp_constant_coefficient_B) = 1) -> exists fom_value_pfp_constant_coefficient_B. ((((exists fom_beta_height_pfp_constant_coefficient_B_entry. fom_beta_height_pfp_constant_coefficient_B_entry + S (fom_value_pfp_constant_coefficient_B) = S ((S (fom_index_pfp_constant_coefficient_B)) * bc)) /\ exists fom_beta_quotient_pfp_constant_coefficient_B_entry. bb = fom_beta_quotient_pfp_constant_coefficient_B_entry * S ((S (fom_index_pfp_constant_coefficient_B)) * bc) + (fom_value_pfp_constant_coefficient_B))) /\ (exists fom_gap_pfp_constant_coefficient_B_value_bound. fom_gap_pfp_constant_coefficient_B_value_bound + S (fom_value_pfp_constant_coefficient_B) = p))) -> (((exists ff_h_pfp_constant_coefficient_constant. ff_h_pfp_constant_coefficient_constant + S (k) = S ((S (0)) * bc)) /\ exists ff_q_pfp_constant_coefficient_constant. bb = ff_q_pfp_constant_coefficient_constant * S ((S (0)) * bc) + (k))) -> (exists pfa_gap_constant_coefficient_index. pfa_gap_constant_coefficient_index + S (i) = (L)) -> (((exists ff_h_pfp_constant_coefficient_entry. ff_h_pfp_constant_coefficient_entry + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_constant_coefficient_entry. ab = ff_q_pfp_constant_coefficient_entry * S ((S (i)) * ac) + (a))) -> (exists pfc_terms_code_constant_coefficient_actual pfc_terms_scale_constant_coefficient_actual pfc_natural_sum_constant_coefficient_actual. ((forall pfc_index_constant_coefficient_actualdiagonal. (exists pfa_gap_constant_coefficient_actualdiagonalbound. pfa_gap_constant_coefficient_actualdiagonalbound + S (pfc_index_constant_coefficient_actualdiagonal) = (S (i))) -> exists pfc_value_constant_coefficient_actualdiagonal. ((((exists ff_h_pfp_constant_coefficient_actualdiagonalentry. ff_h_pfp_constant_coefficient_actualdiagonalentry + S (pfc_value_constant_coefficient_actualdiagonal) = S ((S (pfc_index_constant_coefficient_actualdiagonal)) * pfc_terms_scale_constant_coefficient_actual)) /\ exists ff_q_pfp_constant_coefficient_actualdiagonalentry. pfc_terms_code_constant_coefficient_actual = ff_q_pfp_constant_coefficient_actualdiagonalentry * S ((S (pfc_index_constant_coefficient_actualdiagonal)) * pfc_terms_scale_constant_coefficient_actual) + (pfc_value_constant_coefficient_actualdiagonal))) /\ ((exists pfc_complement_constant_coefficient_actualdiagonalterm pfc_left_constant_coefficient_actualdiagonalterm pfc_right_constant_coefficient_actualdiagonalterm. (((pfc_index_constant_coefficient_actualdiagonal)+pfc_complement_constant_coefficient_actualdiagonalterm=(i)) /\ ((((((exists pfa_gap_constant_coefficient_actualdiagonaltermleftinside. pfa_gap_constant_coefficient_actualdiagonaltermleftinside + S (pfc_index_constant_coefficient_actualdiagonal) = (L)) /\ ((((exists ff_h_pfp_constant_coefficient_actualdiagonaltermleftentry. ff_h_pfp_constant_coefficient_actualdiagonaltermleftentry + S (pfc_left_constant_coefficient_actualdiagonalterm) = S ((S (pfc_index_constant_coefficient_actualdiagonal)) * ac)) /\ exists ff_q_pfp_constant_coefficient_actualdiagonaltermleftentry. ab = ff_q_pfp_constant_coefficient_actualdiagonaltermleftentry * S ((S (pfc_index_constant_coefficient_actualdiagonal)) * ac) + (pfc_left_constant_coefficient_actualdiagonalterm)))))) \/ (((exists pfc_gap_constant_coefficient_actualdiagonaltermleftoutside. pfc_gap_constant_coefficient_actualdiagonaltermleftoutside+(L)=(pfc_index_constant_coefficient_actualdiagonal)) /\ (((pfc_left_constant_coefficient_actualdiagonalterm)=0))))) /\ ((((((exists pfa_gap_constant_coefficient_actualdiagonaltermrightinside. pfa_gap_constant_coefficient_actualdiagonaltermrightinside + S (pfc_complement_constant_coefficient_actualdiagonalterm) = (1)) /\ ((((exists ff_h_pfp_constant_coefficient_actualdiagonaltermrightentry. ff_h_pfp_constant_coefficient_actualdiagonaltermrightentry + S (pfc_right_constant_coefficient_actualdiagonalterm) = S ((S (pfc_complement_constant_coefficient_actualdiagonalterm)) * bc)) /\ exists ff_q_pfp_constant_coefficient_actualdiagonaltermrightentry. bb = ff_q_pfp_constant_coefficient_actualdiagonaltermrightentry * S ((S (pfc_complement_constant_coefficient_actualdiagonalterm)) * bc) + (pfc_right_constant_coefficient_actualdiagonalterm)))))) \/ (((exists pfc_gap_constant_coefficient_actualdiagonaltermrightoutside. pfc_gap_constant_coefficient_actualdiagonaltermrightoutside+(1)=(pfc_complement_constant_coefficient_actualdiagonalterm)) /\ (((pfc_right_constant_coefficient_actualdiagonalterm)=0))))) /\ (((pfc_value_constant_coefficient_actualdiagonal)=pfc_left_constant_coefficient_actualdiagonalterm*pfc_right_constant_coefficient_actualdiagonalterm))))))))))) /\ (((exists fs_u_pfc_constant_coefficient_actualsum fs_v_pfc_constant_coefficient_actualsum. ((((exists fs_h_pfc_constant_coefficient_actualsum_body_start. fs_h_pfc_constant_coefficient_actualsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_constant_coefficient_actualsum)) /\ exists fs_q_pfc_constant_coefficient_actualsum_body_start. fs_u_pfc_constant_coefficient_actualsum = fs_q_pfc_constant_coefficient_actualsum_body_start * S ((S (0)) * fs_v_pfc_constant_coefficient_actualsum) + (0))) /\ ((((exists fs_h_pfc_constant_coefficient_actualsum_body_terminal. fs_h_pfc_constant_coefficient_actualsum_body_terminal + S (pfc_natural_sum_constant_coefficient_actual) = S ((S (S (i))) * fs_v_pfc_constant_coefficient_actualsum)) /\ exists fs_q_pfc_constant_coefficient_actualsum_body_terminal. fs_u_pfc_constant_coefficient_actualsum = fs_q_pfc_constant_coefficient_actualsum_body_terminal * S ((S (S (i))) * fs_v_pfc_constant_coefficient_actualsum) + (pfc_natural_sum_constant_coefficient_actual))) /\ forall fs_i_pfc_constant_coefficient_actualsum_body_steps. (exists fs_lt_pfc_constant_coefficient_actualsum_body_steps_bound. fs_lt_pfc_constant_coefficient_actualsum_body_steps_bound + S fs_i_pfc_constant_coefficient_actualsum_body_steps = S (i)) -> exists fs_a_pfc_constant_coefficient_actualsum_body_steps fs_r_pfc_constant_coefficient_actualsum_body_steps fs_s_pfc_constant_coefficient_actualsum_body_steps. ((((exists fs_h_pfc_constant_coefficient_actualsum_body_steps_summand. fs_h_pfc_constant_coefficient_actualsum_body_steps_summand + S (fs_a_pfc_constant_coefficient_actualsum_body_steps) = S ((S (fs_i_pfc_constant_coefficient_actualsum_body_steps)) * pfc_terms_scale_constant_coefficient_actual)) /\ exists fs_q_pfc_constant_coefficient_actualsum_body_steps_summand. pfc_terms_code_constant_coefficient_actual = fs_q_pfc_constant_coefficient_actualsum_body_steps_summand * S ((S (fs_i_pfc_constant_coefficient_actualsum_body_steps)) * pfc_terms_scale_constant_coefficient_actual) + (fs_a_pfc_constant_coefficient_actualsum_body_steps))) /\ ((((exists fs_h_pfc_constant_coefficient_actualsum_body_steps_partial. fs_h_pfc_constant_coefficient_actualsum_body_steps_partial + S (fs_r_pfc_constant_coefficient_actualsum_body_steps) = S ((S (fs_i_pfc_constant_coefficient_actualsum_body_steps)) * fs_v_pfc_constant_coefficient_actualsum)) /\ exists fs_q_pfc_constant_coefficient_actualsum_body_steps_partial. fs_u_pfc_constant_coefficient_actualsum = fs_q_pfc_constant_coefficient_actualsum_body_steps_partial * S ((S (fs_i_pfc_constant_coefficient_actualsum_body_steps)) * fs_v_pfc_constant_coefficient_actualsum) + (fs_r_pfc_constant_coefficient_actualsum_body_steps))) /\ ((((exists fs_h_pfc_constant_coefficient_actualsum_body_steps_successor. fs_h_pfc_constant_coefficient_actualsum_body_steps_successor + S (fs_s_pfc_constant_coefficient_actualsum_body_steps) = S ((S (S fs_i_pfc_constant_coefficient_actualsum_body_steps)) * fs_v_pfc_constant_coefficient_actualsum)) /\ exists fs_q_pfc_constant_coefficient_actualsum_body_steps_successor. fs_u_pfc_constant_coefficient_actualsum = fs_q_pfc_constant_coefficient_actualsum_body_steps_successor * S ((S (S fs_i_pfc_constant_coefficient_actualsum_body_steps)) * fs_v_pfc_constant_coefficient_actualsum) + (fs_s_pfc_constant_coefficient_actualsum_body_steps))) /\ fs_s_pfc_constant_coefficient_actualsum_body_steps = fs_r_pfc_constant_coefficient_actualsum_body_steps + fs_a_pfc_constant_coefficient_actualsum_body_steps)))))) /\ ((((exists pfa_gap_constant_coefficient_actualresiduebound. pfa_gap_constant_coefficient_actualresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_constant_coefficient_actualresiduecongruence pfa_offset_right_constant_coefficient_actualresiduecongruence. (pfc_natural_sum_constant_coefficient_actual) + (p) * pfa_offset_left_constant_coefficient_actualresiduecongruence = (r) + (p) * pfa_offset_right_constant_coefficient_actualresiduecongruence))))))))) -> (((exists pfa_gap_constant_coefficient_resultleft. pfa_gap_constant_coefficient_resultleft + S (k) = (p)) /\ (((exists pfa_gap_constant_coefficient_resultright. pfa_gap_constant_coefficient_resultright + S (a) = (p)) /\ ((((exists pfa_gap_constant_coefficient_resultresultbound. pfa_gap_constant_coefficient_resultresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_constant_coefficient_resultresultcongruence pfa_offset_right_constant_coefficient_resultresultcongruence. ((k) * (a)) + (p) * pfa_offset_left_constant_coefficient_resultresultcongruence = (r) + (p) * pfa_offset_right_constant_coefficient_resultresultcongruence)))))))))

Constructive proof overview

Generated structural guide

The actual antidiagonal coefficient with a length-one right factor is its actual scalar product, by triangular append and proved vanished prior support.

The unchanged tactic script uses 12 declared prerequisites and contains 158 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_nonzero Alpha theorem; checked-use authorized prime_field_convolution_coefficient_exists Alpha theorem; checked-use authorized prime_field_convolution_coefficient_zero_past_support Alpha theorem; checked-use authorized zero_add Alpha theorem; checked-use authorized PX0003 prime_field_convolution_coefficient_prefix_transport le_refl Alpha theorem; checked-use authorized prime_field_multiply_exists Alpha theorem; checked-use authorized matrix_rank_bounded_prefix_value Alpha theorem; checked-use authorized PX0008 prime_field_convolution_coefficient_append prime_field_add_functional Alpha theorem; checked-use authorized prime_field_add_zero_left Alpha theorem; checked-use authorized prime_field_multiply_commutative Alpha theorem; checked-use authorized

Direct dependents

PX0024 prime_field_polynomial_constant_product_to_scale PX0025 prime_field_polynomial_scale_to_constant_product

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

158 script commands · 34 reading checkpoints · 8 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 (2)
prime field convolution coefficient prefix transportprime field convolution coefficient append

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 ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro k
  8. L8
    intro i
  9. L9
    intro a
  10. L10
    intro r
02Fix variables and assumptionsL11–17

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

  1. L11
    intro hp
  2. L12
    intro hA
  3. L13
    intro hB
  4. L14
    intro hk
  5. L15
    intro hi
  6. L16
    intro ha
  7. L17
    intro hr
03Establish hp0L18–23

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

  1. L18
    have hp0 : ~(p=0)
  2. L19
    intro hpzero
  3. L20
    specialize prime_nonzero (p)
  4. L21
    apply prime_nonzero
  5. L22
    exact hp
  6. L23
    exact hpzero
04Establish hcL24–33

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

  1. L24
    have hc : ∃ c. FpConvolutionCoefficient(p,ab,ac,i,bb,bc,1,i,c)Definitions: FpConvolutionCoefficient
  2. L25
    specialize prime_field_convolution_coefficient_exists (p)
  3. L26
    specialize prime_field_convolution_coefficient_exists (ab)
  4. L27
    specialize prime_field_convolution_coefficient_exists (ac)
  5. L28
    specialize prime_field_convolution_coefficient_exists (i)
  6. L29
    specialize prime_field_convolution_coefficient_exists (bb)
  7. L30
    specialize prime_field_convolution_coefficient_exists (bc)
  8. L31
    specialize prime_field_convolution_coefficient_exists (1)
  9. L32
    specialize prime_field_convolution_coefficient_exists (i)
  10. L33
    apply prime_field_convolution_coefficient_exists
05Use earlier factsL34–34

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

  1. L34
    exact hp0
06Separate the logical casesL35–35

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

  1. L35
    cases hc
07Establish hc0L36–45

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

  1. L36
    have hc0 : x=0
  2. L37
    specialize prime_field_convolution_coefficient_zero_past_support (p)
  3. L38
    specialize prime_field_convolution_coefficient_zero_past_support (ab)
  4. L39
    specialize prime_field_convolution_coefficient_zero_past_support (ac)
  5. L40
    specialize prime_field_convolution_coefficient_zero_past_support (i)
  6. L41
    specialize prime_field_convolution_coefficient_zero_past_support (bb)
  7. L42
    specialize prime_field_convolution_coefficient_zero_past_support (bc)
  8. L43
    specialize prime_field_convolution_coefficient_zero_past_support (1)
  9. L44
    specialize prime_field_convolution_coefficient_zero_past_support (i)
  10. L45
    specialize prime_field_convolution_coefficient_zero_past_support (x)
08Use earlier factsL46–47

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

  1. L46
    apply prime_field_convolution_coefficient_zero_past_support
  2. L47
    exact hp0
09Construct an explicit witnessL48–48

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

  1. L48
    exists 0
10Calculate and transport equalitiesL49–49

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

  1. L49
    simp [zero_add]
11Use earlier factsL50–50

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

  1. L50
    exact hc_witness
12Establish hshortL51–60

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

  1. L51
    have hshort : FpConvolutionCoefficient(p,ab,ac,S i,bb,bc,1,i,r)Definitions: FpConvolutionCoefficient
  2. L52
    specialize prime_field_convolution_coefficient_prefix_transport (p)
  3. L53
    specialize prime_field_convolution_coefficient_prefix_transport (ab)
  4. L54
    specialize prime_field_convolution_coefficient_prefix_transport (ac)
  5. L55
    specialize prime_field_convolution_coefficient_prefix_transport (L)
  6. L56
    specialize prime_field_convolution_coefficient_prefix_transport (ab)
  7. L57
    specialize prime_field_convolution_coefficient_prefix_transport (ac)
  8. L58
    specialize prime_field_convolution_coefficient_prefix_transport (S i)
  9. L59
    specialize prime_field_convolution_coefficient_prefix_transport (bb)
  10. L60
    specialize prime_field_convolution_coefficient_prefix_transport (bc)
13Use earlier factsL61–68

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

  1. L61
    specialize prime_field_convolution_coefficient_prefix_transport (1)
  2. L62
    specialize prime_field_convolution_coefficient_prefix_transport (S i)
  3. L63
    specialize prime_field_convolution_coefficient_prefix_transport (i)
  4. L64
    specialize prime_field_convolution_coefficient_prefix_transport (r)
  5. L65
    apply prime_field_convolution_coefficient_prefix_transport
  6. L66
    exact hi
  7. L67
    specialize le_refl (S i)
  8. L68
    apply le_refl
14Fix variables and assumptionsL69–72

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

  1. L69
    intro j
  2. L70
    intro z
  3. L71
    intro hj
  4. L72
    intro hz
15Use earlier factsL73–76

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

  1. L73
    exact hz
  2. L74
    specialize le_refl (S i)
  3. L75
    apply le_refl
  4. L76
    exact hr
16Establish hmL77–86

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

  1. L77
    have hm : ∃ z. FpMul(p,a,k,z)Definitions: FpMul
  2. L78
    specialize prime_field_multiply_exists (p)
  3. L79
    specialize prime_field_multiply_exists (a)
  4. L80
    specialize prime_field_multiply_exists (k)
  5. L81
    apply prime_field_multiply_exists
  6. L82
    exact hp
  7. L83
    specialize matrix_rank_bounded_prefix_value (ab)
  8. L84
    specialize matrix_rank_bounded_prefix_value (ac)
  9. L85
    specialize matrix_rank_bounded_prefix_value (L)
  10. L86
    specialize matrix_rank_bounded_prefix_value (p)
17Use earlier factsL87–96

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

  1. L87
    specialize matrix_rank_bounded_prefix_value (i)
  2. L88
    specialize matrix_rank_bounded_prefix_value (a)
  3. L89
    apply matrix_rank_bounded_prefix_value
  4. L90
    exact hA
  5. L91
    exact hi
  6. L92
    exact ha
  7. L93
    specialize matrix_rank_bounded_prefix_value (bb)
  8. L94
    specialize matrix_rank_bounded_prefix_value (bc)
  9. L95
    specialize matrix_rank_bounded_prefix_value (1)
  10. L96
    specialize matrix_rank_bounded_prefix_value (p)
18Use earlier factsL97–100

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

  1. L97
    specialize matrix_rank_bounded_prefix_value (0)
  2. L98
    specialize matrix_rank_bounded_prefix_value (k)
  3. L99
    apply matrix_rank_bounded_prefix_value
  4. L100
    exact hB
19Construct an explicit witnessL101–101

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

  1. L101
    exists 0
20Calculate and transport equalitiesL102–102

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

  1. L102
    simp [zero_add]
21Use earlier factsL103–103

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

  1. L103
    exact hk
22Separate the logical casesL104–104

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

  1. L104
    cases hm
23Establish hsL105–114

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

  1. L105
    have hs : ((exists pfa_gap_constant_actual_sumleft. pfa_gap_constant_actual_sumleft + S (x) = (p)) /\ (((exists pfa_gap_constant_actual_sumright. pfa_gap_constant_actual_sumright + S (x1) = (p)) /\ ((((exists pfa_gap_constant_actual_sumresultbound. pfa_gap_constant_actual_sumresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_constant_actual_sumresultcongruence pfa_offset_right_constant_actual_sumresultcongruence. ((x) + (x1)) + (p) * pfa_offset_left_constant_actual_sumresultcongruence = (r) + (p) * pfa_offset_right_constant_actual_sumresultcongruence))))))))
  2. L106
    specialize prime_field_convolution_coefficient_append (p)
  3. L107
    specialize prime_field_convolution_coefficient_append (ab)
  4. L108
    specialize prime_field_convolution_coefficient_append (ac)
  5. L109
    specialize prime_field_convolution_coefficient_append (ab)
  6. L110
    specialize prime_field_convolution_coefficient_append (ac)
  7. L111
    specialize prime_field_convolution_coefficient_append (bb)
  8. L112
    specialize prime_field_convolution_coefficient_append (bc)
  9. L113
    specialize prime_field_convolution_coefficient_append (0)
  10. L114
    specialize prime_field_convolution_coefficient_append (i)
24Use earlier factsL115–120

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

  1. L115
    specialize prime_field_convolution_coefficient_append (a)
  2. L116
    specialize prime_field_convolution_coefficient_append (k)
  3. L117
    specialize prime_field_convolution_coefficient_append (x)
  4. L118
    specialize prime_field_convolution_coefficient_append (x1)
  5. L119
    specialize prime_field_convolution_coefficient_append (r)
  6. L120
    apply prime_field_convolution_coefficient_append
25Fix variables and assumptionsL121–124

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

  1. L121
    intro j
  2. L122
    intro z
  3. L123
    intro hj
  4. L124
    intro hz
26Use earlier factsL125–130

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

  1. L125
    exact hz
  2. L126
    exact ha
  3. L127
    exact hk
  4. L128
    exact hc_witness
  5. L129
    exact hshort
  6. L130
    exact hm_witness
27Calculate and transport equalitiesL131–132

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

  1. L131
    rewrite hc0 at hs
  2. L132
    rewrite hc0 at hs
28Establish heqL133–142

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

  1. L133
    have heq : r=x1
  2. L134
    specialize prime_field_add_functional (p)
  3. L135
    specialize prime_field_add_functional (0)
  4. L136
    specialize prime_field_add_functional (x1)
  5. L137
    specialize prime_field_add_functional (r)
  6. L138
    specialize prime_field_add_functional (x1)
  7. L139
    apply prime_field_add_functional
  8. L140
    exact hs
  9. L141
    specialize prime_field_add_zero_left (p)
  10. L142
    specialize prime_field_add_zero_left (x1)
29Use earlier factsL143–144

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

  1. L143
    apply prime_field_add_zero_left
  2. L144
    exact hp
30Establish hmcL145–146

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

  1. L145
    have hmc : ((exists pfa_gap_constant_product_copyleft. pfa_gap_constant_product_copyleft + S (a) = (p)) /\ (((exists pfa_gap_constant_product_copyright. pfa_gap_constant_product_copyright + S (k) = (p)) /\ ((((exists pfa_gap_constant_product_copyresultbound. pfa_gap_constant_product_copyresultbound + S (x1) = (p)) /\ ((exists pfa_offset_left_constant_product_copyresultcongruence pfa_offset_right_constant_product_copyresultcongruence. ((a) * (k)) + (p) * pfa_offset_left_constant_product_copyresultcongruence = (x1) + (p) * pfa_offset_right_constant_product_copyresultcongruence))))))))
  2. L146
    exact hm_witness
31Separate the logical casesL147–149

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

  1. L147
    cases hmc
  2. L148
    cases hmc_right
  3. L149
    cases hmc_right_right
32Use earlier factsL150–150

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

  1. L150
    exact hmc_right_right_left
33Calculate and transport equalitiesL151–152

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

  1. L151
    rewrite heq
  2. L152
    rewrite heq
34Use earlier factsL153–158

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

  1. L153
    specialize prime_field_multiply_commutative (p)
  2. L154
    specialize prime_field_multiply_commutative (a)
  3. L155
    specialize prime_field_multiply_commutative (k)
  4. L156
    specialize prime_field_multiply_commutative (x1)
  5. L157
    apply prime_field_multiply_commutative
  6. L158
    exact hm_witness

Library-wide reading audit

Original exact command ledger · 158 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro k
  8. 0008intro i
  9. 0009intro a
  10. 0010intro r
  11. 0011intro hp
  12. 0012intro hA
  13. 0013intro hB
  14. 0014intro hk
  15. 0015intro hi
  16. 0016intro ha
  17. 0017intro hr
  18. 0018have hp0 : ~(p=0)
  19. 0019intro hpzero
  20. 0020specialize prime_nonzero (p)
  21. 0021apply prime_nonzero
  22. 0022exact hp
  23. 0023exact hpzero
  24. 0024have hc : exists c. (exists pfc_terms_code_constant_old_coefficient pfc_terms_scale_constant_old_coefficient pfc_natural_sum_constant_old_coefficient. ((forall pfc_index_constant_old_coefficientdiagonal. (exists pfa_gap_constant_old_coefficientdiagonalbound. pfa_gap_constant_old_coefficientdiagonalbound + S (pfc_index_constant_old_coefficientdiagonal) = (S (i))) -> exists pfc_value_constant_old_coefficientdiagonal. ((((exists ff_h_pfp_constant_old_coefficientdiagonalentry. ff_h_pfp_constant_old_coefficientdiagonalentry + S (pfc_value_constant_old_coefficientdiagonal) = S ((S (pfc_index_constant_old_coefficientdiagonal)) * pfc_terms_scale_constant_old_coefficient)) /\ exists ff_q_pfp_constant_old_coefficientdiagonalentry. pfc_terms_code_constant_old_coefficient = ff_q_pfp_constant_old_coefficientdiagonalentry * S ((S (pfc_index_constant_old_coefficientdiagonal)) * pfc_terms_scale_constant_old_coefficient) + (pfc_value_constant_old_coefficientdiagonal))) /\ ((exists pfc_complement_constant_old_coefficientdiagonalterm pfc_left_constant_old_coefficientdiagonalterm pfc_right_constant_old_coefficientdiagonalterm. (((pfc_index_constant_old_coefficientdiagonal)+pfc_complement_constant_old_coefficientdiagonalterm=(i)) /\ ((((((exists pfa_gap_constant_old_coefficientdiagonaltermleftinside. pfa_gap_constant_old_coefficientdiagonaltermleftinside + S (pfc_index_constant_old_coefficientdiagonal) = (i)) /\ ((((exists ff_h_pfp_constant_old_coefficientdiagonaltermleftentry. ff_h_pfp_constant_old_coefficientdiagonaltermleftentry + S (pfc_left_constant_old_coefficientdiagonalterm) = S ((S (pfc_index_constant_old_coefficientdiagonal)) * ac)) /\ exists ff_q_pfp_constant_old_coefficientdiagonaltermleftentry. ab = ff_q_pfp_constant_old_coefficientdiagonaltermleftentry * S ((S (pfc_index_constant_old_coefficientdiagonal)) * ac) + (pfc_left_constant_old_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_constant_old_coefficientdiagonaltermleftoutside. pfc_gap_constant_old_coefficientdiagonaltermleftoutside+(i)=(pfc_index_constant_old_coefficientdiagonal)) /\ (((pfc_left_constant_old_coefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_constant_old_coefficientdiagonaltermrightinside. pfa_gap_constant_old_coefficientdiagonaltermrightinside + S (pfc_complement_constant_old_coefficientdiagonalterm) = (1)) /\ ((((exists ff_h_pfp_constant_old_coefficientdiagonaltermrightentry. ff_h_pfp_constant_old_coefficientdiagonaltermrightentry + S (pfc_right_constant_old_coefficientdiagonalterm) = S ((S (pfc_complement_constant_old_coefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_constant_old_coefficientdiagonaltermrightentry. bb = ff_q_pfp_constant_old_coefficientdiagonaltermrightentry * S ((S (pfc_complement_constant_old_coefficientdiagonalterm)) * bc) + (pfc_right_constant_old_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_constant_old_coefficientdiagonaltermrightoutside. pfc_gap_constant_old_coefficientdiagonaltermrightoutside+(1)=(pfc_complement_constant_old_coefficientdiagonalterm)) /\ (((pfc_right_constant_old_coefficientdiagonalterm)=0))))) /\ (((pfc_value_constant_old_coefficientdiagonal)=pfc_left_constant_old_coefficientdiagonalterm*pfc_right_constant_old_coefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_constant_old_coefficientsum fs_v_pfc_constant_old_coefficientsum. ((((exists fs_h_pfc_constant_old_coefficientsum_body_start. fs_h_pfc_constant_old_coefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_constant_old_coefficientsum)) /\ exists fs_q_pfc_constant_old_coefficientsum_body_start. fs_u_pfc_constant_old_coefficientsum = fs_q_pfc_constant_old_coefficientsum_body_start * S ((S (0)) * fs_v_pfc_constant_old_coefficientsum) + (0))) /\ ((((exists fs_h_pfc_constant_old_coefficientsum_body_terminal. fs_h_pfc_constant_old_coefficientsum_body_terminal + S (pfc_natural_sum_constant_old_coefficient) = S ((S (S (i))) * fs_v_pfc_constant_old_coefficientsum)) /\ exists fs_q_pfc_constant_old_coefficientsum_body_terminal. fs_u_pfc_constant_old_coefficientsum = fs_q_pfc_constant_old_coefficientsum_body_terminal * S ((S (S (i))) * fs_v_pfc_constant_old_coefficientsum) + (pfc_natural_sum_constant_old_coefficient))) /\ forall fs_i_pfc_constant_old_coefficientsum_body_steps. (exists fs_lt_pfc_constant_old_coefficientsum_body_steps_bound. fs_lt_pfc_constant_old_coefficientsum_body_steps_bound + S fs_i_pfc_constant_old_coefficientsum_body_steps = S (i)) -> exists fs_a_pfc_constant_old_coefficientsum_body_steps fs_r_pfc_constant_old_coefficientsum_body_steps fs_s_pfc_constant_old_coefficientsum_body_steps. ((((exists fs_h_pfc_constant_old_coefficientsum_body_steps_summand. fs_h_pfc_constant_old_coefficientsum_body_steps_summand + S (fs_a_pfc_constant_old_coefficientsum_body_steps) = S ((S (fs_i_pfc_constant_old_coefficientsum_body_steps)) * pfc_terms_scale_constant_old_coefficient)) /\ exists fs_q_pfc_constant_old_coefficientsum_body_steps_summand. pfc_terms_code_constant_old_coefficient = fs_q_pfc_constant_old_coefficientsum_body_steps_summand * S ((S (fs_i_pfc_constant_old_coefficientsum_body_steps)) * pfc_terms_scale_constant_old_coefficient) + (fs_a_pfc_constant_old_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_constant_old_coefficientsum_body_steps_partial. fs_h_pfc_constant_old_coefficientsum_body_steps_partial + S (fs_r_pfc_constant_old_coefficientsum_body_steps) = S ((S (fs_i_pfc_constant_old_coefficientsum_body_steps)) * fs_v_pfc_constant_old_coefficientsum)) /\ exists fs_q_pfc_constant_old_coefficientsum_body_steps_partial. fs_u_pfc_constant_old_coefficientsum = fs_q_pfc_constant_old_coefficientsum_body_steps_partial * S ((S (fs_i_pfc_constant_old_coefficientsum_body_steps)) * fs_v_pfc_constant_old_coefficientsum) + (fs_r_pfc_constant_old_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_constant_old_coefficientsum_body_steps_successor. fs_h_pfc_constant_old_coefficientsum_body_steps_successor + S (fs_s_pfc_constant_old_coefficientsum_body_steps) = S ((S (S fs_i_pfc_constant_old_coefficientsum_body_steps)) * fs_v_pfc_constant_old_coefficientsum)) /\ exists fs_q_pfc_constant_old_coefficientsum_body_steps_successor. fs_u_pfc_constant_old_coefficientsum = fs_q_pfc_constant_old_coefficientsum_body_steps_successor * S ((S (S fs_i_pfc_constant_old_coefficientsum_body_steps)) * fs_v_pfc_constant_old_coefficientsum) + (fs_s_pfc_constant_old_coefficientsum_body_steps))) /\ fs_s_pfc_constant_old_coefficientsum_body_steps = fs_r_pfc_constant_old_coefficientsum_body_steps + fs_a_pfc_constant_old_coefficientsum_body_steps)))))) /\ ((((exists pfa_gap_constant_old_coefficientresiduebound. pfa_gap_constant_old_coefficientresiduebound + S (c) = (p)) /\ ((exists pfa_offset_left_constant_old_coefficientresiduecongruence pfa_offset_right_constant_old_coefficientresiduecongruence. (pfc_natural_sum_constant_old_coefficient) + (p) * pfa_offset_left_constant_old_coefficientresiduecongruence = (c) + (p) * pfa_offset_right_constant_old_coefficientresiduecongruence)))))))))
  25. 0025specialize prime_field_convolution_coefficient_exists (p)
  26. 0026specialize prime_field_convolution_coefficient_exists (ab)
  27. 0027specialize prime_field_convolution_coefficient_exists (ac)
  28. 0028specialize prime_field_convolution_coefficient_exists (i)
  29. 0029specialize prime_field_convolution_coefficient_exists (bb)
  30. 0030specialize prime_field_convolution_coefficient_exists (bc)
  31. 0031specialize prime_field_convolution_coefficient_exists (1)
  32. 0032specialize prime_field_convolution_coefficient_exists (i)
  33. 0033apply prime_field_convolution_coefficient_exists
  34. 0034exact hp0
  35. 0035cases hc
  36. 0036have hc0 : x=0
  37. 0037specialize prime_field_convolution_coefficient_zero_past_support (p)
  38. 0038specialize prime_field_convolution_coefficient_zero_past_support (ab)
  39. 0039specialize prime_field_convolution_coefficient_zero_past_support (ac)
  40. 0040specialize prime_field_convolution_coefficient_zero_past_support (i)
  41. 0041specialize prime_field_convolution_coefficient_zero_past_support (bb)
  42. 0042specialize prime_field_convolution_coefficient_zero_past_support (bc)
  43. 0043specialize prime_field_convolution_coefficient_zero_past_support (1)
  44. 0044specialize prime_field_convolution_coefficient_zero_past_support (i)
  45. 0045specialize prime_field_convolution_coefficient_zero_past_support (x)
  46. 0046apply prime_field_convolution_coefficient_zero_past_support
  47. 0047exact hp0
  48. 0048exists 0
  49. 0049simp [zero_add]
  50. 0050exact hc_witness
  51. 0051have hshort : exists pfc_terms_code_constant_short_coefficient pfc_terms_scale_constant_short_coefficient pfc_natural_sum_constant_short_coefficient. ((forall pfc_index_constant_short_coefficientdiagonal. (exists pfa_gap_constant_short_coefficientdiagonalbound. pfa_gap_constant_short_coefficientdiagonalbound + S (pfc_index_constant_short_coefficientdiagonal) = (S (i))) -> exists pfc_value_constant_short_coefficientdiagonal. ((((exists ff_h_pfp_constant_short_coefficientdiagonalentry. ff_h_pfp_constant_short_coefficientdiagonalentry + S (pfc_value_constant_short_coefficientdiagonal) = S ((S (pfc_index_constant_short_coefficientdiagonal)) * pfc_terms_scale_constant_short_coefficient)) /\ exists ff_q_pfp_constant_short_coefficientdiagonalentry. pfc_terms_code_constant_short_coefficient = ff_q_pfp_constant_short_coefficientdiagonalentry * S ((S (pfc_index_constant_short_coefficientdiagonal)) * pfc_terms_scale_constant_short_coefficient) + (pfc_value_constant_short_coefficientdiagonal))) /\ ((exists pfc_complement_constant_short_coefficientdiagonalterm pfc_left_constant_short_coefficientdiagonalterm pfc_right_constant_short_coefficientdiagonalterm. (((pfc_index_constant_short_coefficientdiagonal)+pfc_complement_constant_short_coefficientdiagonalterm=(i)) /\ ((((((exists pfa_gap_constant_short_coefficientdiagonaltermleftinside. pfa_gap_constant_short_coefficientdiagonaltermleftinside + S (pfc_index_constant_short_coefficientdiagonal) = (S i)) /\ ((((exists ff_h_pfp_constant_short_coefficientdiagonaltermleftentry. ff_h_pfp_constant_short_coefficientdiagonaltermleftentry + S (pfc_left_constant_short_coefficientdiagonalterm) = S ((S (pfc_index_constant_short_coefficientdiagonal)) * ac)) /\ exists ff_q_pfp_constant_short_coefficientdiagonaltermleftentry. ab = ff_q_pfp_constant_short_coefficientdiagonaltermleftentry * S ((S (pfc_index_constant_short_coefficientdiagonal)) * ac) + (pfc_left_constant_short_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_constant_short_coefficientdiagonaltermleftoutside. pfc_gap_constant_short_coefficientdiagonaltermleftoutside+(S i)=(pfc_index_constant_short_coefficientdiagonal)) /\ (((pfc_left_constant_short_coefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_constant_short_coefficientdiagonaltermrightinside. pfa_gap_constant_short_coefficientdiagonaltermrightinside + S (pfc_complement_constant_short_coefficientdiagonalterm) = (1)) /\ ((((exists ff_h_pfp_constant_short_coefficientdiagonaltermrightentry. ff_h_pfp_constant_short_coefficientdiagonaltermrightentry + S (pfc_right_constant_short_coefficientdiagonalterm) = S ((S (pfc_complement_constant_short_coefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_constant_short_coefficientdiagonaltermrightentry. bb = ff_q_pfp_constant_short_coefficientdiagonaltermrightentry * S ((S (pfc_complement_constant_short_coefficientdiagonalterm)) * bc) + (pfc_right_constant_short_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_constant_short_coefficientdiagonaltermrightoutside. pfc_gap_constant_short_coefficientdiagonaltermrightoutside+(1)=(pfc_complement_constant_short_coefficientdiagonalterm)) /\ (((pfc_right_constant_short_coefficientdiagonalterm)=0))))) /\ (((pfc_value_constant_short_coefficientdiagonal)=pfc_left_constant_short_coefficientdiagonalterm*pfc_right_constant_short_coefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_constant_short_coefficientsum fs_v_pfc_constant_short_coefficientsum. ((((exists fs_h_pfc_constant_short_coefficientsum_body_start. fs_h_pfc_constant_short_coefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_constant_short_coefficientsum)) /\ exists fs_q_pfc_constant_short_coefficientsum_body_start. fs_u_pfc_constant_short_coefficientsum = fs_q_pfc_constant_short_coefficientsum_body_start * S ((S (0)) * fs_v_pfc_constant_short_coefficientsum) + (0))) /\ ((((exists fs_h_pfc_constant_short_coefficientsum_body_terminal. fs_h_pfc_constant_short_coefficientsum_body_terminal + S (pfc_natural_sum_constant_short_coefficient) = S ((S (S (i))) * fs_v_pfc_constant_short_coefficientsum)) /\ exists fs_q_pfc_constant_short_coefficientsum_body_terminal. fs_u_pfc_constant_short_coefficientsum = fs_q_pfc_constant_short_coefficientsum_body_terminal * S ((S (S (i))) * fs_v_pfc_constant_short_coefficientsum) + (pfc_natural_sum_constant_short_coefficient))) /\ forall fs_i_pfc_constant_short_coefficientsum_body_steps. (exists fs_lt_pfc_constant_short_coefficientsum_body_steps_bound. fs_lt_pfc_constant_short_coefficientsum_body_steps_bound + S fs_i_pfc_constant_short_coefficientsum_body_steps = S (i)) -> exists fs_a_pfc_constant_short_coefficientsum_body_steps fs_r_pfc_constant_short_coefficientsum_body_steps fs_s_pfc_constant_short_coefficientsum_body_steps. ((((exists fs_h_pfc_constant_short_coefficientsum_body_steps_summand. fs_h_pfc_constant_short_coefficientsum_body_steps_summand + S (fs_a_pfc_constant_short_coefficientsum_body_steps) = S ((S (fs_i_pfc_constant_short_coefficientsum_body_steps)) * pfc_terms_scale_constant_short_coefficient)) /\ exists fs_q_pfc_constant_short_coefficientsum_body_steps_summand. pfc_terms_code_constant_short_coefficient = fs_q_pfc_constant_short_coefficientsum_body_steps_summand * S ((S (fs_i_pfc_constant_short_coefficientsum_body_steps)) * pfc_terms_scale_constant_short_coefficient) + (fs_a_pfc_constant_short_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_constant_short_coefficientsum_body_steps_partial. fs_h_pfc_constant_short_coefficientsum_body_steps_partial + S (fs_r_pfc_constant_short_coefficientsum_body_steps) = S ((S (fs_i_pfc_constant_short_coefficientsum_body_steps)) * fs_v_pfc_constant_short_coefficientsum)) /\ exists fs_q_pfc_constant_short_coefficientsum_body_steps_partial. fs_u_pfc_constant_short_coefficientsum = fs_q_pfc_constant_short_coefficientsum_body_steps_partial * S ((S (fs_i_pfc_constant_short_coefficientsum_body_steps)) * fs_v_pfc_constant_short_coefficientsum) + (fs_r_pfc_constant_short_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_constant_short_coefficientsum_body_steps_successor. fs_h_pfc_constant_short_coefficientsum_body_steps_successor + S (fs_s_pfc_constant_short_coefficientsum_body_steps) = S ((S (S fs_i_pfc_constant_short_coefficientsum_body_steps)) * fs_v_pfc_constant_short_coefficientsum)) /\ exists fs_q_pfc_constant_short_coefficientsum_body_steps_successor. fs_u_pfc_constant_short_coefficientsum = fs_q_pfc_constant_short_coefficientsum_body_steps_successor * S ((S (S fs_i_pfc_constant_short_coefficientsum_body_steps)) * fs_v_pfc_constant_short_coefficientsum) + (fs_s_pfc_constant_short_coefficientsum_body_steps))) /\ fs_s_pfc_constant_short_coefficientsum_body_steps = fs_r_pfc_constant_short_coefficientsum_body_steps + fs_a_pfc_constant_short_coefficientsum_body_steps)))))) /\ ((((exists pfa_gap_constant_short_coefficientresiduebound. pfa_gap_constant_short_coefficientresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_constant_short_coefficientresiduecongruence pfa_offset_right_constant_short_coefficientresiduecongruence. (pfc_natural_sum_constant_short_coefficient) + (p) * pfa_offset_left_constant_short_coefficientresiduecongruence = (r) + (p) * pfa_offset_right_constant_short_coefficientresiduecongruence))))))))
  52. 0052specialize prime_field_convolution_coefficient_prefix_transport (p)
  53. 0053specialize prime_field_convolution_coefficient_prefix_transport (ab)
  54. 0054specialize prime_field_convolution_coefficient_prefix_transport (ac)
  55. 0055specialize prime_field_convolution_coefficient_prefix_transport (L)
  56. 0056specialize prime_field_convolution_coefficient_prefix_transport (ab)
  57. 0057specialize prime_field_convolution_coefficient_prefix_transport (ac)
  58. 0058specialize prime_field_convolution_coefficient_prefix_transport (S i)
  59. 0059specialize prime_field_convolution_coefficient_prefix_transport (bb)
  60. 0060specialize prime_field_convolution_coefficient_prefix_transport (bc)
  61. 0061specialize prime_field_convolution_coefficient_prefix_transport (1)
  62. 0062specialize prime_field_convolution_coefficient_prefix_transport (S i)
  63. 0063specialize prime_field_convolution_coefficient_prefix_transport (i)
  64. 0064specialize prime_field_convolution_coefficient_prefix_transport (r)
  65. 0065apply prime_field_convolution_coefficient_prefix_transport
  66. 0066exact hi
  67. 0067specialize le_refl (S i)
  68. 0068apply le_refl
  69. 0069intro j
  70. 0070intro z
  71. 0071intro hj
  72. 0072intro hz
  73. 0073exact hz
  74. 0074specialize le_refl (S i)
  75. 0075apply le_refl
  76. 0076exact hr
  77. 0077have hm : exists z. (((exists pfa_gap_constant_chosen_productleft. pfa_gap_constant_chosen_productleft + S (a) = (p)) /\ (((exists pfa_gap_constant_chosen_productright. pfa_gap_constant_chosen_productright + S (k) = (p)) /\ ((((exists pfa_gap_constant_chosen_productresultbound. pfa_gap_constant_chosen_productresultbound + S (z) = (p)) /\ ((exists pfa_offset_left_constant_chosen_productresultcongruence pfa_offset_right_constant_chosen_productresultcongruence. ((a) * (k)) + (p) * pfa_offset_left_constant_chosen_productresultcongruence = (z) + (p) * pfa_offset_right_constant_chosen_productresultcongruence)))))))))
  78. 0078specialize prime_field_multiply_exists (p)
  79. 0079specialize prime_field_multiply_exists (a)
  80. 0080specialize prime_field_multiply_exists (k)
  81. 0081apply prime_field_multiply_exists
  82. 0082exact hp
  83. 0083specialize matrix_rank_bounded_prefix_value (ab)
  84. 0084specialize matrix_rank_bounded_prefix_value (ac)
  85. 0085specialize matrix_rank_bounded_prefix_value (L)
  86. 0086specialize matrix_rank_bounded_prefix_value (p)
  87. 0087specialize matrix_rank_bounded_prefix_value (i)
  88. 0088specialize matrix_rank_bounded_prefix_value (a)
  89. 0089apply matrix_rank_bounded_prefix_value
  90. 0090exact hA
  91. 0091exact hi
  92. 0092exact ha
  93. 0093specialize matrix_rank_bounded_prefix_value (bb)
  94. 0094specialize matrix_rank_bounded_prefix_value (bc)
  95. 0095specialize matrix_rank_bounded_prefix_value (1)
  96. 0096specialize matrix_rank_bounded_prefix_value (p)
  97. 0097specialize matrix_rank_bounded_prefix_value (0)
  98. 0098specialize matrix_rank_bounded_prefix_value (k)
  99. 0099apply matrix_rank_bounded_prefix_value
  100. 0100exact hB
  101. 0101exists 0
  102. 0102simp [zero_add]
  103. 0103exact hk
  104. 0104cases hm
  105. 0105have hs : ((exists pfa_gap_constant_actual_sumleft. pfa_gap_constant_actual_sumleft + S (x) = (p)) /\ (((exists pfa_gap_constant_actual_sumright. pfa_gap_constant_actual_sumright + S (x1) = (p)) /\ ((((exists pfa_gap_constant_actual_sumresultbound. pfa_gap_constant_actual_sumresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_constant_actual_sumresultcongruence pfa_offset_right_constant_actual_sumresultcongruence. ((x) + (x1)) + (p) * pfa_offset_left_constant_actual_sumresultcongruence = (r) + (p) * pfa_offset_right_constant_actual_sumresultcongruence))))))))
  106. 0106specialize prime_field_convolution_coefficient_append (p)
  107. 0107specialize prime_field_convolution_coefficient_append (ab)
  108. 0108specialize prime_field_convolution_coefficient_append (ac)
  109. 0109specialize prime_field_convolution_coefficient_append (ab)
  110. 0110specialize prime_field_convolution_coefficient_append (ac)
  111. 0111specialize prime_field_convolution_coefficient_append (bb)
  112. 0112specialize prime_field_convolution_coefficient_append (bc)
  113. 0113specialize prime_field_convolution_coefficient_append (0)
  114. 0114specialize prime_field_convolution_coefficient_append (i)
  115. 0115specialize prime_field_convolution_coefficient_append (a)
  116. 0116specialize prime_field_convolution_coefficient_append (k)
  117. 0117specialize prime_field_convolution_coefficient_append (x)
  118. 0118specialize prime_field_convolution_coefficient_append (x1)
  119. 0119specialize prime_field_convolution_coefficient_append (r)
  120. 0120apply prime_field_convolution_coefficient_append
  121. 0121intro j
  122. 0122intro z
  123. 0123intro hj
  124. 0124intro hz
  125. 0125exact hz
  126. 0126exact ha
  127. 0127exact hk
  128. 0128exact hc_witness
  129. 0129exact hshort
  130. 0130exact hm_witness
  131. 0131rewrite hc0 at hs
  132. 0132rewrite hc0 at hs
  133. 0133have heq : r=x1
  134. 0134specialize prime_field_add_functional (p)
  135. 0135specialize prime_field_add_functional (0)
  136. 0136specialize prime_field_add_functional (x1)
  137. 0137specialize prime_field_add_functional (r)
  138. 0138specialize prime_field_add_functional (x1)
  139. 0139apply prime_field_add_functional
  140. 0140exact hs
  141. 0141specialize prime_field_add_zero_left (p)
  142. 0142specialize prime_field_add_zero_left (x1)
  143. 0143apply prime_field_add_zero_left
  144. 0144exact hp
  145. 0145have hmc : ((exists pfa_gap_constant_product_copyleft. pfa_gap_constant_product_copyleft + S (a) = (p)) /\ (((exists pfa_gap_constant_product_copyright. pfa_gap_constant_product_copyright + S (k) = (p)) /\ ((((exists pfa_gap_constant_product_copyresultbound. pfa_gap_constant_product_copyresultbound + S (x1) = (p)) /\ ((exists pfa_offset_left_constant_product_copyresultcongruence pfa_offset_right_constant_product_copyresultcongruence. ((a) * (k)) + (p) * pfa_offset_left_constant_product_copyresultcongruence = (x1) + (p) * pfa_offset_right_constant_product_copyresultcongruence))))))))
  146. 0146exact hm_witness
  147. 0147cases hmc
  148. 0148cases hmc_right
  149. 0149cases hmc_right_right
  150. 0150exact hmc_right_right_left
  151. 0151rewrite heq
  152. 0152rewrite heq
  153. 0153specialize prime_field_multiply_commutative (p)
  154. 0154specialize prime_field_multiply_commutative (a)
  155. 0155specialize prime_field_multiply_commutative (k)
  156. 0156specialize prime_field_multiply_commutative (x1)
  157. 0157apply prime_field_multiply_commutative
  158. 0158exact hm_witness