PG0003

prime_field_polynomial_shift_functional

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic 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))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 63 exact native proof lines.

Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

finite_lt_succ_eq_or_lt Alpha theorem; checked-use authorized beta_at_unique Alpha theorem; checked-use authorized beta_at_exists Alpha theorem; checked-use authorized

Direct dependents

PG000C prime_field_polynomial_convolution_shift_right_equivalent

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 \/ (exists pfa_gap_shift_unique_old_index. pfa_gap_shift_unique_old_index + S (i) = (L))
  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 : exists x. (((exists ff_h_pfp_shift_unique_source_value. ff_h_pfp_shift_unique_source_value + S (x) = S ((S (i)) * c)) /\ exists ff_q_pfp_shift_unique_source_value. b = ff_q_pfp_shift_unique_source_value * S ((S (i)) * c) + (x)))
  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 exact 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 \/ (exists pfa_gap_shift_unique_old_index. pfa_gap_shift_unique_old_index + S (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 : exists x. (((exists ff_h_pfp_shift_unique_source_value. ff_h_pfp_shift_unique_source_value + S (x) = S ((S (i)) * c)) /\ exists ff_q_pfp_shift_unique_source_value. b = ff_q_pfp_shift_unique_source_value * S ((S (i)) * c) + (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