PX0055

polynomial_quotient_length_functional

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

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. ∀ d. ∀ q. ∀ Q. PolynomialQuotientLength(L,d,q) → PolynomialQuotientLength(L,d,Q) → q = Q

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

Definition DAG

PolynomialQuotientLength(L,d,q) · 2

Actual proof prerequisites

le_zero · checked external prerequisiteadd_le_cancel_right · checked external prerequisitezero_add · checked external prerequisiteadd_right_cancel · checked external prerequisite
Original expanded first-order 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

Complete tactic proof in conservative notation

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

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.

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