PG0009

polynomial_product_length_shift_right_nonempty

For two nonempty factors, shifting the right factor raises the proper product length by exactly one; empty factors are explicitly excluded.

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

∀ L. ∀ M. ∀ N. ∀ K. PolynomialProductLength(L,M,N) → ¬L = 0 → ¬M = 0 → PolynomialProductLength(L,S M,K) → K = S N

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

Definition DAG

PolynomialProductLength(L,M,N) · 2

Actual proof prerequisites

succ_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall L M N K. (((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) -> (~(L=0)) -> (~(M=0)) -> (((((L)=0 \/ (S M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((S M)=0)) /\ (((L)+(S M)=S (K)))))))) -> (K=S N)

Complete tactic proof in conservative notation

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

39 script commands · 17 reading checkpoints · 0 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–8

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

  1. L1
    intro L
  2. L2
    intro M
  3. L3
    intro N
  4. L4
    intro K
  5. L5
    intro hold
  6. L6
    intro hL
  7. L7
    intro hM
  8. L8
    intro hnew
02Separate the logical casesL9–12

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

  1. L9
    cases hold
  2. L10
    cases hold_left
  3. L11
    cases hold_left_left
  4. L12
    exfalso
03Use earlier factsL13–14

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

  1. L13
    apply hL
  2. L14
    exact hold_left_left_left
04Separate the logical casesL15–15

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

  1. L15
    exfalso
05Use earlier factsL16–17

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

  1. L16
    apply hM
  2. L17
    exact hold_left_left_right
06Separate the logical casesL18–23

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

  1. L18
    cases hold_right
  2. L19
    cases hold_right_right
  3. L20
    cases hnew
  4. L21
    cases hnew_left
  5. L22
    cases hnew_left_left
  6. L23
    exfalso
07Use earlier factsL24–25

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

  1. L24
    apply hL
  2. L25
    exact hnew_left_left_left
08Separate the logical casesL26–26

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

  1. L26
    exfalso
09Use earlier factsL27–29

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

  1. L27
    specialize succ_ne_zero (M)
  2. L28
    apply succ_ne_zero
  3. L29
    exact hnew_left_left_right
10Separate the logical casesL30–31

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

  1. L30
    cases hnew_right
  2. L31
    cases hnew_right_right
11Use earlier factsL32–32

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

  1. L32
    apply PA2
12Calculate and transport equalitiesL33–34

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

  1. L33
    trans L+S M
  2. L34
    symm
13Use earlier factsL35–35

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

  1. L35
    exact hnew_right_right_right
14Calculate and transport equalitiesL36–36

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

  1. L36
    trans S (L+M)
15Use earlier factsL37–37

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

  1. L37
    apply PA4
16Calculate and transport equalitiesL38–38

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

  1. L38
    congr
17Use earlier factsL39–39

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

  1. L39
    exact hold_right_right_right

Library-wide reading audit

Original defined command ledger · 39 lines
  1. 0001intro L
  2. 0002intro M
  3. 0003intro N
  4. 0004intro K
  5. 0005intro hold
  6. 0006intro hL
  7. 0007intro hM
  8. 0008intro hnew
  9. 0009cases hold
  10. 0010cases hold_left
  11. 0011cases hold_left_left
  12. 0012exfalso
  13. 0013apply hL
  14. 0014exact hold_left_left_left
  15. 0015exfalso
  16. 0016apply hM
  17. 0017exact hold_left_left_right
  18. 0018cases hold_right
  19. 0019cases hold_right_right
  20. 0020cases hnew
  21. 0021cases hnew_left
  22. 0022cases hnew_left_left
  23. 0023exfalso
  24. 0024apply hL
  25. 0025exact hnew_left_left_left
  26. 0026exfalso
  27. 0027specialize succ_ne_zero (M)
  28. 0028apply succ_ne_zero
  29. 0029exact hnew_left_left_right
  30. 0030cases hnew_right
  31. 0031cases hnew_right_right
  32. 0032apply PA2
  33. 0033trans L+S M
  34. 0034symm
  35. 0035exact hnew_right_right_right
  36. 0036trans S (L+M)
  37. 0037apply PA4
  38. 0038congr
  39. 0039exact hold_right_right_right