PX0062

polynomial_diagonal_term_left_padding_zero_left

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

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

∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ M. ∀ AB. ∀ AC. ∀ t. ∀ i. ∀ j. ∀ z. PolynomialLeftPad(ab,ac,L,t,AB,AC) → Lt(j,t) → PolynomialDiagonalTerm(AB,AC,t + L,bb,bc,M,i,j,z) → z = 0

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

Definition DAG

PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t) · 1PolynomialLeftPad(b,c,L,t,d,e) · 1Lt(a,b) · 1

Actual proof prerequisites

polynomial_zero_extended_entry_functional · checked external prerequisitepolynomial_zero_extended_left_pad_beforemul_zero_left · checked external prerequisite
Original expanded first-order 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)

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 · 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.

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 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 defined 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