PX001D

prime_field_polynomial_left_pad_transport

Input and full-output recoding preserve the actual leading-zero block and every copied coefficient.

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. ∀ B. ∀ C. ∀ L. ∀ t. ∀ d. ∀ e. ∀ D. ∀ E. BetaPrefixEqual(b,c,B,C,L) → BetaPrefixEqual(d,e,D,E,t + L) → PolynomialLeftPad(b,c,L,t,d,e) → PolynomialLeftPad(B,C,L,t,D,E)

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

Definition DAG

BetaPrefixEqual(b,c,d,e,l) · 3PolynomialLeftPad(b,c,L,t,d,e) · 2

Actual proof prerequisites

matrix_rank_prefix_equality_symmetric · checked external prerequisitelt_of_lt_of_le · checked external prerequisitele_add_right · checked external prerequisitematrix_recursive_lt_add_left · checked external prerequisite
Original expanded first-order statement 
forall b c B C L t d e D E. (forall mdr_i_pfp_pad_transport_input mdr_a_pfp_pad_transport_input. (exists mdr_gap_pfp_pad_transport_inputb. mdr_gap_pfp_pad_transport_inputb + S (mdr_i_pfp_pad_transport_input) = (L)) -> (((exists ff_h_mdr_pfp_pad_transport_inputo. ff_h_mdr_pfp_pad_transport_inputo + S (mdr_a_pfp_pad_transport_input) = S ((S (mdr_i_pfp_pad_transport_input)) * c)) /\ exists ff_q_mdr_pfp_pad_transport_inputo. b = ff_q_mdr_pfp_pad_transport_inputo * S ((S (mdr_i_pfp_pad_transport_input)) * c) + (mdr_a_pfp_pad_transport_input))) -> (((exists ff_h_mdr_pfp_pad_transport_inputn. ff_h_mdr_pfp_pad_transport_inputn + S (mdr_a_pfp_pad_transport_input) = S ((S (mdr_i_pfp_pad_transport_input)) * C)) /\ exists ff_q_mdr_pfp_pad_transport_inputn. B = ff_q_mdr_pfp_pad_transport_inputn * S ((S (mdr_i_pfp_pad_transport_input)) * C) + (mdr_a_pfp_pad_transport_input)))) -> (forall mdr_i_pfp_pad_transport_output mdr_a_pfp_pad_transport_output. (exists mdr_gap_pfp_pad_transport_outputb. mdr_gap_pfp_pad_transport_outputb + S (mdr_i_pfp_pad_transport_output) = (t+L)) -> (((exists ff_h_mdr_pfp_pad_transport_outputo. ff_h_mdr_pfp_pad_transport_outputo + S (mdr_a_pfp_pad_transport_output) = S ((S (mdr_i_pfp_pad_transport_output)) * e)) /\ exists ff_q_mdr_pfp_pad_transport_outputo. d = ff_q_mdr_pfp_pad_transport_outputo * S ((S (mdr_i_pfp_pad_transport_output)) * e) + (mdr_a_pfp_pad_transport_output))) -> (((exists ff_h_mdr_pfp_pad_transport_outputn. ff_h_mdr_pfp_pad_transport_outputn + S (mdr_a_pfp_pad_transport_output) = S ((S (mdr_i_pfp_pad_transport_output)) * E)) /\ exists ff_q_mdr_pfp_pad_transport_outputn. D = ff_q_mdr_pfp_pad_transport_outputn * S ((S (mdr_i_pfp_pad_transport_output)) * E) + (mdr_a_pfp_pad_transport_output)))) -> (((forall pfp_repeat_index_pad_transport_oldzeros. (exists pfa_gap_pad_transport_oldzerosindex. pfa_gap_pad_transport_oldzerosindex + S (pfp_repeat_index_pad_transport_oldzeros) = (t)) -> (((exists ff_h_pfp_pad_transport_oldzerosentry. ff_h_pfp_pad_transport_oldzerosentry + S (0) = S ((S (pfp_repeat_index_pad_transport_oldzeros)) * e)) /\ exists ff_q_pfp_pad_transport_oldzerosentry. d = ff_q_pfp_pad_transport_oldzerosentry * S ((S (pfp_repeat_index_pad_transport_oldzeros)) * e) + (0)))) /\ ((forall pfrep_index_pad_transport_old pfrep_value_pad_transport_old. (exists pfa_gap_pad_transport_oldbound. pfa_gap_pad_transport_oldbound + S (pfrep_index_pad_transport_old) = (L)) -> (((exists ff_h_pfp_pad_transport_oldinput. ff_h_pfp_pad_transport_oldinput + S (pfrep_value_pad_transport_old) = S ((S (pfrep_index_pad_transport_old)) * c)) /\ exists ff_q_pfp_pad_transport_oldinput. b = ff_q_pfp_pad_transport_oldinput * S ((S (pfrep_index_pad_transport_old)) * c) + (pfrep_value_pad_transport_old))) -> (((exists ff_h_pfp_pad_transport_oldoutput. ff_h_pfp_pad_transport_oldoutput + S (pfrep_value_pad_transport_old) = S ((S ((t)+pfrep_index_pad_transport_old)) * e)) /\ exists ff_q_pfp_pad_transport_oldoutput. d = ff_q_pfp_pad_transport_oldoutput * S ((S ((t)+pfrep_index_pad_transport_old)) * e) + (pfrep_value_pad_transport_old))))))) -> (((forall pfp_repeat_index_pad_transport_newzeros. (exists pfa_gap_pad_transport_newzerosindex. pfa_gap_pad_transport_newzerosindex + S (pfp_repeat_index_pad_transport_newzeros) = (t)) -> (((exists ff_h_pfp_pad_transport_newzerosentry. ff_h_pfp_pad_transport_newzerosentry + S (0) = S ((S (pfp_repeat_index_pad_transport_newzeros)) * E)) /\ exists ff_q_pfp_pad_transport_newzerosentry. D = ff_q_pfp_pad_transport_newzerosentry * S ((S (pfp_repeat_index_pad_transport_newzeros)) * E) + (0)))) /\ ((forall pfrep_index_pad_transport_new pfrep_value_pad_transport_new. (exists pfa_gap_pad_transport_newbound. pfa_gap_pad_transport_newbound + S (pfrep_index_pad_transport_new) = (L)) -> (((exists ff_h_pfp_pad_transport_newinput. ff_h_pfp_pad_transport_newinput + S (pfrep_value_pad_transport_new) = S ((S (pfrep_index_pad_transport_new)) * C)) /\ exists ff_q_pfp_pad_transport_newinput. B = ff_q_pfp_pad_transport_newinput * S ((S (pfrep_index_pad_transport_new)) * C) + (pfrep_value_pad_transport_new))) -> (((exists ff_h_pfp_pad_transport_newoutput. ff_h_pfp_pad_transport_newoutput + S (pfrep_value_pad_transport_new) = S ((S ((t)+pfrep_index_pad_transport_new)) * E)) /\ exists ff_q_pfp_pad_transport_newoutput. D = ff_q_pfp_pad_transport_newoutput * S ((S ((t)+pfrep_index_pad_transport_new)) * E) + (pfrep_value_pad_transport_new)))))))

Complete tactic proof in conservative notation

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

60 script commands · 11 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–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro B
  4. L4
    intro C
  5. L5
    intro L
  6. L6
    intro t
  7. L7
    intro d
  8. L8
    intro e
  9. L9
    intro D
  10. L10
    intro E
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hi
  2. L12
    intro ho
  3. L13
    intro h
03Separate the logical casesL14–14

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

  1. L14
    cases h
04Establish hrL15–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix rank prefix equality symmetric.

  1. L15
    have hr : BetaPrefixEqual(B,C,b,c,L)Definitions: BetaPrefixEqual(B,C,b,c,L)Original native command in the exact edition
  2. L16
    specialize matrix_rank_prefix_equality_symmetric (b)
  3. L17
    specialize matrix_rank_prefix_equality_symmetric (c)
  4. L18
    specialize matrix_rank_prefix_equality_symmetric (B)
  5. L19
    specialize matrix_rank_prefix_equality_symmetric (C)
  6. L20
    specialize matrix_rank_prefix_equality_symmetric (L)
  7. L21
    apply matrix_rank_prefix_equality_symmetric
  8. L22
    exact hi
05Separate the logical casesL23–23

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

  1. L23
    split
06Fix variables and assumptionsL24–25

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

  1. L24
    intro i
  2. L25
    intro hindex
07Use earlier factsL26–35

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

  1. L26
    specialize ho (i)
  2. L27
    specialize ho (0)
  3. L28
    apply ho
  4. L29
    specialize lt_of_lt_of_le (i)
  5. L30
    specialize lt_of_lt_of_le (t)
  6. L31
    specialize lt_of_lt_of_le (t+L)
  7. L32
    apply lt_of_lt_of_le
  8. L33
    exact hindex
  9. L34
    specialize le_add_right (t)
  10. L35
    specialize le_add_right (L)
08Use earlier factsL36–39

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

  1. L36
    apply le_add_right
  2. L37
    specialize h_left (i)
  3. L38
    apply h_left
  4. L39
    exact hindex
09Fix variables and assumptionsL40–43

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

  1. L40
    intro i
  2. L41
    intro a
  3. L42
    intro hindex
  4. L43
    intro ha
10Use earlier factsL44–53

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

  1. L44
    specialize ho (t+i)
  2. L45
    specialize ho (a)
  3. L46
    apply ho
  4. L47
    specialize matrix_recursive_lt_add_left (i)
  5. L48
    specialize matrix_recursive_lt_add_left (L)
  6. L49
    specialize matrix_recursive_lt_add_left (t)
  7. L50
    apply matrix_recursive_lt_add_left
  8. L51
    exact hindex
  9. L52
    specialize h_right (i)
  10. L53
    specialize h_right (a)
11Use earlier factsL54–60

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

  1. L54
    apply h_right
  2. L55
    exact hindex
  3. L56
    specialize hr (i)
  4. L57
    specialize hr (a)
  5. L58
    apply hr
  6. L59
    exact hindex
  7. L60
    exact ha

Library-wide reading audit

Original defined command ledger · 60 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro B
  4. 0004intro C
  5. 0005intro L
  6. 0006intro t
  7. 0007intro d
  8. 0008intro e
  9. 0009intro D
  10. 0010intro E
  11. 0011intro hi
  12. 0012intro ho
  13. 0013intro h
  14. 0014cases h
  15. 0015have hr : BetaPrefixEqual(B,C,b,c,L)
  16. 0016specialize matrix_rank_prefix_equality_symmetric (b)
  17. 0017specialize matrix_rank_prefix_equality_symmetric (c)
  18. 0018specialize matrix_rank_prefix_equality_symmetric (B)
  19. 0019specialize matrix_rank_prefix_equality_symmetric (C)
  20. 0020specialize matrix_rank_prefix_equality_symmetric (L)
  21. 0021apply matrix_rank_prefix_equality_symmetric
  22. 0022exact hi
  23. 0023split
  24. 0024intro i
  25. 0025intro hindex
  26. 0026specialize ho (i)
  27. 0027specialize ho (0)
  28. 0028apply ho
  29. 0029specialize lt_of_lt_of_le (i)
  30. 0030specialize lt_of_lt_of_le (t)
  31. 0031specialize lt_of_lt_of_le (t+L)
  32. 0032apply lt_of_lt_of_le
  33. 0033exact hindex
  34. 0034specialize le_add_right (t)
  35. 0035specialize le_add_right (L)
  36. 0036apply le_add_right
  37. 0037specialize h_left (i)
  38. 0038apply h_left
  39. 0039exact hindex
  40. 0040intro i
  41. 0041intro a
  42. 0042intro hindex
  43. 0043intro ha
  44. 0044specialize ho (t+i)
  45. 0045specialize ho (a)
  46. 0046apply ho
  47. 0047specialize matrix_recursive_lt_add_left (i)
  48. 0048specialize matrix_recursive_lt_add_left (L)
  49. 0049specialize matrix_recursive_lt_add_left (t)
  50. 0050apply matrix_recursive_lt_add_left
  51. 0051exact hindex
  52. 0052specialize h_right (i)
  53. 0053specialize h_right (a)
  54. 0054apply h_right
  55. 0055exact hindex
  56. 0056specialize hr (i)
  57. 0057specialize hr (a)
  58. 0058apply hr
  59. 0059exact hindex
  60. 0060exact ha