PX0055

polynomial_quotient_length_functional

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

The actual short-input or positive-length quotient convention determines exactly one natural length, including L=0 and d=0.

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 d q Q. (((((q)=0) /\ ((exists pfc_gap_length_unique_firstshort. pfc_gap_length_unique_firstshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) -> (((((Q)=0) /\ ((exists pfc_gap_length_unique_secondshort. pfc_gap_length_unique_secondshort+(L)=(d))))) \/ (((~((Q)=0)) /\ (((Q)+(d)=(L)))))) -> q=Q

Constructive proof overview

Generated structural guide

The actual short-input or positive-length quotient convention determines exactly one natural length, including L=0 and d=0.

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

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

Proof neighborhood

Direct dependencies

le_zero Alpha theorem; checked-use authorized add_le_cancel_right Alpha theorem; checked-use authorized zero_add Alpha theorem; checked-use authorized add_right_cancel Alpha theorem; checked-use authorized

Direct dependents

PX0057 prime_field_polynomial_division_quotient_data_functional

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

55 script commands · 18 reading checkpoints · 2 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–6

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

  1. L1
    intro L
  2. L2
    intro d
  3. L3
    intro q
  4. L4
    intro Q
  5. L5
    intro hfirst
  6. L6
    intro hsecond
02Separate the logical casesL7–10

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

  1. L7
    cases hfirst
  2. L8
    cases hfirst_left
  3. L9
    cases hsecond
  4. L10
    cases hsecond_left
03Calculate and transport equalitiesL11–11

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

  1. L11
    trans 0
04Use earlier factsL12–12

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

  1. L12
    exact hfirst_left_left
05Calculate and transport equalitiesL13–13

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

  1. L13
    symm
06Use earlier factsL14–14

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

  1. L14
    exact hsecond_left_left
07Separate the logical casesL15–16

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

  1. L15
    cases hsecond_right
  2. L16
    exfalso
08Use earlier factsL17–23

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

  1. L17
    apply hsecond_right_left
  2. L18
    specialize le_zero (Q)
  3. L19
    apply le_zero
  4. L20
    specialize add_le_cancel_right (Q)
  5. L21
    specialize add_le_cancel_right (0)
  6. L22
    specialize add_le_cancel_right (d)
  7. L23
    apply add_le_cancel_right
09Establish hzeroL24–29

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

  1. L24
    have hzero : 0+d=d
  2. L25
    specialize zero_add (d)
  3. L26
    apply zero_add
  4. L27
    rewrite hzero
  5. L28
    rewrite hsecond_right_right
  6. L29
    exact hfirst_left_right
10Separate the logical casesL30–33

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

  1. L30
    cases hfirst_right
  2. L31
    cases hsecond
  3. L32
    cases hsecond_left
  4. L33
    exfalso
11Use earlier factsL34–40

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

  1. L34
    apply hfirst_right_left
  2. L35
    specialize le_zero (q)
  3. L36
    apply le_zero
  4. L37
    specialize add_le_cancel_right (q)
  5. L38
    specialize add_le_cancel_right (0)
  6. L39
    specialize add_le_cancel_right (d)
  7. L40
    apply add_le_cancel_right
12Establish hzeroL41–46

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

  1. L41
    have hzero : 0+d=d
  2. L42
    specialize zero_add (d)
  3. L43
    apply zero_add
  4. L44
    rewrite hzero
  5. L45
    rewrite hfirst_right_right
  6. L46
    exact hsecond_left_right
13Separate the logical casesL47–47

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

  1. L47
    cases hsecond_right
14Use earlier factsL48–51

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

  1. L48
    specialize add_right_cancel (q)
  2. L49
    specialize add_right_cancel (Q)
  3. L50
    specialize add_right_cancel (d)
  4. L51
    apply add_right_cancel
15Calculate and transport equalitiesL52–52

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

  1. L52
    trans L
16Use earlier factsL53–53

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

  1. L53
    exact hfirst_right_right
17Calculate and transport equalitiesL54–54

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

  1. L54
    symm
18Use earlier factsL55–55

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

  1. L55
    exact hsecond_right_right

Library-wide reading audit

Original exact command ledger · 55 lines
  1. 0001intro L
  2. 0002intro d
  3. 0003intro q
  4. 0004intro Q
  5. 0005intro hfirst
  6. 0006intro hsecond
  7. 0007cases hfirst
  8. 0008cases hfirst_left
  9. 0009cases hsecond
  10. 0010cases hsecond_left
  11. 0011trans 0
  12. 0012exact hfirst_left_left
  13. 0013symm
  14. 0014exact hsecond_left_left
  15. 0015cases hsecond_right
  16. 0016exfalso
  17. 0017apply hsecond_right_left
  18. 0018specialize le_zero (Q)
  19. 0019apply le_zero
  20. 0020specialize add_le_cancel_right (Q)
  21. 0021specialize add_le_cancel_right (0)
  22. 0022specialize add_le_cancel_right (d)
  23. 0023apply add_le_cancel_right
  24. 0024have hzero : 0+d=d
  25. 0025specialize zero_add (d)
  26. 0026apply zero_add
  27. 0027rewrite hzero
  28. 0028rewrite hsecond_right_right
  29. 0029exact hfirst_left_right
  30. 0030cases hfirst_right
  31. 0031cases hsecond
  32. 0032cases hsecond_left
  33. 0033exfalso
  34. 0034apply hfirst_right_left
  35. 0035specialize le_zero (q)
  36. 0036apply le_zero
  37. 0037specialize add_le_cancel_right (q)
  38. 0038specialize add_le_cancel_right (0)
  39. 0039specialize add_le_cancel_right (d)
  40. 0040apply add_le_cancel_right
  41. 0041have hzero : 0+d=d
  42. 0042specialize zero_add (d)
  43. 0043apply zero_add
  44. 0044rewrite hzero
  45. 0045rewrite hfirst_right_right
  46. 0046exact hsecond_left_right
  47. 0047cases hsecond_right
  48. 0048specialize add_right_cancel (q)
  49. 0049specialize add_right_cancel (Q)
  50. 0050specialize add_right_cancel (d)
  51. 0051apply add_right_cancel
  52. 0052trans L
  53. 0053exact hfirst_right_right
  54. 0054symm
  55. 0055exact hsecond_right_right