PX0017

prime_field_polynomial_left_pad_functional

Any two constructed left pads have equal decoded coefficients on the full padded length.

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. ∀ t. ∀ d. ∀ e. ∀ f. ∀ g. PolynomialLeftPad(b,c,L,t,d,e) → PolynomialLeftPad(b,c,L,t,f,g) → BetaPrefixEqual(d,e,f,g,t + L)

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

Definition DAG

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

Actual proof prerequisites

prime_field_polynomial_left_pad_index_casesbeta_at_unique · checked external prerequisitebeta_at_exists · checked external prerequisite
Original expanded first-order statement 
forall b c L t d e f g. (((forall pfp_repeat_index_left_pad_functional_firstzeros. (exists pfa_gap_left_pad_functional_firstzerosindex. pfa_gap_left_pad_functional_firstzerosindex + S (pfp_repeat_index_left_pad_functional_firstzeros) = (t)) -> (((exists ff_h_pfp_left_pad_functional_firstzerosentry. ff_h_pfp_left_pad_functional_firstzerosentry + S (0) = S ((S (pfp_repeat_index_left_pad_functional_firstzeros)) * e)) /\ exists ff_q_pfp_left_pad_functional_firstzerosentry. d = ff_q_pfp_left_pad_functional_firstzerosentry * S ((S (pfp_repeat_index_left_pad_functional_firstzeros)) * e) + (0)))) /\ ((forall pfrep_index_left_pad_functional_first pfrep_value_left_pad_functional_first. (exists pfa_gap_left_pad_functional_firstbound. pfa_gap_left_pad_functional_firstbound + S (pfrep_index_left_pad_functional_first) = (L)) -> (((exists ff_h_pfp_left_pad_functional_firstinput. ff_h_pfp_left_pad_functional_firstinput + S (pfrep_value_left_pad_functional_first) = S ((S (pfrep_index_left_pad_functional_first)) * c)) /\ exists ff_q_pfp_left_pad_functional_firstinput. b = ff_q_pfp_left_pad_functional_firstinput * S ((S (pfrep_index_left_pad_functional_first)) * c) + (pfrep_value_left_pad_functional_first))) -> (((exists ff_h_pfp_left_pad_functional_firstoutput. ff_h_pfp_left_pad_functional_firstoutput + S (pfrep_value_left_pad_functional_first) = S ((S ((t)+pfrep_index_left_pad_functional_first)) * e)) /\ exists ff_q_pfp_left_pad_functional_firstoutput. d = ff_q_pfp_left_pad_functional_firstoutput * S ((S ((t)+pfrep_index_left_pad_functional_first)) * e) + (pfrep_value_left_pad_functional_first))))))) -> (((forall pfp_repeat_index_left_pad_functional_secondzeros. (exists pfa_gap_left_pad_functional_secondzerosindex. pfa_gap_left_pad_functional_secondzerosindex + S (pfp_repeat_index_left_pad_functional_secondzeros) = (t)) -> (((exists ff_h_pfp_left_pad_functional_secondzerosentry. ff_h_pfp_left_pad_functional_secondzerosentry + S (0) = S ((S (pfp_repeat_index_left_pad_functional_secondzeros)) * g)) /\ exists ff_q_pfp_left_pad_functional_secondzerosentry. f = ff_q_pfp_left_pad_functional_secondzerosentry * S ((S (pfp_repeat_index_left_pad_functional_secondzeros)) * g) + (0)))) /\ ((forall pfrep_index_left_pad_functional_second pfrep_value_left_pad_functional_second. (exists pfa_gap_left_pad_functional_secondbound. pfa_gap_left_pad_functional_secondbound + S (pfrep_index_left_pad_functional_second) = (L)) -> (((exists ff_h_pfp_left_pad_functional_secondinput. ff_h_pfp_left_pad_functional_secondinput + S (pfrep_value_left_pad_functional_second) = S ((S (pfrep_index_left_pad_functional_second)) * c)) /\ exists ff_q_pfp_left_pad_functional_secondinput. b = ff_q_pfp_left_pad_functional_secondinput * S ((S (pfrep_index_left_pad_functional_second)) * c) + (pfrep_value_left_pad_functional_second))) -> (((exists ff_h_pfp_left_pad_functional_secondoutput. ff_h_pfp_left_pad_functional_secondoutput + S (pfrep_value_left_pad_functional_second) = S ((S ((t)+pfrep_index_left_pad_functional_second)) * g)) /\ exists ff_q_pfp_left_pad_functional_secondoutput. f = ff_q_pfp_left_pad_functional_secondoutput * S ((S ((t)+pfrep_index_left_pad_functional_second)) * g) + (pfrep_value_left_pad_functional_second))))))) -> (forall mdr_i_pfp_left_pad_functional_result mdr_a_pfp_left_pad_functional_result. (exists mdr_gap_pfp_left_pad_functional_resultb. mdr_gap_pfp_left_pad_functional_resultb + S (mdr_i_pfp_left_pad_functional_result) = (t+L)) -> (((exists ff_h_mdr_pfp_left_pad_functional_resulto. ff_h_mdr_pfp_left_pad_functional_resulto + S (mdr_a_pfp_left_pad_functional_result) = S ((S (mdr_i_pfp_left_pad_functional_result)) * e)) /\ exists ff_q_mdr_pfp_left_pad_functional_resulto. d = ff_q_mdr_pfp_left_pad_functional_resulto * S ((S (mdr_i_pfp_left_pad_functional_result)) * e) + (mdr_a_pfp_left_pad_functional_result))) -> (((exists ff_h_mdr_pfp_left_pad_functional_resultn. ff_h_mdr_pfp_left_pad_functional_resultn + S (mdr_a_pfp_left_pad_functional_result) = S ((S (mdr_i_pfp_left_pad_functional_result)) * g)) /\ exists ff_q_mdr_pfp_left_pad_functional_resultn. f = ff_q_mdr_pfp_left_pad_functional_resultn * S ((S (mdr_i_pfp_left_pad_functional_result)) * g) + (mdr_a_pfp_left_pad_functional_result))))

Complete tactic proof in conservative notation

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

71 script commands · 16 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.

Named ingredients (1)
prime field polynomial left pad index cases
01Fix variables and assumptionsL1–10

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 t
  5. L5
    intro d
  6. L6
    intro e
  7. L7
    intro f
  8. L8
    intro g
  9. L9
    intro hd
  10. L10
    intro hf
02Fix variables and assumptionsL11–14

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

  1. L11
    intro i
  2. L12
    intro a
  3. L13
    intro hi
  4. L14
    intro ha
03Separate the logical casesL15–16

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

  1. L15
    cases hd
  2. L16
    cases hf
04Establish hoL17–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial left pad index cases.

  1. L17
    have ho : Lt(i,t) ∨ (∃ x. Lt(x,L) ∧ i = t + x)Definitions: Lt(i,t)Lt(x,L)Original native command in the exact edition
  2. L18
    specialize prime_field_polynomial_left_pad_index_cases (t)
  3. L19
    specialize prime_field_polynomial_left_pad_index_cases (L)
  4. L20
    specialize prime_field_polynomial_left_pad_index_cases (i)
  5. L21
    apply prime_field_polynomial_left_pad_index_cases
  6. L22
    exact hi
05Separate the logical casesL23–23

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

  1. L23
    cases ho
06Establish 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 (i)
  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
    specialize hd_left (i)
  10. L33
    apply hd_left
07Use earlier factsL34–34

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

  1. L34
    exact ho_left
08Calculate and transport equalitiesL35–36

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

  1. L35
    rewrite heq
  2. L36
    rewrite heq
09Use earlier factsL37–39

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

  1. L37
    specialize hf_left (i)
  2. L38
    apply hf_left
  3. L39
    exact ho_left
10Separate the logical casesL40–41

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

  1. L40
    cases ho_right
  2. L41
    cases ho_right_witness
11Establish hvL42–46

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

  1. L42
    have hv : ∃ z. BetaAt(b,c,x,z)Definitions: BetaAt(b,c,x,z)Original native command in the exact edition
  2. L43
    specialize beta_at_exists (b)
  3. L44
    specialize beta_at_exists (c)
  4. L45
    specialize beta_at_exists (x)
  5. L46
    apply beta_at_exists
12Separate the logical casesL47–47

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

  1. L47
    cases hv
13Establish heqL48–57

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

  1. L48
    have heq : a=x1
  2. L49
    specialize beta_at_unique (d)
  3. L50
    specialize beta_at_unique (e)
  4. L51
    specialize beta_at_unique (t+x)
  5. L52
    specialize beta_at_unique (a)
  6. L53
    specialize beta_at_unique (x1)
  7. L54
    apply beta_at_unique
  8. L55
    rewrite ho_right_witness_right at ha
  9. L56
    rewrite ho_right_witness_right at ha
  10. L57
    exact ha
14Use earlier factsL58–62

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

  1. L58
    specialize hd_right (x)
  2. L59
    specialize hd_right (x1)
  3. L60
    apply hd_right
  4. L61
    exact ho_right_witness_left
  5. L62
    exact hv_witness
15Calculate and transport equalitiesL63–66

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

  1. L63
    rewrite ho_right_witness_right
  2. L64
    rewrite ho_right_witness_right
  3. L65
    rewrite heq
  4. L66
    rewrite heq
16Use earlier factsL67–71

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

  1. L67
    specialize hf_right (x)
  2. L68
    specialize hf_right (x1)
  3. L69
    apply hf_right
  4. L70
    exact ho_right_witness_left
  5. L71
    exact hv_witness

Library-wide reading audit

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