PX006B

polynomial_product_length_left_padding_right

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic 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)) -> (((((L)=0 \/ (t+M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((t+M)=0)) /\ (((L)+(t+M)=S (K)))))))) -> (K=t+N)

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 44 exact native proof lines.

Alpha v34 checked-use · first admitted v33 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

add_eq_zero_right Alpha theorem; checked-use authorized succ_injective Alpha theorem; checked-use authorized add_assoc Alpha theorem; checked-use authorized add_comm Alpha theorem; checked-use authorized

Direct dependents

PX006D prime_field_polynomial_convolution_left_padding_nonempty_right

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

44 script commands · 14 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.

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–26

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

  1. L25
    apply hL
  2. L26
    exact hnew_left_left_left
08Separate the logical casesL27–27

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

  1. L27
    exfalso
09Use earlier factsL28–32

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

  1. L28
    apply hM
  2. L29
    specialize add_eq_zero_right (t)
  3. L30
    specialize add_eq_zero_right (M)
  4. L31
    apply add_eq_zero_right
  5. 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 (L)+(t+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–44

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

  1. L41
    trans t+(L+M)
  2. L42
    simp [add_assoc,add_comm]
  3. L43
    rewrite hold_right_right_right
  4. L44
    simp

Library-wide reading audit

Original exact 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. 0026exact hnew_left_left_left
  27. 0027exfalso
  28. 0028apply hM
  29. 0029specialize add_eq_zero_right (t)
  30. 0030specialize add_eq_zero_right (M)
  31. 0031apply add_eq_zero_right
  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 (L)+(t+M)
  39. 0039symm
  40. 0040exact hnew_right_right_right
  41. 0041trans t+(L+M)
  42. 0042simp [add_assoc,add_comm]
  43. 0043rewrite hold_right_right_right
  44. 0044simp