PX0001

polynomial_diagonal_left_prefix_transport

A genuine antidiagonal term below a shared left prefix survives changing its code and its declared input length.

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. ∀ AB. ∀ AC. ∀ K. ∀ bb. ∀ bc. ∀ M. ∀ N. ∀ i. ∀ j. ∀ t. Le(N,L) → Le(N,K) → BetaPrefixEqual(ab,ac,AB,AC,N) → Lt(j,N) → PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t) → PolynomialDiagonalTerm(AB,AC,K,bb,bc,M,i,j,t)

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

Definition DAG

BetaPrefixEqual(b,c,d,e,l) · 1PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t) · 2Le(a,b) · 2Lt(a,b) · 3BetaAt(b,c,i,x) · 1

Actual proof prerequisites

lt_of_lt_of_le · checked external prerequisitepolynomial_zero_extended_entry_inside · checked external prerequisite
Original expanded first-order statement 
forall ab ac L AB AC K bb bc M N i j t. (exists pfc_gap_tri_term_old_length. pfc_gap_tri_term_old_length+(N)=(L)) -> (exists pfc_gap_tri_term_new_length. pfc_gap_tri_term_new_length+(N)=(K)) -> (forall mdr_i_pfp_tri_term_equal mdr_a_pfp_tri_term_equal. (exists mdr_gap_pfp_tri_term_equalb. mdr_gap_pfp_tri_term_equalb + S (mdr_i_pfp_tri_term_equal) = (N)) -> (((exists ff_h_mdr_pfp_tri_term_equalo. ff_h_mdr_pfp_tri_term_equalo + S (mdr_a_pfp_tri_term_equal) = S ((S (mdr_i_pfp_tri_term_equal)) * ac)) /\ exists ff_q_mdr_pfp_tri_term_equalo. ab = ff_q_mdr_pfp_tri_term_equalo * S ((S (mdr_i_pfp_tri_term_equal)) * ac) + (mdr_a_pfp_tri_term_equal))) -> (((exists ff_h_mdr_pfp_tri_term_equaln. ff_h_mdr_pfp_tri_term_equaln + S (mdr_a_pfp_tri_term_equal) = S ((S (mdr_i_pfp_tri_term_equal)) * AC)) /\ exists ff_q_mdr_pfp_tri_term_equaln. AB = ff_q_mdr_pfp_tri_term_equaln * S ((S (mdr_i_pfp_tri_term_equal)) * AC) + (mdr_a_pfp_tri_term_equal)))) -> (exists pfa_gap_tri_term_index. pfa_gap_tri_term_index + S (j) = (N)) -> (exists pfc_complement_tri_term_old pfc_left_tri_term_old pfc_right_tri_term_old. (((j)+pfc_complement_tri_term_old=(i)) /\ ((((((exists pfa_gap_tri_term_oldleftinside. pfa_gap_tri_term_oldleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_tri_term_oldleftentry. ff_h_pfp_tri_term_oldleftentry + S (pfc_left_tri_term_old) = S ((S (j)) * ac)) /\ exists ff_q_pfp_tri_term_oldleftentry. ab = ff_q_pfp_tri_term_oldleftentry * S ((S (j)) * ac) + (pfc_left_tri_term_old)))))) \/ (((exists pfc_gap_tri_term_oldleftoutside. pfc_gap_tri_term_oldleftoutside+(L)=(j)) /\ (((pfc_left_tri_term_old)=0))))) /\ ((((((exists pfa_gap_tri_term_oldrightinside. pfa_gap_tri_term_oldrightinside + S (pfc_complement_tri_term_old) = (M)) /\ ((((exists ff_h_pfp_tri_term_oldrightentry. ff_h_pfp_tri_term_oldrightentry + S (pfc_right_tri_term_old) = S ((S (pfc_complement_tri_term_old)) * bc)) /\ exists ff_q_pfp_tri_term_oldrightentry. bb = ff_q_pfp_tri_term_oldrightentry * S ((S (pfc_complement_tri_term_old)) * bc) + (pfc_right_tri_term_old)))))) \/ (((exists pfc_gap_tri_term_oldrightoutside. pfc_gap_tri_term_oldrightoutside+(M)=(pfc_complement_tri_term_old)) /\ (((pfc_right_tri_term_old)=0))))) /\ (((t)=pfc_left_tri_term_old*pfc_right_tri_term_old)))))))) -> (exists pfc_complement_tri_term_new pfc_left_tri_term_new pfc_right_tri_term_new. (((j)+pfc_complement_tri_term_new=(i)) /\ ((((((exists pfa_gap_tri_term_newleftinside. pfa_gap_tri_term_newleftinside + S (j) = (K)) /\ ((((exists ff_h_pfp_tri_term_newleftentry. ff_h_pfp_tri_term_newleftentry + S (pfc_left_tri_term_new) = S ((S (j)) * AC)) /\ exists ff_q_pfp_tri_term_newleftentry. AB = ff_q_pfp_tri_term_newleftentry * S ((S (j)) * AC) + (pfc_left_tri_term_new)))))) \/ (((exists pfc_gap_tri_term_newleftoutside. pfc_gap_tri_term_newleftoutside+(K)=(j)) /\ (((pfc_left_tri_term_new)=0))))) /\ ((((((exists pfa_gap_tri_term_newrightinside. pfa_gap_tri_term_newrightinside + S (pfc_complement_tri_term_new) = (M)) /\ ((((exists ff_h_pfp_tri_term_newrightentry. ff_h_pfp_tri_term_newrightentry + S (pfc_right_tri_term_new) = S ((S (pfc_complement_tri_term_new)) * bc)) /\ exists ff_q_pfp_tri_term_newrightentry. bb = ff_q_pfp_tri_term_newrightentry * S ((S (pfc_complement_tri_term_new)) * bc) + (pfc_right_tri_term_new)))))) \/ (((exists pfc_gap_tri_term_newrightoutside. pfc_gap_tri_term_newrightoutside+(M)=(pfc_complement_tri_term_new)) /\ (((pfc_right_tri_term_new)=0))))) /\ (((t)=pfc_left_tri_term_new*pfc_right_tri_term_new))))))))

Complete tactic proof in conservative notation

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

64 script commands · 13 reading checkpoints · 3 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.

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 AB
  5. L5
    intro AC
  6. L6
    intro K
  7. L7
    intro bb
  8. L8
    intro bc
  9. L9
    intro M
  10. L10
    intro N
02Fix variables and assumptionsL11–18

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

  1. L11
    intro i
  2. L12
    intro j
  3. L13
    intro t
  4. L14
    intro hl
  5. L15
    intro hk
  6. L16
    intro he
  7. L17
    intro hj
  8. L18
    intro ht
03Separate the logical casesL19–24

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

  1. L19
    cases ht
  2. L20
    cases ht_witness
  3. L21
    cases ht_witness_witness
  4. L22
    cases ht_witness_witness_witness
  5. L23
    cases ht_witness_witness_witness_right
  6. L24
    cases ht_witness_witness_witness_right_right
04Establish hjlL25–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt of lt of le.

  1. L25
  2. L26
    specialize lt_of_lt_of_le (j)
  3. L27
    specialize lt_of_lt_of_le (N)
  4. L28
    specialize lt_of_lt_of_le (L)
  5. L29
    apply lt_of_lt_of_le
  6. L30
    exact hj
  7. L31
    exact hl
05Establish hjkL32–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt of lt of le.

  1. L32
  2. L33
    specialize lt_of_lt_of_le (j)
  3. L34
    specialize lt_of_lt_of_le (N)
  4. L35
    specialize lt_of_lt_of_le (K)
  5. L36
    apply lt_of_lt_of_le
  6. L37
    exact hj
  7. L38
    exact hk
06Establish haL39–47

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

  1. L39
  2. L40
    specialize polynomial_zero_extended_entry_inside (ab)
  3. L41
    specialize polynomial_zero_extended_entry_inside (ac)
  4. L42
    specialize polynomial_zero_extended_entry_inside (L)
  5. L43
    specialize polynomial_zero_extended_entry_inside (j)
  6. L44
    specialize polynomial_zero_extended_entry_inside (x1)
  7. L45
    apply polynomial_zero_extended_entry_inside
  8. L46
    exact hjl
  9. L47
    exact ht_witness_witness_witness_right_left
07Construct an explicit witnessL48–50

Supply the displayed value, then prove that it has the required property.

  1. L48
    exists x
  2. L49
    exists x1
  3. L50
    exists x2
08Separate the logical casesL51–51

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

  1. L51
    split
09Use earlier factsL52–52

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

  1. L52
    exact ht_witness_witness_witness_left
10Separate the logical casesL53–55

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

  1. L53
    split
  2. L54
    left
  3. L55
    split
11Use earlier factsL56–61

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

  1. L56
    exact hjk
  2. L57
    specialize he (j)
  3. L58
    specialize he (x1)
  4. L59
    apply he
  5. L60
    exact hj
  6. L61
    exact ha
12Separate the logical casesL62–62

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

  1. L62
    split
13Use earlier factsL63–64

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

  1. L63
    exact ht_witness_witness_witness_right_right_left
  2. L64
    exact ht_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 64 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro L
  4. 0004intro AB
  5. 0005intro AC
  6. 0006intro K
  7. 0007intro bb
  8. 0008intro bc
  9. 0009intro M
  10. 0010intro N
  11. 0011intro i
  12. 0012intro j
  13. 0013intro t
  14. 0014intro hl
  15. 0015intro hk
  16. 0016intro he
  17. 0017intro hj
  18. 0018intro ht
  19. 0019cases ht
  20. 0020cases ht_witness
  21. 0021cases ht_witness_witness
  22. 0022cases ht_witness_witness_witness
  23. 0023cases ht_witness_witness_witness_right
  24. 0024cases ht_witness_witness_witness_right_right
  25. 0025have hjl : Lt(j,L)
  26. 0026specialize lt_of_lt_of_le (j)
  27. 0027specialize lt_of_lt_of_le (N)
  28. 0028specialize lt_of_lt_of_le (L)
  29. 0029apply lt_of_lt_of_le
  30. 0030exact hj
  31. 0031exact hl
  32. 0032have hjk : Lt(j,K)
  33. 0033specialize lt_of_lt_of_le (j)
  34. 0034specialize lt_of_lt_of_le (N)
  35. 0035specialize lt_of_lt_of_le (K)
  36. 0036apply lt_of_lt_of_le
  37. 0037exact hj
  38. 0038exact hk
  39. 0039have ha : BetaAt(ab,ac,j,x1)
  40. 0040specialize polynomial_zero_extended_entry_inside (ab)
  41. 0041specialize polynomial_zero_extended_entry_inside (ac)
  42. 0042specialize polynomial_zero_extended_entry_inside (L)
  43. 0043specialize polynomial_zero_extended_entry_inside (j)
  44. 0044specialize polynomial_zero_extended_entry_inside (x1)
  45. 0045apply polynomial_zero_extended_entry_inside
  46. 0046exact hjl
  47. 0047exact ht_witness_witness_witness_right_left
  48. 0048exists x
  49. 0049exists x1
  50. 0050exists x2
  51. 0051split
  52. 0052exact ht_witness_witness_witness_left
  53. 0053split
  54. 0054left
  55. 0055split
  56. 0056exact hjk
  57. 0057specialize he (j)
  58. 0058specialize he (x1)
  59. 0059apply he
  60. 0060exact hj
  61. 0061exact ha
  62. 0062split
  63. 0063exact ht_witness_witness_witness_right_right_left
  64. 0064exact ht_witness_witness_witness_right_right_right