PG0003

prime_field_polynomial_shift_functional

Two actual shifts agree on their successor-length decoded prefix; neither raw code nor any later entry is identified.

Alpha v34 checked-use · first admitted v34 · 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.

All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ L. ∀ d. ∀ e. ∀ f. ∀ g. PolynomialShift(b,c,L,d,e) → PolynomialShift(b,c,L,f,g) → BetaPrefixEqual(d,e,f,g,S L)

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

Definition DAG

BetaPrefixEqual(b,c,d,e,l) · 1PolynomialShift(b,c,L,d,e) · 2Lt(a,b) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

finite_lt_succ_eq_or_lt · checked external prerequisitebeta_at_unique · checked external prerequisitebeta_at_exists · checked external prerequisite
Original expanded first-order statement 
forall b c L d e f g. (((forall mdr_i_pfp_shift_unique_firstprefix mdr_a_pfp_shift_unique_firstprefix. (exists mdr_gap_pfp_shift_unique_firstprefixb. mdr_gap_pfp_shift_unique_firstprefixb + S (mdr_i_pfp_shift_unique_firstprefix) = (L)) -> (((exists ff_h_mdr_pfp_shift_unique_firstprefixo. ff_h_mdr_pfp_shift_unique_firstprefixo + S (mdr_a_pfp_shift_unique_firstprefix) = S ((S (mdr_i_pfp_shift_unique_firstprefix)) * c)) /\ exists ff_q_mdr_pfp_shift_unique_firstprefixo. b = ff_q_mdr_pfp_shift_unique_firstprefixo * S ((S (mdr_i_pfp_shift_unique_firstprefix)) * c) + (mdr_a_pfp_shift_unique_firstprefix))) -> (((exists ff_h_mdr_pfp_shift_unique_firstprefixn. ff_h_mdr_pfp_shift_unique_firstprefixn + S (mdr_a_pfp_shift_unique_firstprefix) = S ((S (mdr_i_pfp_shift_unique_firstprefix)) * e)) /\ exists ff_q_mdr_pfp_shift_unique_firstprefixn. d = ff_q_mdr_pfp_shift_unique_firstprefixn * S ((S (mdr_i_pfp_shift_unique_firstprefix)) * e) + (mdr_a_pfp_shift_unique_firstprefix)))) /\ ((((exists ff_h_pfp_shift_unique_firstlast. ff_h_pfp_shift_unique_firstlast + S (0) = S ((S (L)) * e)) /\ exists ff_q_pfp_shift_unique_firstlast. d = ff_q_pfp_shift_unique_firstlast * S ((S (L)) * e) + (0)))))) -> (((forall mdr_i_pfp_shift_unique_secondprefix mdr_a_pfp_shift_unique_secondprefix. (exists mdr_gap_pfp_shift_unique_secondprefixb. mdr_gap_pfp_shift_unique_secondprefixb + S (mdr_i_pfp_shift_unique_secondprefix) = (L)) -> (((exists ff_h_mdr_pfp_shift_unique_secondprefixo. ff_h_mdr_pfp_shift_unique_secondprefixo + S (mdr_a_pfp_shift_unique_secondprefix) = S ((S (mdr_i_pfp_shift_unique_secondprefix)) * c)) /\ exists ff_q_mdr_pfp_shift_unique_secondprefixo. b = ff_q_mdr_pfp_shift_unique_secondprefixo * S ((S (mdr_i_pfp_shift_unique_secondprefix)) * c) + (mdr_a_pfp_shift_unique_secondprefix))) -> (((exists ff_h_mdr_pfp_shift_unique_secondprefixn. ff_h_mdr_pfp_shift_unique_secondprefixn + S (mdr_a_pfp_shift_unique_secondprefix) = S ((S (mdr_i_pfp_shift_unique_secondprefix)) * g)) /\ exists ff_q_mdr_pfp_shift_unique_secondprefixn. f = ff_q_mdr_pfp_shift_unique_secondprefixn * S ((S (mdr_i_pfp_shift_unique_secondprefix)) * g) + (mdr_a_pfp_shift_unique_secondprefix)))) /\ ((((exists ff_h_pfp_shift_unique_secondlast. ff_h_pfp_shift_unique_secondlast + S (0) = S ((S (L)) * g)) /\ exists ff_q_pfp_shift_unique_secondlast. f = ff_q_pfp_shift_unique_secondlast * S ((S (L)) * g) + (0)))))) -> (forall mdr_i_pfp_shift_unique_result mdr_a_pfp_shift_unique_result. (exists mdr_gap_pfp_shift_unique_resultb. mdr_gap_pfp_shift_unique_resultb + S (mdr_i_pfp_shift_unique_result) = (S L)) -> (((exists ff_h_mdr_pfp_shift_unique_resulto. ff_h_mdr_pfp_shift_unique_resulto + S (mdr_a_pfp_shift_unique_result) = S ((S (mdr_i_pfp_shift_unique_result)) * e)) /\ exists ff_q_mdr_pfp_shift_unique_resulto. d = ff_q_mdr_pfp_shift_unique_resulto * S ((S (mdr_i_pfp_shift_unique_result)) * e) + (mdr_a_pfp_shift_unique_result))) -> (((exists ff_h_mdr_pfp_shift_unique_resultn. ff_h_mdr_pfp_shift_unique_resultn + S (mdr_a_pfp_shift_unique_result) = S ((S (mdr_i_pfp_shift_unique_result)) * g)) /\ exists ff_q_mdr_pfp_shift_unique_resultn. f = ff_q_mdr_pfp_shift_unique_resultn * S ((S (mdr_i_pfp_shift_unique_result)) * g) + (mdr_a_pfp_shift_unique_result))))

Complete tactic proof in conservative notation

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

63 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–9

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 d
  5. L5
    intro e
  6. L6
    intro f
  7. L7
    intro g
  8. L8
    intro hd
  9. L9
    intro hf
02Separate the logical casesL10–11

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

  1. L10
    cases hd
  2. L11
    cases hf
03Fix variables and assumptionsL12–15

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

  1. L12
    intro i
  2. L13
    intro a
  3. L14
    intro hi
  4. L15
    intro ha
04Establish hoL16–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L16
    have ho : i = L ∨ Lt(i,L)Definitions: Lt(i,L)Original native command in the exact edition
  2. L17
    specialize finite_lt_succ_eq_or_lt (L)
  3. L18
    specialize finite_lt_succ_eq_or_lt (i)
  4. L19
    apply finite_lt_succ_eq_or_lt
  5. L20
    exact hi
05Separate the logical casesL21–21

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

  1. L21
    cases ho
06Calculate and transport equalitiesL22–23

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

  1. L22
    rewrite ho_left at ha
  2. L23
    rewrite ho_left at ha
07Establish heqL24–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L24
    have heq : a=0
  2. L25
    specialize beta_at_unique (d)
  3. L26
    specialize beta_at_unique (e)
  4. L27
    specialize beta_at_unique (L)
  5. L28
    specialize beta_at_unique (a)
  6. L29
    specialize beta_at_unique (0)
  7. L30
    apply beta_at_unique
  8. L31
    exact ha
  9. L32
    exact hd_right
  10. L33
    rewrite ho_left
08Calculate and transport equalitiesL34–36

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

  1. L34
    rewrite ho_left
  2. L35
    rewrite heq
  3. L36
    rewrite heq
09Use earlier factsL37–37

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

  1. L37
    exact hf_right
10Establish hxL38–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at exists.

  1. L38
    have hx : ∃ x. BetaAt(b,c,i,x)Definitions: BetaAt(b,c,i,x)Original native command in the exact edition
  2. L39
    specialize beta_at_exists (b)
  3. L40
    specialize beta_at_exists (c)
  4. L41
    specialize beta_at_exists (i)
  5. L42
    apply beta_at_exists
11Separate the logical casesL43–43

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

  1. L43
    cases hx
12Establish heqL44–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L44
    have heq : a=x
  2. L45
    specialize beta_at_unique (d)
  3. L46
    specialize beta_at_unique (e)
  4. L47
    specialize beta_at_unique (i)
  5. L48
    specialize beta_at_unique (a)
  6. L49
    specialize beta_at_unique (x)
  7. L50
    apply beta_at_unique
  8. L51
    exact ha
  9. L52
    specialize hd_left (i)
  10. L53
    specialize hd_left (x)
13Use earlier factsL54–56

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

  1. L54
    apply hd_left
  2. L55
    exact ho_right
  3. L56
    exact hx_witness
14Calculate and transport equalitiesL57–58

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

  1. L57
    rewrite heq
  2. L58
    rewrite heq
15Use earlier factsL59–63

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

  1. L59
    specialize hf_left (i)
  2. L60
    specialize hf_left (x)
  3. L61
    apply hf_left
  4. L62
    exact ho_right
  5. L63
    exact hx_witness

Library-wide reading audit

Original defined command ledger · 63 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro L
  4. 0004intro d
  5. 0005intro e
  6. 0006intro f
  7. 0007intro g
  8. 0008intro hd
  9. 0009intro hf
  10. 0010cases hd
  11. 0011cases hf
  12. 0012intro i
  13. 0013intro a
  14. 0014intro hi
  15. 0015intro ha
  16. 0016have ho : i = L ∨ Lt(i,L)
  17. 0017specialize finite_lt_succ_eq_or_lt (L)
  18. 0018specialize finite_lt_succ_eq_or_lt (i)
  19. 0019apply finite_lt_succ_eq_or_lt
  20. 0020exact hi
  21. 0021cases ho
  22. 0022rewrite ho_left at ha
  23. 0023rewrite ho_left at ha
  24. 0024have heq : a=0
  25. 0025specialize beta_at_unique (d)
  26. 0026specialize beta_at_unique (e)
  27. 0027specialize beta_at_unique (L)
  28. 0028specialize beta_at_unique (a)
  29. 0029specialize beta_at_unique (0)
  30. 0030apply beta_at_unique
  31. 0031exact ha
  32. 0032exact hd_right
  33. 0033rewrite ho_left
  34. 0034rewrite ho_left
  35. 0035rewrite heq
  36. 0036rewrite heq
  37. 0037exact hf_right
  38. 0038have hx : ∃ x. BetaAt(b,c,i,x)
  39. 0039specialize beta_at_exists (b)
  40. 0040specialize beta_at_exists (c)
  41. 0041specialize beta_at_exists (i)
  42. 0042apply beta_at_exists
  43. 0043cases hx
  44. 0044have heq : a=x
  45. 0045specialize beta_at_unique (d)
  46. 0046specialize beta_at_unique (e)
  47. 0047specialize beta_at_unique (i)
  48. 0048specialize beta_at_unique (a)
  49. 0049specialize beta_at_unique (x)
  50. 0050apply beta_at_unique
  51. 0051exact ha
  52. 0052specialize hd_left (i)
  53. 0053specialize hd_left (x)
  54. 0054apply hd_left
  55. 0055exact ho_right
  56. 0056exact hx_witness
  57. 0057rewrite heq
  58. 0058rewrite heq
  59. 0059specialize hf_left (i)
  60. 0060specialize hf_left (x)
  61. 0061apply hf_left
  62. 0062exact ho_right
  63. 0063exact hx_witness