PX006A

polynomial_product_length_left_padding_left

For two nonempty input representations, padding the left factor increases the actual product length by exactly the padding count; empty factors are excluded explicitly.

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

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

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

Definition DAG

PolynomialProductLength(L,M,N) · 2

Actual proof prerequisites

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

Complete tactic proof in conservative notation

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

44 script commands · 16 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–9

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 t
  5. L5
    intro K
  6. L6
    intro hold
  7. L7
    intro hL
  8. L8
    intro hM
  9. L9
    intro hnew
02Separate the logical casesL10–13

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

  1. L10
    cases hold
  2. L11
    cases hold_left
  3. L12
    cases hold_left_left
  4. L13
    exfalso
03Use earlier factsL14–15

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

  1. L14
    apply hL
  2. L15
    exact hold_left_left_left
04Separate the logical casesL16–16

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

  1. L16
    exfalso
05Use earlier factsL17–18

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

  1. L17
    apply hM
  2. L18
    exact hold_left_left_right
06Separate the logical casesL19–24

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

  1. L19
    cases hold_right
  2. L20
    cases hold_right_right
  3. L21
    cases hnew
  4. L22
    cases hnew_left
  5. L23
    cases hnew_left_left
  6. L24
    exfalso
07Use earlier factsL25–29

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

  1. L25
    apply hL
  2. L26
    specialize add_eq_zero_right (t)
  3. L27
    specialize add_eq_zero_right (L)
  4. L28
    apply add_eq_zero_right
  5. L29
    exact hnew_left_left_left
08Separate the logical casesL30–30

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

  1. L30
    exfalso
09Use earlier factsL31–32

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

  1. L31
    apply hM
  2. L32
    exact hnew_left_left_right
10Separate the logical casesL33–34

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

  1. L33
    cases hnew_right
  2. L34
    cases hnew_right_right
11Use earlier factsL35–37

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

  1. L35
    specialize succ_injective (K)
  2. L36
    specialize succ_injective (t+N)
  3. L37
    apply succ_injective
12Calculate and transport equalitiesL38–39

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

  1. L38
    trans (t+L)+(M)
  2. L39
    symm
13Use earlier factsL40–40

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

  1. L40
    exact hnew_right_right_right
14Calculate and transport equalitiesL41–41

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

  1. L41
    trans t+(L+M)
15Use earlier factsL42–42

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

  1. L42
    apply add_assoc
16Calculate and transport equalitiesL43–44

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

  1. L43
    rewrite hold_right_right_right
  2. L44
    simp

Library-wide reading audit

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