PG004F

prime_field_convolution_coefficient_left_constant

Every actual in-range constant-left convolution coefficient is the canonical residue of the ordered product k*a. Both input bounds and the actual natural-sum witness are explicit; primality is unnecessary for this implication.

Alpha v34 checked-use · first admitted v34 · 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.

All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ p. ∀ k. ∀ kb. ∀ kc. ∀ ab. ∀ ac. ∀ L. ∀ i. ∀ a. ∀ r. BetaAt(kb,kc,0,k) → Lt(i,L) → BetaAt(ab,ac,i,a) → Lt(k,p) → Lt(a,p) → FpConvolutionCoefficient(p,kb,kc,1,ab,ac,L,i,r) → FpMul(p,k,a,r)

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

Definition DAG

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

Actual proof prerequisites

polynomial_diagonal_left_constant_natural_sum
Original expanded first-order statement 
forall p k kb kc ab ac L i a r. (((exists ff_h_pfp_left_constant_coefficient_K. ff_h_pfp_left_constant_coefficient_K + S (k) = S ((S (0)) * kc)) /\ exists ff_q_pfp_left_constant_coefficient_K. kb = ff_q_pfp_left_constant_coefficient_K * S ((S (0)) * kc) + (k))) -> (exists pfa_gap_left_constant_coefficient_index. pfa_gap_left_constant_coefficient_index + S (i) = (L)) -> (((exists ff_h_pfp_left_constant_coefficient_A. ff_h_pfp_left_constant_coefficient_A + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_left_constant_coefficient_A. ab = ff_q_pfp_left_constant_coefficient_A * S ((S (i)) * ac) + (a))) -> (exists pfa_gap_left_constant_coefficient_k_bound. pfa_gap_left_constant_coefficient_k_bound + S (k) = (p)) -> (exists pfa_gap_left_constant_coefficient_a_bound. pfa_gap_left_constant_coefficient_a_bound + S (a) = (p)) -> (exists pfc_terms_code_left_constant_coefficient_actual pfc_terms_scale_left_constant_coefficient_actual pfc_natural_sum_left_constant_coefficient_actual. ((forall pfc_index_left_constant_coefficient_actualdiagonal. (exists pfa_gap_left_constant_coefficient_actualdiagonalbound. pfa_gap_left_constant_coefficient_actualdiagonalbound + S (pfc_index_left_constant_coefficient_actualdiagonal) = (S (i))) -> exists pfc_value_left_constant_coefficient_actualdiagonal. ((((exists ff_h_pfp_left_constant_coefficient_actualdiagonalentry. ff_h_pfp_left_constant_coefficient_actualdiagonalentry + S (pfc_value_left_constant_coefficient_actualdiagonal) = S ((S (pfc_index_left_constant_coefficient_actualdiagonal)) * pfc_terms_scale_left_constant_coefficient_actual)) /\ exists ff_q_pfp_left_constant_coefficient_actualdiagonalentry. pfc_terms_code_left_constant_coefficient_actual = ff_q_pfp_left_constant_coefficient_actualdiagonalentry * S ((S (pfc_index_left_constant_coefficient_actualdiagonal)) * pfc_terms_scale_left_constant_coefficient_actual) + (pfc_value_left_constant_coefficient_actualdiagonal))) /\ ((exists pfc_complement_left_constant_coefficient_actualdiagonalterm pfc_left_left_constant_coefficient_actualdiagonalterm pfc_right_left_constant_coefficient_actualdiagonalterm. (((pfc_index_left_constant_coefficient_actualdiagonal)+pfc_complement_left_constant_coefficient_actualdiagonalterm=(i)) /\ ((((((exists pfa_gap_left_constant_coefficient_actualdiagonaltermleftinside. pfa_gap_left_constant_coefficient_actualdiagonaltermleftinside + S (pfc_index_left_constant_coefficient_actualdiagonal) = (1)) /\ ((((exists ff_h_pfp_left_constant_coefficient_actualdiagonaltermleftentry. ff_h_pfp_left_constant_coefficient_actualdiagonaltermleftentry + S (pfc_left_left_constant_coefficient_actualdiagonalterm) = S ((S (pfc_index_left_constant_coefficient_actualdiagonal)) * kc)) /\ exists ff_q_pfp_left_constant_coefficient_actualdiagonaltermleftentry. kb = ff_q_pfp_left_constant_coefficient_actualdiagonaltermleftentry * S ((S (pfc_index_left_constant_coefficient_actualdiagonal)) * kc) + (pfc_left_left_constant_coefficient_actualdiagonalterm)))))) \/ (((exists pfc_gap_left_constant_coefficient_actualdiagonaltermleftoutside. pfc_gap_left_constant_coefficient_actualdiagonaltermleftoutside+(1)=(pfc_index_left_constant_coefficient_actualdiagonal)) /\ (((pfc_left_left_constant_coefficient_actualdiagonalterm)=0))))) /\ ((((((exists pfa_gap_left_constant_coefficient_actualdiagonaltermrightinside. pfa_gap_left_constant_coefficient_actualdiagonaltermrightinside + S (pfc_complement_left_constant_coefficient_actualdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_left_constant_coefficient_actualdiagonaltermrightentry. ff_h_pfp_left_constant_coefficient_actualdiagonaltermrightentry + S (pfc_right_left_constant_coefficient_actualdiagonalterm) = S ((S (pfc_complement_left_constant_coefficient_actualdiagonalterm)) * ac)) /\ exists ff_q_pfp_left_constant_coefficient_actualdiagonaltermrightentry. ab = ff_q_pfp_left_constant_coefficient_actualdiagonaltermrightentry * S ((S (pfc_complement_left_constant_coefficient_actualdiagonalterm)) * ac) + (pfc_right_left_constant_coefficient_actualdiagonalterm)))))) \/ (((exists pfc_gap_left_constant_coefficient_actualdiagonaltermrightoutside. pfc_gap_left_constant_coefficient_actualdiagonaltermrightoutside+(L)=(pfc_complement_left_constant_coefficient_actualdiagonalterm)) /\ (((pfc_right_left_constant_coefficient_actualdiagonalterm)=0))))) /\ (((pfc_value_left_constant_coefficient_actualdiagonal)=pfc_left_left_constant_coefficient_actualdiagonalterm*pfc_right_left_constant_coefficient_actualdiagonalterm))))))))))) /\ (((exists fs_u_pfc_left_constant_coefficient_actualsum fs_v_pfc_left_constant_coefficient_actualsum. ((((exists fs_h_pfc_left_constant_coefficient_actualsum_body_start. fs_h_pfc_left_constant_coefficient_actualsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_left_constant_coefficient_actualsum)) /\ exists fs_q_pfc_left_constant_coefficient_actualsum_body_start. fs_u_pfc_left_constant_coefficient_actualsum = fs_q_pfc_left_constant_coefficient_actualsum_body_start * S ((S (0)) * fs_v_pfc_left_constant_coefficient_actualsum) + (0))) /\ ((((exists fs_h_pfc_left_constant_coefficient_actualsum_body_terminal. fs_h_pfc_left_constant_coefficient_actualsum_body_terminal + S (pfc_natural_sum_left_constant_coefficient_actual) = S ((S (S (i))) * fs_v_pfc_left_constant_coefficient_actualsum)) /\ exists fs_q_pfc_left_constant_coefficient_actualsum_body_terminal. fs_u_pfc_left_constant_coefficient_actualsum = fs_q_pfc_left_constant_coefficient_actualsum_body_terminal * S ((S (S (i))) * fs_v_pfc_left_constant_coefficient_actualsum) + (pfc_natural_sum_left_constant_coefficient_actual))) /\ forall fs_i_pfc_left_constant_coefficient_actualsum_body_steps. (exists fs_lt_pfc_left_constant_coefficient_actualsum_body_steps_bound. fs_lt_pfc_left_constant_coefficient_actualsum_body_steps_bound + S fs_i_pfc_left_constant_coefficient_actualsum_body_steps = S (i)) -> exists fs_a_pfc_left_constant_coefficient_actualsum_body_steps fs_r_pfc_left_constant_coefficient_actualsum_body_steps fs_s_pfc_left_constant_coefficient_actualsum_body_steps. ((((exists fs_h_pfc_left_constant_coefficient_actualsum_body_steps_summand. fs_h_pfc_left_constant_coefficient_actualsum_body_steps_summand + S (fs_a_pfc_left_constant_coefficient_actualsum_body_steps) = S ((S (fs_i_pfc_left_constant_coefficient_actualsum_body_steps)) * pfc_terms_scale_left_constant_coefficient_actual)) /\ exists fs_q_pfc_left_constant_coefficient_actualsum_body_steps_summand. pfc_terms_code_left_constant_coefficient_actual = fs_q_pfc_left_constant_coefficient_actualsum_body_steps_summand * S ((S (fs_i_pfc_left_constant_coefficient_actualsum_body_steps)) * pfc_terms_scale_left_constant_coefficient_actual) + (fs_a_pfc_left_constant_coefficient_actualsum_body_steps))) /\ ((((exists fs_h_pfc_left_constant_coefficient_actualsum_body_steps_partial. fs_h_pfc_left_constant_coefficient_actualsum_body_steps_partial + S (fs_r_pfc_left_constant_coefficient_actualsum_body_steps) = S ((S (fs_i_pfc_left_constant_coefficient_actualsum_body_steps)) * fs_v_pfc_left_constant_coefficient_actualsum)) /\ exists fs_q_pfc_left_constant_coefficient_actualsum_body_steps_partial. fs_u_pfc_left_constant_coefficient_actualsum = fs_q_pfc_left_constant_coefficient_actualsum_body_steps_partial * S ((S (fs_i_pfc_left_constant_coefficient_actualsum_body_steps)) * fs_v_pfc_left_constant_coefficient_actualsum) + (fs_r_pfc_left_constant_coefficient_actualsum_body_steps))) /\ ((((exists fs_h_pfc_left_constant_coefficient_actualsum_body_steps_successor. fs_h_pfc_left_constant_coefficient_actualsum_body_steps_successor + S (fs_s_pfc_left_constant_coefficient_actualsum_body_steps) = S ((S (S fs_i_pfc_left_constant_coefficient_actualsum_body_steps)) * fs_v_pfc_left_constant_coefficient_actualsum)) /\ exists fs_q_pfc_left_constant_coefficient_actualsum_body_steps_successor. fs_u_pfc_left_constant_coefficient_actualsum = fs_q_pfc_left_constant_coefficient_actualsum_body_steps_successor * S ((S (S fs_i_pfc_left_constant_coefficient_actualsum_body_steps)) * fs_v_pfc_left_constant_coefficient_actualsum) + (fs_s_pfc_left_constant_coefficient_actualsum_body_steps))) /\ fs_s_pfc_left_constant_coefficient_actualsum_body_steps = fs_r_pfc_left_constant_coefficient_actualsum_body_steps + fs_a_pfc_left_constant_coefficient_actualsum_body_steps)))))) /\ ((((exists pfa_gap_left_constant_coefficient_actualresiduebound. pfa_gap_left_constant_coefficient_actualresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_left_constant_coefficient_actualresiduecongruence pfa_offset_right_left_constant_coefficient_actualresiduecongruence. (pfc_natural_sum_left_constant_coefficient_actual) + (p) * pfa_offset_left_left_constant_coefficient_actualresiduecongruence = (r) + (p) * pfa_offset_right_left_constant_coefficient_actualresiduecongruence))))))))) -> (((exists pfa_gap_left_constant_coefficient_resultleft. pfa_gap_left_constant_coefficient_resultleft + S (k) = (p)) /\ (((exists pfa_gap_left_constant_coefficient_resultright. pfa_gap_left_constant_coefficient_resultright + S (a) = (p)) /\ ((((exists pfa_gap_left_constant_coefficient_resultresultbound. pfa_gap_left_constant_coefficient_resultresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_left_constant_coefficient_resultresultcongruence pfa_offset_right_left_constant_coefficient_resultresultcongruence. ((k) * (a)) + (p) * pfa_offset_left_left_constant_coefficient_resultresultcongruence = (r) + (p) * pfa_offset_right_left_constant_coefficient_resultresultcongruence)))))))))

Complete tactic proof in conservative notation

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

45 script commands · 10 reading checkpoints · 1 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 left constant natural sum
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro kb
  4. L4
    intro kc
  5. L5
    intro ab
  6. L6
    intro ac
  7. L7
    intro L
  8. L8
    intro i
  9. L9
    intro a
  10. L10
    intro r
02Fix variables and assumptionsL11–16

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

  1. L11
    intro hk
  2. L12
    intro hi
  3. L13
    intro ha
  4. L14
    intro hkb
  5. L15
    intro hab
  6. L16
    intro hr
03Separate the logical casesL17–21

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

  1. L17
    cases hr
  2. L18
    cases hr_witness
  3. L19
    cases hr_witness_witness
  4. L20
    cases hr_witness_witness_witness
  5. L21
    cases hr_witness_witness_witness_right
04Establish hnL22–31

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

  1. L22
    have hn : x2=k*a
  2. L23
    specialize polynomial_diagonal_left_constant_natural_sum (k)
  3. L24
    specialize polynomial_diagonal_left_constant_natural_sum (kb)
  4. L25
    specialize polynomial_diagonal_left_constant_natural_sum (kc)
  5. L26
    specialize polynomial_diagonal_left_constant_natural_sum (ab)
  6. L27
    specialize polynomial_diagonal_left_constant_natural_sum (ac)
  7. L28
    specialize polynomial_diagonal_left_constant_natural_sum (L)
  8. L29
    specialize polynomial_diagonal_left_constant_natural_sum (i)
  9. L30
    specialize polynomial_diagonal_left_constant_natural_sum (a)
  10. L31
    specialize polynomial_diagonal_left_constant_natural_sum (x)
05Use earlier factsL32–39

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

  1. L32
    specialize polynomial_diagonal_left_constant_natural_sum (x1)
  2. L33
    specialize polynomial_diagonal_left_constant_natural_sum (x2)
  3. L34
    apply polynomial_diagonal_left_constant_natural_sum
  4. L35
    exact hk
  5. L36
    exact hi
  6. L37
    exact ha
  7. L38
    exact hr_witness_witness_witness_left
  8. L39
    exact hr_witness_witness_witness_right_left
06Calculate and transport equalitiesL40–40

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

  1. L40
    rewrite hn at hr_witness_witness_witness_right_right
07Separate the logical casesL41–41

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

  1. L41
    split
08Use earlier factsL42–42

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

  1. L42
    exact hkb
09Separate the logical casesL43–43

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

  1. L43
    split
10Use earlier factsL44–45

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

  1. L44
    exact hab
  2. L45
    exact hr_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 45 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro kb
  4. 0004intro kc
  5. 0005intro ab
  6. 0006intro ac
  7. 0007intro L
  8. 0008intro i
  9. 0009intro a
  10. 0010intro r
  11. 0011intro hk
  12. 0012intro hi
  13. 0013intro ha
  14. 0014intro hkb
  15. 0015intro hab
  16. 0016intro hr
  17. 0017cases hr
  18. 0018cases hr_witness
  19. 0019cases hr_witness_witness
  20. 0020cases hr_witness_witness_witness
  21. 0021cases hr_witness_witness_witness_right
  22. 0022have hn : x2=k*a
  23. 0023specialize polynomial_diagonal_left_constant_natural_sum (k)
  24. 0024specialize polynomial_diagonal_left_constant_natural_sum (kb)
  25. 0025specialize polynomial_diagonal_left_constant_natural_sum (kc)
  26. 0026specialize polynomial_diagonal_left_constant_natural_sum (ab)
  27. 0027specialize polynomial_diagonal_left_constant_natural_sum (ac)
  28. 0028specialize polynomial_diagonal_left_constant_natural_sum (L)
  29. 0029specialize polynomial_diagonal_left_constant_natural_sum (i)
  30. 0030specialize polynomial_diagonal_left_constant_natural_sum (a)
  31. 0031specialize polynomial_diagonal_left_constant_natural_sum (x)
  32. 0032specialize polynomial_diagonal_left_constant_natural_sum (x1)
  33. 0033specialize polynomial_diagonal_left_constant_natural_sum (x2)
  34. 0034apply polynomial_diagonal_left_constant_natural_sum
  35. 0035exact hk
  36. 0036exact hi
  37. 0037exact ha
  38. 0038exact hr_witness_witness_witness_left
  39. 0039exact hr_witness_witness_witness_right_left
  40. 0040rewrite hn at hr_witness_witness_witness_right_right
  41. 0041split
  42. 0042exact hkb
  43. 0043split
  44. 0044exact hab
  45. 0045exact hr_witness_witness_witness_right_right