PX0027

prime_field_polynomial_quotient_scalar_cancellation

The actual inverse scalar solves the triangular coefficient equation, including prime two and an arbitrary nonzero divisor head.

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

∀ p. ∀ b. ∀ k. ∀ c. ∀ s. ∀ a. ∀ q. ∀ t. ∀ r. Prime(p) → FpInv(p,b,k) → FpAdd(p,c,s,a) → FpMul(p,k,s,q) → FpMul(p,q,b,t) → FpAdd(p,c,t,r) → r = a

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

Definition DAG

FpAdd(p,a,b,c) · 2FpMul(p,a,b,c) · 2FpInv(p,a,b) · 1Prime(p) · 1

Actual proof prerequisites

prime_field_multiply_associative · checked external prerequisiteprime_field_multiply_one_left · checked external prerequisiteprime_field_multiply_commutative · checked external prerequisiteprime_field_add_functional · checked external prerequisite
Original expanded first-order statement 
forall p b k c s a q t r. (~((p) = 1) /\ forall pfa_factor_left_division_scalar_prime pfa_factor_right_division_scalar_prime. (p) = pfa_factor_left_division_scalar_prime * pfa_factor_right_division_scalar_prime -> pfa_factor_left_division_scalar_prime = 1 \/ pfa_factor_right_division_scalar_prime = 1) -> (((~((b) = 0)) /\ ((((exists pfa_gap_division_scalar_inversemultiplicationleft. pfa_gap_division_scalar_inversemultiplicationleft + S (b) = (p)) /\ (((exists pfa_gap_division_scalar_inversemultiplicationright. pfa_gap_division_scalar_inversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_division_scalar_inversemultiplicationresultbound. pfa_gap_division_scalar_inversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_scalar_inversemultiplicationresultcongruence pfa_offset_right_division_scalar_inversemultiplicationresultcongruence. ((b) * (k)) + (p) * pfa_offset_left_division_scalar_inversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_scalar_inversemultiplicationresultcongruence)))))))))))) -> (((exists pfa_gap_division_scalar_differenceleft. pfa_gap_division_scalar_differenceleft + S (c) = (p)) /\ (((exists pfa_gap_division_scalar_differenceright. pfa_gap_division_scalar_differenceright + S (s) = (p)) /\ ((((exists pfa_gap_division_scalar_differenceresultbound. pfa_gap_division_scalar_differenceresultbound + S (a) = (p)) /\ ((exists pfa_offset_left_division_scalar_differenceresultcongruence pfa_offset_right_division_scalar_differenceresultcongruence. ((c) + (s)) + (p) * pfa_offset_left_division_scalar_differenceresultcongruence = (a) + (p) * pfa_offset_right_division_scalar_differenceresultcongruence))))))))) -> (((exists pfa_gap_division_scalar_quotientleft. pfa_gap_division_scalar_quotientleft + S (k) = (p)) /\ (((exists pfa_gap_division_scalar_quotientright. pfa_gap_division_scalar_quotientright + S (s) = (p)) /\ ((((exists pfa_gap_division_scalar_quotientresultbound. pfa_gap_division_scalar_quotientresultbound + S (q) = (p)) /\ ((exists pfa_offset_left_division_scalar_quotientresultcongruence pfa_offset_right_division_scalar_quotientresultcongruence. ((k) * (s)) + (p) * pfa_offset_left_division_scalar_quotientresultcongruence = (q) + (p) * pfa_offset_right_division_scalar_quotientresultcongruence))))))))) -> (((exists pfa_gap_division_scalar_productleft. pfa_gap_division_scalar_productleft + S (q) = (p)) /\ (((exists pfa_gap_division_scalar_productright. pfa_gap_division_scalar_productright + S (b) = (p)) /\ ((((exists pfa_gap_division_scalar_productresultbound. pfa_gap_division_scalar_productresultbound + S (t) = (p)) /\ ((exists pfa_offset_left_division_scalar_productresultcongruence pfa_offset_right_division_scalar_productresultcongruence. ((q) * (b)) + (p) * pfa_offset_left_division_scalar_productresultcongruence = (t) + (p) * pfa_offset_right_division_scalar_productresultcongruence))))))))) -> (((exists pfa_gap_division_scalar_sumleft. pfa_gap_division_scalar_sumleft + S (c) = (p)) /\ (((exists pfa_gap_division_scalar_sumright. pfa_gap_division_scalar_sumright + S (t) = (p)) /\ ((((exists pfa_gap_division_scalar_sumresultbound. pfa_gap_division_scalar_sumresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_division_scalar_sumresultcongruence pfa_offset_right_division_scalar_sumresultcongruence. ((c) + (t)) + (p) * pfa_offset_left_division_scalar_sumresultcongruence = (r) + (p) * pfa_offset_right_division_scalar_sumresultcongruence))))))))) -> r=a

Complete tactic proof in conservative notation

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

51 script commands · 8 reading checkpoints · 1 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–10

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro k
  4. L4
    intro c
  5. L5
    intro s
  6. L6
    intro a
  7. L7
    intro q
  8. L8
    intro t
  9. L9
    intro r
  10. L10
    intro hp
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hk
  2. L12
    intro ha
  3. L13
    intro hq
  4. L14
    intro ht
  5. L15
    intro hr
03Separate the logical casesL16–18

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

  1. L16
    cases hk
  2. L17
    cases hq
  3. L18
    cases hq_right
04Establish heqL19–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field multiply associative.

  1. L19
    have heq : s=t
  2. L20
    specialize prime_field_multiply_associative (p)
  3. L21
    specialize prime_field_multiply_associative (b)
  4. L22
    specialize prime_field_multiply_associative (k)
  5. L23
    specialize prime_field_multiply_associative (s)
  6. L24
    specialize prime_field_multiply_associative (1)
  7. L25
    specialize prime_field_multiply_associative (q)
  8. L26
    specialize prime_field_multiply_associative (s)
  9. L27
    specialize prime_field_multiply_associative (t)
  10. L28
    apply prime_field_multiply_associative
05Use earlier factsL29–38

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

  1. L29
    exact hk_right
  2. L30
    specialize prime_field_multiply_one_left (p)
  3. L31
    specialize prime_field_multiply_one_left (s)
  4. L32
    apply prime_field_multiply_one_left
  5. L33
    exact hp
  6. L34
    exact hq_right_left
  7. L35
    exact hq
  8. L36
    specialize prime_field_multiply_commutative (p)
  9. L37
    specialize prime_field_multiply_commutative (q)
  10. L38
    specialize prime_field_multiply_commutative (b)
06Use earlier factsL39–41

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

  1. L39
    specialize prime_field_multiply_commutative (t)
  2. L40
    apply prime_field_multiply_commutative
  3. L41
    exact ht
07Calculate and transport equalitiesL42–43

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

  1. L42
    rewrite heq at ha
  2. L43
    rewrite heq at ha
08Use earlier factsL44–51

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

  1. L44
    specialize prime_field_add_functional (p)
  2. L45
    specialize prime_field_add_functional (c)
  3. L46
    specialize prime_field_add_functional (t)
  4. L47
    specialize prime_field_add_functional (r)
  5. L48
    specialize prime_field_add_functional (a)
  6. L49
    apply prime_field_add_functional
  7. L50
    exact hr
  8. L51
    exact ha

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro k
  4. 0004intro c
  5. 0005intro s
  6. 0006intro a
  7. 0007intro q
  8. 0008intro t
  9. 0009intro r
  10. 0010intro hp
  11. 0011intro hk
  12. 0012intro ha
  13. 0013intro hq
  14. 0014intro ht
  15. 0015intro hr
  16. 0016cases hk
  17. 0017cases hq
  18. 0018cases hq_right
  19. 0019have heq : s=t
  20. 0020specialize prime_field_multiply_associative (p)
  21. 0021specialize prime_field_multiply_associative (b)
  22. 0022specialize prime_field_multiply_associative (k)
  23. 0023specialize prime_field_multiply_associative (s)
  24. 0024specialize prime_field_multiply_associative (1)
  25. 0025specialize prime_field_multiply_associative (q)
  26. 0026specialize prime_field_multiply_associative (s)
  27. 0027specialize prime_field_multiply_associative (t)
  28. 0028apply prime_field_multiply_associative
  29. 0029exact hk_right
  30. 0030specialize prime_field_multiply_one_left (p)
  31. 0031specialize prime_field_multiply_one_left (s)
  32. 0032apply prime_field_multiply_one_left
  33. 0033exact hp
  34. 0034exact hq_right_left
  35. 0035exact hq
  36. 0036specialize prime_field_multiply_commutative (p)
  37. 0037specialize prime_field_multiply_commutative (q)
  38. 0038specialize prime_field_multiply_commutative (b)
  39. 0039specialize prime_field_multiply_commutative (t)
  40. 0040apply prime_field_multiply_commutative
  41. 0041exact ht
  42. 0042rewrite heq at ha
  43. 0043rewrite heq at ha
  44. 0044specialize prime_field_add_functional (p)
  45. 0045specialize prime_field_add_functional (c)
  46. 0046specialize prime_field_add_functional (t)
  47. 0047specialize prime_field_add_functional (r)
  48. 0048specialize prime_field_add_functional (a)
  49. 0049apply prime_field_add_functional
  50. 0050exact hr
  51. 0051exact ha