PX0006

polynomial_diagonal_last_term_left_append

The sole new last antidiagonal term is exactly the appended coefficient times the nonempty right prefix head.

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. ∀ bb. ∀ bc. ∀ d. ∀ N. ∀ a. ∀ b. ∀ t. BetaAt(ab,ac,N,a) → BetaAt(bb,bc,0,b) → PolynomialDiagonalTerm(ab,ac,S N,bb,bc,S d,N,N,t) → t = a · b

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

Definition DAG

PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

add_left_cancel · checked external prerequisitepolynomial_zero_extended_entry_functional · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall ab ac bb bc d N a b t. (((exists ff_h_pfp_tri_last_new_entry. ff_h_pfp_tri_last_new_entry + S (a) = S ((S (N)) * ac)) /\ exists ff_q_pfp_tri_last_new_entry. ab = ff_q_pfp_tri_last_new_entry * S ((S (N)) * ac) + (a))) -> (((exists ff_h_pfp_tri_last_leading_entry. ff_h_pfp_tri_last_leading_entry + S (b) = S ((S (0)) * bc)) /\ exists ff_q_pfp_tri_last_leading_entry. bb = ff_q_pfp_tri_last_leading_entry * S ((S (0)) * bc) + (b))) -> (exists pfc_complement_tri_last_new pfc_left_tri_last_new pfc_right_tri_last_new. (((N)+pfc_complement_tri_last_new=(N)) /\ ((((((exists pfa_gap_tri_last_newleftinside. pfa_gap_tri_last_newleftinside + S (N) = (S N)) /\ ((((exists ff_h_pfp_tri_last_newleftentry. ff_h_pfp_tri_last_newleftentry + S (pfc_left_tri_last_new) = S ((S (N)) * ac)) /\ exists ff_q_pfp_tri_last_newleftentry. ab = ff_q_pfp_tri_last_newleftentry * S ((S (N)) * ac) + (pfc_left_tri_last_new)))))) \/ (((exists pfc_gap_tri_last_newleftoutside. pfc_gap_tri_last_newleftoutside+(S N)=(N)) /\ (((pfc_left_tri_last_new)=0))))) /\ ((((((exists pfa_gap_tri_last_newrightinside. pfa_gap_tri_last_newrightinside + S (pfc_complement_tri_last_new) = (S d)) /\ ((((exists ff_h_pfp_tri_last_newrightentry. ff_h_pfp_tri_last_newrightentry + S (pfc_right_tri_last_new) = S ((S (pfc_complement_tri_last_new)) * bc)) /\ exists ff_q_pfp_tri_last_newrightentry. bb = ff_q_pfp_tri_last_newrightentry * S ((S (pfc_complement_tri_last_new)) * bc) + (pfc_right_tri_last_new)))))) \/ (((exists pfc_gap_tri_last_newrightoutside. pfc_gap_tri_last_newrightoutside+(S d)=(pfc_complement_tri_last_new)) /\ (((pfc_right_tri_last_new)=0))))) /\ (((t)=pfc_left_tri_last_new*pfc_right_tri_last_new)))))))) -> t=a*b

Complete tactic proof in conservative notation

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

63 script commands · 18 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 bb
  4. L4
    intro bc
  5. L5
    intro d
  6. L6
    intro N
  7. L7
    intro a
  8. L8
    intro b
  9. L9
    intro t
  10. L10
    intro ha
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hb
  2. L12
    intro ht
03Separate the logical casesL13–18

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

  1. L13
    cases ht
  2. L14
    cases ht_witness
  3. L15
    cases ht_witness_witness
  4. L16
    cases ht_witness_witness_witness
  5. L17
    cases ht_witness_witness_witness_right
  6. L18
    cases ht_witness_witness_witness_right_right
04Establish hkL19–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add left cancel.

  1. L19
    have hk : x=0
  2. L20
    specialize add_left_cancel (N)
  3. L21
    specialize add_left_cancel (x)
  4. L22
    specialize add_left_cancel (0)
  5. L23
    apply add_left_cancel
  6. L24
    trans N
  7. L25
    exact ht_witness_witness_witness_left
  8. L26
    simp
  9. L27
    rewrite hk at ht_witness_witness_witness_right_right_left
  10. L28
    rewrite hk at ht_witness_witness_witness_right_right_left
05Calculate and transport equalitiesL29–30

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

  1. L29
    rewrite hk at ht_witness_witness_witness_right_right_left
  2. L30
    rewrite hk at ht_witness_witness_witness_right_right_left
06Establish hleftL31–39

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

  1. L31
    have hleft : x1=a
  2. L32
    specialize polynomial_zero_extended_entry_functional (ab)
  3. L33
    specialize polynomial_zero_extended_entry_functional (ac)
  4. L34
    specialize polynomial_zero_extended_entry_functional (S N)
  5. L35
    specialize polynomial_zero_extended_entry_functional (N)
  6. L36
    specialize polynomial_zero_extended_entry_functional (x1)
  7. L37
    specialize polynomial_zero_extended_entry_functional (a)
  8. L38
    apply polynomial_zero_extended_entry_functional
  9. L39
    exact ht_witness_witness_witness_right_left
07Separate the logical casesL40–41

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

  1. L40
    left
  2. L41
    split
08Construct an explicit witnessL42–42

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

  1. L42
    exists 0
09Use earlier factsL43–44

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

  1. L43
    apply zero_add
  2. L44
    exact ha
10Establish hrightL45–53

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

  1. L45
    have hright : x2=b
  2. L46
    specialize polynomial_zero_extended_entry_functional (bb)
  3. L47
    specialize polynomial_zero_extended_entry_functional (bc)
  4. L48
    specialize polynomial_zero_extended_entry_functional (S d)
  5. L49
    specialize polynomial_zero_extended_entry_functional (0)
  6. L50
    specialize polynomial_zero_extended_entry_functional (x2)
  7. L51
    specialize polynomial_zero_extended_entry_functional (b)
  8. L52
    apply polynomial_zero_extended_entry_functional
  9. L53
    exact ht_witness_witness_witness_right_right_left
11Separate the logical casesL54–55

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

  1. L54
    left
  2. L55
    split
12Construct an explicit witnessL56–56

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

  1. L56
    exists d
13Calculate and transport equalitiesL57–57

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

  1. L57
    simp
14Use earlier factsL58–58

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

  1. L58
    exact hb
15Calculate and transport equalitiesL59–59

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

  1. L59
    trans x1*x2
16Use earlier factsL60–60

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

  1. L60
    exact ht_witness_witness_witness_right_right_right
17Calculate and transport equalitiesL61–61

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

  1. L61
    congr
18Use earlier factsL62–63

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

  1. L62
    exact hleft
  2. L63
    exact hright

Library-wide reading audit

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