PX0062

polynomial_diagonal_term_left_padding_zero_left

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

A genuine antidiagonal term is zero when its left factor index lies in the actual leading padding block.

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 ab ac L bb bc M AB AC t i j z. (((forall pfp_repeat_index_zero_term_pad_leftzeros. (exists pfa_gap_zero_term_pad_leftzerosindex. pfa_gap_zero_term_pad_leftzerosindex + S (pfp_repeat_index_zero_term_pad_leftzeros) = (t)) -> (((exists ff_h_pfp_zero_term_pad_leftzerosentry. ff_h_pfp_zero_term_pad_leftzerosentry + S (0) = S ((S (pfp_repeat_index_zero_term_pad_leftzeros)) * AC)) /\ exists ff_q_pfp_zero_term_pad_leftzerosentry. AB = ff_q_pfp_zero_term_pad_leftzerosentry * S ((S (pfp_repeat_index_zero_term_pad_leftzeros)) * AC) + (0)))) /\ ((forall pfrep_index_zero_term_pad_left pfrep_value_zero_term_pad_left. (exists pfa_gap_zero_term_pad_leftbound. pfa_gap_zero_term_pad_leftbound + S (pfrep_index_zero_term_pad_left) = (L)) -> (((exists ff_h_pfp_zero_term_pad_leftinput. ff_h_pfp_zero_term_pad_leftinput + S (pfrep_value_zero_term_pad_left) = S ((S (pfrep_index_zero_term_pad_left)) * ac)) /\ exists ff_q_pfp_zero_term_pad_leftinput. ab = ff_q_pfp_zero_term_pad_leftinput * S ((S (pfrep_index_zero_term_pad_left)) * ac) + (pfrep_value_zero_term_pad_left))) -> (((exists ff_h_pfp_zero_term_pad_leftoutput. ff_h_pfp_zero_term_pad_leftoutput + S (pfrep_value_zero_term_pad_left) = S ((S ((t)+pfrep_index_zero_term_pad_left)) * AC)) /\ exists ff_q_pfp_zero_term_pad_leftoutput. AB = ff_q_pfp_zero_term_pad_leftoutput * S ((S ((t)+pfrep_index_zero_term_pad_left)) * AC) + (pfrep_value_zero_term_pad_left))))))) -> (exists pfa_gap_term_zero_left_bound. pfa_gap_term_zero_left_bound + S (j) = (t)) -> (exists pfc_complement_zero_term_actual_left pfc_left_zero_term_actual_left pfc_right_zero_term_actual_left. (((j)+pfc_complement_zero_term_actual_left=(i)) /\ ((((((exists pfa_gap_zero_term_actual_leftleftinside. pfa_gap_zero_term_actual_leftleftinside + S (j) = (t+L)) /\ ((((exists ff_h_pfp_zero_term_actual_leftleftentry. ff_h_pfp_zero_term_actual_leftleftentry + S (pfc_left_zero_term_actual_left) = S ((S (j)) * AC)) /\ exists ff_q_pfp_zero_term_actual_leftleftentry. AB = ff_q_pfp_zero_term_actual_leftleftentry * S ((S (j)) * AC) + (pfc_left_zero_term_actual_left)))))) \/ (((exists pfc_gap_zero_term_actual_leftleftoutside. pfc_gap_zero_term_actual_leftleftoutside+(t+L)=(j)) /\ (((pfc_left_zero_term_actual_left)=0))))) /\ ((((((exists pfa_gap_zero_term_actual_leftrightinside. pfa_gap_zero_term_actual_leftrightinside + S (pfc_complement_zero_term_actual_left) = (M)) /\ ((((exists ff_h_pfp_zero_term_actual_leftrightentry. ff_h_pfp_zero_term_actual_leftrightentry + S (pfc_right_zero_term_actual_left) = S ((S (pfc_complement_zero_term_actual_left)) * bc)) /\ exists ff_q_pfp_zero_term_actual_leftrightentry. bb = ff_q_pfp_zero_term_actual_leftrightentry * S ((S (pfc_complement_zero_term_actual_left)) * bc) + (pfc_right_zero_term_actual_left)))))) \/ (((exists pfc_gap_zero_term_actual_leftrightoutside. pfc_gap_zero_term_actual_leftrightoutside+(M)=(pfc_complement_zero_term_actual_left)) /\ (((pfc_right_zero_term_actual_left)=0))))) /\ (((z)=pfc_left_zero_term_actual_left*pfc_right_zero_term_actual_left)))))))) -> (z=0)

Constructive proof overview

Generated structural guide

A genuine antidiagonal term is zero when its left factor index lies in the actual leading padding block.

The unchanged tactic script uses 3 declared prerequisites and contains 45 exact native proof lines.

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

Proof neighborhood

Direct dependencies

polynomial_zero_extended_entry_functional Alpha theorem; checked-use authorized PX005C polynomial_zero_extended_left_pad_before mul_zero_left Alpha theorem; checked-use authorized

Direct dependents

PX0064 polynomial_diagonal_left_padding_left PX0068 prime_field_convolution_coefficient_before_left_padding_left

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

45 script commands · 9 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.

Named ingredients (1)
polynomial zero extended left pad before
01Fix variables and assumptionsL1–10

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

  1. L1
    intro ab
  2. L2
    intro ac
  3. L3
    intro L
  4. L4
    intro bb
  5. L5
    intro bc
  6. L6
    intro M
  7. L7
    intro AB
  8. L8
    intro AC
  9. L9
    intro t
  10. L10
    intro i
02Fix variables and assumptionsL11–15

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

  1. L11
    intro j
  2. L12
    intro z
  3. L13
    intro hpad
  4. L14
    intro hbound
  5. L15
    intro ht
03Separate the logical casesL16–21

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

  1. L16
    cases ht
  2. L17
    cases ht_witness
  3. L18
    cases ht_witness_witness
  4. L19
    cases ht_witness_witness_witness
  5. L20
    cases ht_witness_witness_witness_right
  6. L21
    cases ht_witness_witness_witness_right_right
04Establish hzeroL22–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial zero extended entry functional.

  1. L22
    have hzero : x1=0
  2. L23
    specialize polynomial_zero_extended_entry_functional (AB)
  3. L24
    specialize polynomial_zero_extended_entry_functional (AC)
  4. L25
    specialize polynomial_zero_extended_entry_functional (t+L)
  5. L26
    specialize polynomial_zero_extended_entry_functional (j)
  6. L27
    specialize polynomial_zero_extended_entry_functional (x1)
  7. L28
    specialize polynomial_zero_extended_entry_functional (0)
  8. L29
    apply polynomial_zero_extended_entry_functional
  9. L30
    exact ht_witness_witness_witness_right_left
  10. L31
    specialize polynomial_zero_extended_left_pad_before (ab)
05Use earlier factsL32–40

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

  1. L32
    specialize polynomial_zero_extended_left_pad_before (ac)
  2. L33
    specialize polynomial_zero_extended_left_pad_before (L)
  3. L34
    specialize polynomial_zero_extended_left_pad_before (t)
  4. L35
    specialize polynomial_zero_extended_left_pad_before (AB)
  5. L36
    specialize polynomial_zero_extended_left_pad_before (AC)
  6. L37
    specialize polynomial_zero_extended_left_pad_before (j)
  7. L38
    apply polynomial_zero_extended_left_pad_before
  8. L39
    exact hpad
  9. L40
    exact hbound
06Calculate and transport equalitiesL41–41

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

  1. L41
    trans x1*x2
07Use earlier factsL42–42

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

  1. L42
    exact ht_witness_witness_witness_right_right_right
08Calculate and transport equalitiesL43–43

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

  1. L43
    rewrite hzero
09Use earlier factsL44–45

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

  1. L44
    specialize mul_zero_left (x2)
  2. L45
    apply mul_zero_left

Library-wide reading audit

Original exact command ledger · 45 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro L
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro M
  7. 0007intro AB
  8. 0008intro AC
  9. 0009intro t
  10. 0010intro i
  11. 0011intro j
  12. 0012intro z
  13. 0013intro hpad
  14. 0014intro hbound
  15. 0015intro ht
  16. 0016cases ht
  17. 0017cases ht_witness
  18. 0018cases ht_witness_witness
  19. 0019cases ht_witness_witness_witness
  20. 0020cases ht_witness_witness_witness_right
  21. 0021cases ht_witness_witness_witness_right_right
  22. 0022have hzero : x1=0
  23. 0023specialize polynomial_zero_extended_entry_functional (AB)
  24. 0024specialize polynomial_zero_extended_entry_functional (AC)
  25. 0025specialize polynomial_zero_extended_entry_functional (t+L)
  26. 0026specialize polynomial_zero_extended_entry_functional (j)
  27. 0027specialize polynomial_zero_extended_entry_functional (x1)
  28. 0028specialize polynomial_zero_extended_entry_functional (0)
  29. 0029apply polynomial_zero_extended_entry_functional
  30. 0030exact ht_witness_witness_witness_right_left
  31. 0031specialize polynomial_zero_extended_left_pad_before (ab)
  32. 0032specialize polynomial_zero_extended_left_pad_before (ac)
  33. 0033specialize polynomial_zero_extended_left_pad_before (L)
  34. 0034specialize polynomial_zero_extended_left_pad_before (t)
  35. 0035specialize polynomial_zero_extended_left_pad_before (AB)
  36. 0036specialize polynomial_zero_extended_left_pad_before (AC)
  37. 0037specialize polynomial_zero_extended_left_pad_before (j)
  38. 0038apply polynomial_zero_extended_left_pad_before
  39. 0039exact hpad
  40. 0040exact hbound
  41. 0041trans x1*x2
  42. 0042exact ht_witness_witness_witness_right_right_right
  43. 0043rewrite hzero
  44. 0044specialize mul_zero_left (x2)
  45. 0045apply mul_zero_left