PX0069

prime_field_convolution_coefficient_before_left_padding_right

Every actual convolution coefficient before the added leading block is zero at a nonzero modulus.

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. ∀ M. ∀ BB. ∀ BC. ∀ t. ∀ i. ∀ r. ¬p = 0 → PolynomialLeftPad(bb,bc,M,t,BB,BC) → Lt(i,t) → FpConvolutionCoefficient(p,ab,ac,L,BB,BC,t + M,i,r) → r = 0

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

Definition DAG

PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t) · 1FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,r) · 1PolynomialLeftPad(b,c,L,t,d,e) · 1Lt(a,b) · 1BetaAt(b,c,i,x) · 1Repeat(b,c,a,l) · 1

Actual proof prerequisites

polynomial_diagonal_term_left_padding_zero_rightle_trans · checked external prerequisitebeta_repeat_sum_exact · checked external prerequisiteprime_field_residue_bounded_value · checked external prerequisiteone_le_of_ne_zero · checked external prerequisitele_add_right · checked external prerequisite
Original expanded first-order statement 
forall p ab ac L bb bc M BB BC t i r. (~(p=0)) -> (((forall pfp_repeat_index_before_coefficient_pad_rightzeros. (exists pfa_gap_before_coefficient_pad_rightzerosindex. pfa_gap_before_coefficient_pad_rightzerosindex + S (pfp_repeat_index_before_coefficient_pad_rightzeros) = (t)) -> (((exists ff_h_pfp_before_coefficient_pad_rightzerosentry. ff_h_pfp_before_coefficient_pad_rightzerosentry + S (0) = S ((S (pfp_repeat_index_before_coefficient_pad_rightzeros)) * BC)) /\ exists ff_q_pfp_before_coefficient_pad_rightzerosentry. BB = ff_q_pfp_before_coefficient_pad_rightzerosentry * S ((S (pfp_repeat_index_before_coefficient_pad_rightzeros)) * BC) + (0)))) /\ ((forall pfrep_index_before_coefficient_pad_right pfrep_value_before_coefficient_pad_right. (exists pfa_gap_before_coefficient_pad_rightbound. pfa_gap_before_coefficient_pad_rightbound + S (pfrep_index_before_coefficient_pad_right) = (M)) -> (((exists ff_h_pfp_before_coefficient_pad_rightinput. ff_h_pfp_before_coefficient_pad_rightinput + S (pfrep_value_before_coefficient_pad_right) = S ((S (pfrep_index_before_coefficient_pad_right)) * bc)) /\ exists ff_q_pfp_before_coefficient_pad_rightinput. bb = ff_q_pfp_before_coefficient_pad_rightinput * S ((S (pfrep_index_before_coefficient_pad_right)) * bc) + (pfrep_value_before_coefficient_pad_right))) -> (((exists ff_h_pfp_before_coefficient_pad_rightoutput. ff_h_pfp_before_coefficient_pad_rightoutput + S (pfrep_value_before_coefficient_pad_right) = S ((S ((t)+pfrep_index_before_coefficient_pad_right)) * BC)) /\ exists ff_q_pfp_before_coefficient_pad_rightoutput. BB = ff_q_pfp_before_coefficient_pad_rightoutput * S ((S ((t)+pfrep_index_before_coefficient_pad_right)) * BC) + (pfrep_value_before_coefficient_pad_right))))))) -> (exists pfa_gap_before_coefficient_index_right. pfa_gap_before_coefficient_index_right + S (i) = (t)) -> (exists pfc_terms_code_before_coefficient_actual_right pfc_terms_scale_before_coefficient_actual_right pfc_natural_sum_before_coefficient_actual_right. ((forall pfc_index_before_coefficient_actual_rightdiagonal. (exists pfa_gap_before_coefficient_actual_rightdiagonalbound. pfa_gap_before_coefficient_actual_rightdiagonalbound + S (pfc_index_before_coefficient_actual_rightdiagonal) = (S (i))) -> exists pfc_value_before_coefficient_actual_rightdiagonal. ((((exists ff_h_pfp_before_coefficient_actual_rightdiagonalentry. ff_h_pfp_before_coefficient_actual_rightdiagonalentry + S (pfc_value_before_coefficient_actual_rightdiagonal) = S ((S (pfc_index_before_coefficient_actual_rightdiagonal)) * pfc_terms_scale_before_coefficient_actual_right)) /\ exists ff_q_pfp_before_coefficient_actual_rightdiagonalentry. pfc_terms_code_before_coefficient_actual_right = ff_q_pfp_before_coefficient_actual_rightdiagonalentry * S ((S (pfc_index_before_coefficient_actual_rightdiagonal)) * pfc_terms_scale_before_coefficient_actual_right) + (pfc_value_before_coefficient_actual_rightdiagonal))) /\ ((exists pfc_complement_before_coefficient_actual_rightdiagonalterm pfc_left_before_coefficient_actual_rightdiagonalterm pfc_right_before_coefficient_actual_rightdiagonalterm. (((pfc_index_before_coefficient_actual_rightdiagonal)+pfc_complement_before_coefficient_actual_rightdiagonalterm=(i)) /\ ((((((exists pfa_gap_before_coefficient_actual_rightdiagonaltermleftinside. pfa_gap_before_coefficient_actual_rightdiagonaltermleftinside + S (pfc_index_before_coefficient_actual_rightdiagonal) = (L)) /\ ((((exists ff_h_pfp_before_coefficient_actual_rightdiagonaltermleftentry. ff_h_pfp_before_coefficient_actual_rightdiagonaltermleftentry + S (pfc_left_before_coefficient_actual_rightdiagonalterm) = S ((S (pfc_index_before_coefficient_actual_rightdiagonal)) * ac)) /\ exists ff_q_pfp_before_coefficient_actual_rightdiagonaltermleftentry. ab = ff_q_pfp_before_coefficient_actual_rightdiagonaltermleftentry * S ((S (pfc_index_before_coefficient_actual_rightdiagonal)) * ac) + (pfc_left_before_coefficient_actual_rightdiagonalterm)))))) \/ (((exists pfc_gap_before_coefficient_actual_rightdiagonaltermleftoutside. pfc_gap_before_coefficient_actual_rightdiagonaltermleftoutside+(L)=(pfc_index_before_coefficient_actual_rightdiagonal)) /\ (((pfc_left_before_coefficient_actual_rightdiagonalterm)=0))))) /\ ((((((exists pfa_gap_before_coefficient_actual_rightdiagonaltermrightinside. pfa_gap_before_coefficient_actual_rightdiagonaltermrightinside + S (pfc_complement_before_coefficient_actual_rightdiagonalterm) = (t+M)) /\ ((((exists ff_h_pfp_before_coefficient_actual_rightdiagonaltermrightentry. ff_h_pfp_before_coefficient_actual_rightdiagonaltermrightentry + S (pfc_right_before_coefficient_actual_rightdiagonalterm) = S ((S (pfc_complement_before_coefficient_actual_rightdiagonalterm)) * BC)) /\ exists ff_q_pfp_before_coefficient_actual_rightdiagonaltermrightentry. BB = ff_q_pfp_before_coefficient_actual_rightdiagonaltermrightentry * S ((S (pfc_complement_before_coefficient_actual_rightdiagonalterm)) * BC) + (pfc_right_before_coefficient_actual_rightdiagonalterm)))))) \/ (((exists pfc_gap_before_coefficient_actual_rightdiagonaltermrightoutside. pfc_gap_before_coefficient_actual_rightdiagonaltermrightoutside+(t+M)=(pfc_complement_before_coefficient_actual_rightdiagonalterm)) /\ (((pfc_right_before_coefficient_actual_rightdiagonalterm)=0))))) /\ (((pfc_value_before_coefficient_actual_rightdiagonal)=pfc_left_before_coefficient_actual_rightdiagonalterm*pfc_right_before_coefficient_actual_rightdiagonalterm))))))))))) /\ (((exists fs_u_pfc_before_coefficient_actual_rightsum fs_v_pfc_before_coefficient_actual_rightsum. ((((exists fs_h_pfc_before_coefficient_actual_rightsum_body_start. fs_h_pfc_before_coefficient_actual_rightsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_before_coefficient_actual_rightsum)) /\ exists fs_q_pfc_before_coefficient_actual_rightsum_body_start. fs_u_pfc_before_coefficient_actual_rightsum = fs_q_pfc_before_coefficient_actual_rightsum_body_start * S ((S (0)) * fs_v_pfc_before_coefficient_actual_rightsum) + (0))) /\ ((((exists fs_h_pfc_before_coefficient_actual_rightsum_body_terminal. fs_h_pfc_before_coefficient_actual_rightsum_body_terminal + S (pfc_natural_sum_before_coefficient_actual_right) = S ((S (S (i))) * fs_v_pfc_before_coefficient_actual_rightsum)) /\ exists fs_q_pfc_before_coefficient_actual_rightsum_body_terminal. fs_u_pfc_before_coefficient_actual_rightsum = fs_q_pfc_before_coefficient_actual_rightsum_body_terminal * S ((S (S (i))) * fs_v_pfc_before_coefficient_actual_rightsum) + (pfc_natural_sum_before_coefficient_actual_right))) /\ forall fs_i_pfc_before_coefficient_actual_rightsum_body_steps. (exists fs_lt_pfc_before_coefficient_actual_rightsum_body_steps_bound. fs_lt_pfc_before_coefficient_actual_rightsum_body_steps_bound + S fs_i_pfc_before_coefficient_actual_rightsum_body_steps = S (i)) -> exists fs_a_pfc_before_coefficient_actual_rightsum_body_steps fs_r_pfc_before_coefficient_actual_rightsum_body_steps fs_s_pfc_before_coefficient_actual_rightsum_body_steps. ((((exists fs_h_pfc_before_coefficient_actual_rightsum_body_steps_summand. fs_h_pfc_before_coefficient_actual_rightsum_body_steps_summand + S (fs_a_pfc_before_coefficient_actual_rightsum_body_steps) = S ((S (fs_i_pfc_before_coefficient_actual_rightsum_body_steps)) * pfc_terms_scale_before_coefficient_actual_right)) /\ exists fs_q_pfc_before_coefficient_actual_rightsum_body_steps_summand. pfc_terms_code_before_coefficient_actual_right = fs_q_pfc_before_coefficient_actual_rightsum_body_steps_summand * S ((S (fs_i_pfc_before_coefficient_actual_rightsum_body_steps)) * pfc_terms_scale_before_coefficient_actual_right) + (fs_a_pfc_before_coefficient_actual_rightsum_body_steps))) /\ ((((exists fs_h_pfc_before_coefficient_actual_rightsum_body_steps_partial. fs_h_pfc_before_coefficient_actual_rightsum_body_steps_partial + S (fs_r_pfc_before_coefficient_actual_rightsum_body_steps) = S ((S (fs_i_pfc_before_coefficient_actual_rightsum_body_steps)) * fs_v_pfc_before_coefficient_actual_rightsum)) /\ exists fs_q_pfc_before_coefficient_actual_rightsum_body_steps_partial. fs_u_pfc_before_coefficient_actual_rightsum = fs_q_pfc_before_coefficient_actual_rightsum_body_steps_partial * S ((S (fs_i_pfc_before_coefficient_actual_rightsum_body_steps)) * fs_v_pfc_before_coefficient_actual_rightsum) + (fs_r_pfc_before_coefficient_actual_rightsum_body_steps))) /\ ((((exists fs_h_pfc_before_coefficient_actual_rightsum_body_steps_successor. fs_h_pfc_before_coefficient_actual_rightsum_body_steps_successor + S (fs_s_pfc_before_coefficient_actual_rightsum_body_steps) = S ((S (S fs_i_pfc_before_coefficient_actual_rightsum_body_steps)) * fs_v_pfc_before_coefficient_actual_rightsum)) /\ exists fs_q_pfc_before_coefficient_actual_rightsum_body_steps_successor. fs_u_pfc_before_coefficient_actual_rightsum = fs_q_pfc_before_coefficient_actual_rightsum_body_steps_successor * S ((S (S fs_i_pfc_before_coefficient_actual_rightsum_body_steps)) * fs_v_pfc_before_coefficient_actual_rightsum) + (fs_s_pfc_before_coefficient_actual_rightsum_body_steps))) /\ fs_s_pfc_before_coefficient_actual_rightsum_body_steps = fs_r_pfc_before_coefficient_actual_rightsum_body_steps + fs_a_pfc_before_coefficient_actual_rightsum_body_steps)))))) /\ ((((exists pfa_gap_before_coefficient_actual_rightresiduebound. pfa_gap_before_coefficient_actual_rightresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_before_coefficient_actual_rightresiduecongruence pfa_offset_right_before_coefficient_actual_rightresiduecongruence. (pfc_natural_sum_before_coefficient_actual_right) + (p) * pfa_offset_left_before_coefficient_actual_rightresiduecongruence = (r) + (p) * pfa_offset_right_before_coefficient_actual_rightresiduecongruence))))))))) -> (r=0)

Complete tactic proof in conservative notation

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

77 script commands · 14 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
polynomial diagonal term left padding zero right
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 M
  8. L8
    intro BB
  9. L9
    intro BC
  10. L10
    intro t
02Fix variables and assumptionsL11–16

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

  1. L11
    intro i
  2. L12
    intro r
  3. L13
    intro hp
  4. L14
    intro hpad
  5. L15
    intro hi
  6. L16
    intro hc
03Separate the logical casesL17–21

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

  1. L17
    cases hc
  2. L18
    cases hc_witness
  3. L19
    cases hc_witness_witness
  4. L20
    cases hc_witness_witness_witness
  5. L21
    cases hc_witness_witness_witness_right
04Establish hzL22–24

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

  1. L22
  2. L23
    intro j
  3. L24
    intro hj
05Establish htL25–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hc witness witness witness left.

  1. L25
    have ht : ∃ z. BetaAt(x,x1,j,z) ∧ PolynomialDiagonalTerm(ab,ac,L,BB,BC,t + M,i,j,z)Definitions: BetaAt(x,x1,j,z)PolynomialDiagonalTerm(ab,ac,L,BB,BC,t + M,i,j,z)Original native command in the exact edition
  2. L26
    specialize hc_witness_witness_witness_left (j)
  3. L27
    apply hc_witness_witness_witness_left
  4. L28
    exact hj
06Separate the logical casesL29–30

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

  1. L29
    cases ht
  2. L30
    cases ht_witness
07Establish heqL31–40

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

  1. L31
    have heq : x3=0
  2. L32
    specialize polynomial_diagonal_term_left_padding_zero_right (ab)
  3. L33
    specialize polynomial_diagonal_term_left_padding_zero_right (ac)
  4. L34
    specialize polynomial_diagonal_term_left_padding_zero_right (L)
  5. L35
    specialize polynomial_diagonal_term_left_padding_zero_right (bb)
  6. L36
    specialize polynomial_diagonal_term_left_padding_zero_right (bc)
  7. L37
    specialize polynomial_diagonal_term_left_padding_zero_right (M)
  8. L38
    specialize polynomial_diagonal_term_left_padding_zero_right (BB)
  9. L39
    specialize polynomial_diagonal_term_left_padding_zero_right (BC)
  10. L40
    specialize polynomial_diagonal_term_left_padding_zero_right (t)
08Use earlier factsL41–50

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

  1. L41
    specialize polynomial_diagonal_term_left_padding_zero_right (i)
  2. L42
    specialize polynomial_diagonal_term_left_padding_zero_right (j)
  3. L43
    specialize polynomial_diagonal_term_left_padding_zero_right (x3)
  4. L44
    apply polynomial_diagonal_term_left_padding_zero_right
  5. L45
    exact hpad
  6. L46
    specialize le_trans (S i)
  7. L47
    specialize le_trans (t)
  8. L48
    specialize le_trans (t+j)
  9. L49
    apply le_trans
  10. L50
    exact hi
09Use earlier factsL51–54

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

  1. L51
    specialize le_add_right (t)
  2. L52
    specialize le_add_right (j)
  3. L53
    apply le_add_right
  4. L54
    exact ht_witness_right
10Calculate and transport equalitiesL55–56

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

  1. L55
    rewrite heq at ht_witness_left
  2. L56
    rewrite heq at ht_witness_left
11Use earlier factsL57–57

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

  1. L57
    exact ht_witness_left
12Establish hsumL58–67

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

  1. L58
    have hsum : x2=0
  2. L59
    trans (S i)*0
  3. L60
    specialize beta_repeat_sum_exact (x)
  4. L61
    specialize beta_repeat_sum_exact (x1)
  5. L62
    specialize beta_repeat_sum_exact (0)
  6. L63
    specialize beta_repeat_sum_exact (S i)
  7. L64
    specialize beta_repeat_sum_exact (x2)
  8. L65
    apply beta_repeat_sum_exact
  9. L66
    exact hz
  10. L67
    exact hc_witness_witness_witness_right_left
13Calculate and transport equalitiesL68–69

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

  1. L68
    simp
  2. L69
    rewrite hsum at hc_witness_witness_witness_right_right
14Use earlier factsL70–77

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

  1. L70
    specialize prime_field_residue_bounded_value (p)
  2. L71
    specialize prime_field_residue_bounded_value (0)
  3. L72
    specialize prime_field_residue_bounded_value (r)
  4. L73
    apply prime_field_residue_bounded_value
  5. L74
    specialize one_le_of_ne_zero (p)
  6. L75
    apply one_le_of_ne_zero
  7. L76
    exact hp
  8. L77
    exact hc_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 77 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro BB
  9. 0009intro BC
  10. 0010intro t
  11. 0011intro i
  12. 0012intro r
  13. 0013intro hp
  14. 0014intro hpad
  15. 0015intro hi
  16. 0016intro hc
  17. 0017cases hc
  18. 0018cases hc_witness
  19. 0019cases hc_witness_witness
  20. 0020cases hc_witness_witness_witness
  21. 0021cases hc_witness_witness_witness_right
  22. 0022have hz : Repeat(x,x1,0,S i)
  23. 0023intro j
  24. 0024intro hj
  25. 0025have ht : ∃ z. BetaAt(x,x1,j,z) ∧ PolynomialDiagonalTerm(ab,ac,L,BB,BC,t + M,i,j,z)
  26. 0026specialize hc_witness_witness_witness_left (j)
  27. 0027apply hc_witness_witness_witness_left
  28. 0028exact hj
  29. 0029cases ht
  30. 0030cases ht_witness
  31. 0031have heq : x3=0
  32. 0032specialize polynomial_diagonal_term_left_padding_zero_right (ab)
  33. 0033specialize polynomial_diagonal_term_left_padding_zero_right (ac)
  34. 0034specialize polynomial_diagonal_term_left_padding_zero_right (L)
  35. 0035specialize polynomial_diagonal_term_left_padding_zero_right (bb)
  36. 0036specialize polynomial_diagonal_term_left_padding_zero_right (bc)
  37. 0037specialize polynomial_diagonal_term_left_padding_zero_right (M)
  38. 0038specialize polynomial_diagonal_term_left_padding_zero_right (BB)
  39. 0039specialize polynomial_diagonal_term_left_padding_zero_right (BC)
  40. 0040specialize polynomial_diagonal_term_left_padding_zero_right (t)
  41. 0041specialize polynomial_diagonal_term_left_padding_zero_right (i)
  42. 0042specialize polynomial_diagonal_term_left_padding_zero_right (j)
  43. 0043specialize polynomial_diagonal_term_left_padding_zero_right (x3)
  44. 0044apply polynomial_diagonal_term_left_padding_zero_right
  45. 0045exact hpad
  46. 0046specialize le_trans (S i)
  47. 0047specialize le_trans (t)
  48. 0048specialize le_trans (t+j)
  49. 0049apply le_trans
  50. 0050exact hi
  51. 0051specialize le_add_right (t)
  52. 0052specialize le_add_right (j)
  53. 0053apply le_add_right
  54. 0054exact ht_witness_right
  55. 0055rewrite heq at ht_witness_left
  56. 0056rewrite heq at ht_witness_left
  57. 0057exact ht_witness_left
  58. 0058have hsum : x2=0
  59. 0059trans (S i)*0
  60. 0060specialize beta_repeat_sum_exact (x)
  61. 0061specialize beta_repeat_sum_exact (x1)
  62. 0062specialize beta_repeat_sum_exact (0)
  63. 0063specialize beta_repeat_sum_exact (S i)
  64. 0064specialize beta_repeat_sum_exact (x2)
  65. 0065apply beta_repeat_sum_exact
  66. 0066exact hz
  67. 0067exact hc_witness_witness_witness_right_left
  68. 0068simp
  69. 0069rewrite hsum at hc_witness_witness_witness_right_right
  70. 0070specialize prime_field_residue_bounded_value (p)
  71. 0071specialize prime_field_residue_bounded_value (0)
  72. 0072specialize prime_field_residue_bounded_value (r)
  73. 0073apply prime_field_residue_bounded_value
  74. 0074specialize one_le_of_ne_zero (p)
  75. 0075apply one_le_of_ne_zero
  76. 0076exact hp
  77. 0077exact hc_witness_witness_witness_right_right