PX0026

prime_field_polynomial_inverse_scale

An actual inverse scalar gives the reverse coefficient action, with a constructed intermediate table and exact decoded transport; no unit-associate law is assumed.

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. ∀ a. ∀ k. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ L. Prime(p) → FpInv(p,a,k) → FpPolyScale(p,k,ab,ac,bb,bc,L) → FpPolyScale(p,a,bb,bc,ab,ac,L)

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

Definition DAG

FpMul(p,a,b,c) · 1FpInv(p,a,b) · 1BetaPrefixInto(b,c,l,B) · 2BetaPrefixEqual(b,c,d,e,l) · 1FpPolyScale(p,k,ab,ac,bb,bc,l) · 3Prime(p) · 1

Actual proof prerequisites

prime_field_polynomial_scale_bounded · checked external prerequisiteprime_field_polynomial_scale_exists · checked external prerequisiteprime_nonzero · checked external prerequisiteprime_field_polynomial_scale_associative · checked external prerequisiteprime_field_polynomial_scale_one · checked external prerequisiteprime_field_polynomial_scale_transport · checked external prerequisite
Original expanded first-order statement 
forall p a k ab ac bb bc L. (~((p) = 1) /\ forall pfa_factor_left_inverse_scale_prime pfa_factor_right_inverse_scale_prime. (p) = pfa_factor_left_inverse_scale_prime * pfa_factor_right_inverse_scale_prime -> pfa_factor_left_inverse_scale_prime = 1 \/ pfa_factor_right_inverse_scale_prime = 1) -> (((~((a) = 0)) /\ ((((exists pfa_gap_inverse_scale_inversemultiplicationleft. pfa_gap_inverse_scale_inversemultiplicationleft + S (a) = (p)) /\ (((exists pfa_gap_inverse_scale_inversemultiplicationright. pfa_gap_inverse_scale_inversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_inverse_scale_inversemultiplicationresultbound. pfa_gap_inverse_scale_inversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_inverse_scale_inversemultiplicationresultcongruence pfa_offset_right_inverse_scale_inversemultiplicationresultcongruence. ((a) * (k)) + (p) * pfa_offset_left_inverse_scale_inversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_inverse_scale_inversemultiplicationresultcongruence)))))))))))) -> (((exists pfa_gap_inverse_scale_forwardscalar. pfa_gap_inverse_scale_forwardscalar + S (k) = (p)) /\ ((forall pfp_index_inverse_scale_forward. (exists pfa_gap_inverse_scale_forwardindex. pfa_gap_inverse_scale_forwardindex + S (pfp_index_inverse_scale_forward) = (L)) -> exists pfp_source_inverse_scale_forward pfp_value_inverse_scale_forward. ((((exists ff_h_pfp_inverse_scale_forwardsource. ff_h_pfp_inverse_scale_forwardsource + S (pfp_source_inverse_scale_forward) = S ((S (pfp_index_inverse_scale_forward)) * ac)) /\ exists ff_q_pfp_inverse_scale_forwardsource. ab = ff_q_pfp_inverse_scale_forwardsource * S ((S (pfp_index_inverse_scale_forward)) * ac) + (pfp_source_inverse_scale_forward))) /\ (((((exists ff_h_pfp_inverse_scale_forwardtarget. ff_h_pfp_inverse_scale_forwardtarget + S (pfp_value_inverse_scale_forward) = S ((S (pfp_index_inverse_scale_forward)) * bc)) /\ exists ff_q_pfp_inverse_scale_forwardtarget. bb = ff_q_pfp_inverse_scale_forwardtarget * S ((S (pfp_index_inverse_scale_forward)) * bc) + (pfp_value_inverse_scale_forward))) /\ ((((exists pfa_gap_inverse_scale_forwardoperationleft. pfa_gap_inverse_scale_forwardoperationleft + S (k) = (p)) /\ (((exists pfa_gap_inverse_scale_forwardoperationright. pfa_gap_inverse_scale_forwardoperationright + S (pfp_source_inverse_scale_forward) = (p)) /\ ((((exists pfa_gap_inverse_scale_forwardoperationresultbound. pfa_gap_inverse_scale_forwardoperationresultbound + S (pfp_value_inverse_scale_forward) = (p)) /\ ((exists pfa_offset_left_inverse_scale_forwardoperationresultcongruence pfa_offset_right_inverse_scale_forwardoperationresultcongruence. ((k) * (pfp_source_inverse_scale_forward)) + (p) * pfa_offset_left_inverse_scale_forwardoperationresultcongruence = (pfp_value_inverse_scale_forward) + (p) * pfa_offset_right_inverse_scale_forwardoperationresultcongruence))))))))))))))))) -> (((exists pfa_gap_inverse_scale_backwardscalar. pfa_gap_inverse_scale_backwardscalar + S (a) = (p)) /\ ((forall pfp_index_inverse_scale_backward. (exists pfa_gap_inverse_scale_backwardindex. pfa_gap_inverse_scale_backwardindex + S (pfp_index_inverse_scale_backward) = (L)) -> exists pfp_source_inverse_scale_backward pfp_value_inverse_scale_backward. ((((exists ff_h_pfp_inverse_scale_backwardsource. ff_h_pfp_inverse_scale_backwardsource + S (pfp_source_inverse_scale_backward) = S ((S (pfp_index_inverse_scale_backward)) * bc)) /\ exists ff_q_pfp_inverse_scale_backwardsource. bb = ff_q_pfp_inverse_scale_backwardsource * S ((S (pfp_index_inverse_scale_backward)) * bc) + (pfp_source_inverse_scale_backward))) /\ (((((exists ff_h_pfp_inverse_scale_backwardtarget. ff_h_pfp_inverse_scale_backwardtarget + S (pfp_value_inverse_scale_backward) = S ((S (pfp_index_inverse_scale_backward)) * ac)) /\ exists ff_q_pfp_inverse_scale_backwardtarget. ab = ff_q_pfp_inverse_scale_backwardtarget * S ((S (pfp_index_inverse_scale_backward)) * ac) + (pfp_value_inverse_scale_backward))) /\ ((((exists pfa_gap_inverse_scale_backwardoperationleft. pfa_gap_inverse_scale_backwardoperationleft + S (a) = (p)) /\ (((exists pfa_gap_inverse_scale_backwardoperationright. pfa_gap_inverse_scale_backwardoperationright + S (pfp_source_inverse_scale_backward) = (p)) /\ ((((exists pfa_gap_inverse_scale_backwardoperationresultbound. pfa_gap_inverse_scale_backwardoperationresultbound + S (pfp_value_inverse_scale_backward) = (p)) /\ ((exists pfa_offset_left_inverse_scale_backwardoperationresultcongruence pfa_offset_right_inverse_scale_backwardoperationresultcongruence. ((a) * (pfp_source_inverse_scale_backward)) + (p) * pfa_offset_left_inverse_scale_backwardoperationresultcongruence = (pfp_value_inverse_scale_backward) + (p) * pfa_offset_right_inverse_scale_backwardoperationresultcongruence)))))))))))))))))

Complete tactic proof in conservative notation

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

88 script commands · 15 reading checkpoints · 4 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 a
  3. L3
    intro k
  4. L4
    intro ab
  5. L5
    intro ac
  6. L6
    intro bb
  7. L7
    intro bc
  8. L8
    intro L
  9. L9
    intro hp
  10. L10
    intro hinv
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hs
03Establish hboundL12–21

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

  1. L12
    have hbound : BetaPrefixInto(ab,ac,L,p) ∧ BetaPrefixInto(bb,bc,L,p)Definitions: BetaPrefixInto(ab,ac,L,p)BetaPrefixInto(bb,bc,L,p)Original native command in the exact edition
  2. L13
    specialize prime_field_polynomial_scale_bounded (p)
  3. L14
    specialize prime_field_polynomial_scale_bounded (k)
  4. L15
    specialize prime_field_polynomial_scale_bounded (ab)
  5. L16
    specialize prime_field_polynomial_scale_bounded (ac)
  6. L17
    specialize prime_field_polynomial_scale_bounded (bb)
  7. L18
    specialize prime_field_polynomial_scale_bounded (bc)
  8. L19
    specialize prime_field_polynomial_scale_bounded (L)
  9. L20
    apply prime_field_polynomial_scale_bounded
  10. L21
    exact hs
04Separate the logical casesL22–23

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

  1. L22
    cases hbound
  2. L23
    cases hinv
05Establish hmL24–25

Establish this local claim before using it. It is not an additional assumption.

  1. L24
  2. L25
    exact hinv_right
06Separate the logical casesL26–28

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

  1. L26
    cases hinv_right
  2. L27
    cases hinv_right_right
  3. L28
    cases hinv_right_right_right
07Establish hrL29–38

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

  1. L29
    have hr : ∃ cb. ∃ cc. FpPolyScale(p,a,bb,bc,cb,cc,L)Definitions: FpPolyScale(p,a,bb,bc,cb,cc,L)Original native command in the exact edition
  2. L30
    specialize prime_field_polynomial_scale_exists (p)
  3. L31
    specialize prime_field_polynomial_scale_exists (a)
  4. L32
    specialize prime_field_polynomial_scale_exists (bb)
  5. L33
    specialize prime_field_polynomial_scale_exists (bc)
  6. L34
    specialize prime_field_polynomial_scale_exists (L)
  7. L35
    apply prime_field_polynomial_scale_exists
  8. L36
    intro hpzero
  9. L37
    specialize prime_nonzero (p)
  10. L38
    apply prime_nonzero
08Use earlier factsL39–42

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

  1. L39
    exact hp
  2. L40
    exact hpzero
  3. L41
    exact hinv_right_left
  4. L42
    exact hbound_right
09Separate the logical casesL43–44

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

  1. L43
    cases hr
  2. L44
    cases hr_witness
10Establish heL45–54

Establish this local claim before using it. It is not an additional assumption.

  1. L45
    have he : BetaPrefixEqual(x,x1,ab,ac,L)Definitions: BetaPrefixEqual(x,x1,ab,ac,L)Original native command in the exact edition
  2. L46
    specialize prime_field_polynomial_scale_associative (p)
  3. L47
    specialize prime_field_polynomial_scale_associative (a)
  4. L48
    specialize prime_field_polynomial_scale_associative (k)
  5. L49
    specialize prime_field_polynomial_scale_associative (1)
  6. L50
    specialize prime_field_polynomial_scale_associative (ab)
  7. L51
    specialize prime_field_polynomial_scale_associative (ac)
  8. L52
    specialize prime_field_polynomial_scale_associative (bb)
  9. L53
    specialize prime_field_polynomial_scale_associative (bc)
  10. L54
    specialize prime_field_polynomial_scale_associative (x)
11Use earlier factsL55–64

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

  1. L55
    specialize prime_field_polynomial_scale_associative (x1)
  2. L56
    specialize prime_field_polynomial_scale_associative (ab)
  3. L57
    specialize prime_field_polynomial_scale_associative (ac)
  4. L58
    specialize prime_field_polynomial_scale_associative (L)
  5. L59
    apply prime_field_polynomial_scale_associative
  6. L60
    exact hm
  7. L61
    exact hs
  8. L62
    exact hr_witness_witness
  9. L63
    specialize prime_field_polynomial_scale_one (p)
  10. L64
    specialize prime_field_polynomial_scale_one (ab)
12Use earlier factsL65–74

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

  1. L65
    specialize prime_field_polynomial_scale_one (ac)
  2. L66
    specialize prime_field_polynomial_scale_one (L)
  3. L67
    apply prime_field_polynomial_scale_one
  4. L68
    exact hp
  5. L69
    exact hbound_left
  6. L70
    specialize prime_field_polynomial_scale_transport (p)
  7. L71
    specialize prime_field_polynomial_scale_transport (a)
  8. L72
    specialize prime_field_polynomial_scale_transport (bb)
  9. L73
    specialize prime_field_polynomial_scale_transport (bc)
  10. L74
    specialize prime_field_polynomial_scale_transport (x)
13Use earlier factsL75–81

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

  1. L75
    specialize prime_field_polynomial_scale_transport (x1)
  2. L76
    specialize prime_field_polynomial_scale_transport (bb)
  3. L77
    specialize prime_field_polynomial_scale_transport (bc)
  4. L78
    specialize prime_field_polynomial_scale_transport (ab)
  5. L79
    specialize prime_field_polynomial_scale_transport (ac)
  6. L80
    specialize prime_field_polynomial_scale_transport (L)
  7. L81
    apply prime_field_polynomial_scale_transport
14Fix variables and assumptionsL82–85

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

  1. L82
    intro i
  2. L83
    intro r
  3. L84
    intro hi
  4. L85
    intro hat
15Use earlier factsL86–88

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

  1. L86
    exact hat
  2. L87
    exact he
  3. L88
    exact hr_witness_witness

Library-wide reading audit

Original defined command ledger · 88 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro k
  4. 0004intro ab
  5. 0005intro ac
  6. 0006intro bb
  7. 0007intro bc
  8. 0008intro L
  9. 0009intro hp
  10. 0010intro hinv
  11. 0011intro hs
  12. 0012have hbound : BetaPrefixInto(ab,ac,L,p) ∧ BetaPrefixInto(bb,bc,L,p)
  13. 0013specialize prime_field_polynomial_scale_bounded (p)
  14. 0014specialize prime_field_polynomial_scale_bounded (k)
  15. 0015specialize prime_field_polynomial_scale_bounded (ab)
  16. 0016specialize prime_field_polynomial_scale_bounded (ac)
  17. 0017specialize prime_field_polynomial_scale_bounded (bb)
  18. 0018specialize prime_field_polynomial_scale_bounded (bc)
  19. 0019specialize prime_field_polynomial_scale_bounded (L)
  20. 0020apply prime_field_polynomial_scale_bounded
  21. 0021exact hs
  22. 0022cases hbound
  23. 0023cases hinv
  24. 0024have hm : FpMul(p,a,k,1)
  25. 0025exact hinv_right
  26. 0026cases hinv_right
  27. 0027cases hinv_right_right
  28. 0028cases hinv_right_right_right
  29. 0029have hr : ∃ cb. ∃ cc. FpPolyScale(p,a,bb,bc,cb,cc,L)
  30. 0030specialize prime_field_polynomial_scale_exists (p)
  31. 0031specialize prime_field_polynomial_scale_exists (a)
  32. 0032specialize prime_field_polynomial_scale_exists (bb)
  33. 0033specialize prime_field_polynomial_scale_exists (bc)
  34. 0034specialize prime_field_polynomial_scale_exists (L)
  35. 0035apply prime_field_polynomial_scale_exists
  36. 0036intro hpzero
  37. 0037specialize prime_nonzero (p)
  38. 0038apply prime_nonzero
  39. 0039exact hp
  40. 0040exact hpzero
  41. 0041exact hinv_right_left
  42. 0042exact hbound_right
  43. 0043cases hr
  44. 0044cases hr_witness
  45. 0045have he : BetaPrefixEqual(x,x1,ab,ac,L)
  46. 0046specialize prime_field_polynomial_scale_associative (p)
  47. 0047specialize prime_field_polynomial_scale_associative (a)
  48. 0048specialize prime_field_polynomial_scale_associative (k)
  49. 0049specialize prime_field_polynomial_scale_associative (1)
  50. 0050specialize prime_field_polynomial_scale_associative (ab)
  51. 0051specialize prime_field_polynomial_scale_associative (ac)
  52. 0052specialize prime_field_polynomial_scale_associative (bb)
  53. 0053specialize prime_field_polynomial_scale_associative (bc)
  54. 0054specialize prime_field_polynomial_scale_associative (x)
  55. 0055specialize prime_field_polynomial_scale_associative (x1)
  56. 0056specialize prime_field_polynomial_scale_associative (ab)
  57. 0057specialize prime_field_polynomial_scale_associative (ac)
  58. 0058specialize prime_field_polynomial_scale_associative (L)
  59. 0059apply prime_field_polynomial_scale_associative
  60. 0060exact hm
  61. 0061exact hs
  62. 0062exact hr_witness_witness
  63. 0063specialize prime_field_polynomial_scale_one (p)
  64. 0064specialize prime_field_polynomial_scale_one (ab)
  65. 0065specialize prime_field_polynomial_scale_one (ac)
  66. 0066specialize prime_field_polynomial_scale_one (L)
  67. 0067apply prime_field_polynomial_scale_one
  68. 0068exact hp
  69. 0069exact hbound_left
  70. 0070specialize prime_field_polynomial_scale_transport (p)
  71. 0071specialize prime_field_polynomial_scale_transport (a)
  72. 0072specialize prime_field_polynomial_scale_transport (bb)
  73. 0073specialize prime_field_polynomial_scale_transport (bc)
  74. 0074specialize prime_field_polynomial_scale_transport (x)
  75. 0075specialize prime_field_polynomial_scale_transport (x1)
  76. 0076specialize prime_field_polynomial_scale_transport (bb)
  77. 0077specialize prime_field_polynomial_scale_transport (bc)
  78. 0078specialize prime_field_polynomial_scale_transport (ab)
  79. 0079specialize prime_field_polynomial_scale_transport (ac)
  80. 0080specialize prime_field_polynomial_scale_transport (L)
  81. 0081apply prime_field_polynomial_scale_transport
  82. 0082intro i
  83. 0083intro r
  84. 0084intro hi
  85. 0085intro hat
  86. 0086exact hat
  87. 0087exact he
  88. 0088exact hr_witness_witness