PX000D

prime_field_polynomial_power_coefficient_functional

The actual coefficient of a formal power is unique, including the exterior and empty-prefix cases.

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

∀ b. ∀ c. ∀ L. PolynomialEquivalent(b,c,L,b,c,L)

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

Definition DAG

PolynomialEquivalent(b,c,L,d,e,M) · 1

Actual proof prerequisites

add_right_cancel · checked external prerequisitebeta_at_unique · checked external prerequisitelt_not_le · checked external prerequisite
Original expanded first-order statement 
forall b c L k a r. ((exists pfrep_position_power_unique_a. ((pfrep_position_power_unique_a+S (k)=(L)) /\ ((((exists ff_h_pfp_power_unique_aentry. ff_h_pfp_power_unique_aentry + S (a) = S ((S (pfrep_position_power_unique_a)) * c)) /\ exists ff_q_pfp_power_unique_aentry. b = ff_q_pfp_power_unique_aentry * S ((S (pfrep_position_power_unique_a)) * c) + (a)))))) \/ (((exists pfrep_gap_power_unique_aoutside. pfrep_gap_power_unique_aoutside+(L)=(k)) /\ (((a)=0))))) -> ((exists pfrep_position_power_unique_r. ((pfrep_position_power_unique_r+S (k)=(L)) /\ ((((exists ff_h_pfp_power_unique_rentry. ff_h_pfp_power_unique_rentry + S (r) = S ((S (pfrep_position_power_unique_r)) * c)) /\ exists ff_q_pfp_power_unique_rentry. b = ff_q_pfp_power_unique_rentry * S ((S (pfrep_position_power_unique_r)) * c) + (r)))))) \/ (((exists pfrep_gap_power_unique_routside. pfrep_gap_power_unique_routside+(L)=(k)) /\ (((r)=0))))) -> a=r

Complete tactic proof in conservative notation

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

57 script commands · 18 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–8

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro L
  4. L4
    intro k
  5. L5
    intro a
  6. L6
    intro r
  7. L7
    intro ha
  8. L8
    intro hr
02Separate the logical casesL9–14

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

  1. L9
    cases ha
  2. L10
    cases ha_left
  3. L11
    cases ha_left_witness
  4. L12
    cases hr
  5. L13
    cases hr_left
  6. L14
    cases hr_left_witness
03Establish heqL15–24

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

  1. L15
    have heq : x=x1
  2. L16
    specialize add_right_cancel (x)
  3. L17
    specialize add_right_cancel (x1)
  4. L18
    specialize add_right_cancel (S k)
  5. L19
    apply add_right_cancel
  6. L20
    trans L
  7. L21
    exact ha_left_witness_left
  8. L22
    symm
  9. L23
    exact hr_left_witness_left
  10. L24
    rewrite heq at ha_left_witness_right
04Calculate and transport equalitiesL25–25

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

  1. L25
    rewrite heq at ha_left_witness_right
05Use earlier factsL26–33

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

  1. L26
    specialize beta_at_unique (b)
  2. L27
    specialize beta_at_unique (c)
  3. L28
    specialize beta_at_unique (x1)
  4. L29
    specialize beta_at_unique (a)
  5. L30
    specialize beta_at_unique (r)
  6. L31
    apply beta_at_unique
  7. L32
    exact ha_left_witness_right
  8. L33
    exact hr_left_witness_right
06Separate the logical casesL34–35

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

  1. L34
    cases hr_right
  2. L35
    exfalso
07Use earlier factsL36–38

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

  1. L36
    specialize lt_not_le (k)
  2. L37
    specialize lt_not_le (L)
  3. L38
    apply lt_not_le
08Construct an explicit witnessL39–39

Supply the displayed value, then prove that it has the required property.

  1. L39
    exists x
09Use earlier factsL40–41

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

  1. L40
    exact ha_left_witness_left
  2. L41
    exact hr_right_left
10Separate the logical casesL42–46

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

  1. L42
    cases ha_right
  2. L43
    cases hr
  3. L44
    cases hr_left
  4. L45
    cases hr_left_witness
  5. L46
    exfalso
11Use earlier factsL47–49

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

  1. L47
    specialize lt_not_le (k)
  2. L48
    specialize lt_not_le (L)
  3. L49
    apply lt_not_le
12Construct an explicit witnessL50–50

Supply the displayed value, then prove that it has the required property.

  1. L50
    exists x
13Use earlier factsL51–52

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

  1. L51
    exact hr_left_witness_left
  2. L52
    exact ha_right_left
14Separate the logical casesL53–53

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

  1. L53
    cases hr_right
15Calculate and transport equalitiesL54–54

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

  1. L54
    trans 0
16Use earlier factsL55–55

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

  1. L55
    exact ha_right_right
17Calculate and transport equalitiesL56–56

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

  1. L56
    symm
18Use earlier factsL57–57

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

  1. L57
    exact hr_right_right

Library-wide reading audit

Original defined command ledger · 57 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro L
  4. 0004intro k
  5. 0005intro a
  6. 0006intro r
  7. 0007intro ha
  8. 0008intro hr
  9. 0009cases ha
  10. 0010cases ha_left
  11. 0011cases ha_left_witness
  12. 0012cases hr
  13. 0013cases hr_left
  14. 0014cases hr_left_witness
  15. 0015have heq : x=x1
  16. 0016specialize add_right_cancel (x)
  17. 0017specialize add_right_cancel (x1)
  18. 0018specialize add_right_cancel (S k)
  19. 0019apply add_right_cancel
  20. 0020trans L
  21. 0021exact ha_left_witness_left
  22. 0022symm
  23. 0023exact hr_left_witness_left
  24. 0024rewrite heq at ha_left_witness_right
  25. 0025rewrite heq at ha_left_witness_right
  26. 0026specialize beta_at_unique (b)
  27. 0027specialize beta_at_unique (c)
  28. 0028specialize beta_at_unique (x1)
  29. 0029specialize beta_at_unique (a)
  30. 0030specialize beta_at_unique (r)
  31. 0031apply beta_at_unique
  32. 0032exact ha_left_witness_right
  33. 0033exact hr_left_witness_right
  34. 0034cases hr_right
  35. 0035exfalso
  36. 0036specialize lt_not_le (k)
  37. 0037specialize lt_not_le (L)
  38. 0038apply lt_not_le
  39. 0039exists x
  40. 0040exact ha_left_witness_left
  41. 0041exact hr_right_left
  42. 0042cases ha_right
  43. 0043cases hr
  44. 0044cases hr_left
  45. 0045cases hr_left_witness
  46. 0046exfalso
  47. 0047specialize lt_not_le (k)
  48. 0048specialize lt_not_le (L)
  49. 0049apply lt_not_le
  50. 0050exists x
  51. 0051exact hr_left_witness_left
  52. 0052exact ha_right_left
  53. 0053cases hr_right
  54. 0054trans 0
  55. 0055exact ha_right_right
  56. 0056symm
  57. 0057exact hr_right_right