PX0023

prime_field_polynomial_constant_right_coefficient

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

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

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

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

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ k. ∀ i. ∀ a. ∀ r. Prime(p) → BetaPrefixInto(ab,ac,L,p) → BetaPrefixInto(bb,bc,1,p) → BetaAt(bb,bc,0,k) → Lt(i,L) → BetaAt(ab,ac,i,a) → FpConvolutionCoefficient(p,ab,ac,L,bb,bc,1,i,r) → FpMul(p,k,a,r)

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

Definition DAG

FpAdd(p,a,b,c) · 1FpMul(p,a,b,c) · 3BetaPrefixInto(b,c,l,B) · 2FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,r) · 3Lt(a,b) · 1Prime(p) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

prime_nonzero · checked external prerequisiteprime_field_convolution_coefficient_exists · checked external prerequisiteprime_field_convolution_coefficient_zero_past_support · checked external prerequisitezero_add · checked external prerequisiteprime_field_convolution_coefficient_prefix_transportle_refl · checked external prerequisiteprime_field_multiply_exists · checked external prerequisitematrix_rank_bounded_prefix_value · checked external prerequisiteprime_field_convolution_coefficient_appendprime_field_add_functional · checked external prerequisiteprime_field_add_zero_left · checked external prerequisiteprime_field_multiply_commutative · checked external prerequisite
Original expanded first-order 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)))))))))

Complete tactic proof in conservative notation

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

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.

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 (2)
prime field convolution coefficient prefix transportprime field convolution coefficient append
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(p,ab,ac,i,bb,bc,1,i,c)Original native command in the exact edition
  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(p,ab,ac,S i,bb,bc,1,i,r)Original native command in the exact edition
  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(p,a,k,z)Original native command in the exact edition
  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
  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
  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 defined 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 : ∃ c. FpConvolutionCoefficient(p,ab,ac,i,bb,bc,1,i,c)
  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 : FpConvolutionCoefficient(p,ab,ac,S i,bb,bc,1,i,r)
  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 : ∃ z. FpMul(p,a,k,z)
  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 : FpAdd(p,x,x1,r)
  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 : FpMul(p,a,k,x1)
  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