PX001D

prime_field_polynomial_left_pad_transport

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

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

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 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)))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 60 exact native proof lines.

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

Proof neighborhood

Direct dependencies

matrix_rank_prefix_equality_symmetric Alpha theorem; checked-use authorized lt_of_lt_of_le Alpha theorem; checked-use authorized le_add_right Alpha theorem; checked-use authorized matrix_recursive_lt_add_left Alpha theorem; checked-use authorized

Direct dependents

PX0072 prime_field_polynomial_equivalent_implies_left_pad PX0073 prime_field_polynomial_add_left_pad_output PX0074 prime_field_polynomial_subtract_left_pad_output

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

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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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
  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 exact 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 : forall mdr_i_pfp_pad_transport_reverse mdr_a_pfp_pad_transport_reverse. (exists mdr_gap_pfp_pad_transport_reverseb. mdr_gap_pfp_pad_transport_reverseb + S (mdr_i_pfp_pad_transport_reverse) = (L)) -> (((exists ff_h_mdr_pfp_pad_transport_reverseo. ff_h_mdr_pfp_pad_transport_reverseo + S (mdr_a_pfp_pad_transport_reverse) = S ((S (mdr_i_pfp_pad_transport_reverse)) * C)) /\ exists ff_q_mdr_pfp_pad_transport_reverseo. B = ff_q_mdr_pfp_pad_transport_reverseo * S ((S (mdr_i_pfp_pad_transport_reverse)) * C) + (mdr_a_pfp_pad_transport_reverse))) -> (((exists ff_h_mdr_pfp_pad_transport_reversen. ff_h_mdr_pfp_pad_transport_reversen + S (mdr_a_pfp_pad_transport_reverse) = S ((S (mdr_i_pfp_pad_transport_reverse)) * c)) /\ exists ff_q_mdr_pfp_pad_transport_reversen. b = ff_q_mdr_pfp_pad_transport_reversen * S ((S (mdr_i_pfp_pad_transport_reverse)) * c) + (mdr_a_pfp_pad_transport_reverse)))
  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