PX0068

prime_field_convolution_coefficient_before_left_padding_left

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. ∀ AB. ∀ AC. ∀ t. ∀ i. ∀ r. ¬p = 0 → PolynomialLeftPad(ab,ac,L,t,AB,AC) → Lt(i,t) → FpConvolutionCoefficient(p,AB,AC,t + L,bb,bc,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_leftle_trans · checked external prerequisitebeta_repeat_sum_exact · checked external prerequisiteprime_field_residue_bounded_value · checked external prerequisiteone_le_of_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall p ab ac L bb bc M AB AC t i r. (~(p=0)) -> (((forall pfp_repeat_index_before_coefficient_pad_leftzeros. (exists pfa_gap_before_coefficient_pad_leftzerosindex. pfa_gap_before_coefficient_pad_leftzerosindex + S (pfp_repeat_index_before_coefficient_pad_leftzeros) = (t)) -> (((exists ff_h_pfp_before_coefficient_pad_leftzerosentry. ff_h_pfp_before_coefficient_pad_leftzerosentry + S (0) = S ((S (pfp_repeat_index_before_coefficient_pad_leftzeros)) * AC)) /\ exists ff_q_pfp_before_coefficient_pad_leftzerosentry. AB = ff_q_pfp_before_coefficient_pad_leftzerosentry * S ((S (pfp_repeat_index_before_coefficient_pad_leftzeros)) * AC) + (0)))) /\ ((forall pfrep_index_before_coefficient_pad_left pfrep_value_before_coefficient_pad_left. (exists pfa_gap_before_coefficient_pad_leftbound. pfa_gap_before_coefficient_pad_leftbound + S (pfrep_index_before_coefficient_pad_left) = (L)) -> (((exists ff_h_pfp_before_coefficient_pad_leftinput. ff_h_pfp_before_coefficient_pad_leftinput + S (pfrep_value_before_coefficient_pad_left) = S ((S (pfrep_index_before_coefficient_pad_left)) * ac)) /\ exists ff_q_pfp_before_coefficient_pad_leftinput. ab = ff_q_pfp_before_coefficient_pad_leftinput * S ((S (pfrep_index_before_coefficient_pad_left)) * ac) + (pfrep_value_before_coefficient_pad_left))) -> (((exists ff_h_pfp_before_coefficient_pad_leftoutput. ff_h_pfp_before_coefficient_pad_leftoutput + S (pfrep_value_before_coefficient_pad_left) = S ((S ((t)+pfrep_index_before_coefficient_pad_left)) * AC)) /\ exists ff_q_pfp_before_coefficient_pad_leftoutput. AB = ff_q_pfp_before_coefficient_pad_leftoutput * S ((S ((t)+pfrep_index_before_coefficient_pad_left)) * AC) + (pfrep_value_before_coefficient_pad_left))))))) -> (exists pfa_gap_before_coefficient_index_left. pfa_gap_before_coefficient_index_left + S (i) = (t)) -> (exists pfc_terms_code_before_coefficient_actual_left pfc_terms_scale_before_coefficient_actual_left pfc_natural_sum_before_coefficient_actual_left. ((forall pfc_index_before_coefficient_actual_leftdiagonal. (exists pfa_gap_before_coefficient_actual_leftdiagonalbound. pfa_gap_before_coefficient_actual_leftdiagonalbound + S (pfc_index_before_coefficient_actual_leftdiagonal) = (S (i))) -> exists pfc_value_before_coefficient_actual_leftdiagonal. ((((exists ff_h_pfp_before_coefficient_actual_leftdiagonalentry. ff_h_pfp_before_coefficient_actual_leftdiagonalentry + S (pfc_value_before_coefficient_actual_leftdiagonal) = S ((S (pfc_index_before_coefficient_actual_leftdiagonal)) * pfc_terms_scale_before_coefficient_actual_left)) /\ exists ff_q_pfp_before_coefficient_actual_leftdiagonalentry. pfc_terms_code_before_coefficient_actual_left = ff_q_pfp_before_coefficient_actual_leftdiagonalentry * S ((S (pfc_index_before_coefficient_actual_leftdiagonal)) * pfc_terms_scale_before_coefficient_actual_left) + (pfc_value_before_coefficient_actual_leftdiagonal))) /\ ((exists pfc_complement_before_coefficient_actual_leftdiagonalterm pfc_left_before_coefficient_actual_leftdiagonalterm pfc_right_before_coefficient_actual_leftdiagonalterm. (((pfc_index_before_coefficient_actual_leftdiagonal)+pfc_complement_before_coefficient_actual_leftdiagonalterm=(i)) /\ ((((((exists pfa_gap_before_coefficient_actual_leftdiagonaltermleftinside. pfa_gap_before_coefficient_actual_leftdiagonaltermleftinside + S (pfc_index_before_coefficient_actual_leftdiagonal) = (t+L)) /\ ((((exists ff_h_pfp_before_coefficient_actual_leftdiagonaltermleftentry. ff_h_pfp_before_coefficient_actual_leftdiagonaltermleftentry + S (pfc_left_before_coefficient_actual_leftdiagonalterm) = S ((S (pfc_index_before_coefficient_actual_leftdiagonal)) * AC)) /\ exists ff_q_pfp_before_coefficient_actual_leftdiagonaltermleftentry. AB = ff_q_pfp_before_coefficient_actual_leftdiagonaltermleftentry * S ((S (pfc_index_before_coefficient_actual_leftdiagonal)) * AC) + (pfc_left_before_coefficient_actual_leftdiagonalterm)))))) \/ (((exists pfc_gap_before_coefficient_actual_leftdiagonaltermleftoutside. pfc_gap_before_coefficient_actual_leftdiagonaltermleftoutside+(t+L)=(pfc_index_before_coefficient_actual_leftdiagonal)) /\ (((pfc_left_before_coefficient_actual_leftdiagonalterm)=0))))) /\ ((((((exists pfa_gap_before_coefficient_actual_leftdiagonaltermrightinside. pfa_gap_before_coefficient_actual_leftdiagonaltermrightinside + S (pfc_complement_before_coefficient_actual_leftdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_before_coefficient_actual_leftdiagonaltermrightentry. ff_h_pfp_before_coefficient_actual_leftdiagonaltermrightentry + S (pfc_right_before_coefficient_actual_leftdiagonalterm) = S ((S (pfc_complement_before_coefficient_actual_leftdiagonalterm)) * bc)) /\ exists ff_q_pfp_before_coefficient_actual_leftdiagonaltermrightentry. bb = ff_q_pfp_before_coefficient_actual_leftdiagonaltermrightentry * S ((S (pfc_complement_before_coefficient_actual_leftdiagonalterm)) * bc) + (pfc_right_before_coefficient_actual_leftdiagonalterm)))))) \/ (((exists pfc_gap_before_coefficient_actual_leftdiagonaltermrightoutside. pfc_gap_before_coefficient_actual_leftdiagonaltermrightoutside+(M)=(pfc_complement_before_coefficient_actual_leftdiagonalterm)) /\ (((pfc_right_before_coefficient_actual_leftdiagonalterm)=0))))) /\ (((pfc_value_before_coefficient_actual_leftdiagonal)=pfc_left_before_coefficient_actual_leftdiagonalterm*pfc_right_before_coefficient_actual_leftdiagonalterm))))))))))) /\ (((exists fs_u_pfc_before_coefficient_actual_leftsum fs_v_pfc_before_coefficient_actual_leftsum. ((((exists fs_h_pfc_before_coefficient_actual_leftsum_body_start. fs_h_pfc_before_coefficient_actual_leftsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_before_coefficient_actual_leftsum)) /\ exists fs_q_pfc_before_coefficient_actual_leftsum_body_start. fs_u_pfc_before_coefficient_actual_leftsum = fs_q_pfc_before_coefficient_actual_leftsum_body_start * S ((S (0)) * fs_v_pfc_before_coefficient_actual_leftsum) + (0))) /\ ((((exists fs_h_pfc_before_coefficient_actual_leftsum_body_terminal. fs_h_pfc_before_coefficient_actual_leftsum_body_terminal + S (pfc_natural_sum_before_coefficient_actual_left) = S ((S (S (i))) * fs_v_pfc_before_coefficient_actual_leftsum)) /\ exists fs_q_pfc_before_coefficient_actual_leftsum_body_terminal. fs_u_pfc_before_coefficient_actual_leftsum = fs_q_pfc_before_coefficient_actual_leftsum_body_terminal * S ((S (S (i))) * fs_v_pfc_before_coefficient_actual_leftsum) + (pfc_natural_sum_before_coefficient_actual_left))) /\ forall fs_i_pfc_before_coefficient_actual_leftsum_body_steps. (exists fs_lt_pfc_before_coefficient_actual_leftsum_body_steps_bound. fs_lt_pfc_before_coefficient_actual_leftsum_body_steps_bound + S fs_i_pfc_before_coefficient_actual_leftsum_body_steps = S (i)) -> exists fs_a_pfc_before_coefficient_actual_leftsum_body_steps fs_r_pfc_before_coefficient_actual_leftsum_body_steps fs_s_pfc_before_coefficient_actual_leftsum_body_steps. ((((exists fs_h_pfc_before_coefficient_actual_leftsum_body_steps_summand. fs_h_pfc_before_coefficient_actual_leftsum_body_steps_summand + S (fs_a_pfc_before_coefficient_actual_leftsum_body_steps) = S ((S (fs_i_pfc_before_coefficient_actual_leftsum_body_steps)) * pfc_terms_scale_before_coefficient_actual_left)) /\ exists fs_q_pfc_before_coefficient_actual_leftsum_body_steps_summand. pfc_terms_code_before_coefficient_actual_left = fs_q_pfc_before_coefficient_actual_leftsum_body_steps_summand * S ((S (fs_i_pfc_before_coefficient_actual_leftsum_body_steps)) * pfc_terms_scale_before_coefficient_actual_left) + (fs_a_pfc_before_coefficient_actual_leftsum_body_steps))) /\ ((((exists fs_h_pfc_before_coefficient_actual_leftsum_body_steps_partial. fs_h_pfc_before_coefficient_actual_leftsum_body_steps_partial + S (fs_r_pfc_before_coefficient_actual_leftsum_body_steps) = S ((S (fs_i_pfc_before_coefficient_actual_leftsum_body_steps)) * fs_v_pfc_before_coefficient_actual_leftsum)) /\ exists fs_q_pfc_before_coefficient_actual_leftsum_body_steps_partial. fs_u_pfc_before_coefficient_actual_leftsum = fs_q_pfc_before_coefficient_actual_leftsum_body_steps_partial * S ((S (fs_i_pfc_before_coefficient_actual_leftsum_body_steps)) * fs_v_pfc_before_coefficient_actual_leftsum) + (fs_r_pfc_before_coefficient_actual_leftsum_body_steps))) /\ ((((exists fs_h_pfc_before_coefficient_actual_leftsum_body_steps_successor. fs_h_pfc_before_coefficient_actual_leftsum_body_steps_successor + S (fs_s_pfc_before_coefficient_actual_leftsum_body_steps) = S ((S (S fs_i_pfc_before_coefficient_actual_leftsum_body_steps)) * fs_v_pfc_before_coefficient_actual_leftsum)) /\ exists fs_q_pfc_before_coefficient_actual_leftsum_body_steps_successor. fs_u_pfc_before_coefficient_actual_leftsum = fs_q_pfc_before_coefficient_actual_leftsum_body_steps_successor * S ((S (S fs_i_pfc_before_coefficient_actual_leftsum_body_steps)) * fs_v_pfc_before_coefficient_actual_leftsum) + (fs_s_pfc_before_coefficient_actual_leftsum_body_steps))) /\ fs_s_pfc_before_coefficient_actual_leftsum_body_steps = fs_r_pfc_before_coefficient_actual_leftsum_body_steps + fs_a_pfc_before_coefficient_actual_leftsum_body_steps)))))) /\ ((((exists pfa_gap_before_coefficient_actual_leftresiduebound. pfa_gap_before_coefficient_actual_leftresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_before_coefficient_actual_leftresiduecongruence pfa_offset_right_before_coefficient_actual_leftresiduecongruence. (pfc_natural_sum_before_coefficient_actual_left) + (p) * pfa_offset_left_before_coefficient_actual_leftresiduecongruence = (r) + (p) * pfa_offset_right_before_coefficient_actual_leftresiduecongruence))))))))) -> (r=0)

Complete tactic proof in conservative notation

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

75 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 left
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 AB
  9. L9
    intro AC
  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,t + L,bb,bc,M,i,j,z)Definitions: BetaAt(x,x1,j,z)PolynomialDiagonalTerm(AB,AC,t + L,bb,bc,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_left (ab)
  3. L33
    specialize polynomial_diagonal_term_left_padding_zero_left (ac)
  4. L34
    specialize polynomial_diagonal_term_left_padding_zero_left (L)
  5. L35
    specialize polynomial_diagonal_term_left_padding_zero_left (bb)
  6. L36
    specialize polynomial_diagonal_term_left_padding_zero_left (bc)
  7. L37
    specialize polynomial_diagonal_term_left_padding_zero_left (M)
  8. L38
    specialize polynomial_diagonal_term_left_padding_zero_left (AB)
  9. L39
    specialize polynomial_diagonal_term_left_padding_zero_left (AC)
  10. L40
    specialize polynomial_diagonal_term_left_padding_zero_left (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_left (i)
  2. L42
    specialize polynomial_diagonal_term_left_padding_zero_left (j)
  3. L43
    specialize polynomial_diagonal_term_left_padding_zero_left (x3)
  4. L44
    apply polynomial_diagonal_term_left_padding_zero_left
  5. L45
    exact hpad
  6. L46
    specialize le_trans (S j)
  7. L47
    specialize le_trans (S i)
  8. L48
    specialize le_trans (t)
  9. L49
    apply le_trans
  10. L50
    exact hj
09Use earlier factsL51–52

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

  1. L51
    exact hi
  2. L52
    exact ht_witness_right
10Calculate and transport equalitiesL53–54

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

  1. L53
    rewrite heq at ht_witness_left
  2. L54
    rewrite heq at ht_witness_left
11Use earlier factsL55–55

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

  1. L55
    exact ht_witness_left
12Establish hsumL56–65

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

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

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

  1. L66
    simp
  2. L67
    rewrite hsum at hc_witness_witness_witness_right_right
14Use earlier factsL68–75

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

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

Library-wide reading audit

Original defined command ledger · 75 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro AB
  9. 0009intro AC
  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,t + L,bb,bc,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_left (ab)
  33. 0033specialize polynomial_diagonal_term_left_padding_zero_left (ac)
  34. 0034specialize polynomial_diagonal_term_left_padding_zero_left (L)
  35. 0035specialize polynomial_diagonal_term_left_padding_zero_left (bb)
  36. 0036specialize polynomial_diagonal_term_left_padding_zero_left (bc)
  37. 0037specialize polynomial_diagonal_term_left_padding_zero_left (M)
  38. 0038specialize polynomial_diagonal_term_left_padding_zero_left (AB)
  39. 0039specialize polynomial_diagonal_term_left_padding_zero_left (AC)
  40. 0040specialize polynomial_diagonal_term_left_padding_zero_left (t)
  41. 0041specialize polynomial_diagonal_term_left_padding_zero_left (i)
  42. 0042specialize polynomial_diagonal_term_left_padding_zero_left (j)
  43. 0043specialize polynomial_diagonal_term_left_padding_zero_left (x3)
  44. 0044apply polynomial_diagonal_term_left_padding_zero_left
  45. 0045exact hpad
  46. 0046specialize le_trans (S j)
  47. 0047specialize le_trans (S i)
  48. 0048specialize le_trans (t)
  49. 0049apply le_trans
  50. 0050exact hj
  51. 0051exact hi
  52. 0052exact ht_witness_right
  53. 0053rewrite heq at ht_witness_left
  54. 0054rewrite heq at ht_witness_left
  55. 0055exact ht_witness_left
  56. 0056have hsum : x2=0
  57. 0057trans (S i)*0
  58. 0058specialize beta_repeat_sum_exact (x)
  59. 0059specialize beta_repeat_sum_exact (x1)
  60. 0060specialize beta_repeat_sum_exact (0)
  61. 0061specialize beta_repeat_sum_exact (S i)
  62. 0062specialize beta_repeat_sum_exact (x2)
  63. 0063apply beta_repeat_sum_exact
  64. 0064exact hz
  65. 0065exact hc_witness_witness_witness_right_left
  66. 0066simp
  67. 0067rewrite hsum at hc_witness_witness_witness_right_right
  68. 0068specialize prime_field_residue_bounded_value (p)
  69. 0069specialize prime_field_residue_bounded_value (0)
  70. 0070specialize prime_field_residue_bounded_value (r)
  71. 0071apply prime_field_residue_bounded_value
  72. 0072specialize one_le_of_ne_zero (p)
  73. 0073apply one_le_of_ne_zero
  74. 0074exact hp
  75. 0075exact hc_witness_witness_witness_right_right