PX0072

prime_field_polynomial_equivalent_implies_left_pad

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

Formal equivalence to a prefix of length t+L forces its actual leading-zero block and every copied source coefficient; construct a real padding and transport it by decoded equality, with no prime assumption.

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 t d e. (forall pfrep_power_converse_input pfrep_left_converse_input pfrep_right_converse_input. ((exists pfrep_position_converse_inputfirst. ((pfrep_position_converse_inputfirst+S (pfrep_power_converse_input)=(L)) /\ ((((exists ff_h_pfp_converse_inputfirstentry. ff_h_pfp_converse_inputfirstentry + S (pfrep_left_converse_input) = S ((S (pfrep_position_converse_inputfirst)) * c)) /\ exists ff_q_pfp_converse_inputfirstentry. b = ff_q_pfp_converse_inputfirstentry * S ((S (pfrep_position_converse_inputfirst)) * c) + (pfrep_left_converse_input)))))) \/ (((exists pfrep_gap_converse_inputfirstoutside. pfrep_gap_converse_inputfirstoutside+(L)=(pfrep_power_converse_input)) /\ (((pfrep_left_converse_input)=0))))) -> ((exists pfrep_position_converse_inputsecond. ((pfrep_position_converse_inputsecond+S (pfrep_power_converse_input)=(t+L)) /\ ((((exists ff_h_pfp_converse_inputsecondentry. ff_h_pfp_converse_inputsecondentry + S (pfrep_right_converse_input) = S ((S (pfrep_position_converse_inputsecond)) * e)) /\ exists ff_q_pfp_converse_inputsecondentry. d = ff_q_pfp_converse_inputsecondentry * S ((S (pfrep_position_converse_inputsecond)) * e) + (pfrep_right_converse_input)))))) \/ (((exists pfrep_gap_converse_inputsecondoutside. pfrep_gap_converse_inputsecondoutside+(t+L)=(pfrep_power_converse_input)) /\ (((pfrep_right_converse_input)=0))))) -> pfrep_left_converse_input=pfrep_right_converse_input) -> (((forall pfp_repeat_index_converse_resultzeros. (exists pfa_gap_converse_resultzerosindex. pfa_gap_converse_resultzerosindex + S (pfp_repeat_index_converse_resultzeros) = (t)) -> (((exists ff_h_pfp_converse_resultzerosentry. ff_h_pfp_converse_resultzerosentry + S (0) = S ((S (pfp_repeat_index_converse_resultzeros)) * e)) /\ exists ff_q_pfp_converse_resultzerosentry. d = ff_q_pfp_converse_resultzerosentry * S ((S (pfp_repeat_index_converse_resultzeros)) * e) + (0)))) /\ ((forall pfrep_index_converse_result pfrep_value_converse_result. (exists pfa_gap_converse_resultbound. pfa_gap_converse_resultbound + S (pfrep_index_converse_result) = (L)) -> (((exists ff_h_pfp_converse_resultinput. ff_h_pfp_converse_resultinput + S (pfrep_value_converse_result) = S ((S (pfrep_index_converse_result)) * c)) /\ exists ff_q_pfp_converse_resultinput. b = ff_q_pfp_converse_resultinput * S ((S (pfrep_index_converse_result)) * c) + (pfrep_value_converse_result))) -> (((exists ff_h_pfp_converse_resultoutput. ff_h_pfp_converse_resultoutput + S (pfrep_value_converse_result) = S ((S ((t)+pfrep_index_converse_result)) * e)) /\ exists ff_q_pfp_converse_resultoutput. d = ff_q_pfp_converse_resultoutput * S ((S ((t)+pfrep_index_converse_result)) * e) + (pfrep_value_converse_result)))))))

Constructive proof overview

Generated structural guide

Formal equivalence to a prefix of length t+L forces its actual leading-zero block and every copied source coefficient; construct a real padding and transport it by decoded equality, with no prime assumption.

The unchanged tactic script uses 6 declared prerequisites and contains 72 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PX0014 prime_field_polynomial_left_pad_exists PX001B prime_field_polynomial_left_pad_equivalent PX000F prime_field_polynomial_equivalent_symmetric PX0010 prime_field_polynomial_equivalent_transitive PX0012 prime_field_polynomial_equivalent_implies_equal_same_length PX001D prime_field_polynomial_left_pad_transport

Direct dependents

PX0075 prime_field_polynomial_add_equivalent_congruent PX0076 prime_field_polynomial_subtract_equivalent_congruent PX0077 prime_field_polynomial_convolution_equivalent_congruent_left PX0078 prime_field_polynomial_convolution_equivalent_congruent_right

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

72 script commands · 11 reading checkpoints · 5 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.

Named ingredients (6)
prime field polynomial left pad existsprime field polynomial left pad equivalentprime field polynomial equivalent symmetricprime field polynomial equivalent transitiveprime field polynomial equivalent implies equal same lengthprime field polynomial left pad transport

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

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 he
02Establish hpL8–13

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

  1. L8
    have hp : ∃ B. ∃ C. PolynomialLeftPad(b,c,L,t,B,C)Definitions: PolynomialLeftPad
  2. L9
    specialize prime_field_polynomial_left_pad_exists (b)
  3. L10
    specialize prime_field_polynomial_left_pad_exists (c)
  4. L11
    specialize prime_field_polynomial_left_pad_exists (t)
  5. L12
    specialize prime_field_polynomial_left_pad_exists (L)
  6. L13
    apply prime_field_polynomial_left_pad_exists
03Separate the logical casesL14–15

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

  1. L14
    cases hp
  2. L15
    cases hp_witness
04Establish hsL16–24

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

  1. L16
    have hs : PolynomialEquivalent(b,c,L,x,x1,t + L)Definitions: PolynomialEquivalent
  2. L17
    specialize prime_field_polynomial_left_pad_equivalent (b)
  3. L18
    specialize prime_field_polynomial_left_pad_equivalent (c)
  4. L19
    specialize prime_field_polynomial_left_pad_equivalent (L)
  5. L20
    specialize prime_field_polynomial_left_pad_equivalent (t)
  6. L21
    specialize prime_field_polynomial_left_pad_equivalent (x)
  7. L22
    specialize prime_field_polynomial_left_pad_equivalent (x1)
  8. L23
    apply prime_field_polynomial_left_pad_equivalent
  9. L24
    exact hp_witness_witness
05Establish hrL25–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial equivalent symmetric.

  1. L25
    have hr : PolynomialEquivalent(x,x1,t + L,b,c,L)Definitions: PolynomialEquivalent
  2. L26
    specialize prime_field_polynomial_equivalent_symmetric (b)
  3. L27
    specialize prime_field_polynomial_equivalent_symmetric (c)
  4. L28
    specialize prime_field_polynomial_equivalent_symmetric (L)
  5. L29
    specialize prime_field_polynomial_equivalent_symmetric (x)
  6. L30
    specialize prime_field_polynomial_equivalent_symmetric (x1)
  7. L31
    specialize prime_field_polynomial_equivalent_symmetric (t+L)
  8. L32
    apply prime_field_polynomial_equivalent_symmetric
  9. L33
    exact hs
06Establish htL34–43

Establish this local claim before using it. It is not an additional assumption.

  1. L34
    have ht : PolynomialEquivalent(x,x1,t + L,d,e,t + L)Definitions: PolynomialEquivalent
  2. L35
    specialize prime_field_polynomial_equivalent_transitive (x)
  3. L36
    specialize prime_field_polynomial_equivalent_transitive (x1)
  4. L37
    specialize prime_field_polynomial_equivalent_transitive (t+L)
  5. L38
    specialize prime_field_polynomial_equivalent_transitive (b)
  6. L39
    specialize prime_field_polynomial_equivalent_transitive (c)
  7. L40
    specialize prime_field_polynomial_equivalent_transitive (L)
  8. L41
    specialize prime_field_polynomial_equivalent_transitive (d)
  9. L42
    specialize prime_field_polynomial_equivalent_transitive (e)
  10. L43
    specialize prime_field_polynomial_equivalent_transitive (t+L)
07Use earlier factsL44–46

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

  1. L44
    apply prime_field_polynomial_equivalent_transitive
  2. L45
    exact hr
  3. L46
    exact he
08Establish hvL47–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial equivalent implies equal same length.

  1. L47
    have hv : BetaPrefixEqual(x,x1,d,e,t + L)Definitions: BetaPrefixEqual
  2. L48
    specialize prime_field_polynomial_equivalent_implies_equal_same_length (x)
  3. L49
    specialize prime_field_polynomial_equivalent_implies_equal_same_length (x1)
  4. L50
    specialize prime_field_polynomial_equivalent_implies_equal_same_length (d)
  5. L51
    specialize prime_field_polynomial_equivalent_implies_equal_same_length (e)
  6. L52
    specialize prime_field_polynomial_equivalent_implies_equal_same_length (t+L)
  7. L53
    apply prime_field_polynomial_equivalent_implies_equal_same_length
  8. L54
    exact ht
  9. L55
    specialize prime_field_polynomial_left_pad_transport (b)
  10. L56
    specialize prime_field_polynomial_left_pad_transport (c)
09Use earlier factsL57–65

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

  1. L57
    specialize prime_field_polynomial_left_pad_transport (b)
  2. L58
    specialize prime_field_polynomial_left_pad_transport (c)
  3. L59
    specialize prime_field_polynomial_left_pad_transport (L)
  4. L60
    specialize prime_field_polynomial_left_pad_transport (t)
  5. L61
    specialize prime_field_polynomial_left_pad_transport (x)
  6. L62
    specialize prime_field_polynomial_left_pad_transport (x1)
  7. L63
    specialize prime_field_polynomial_left_pad_transport (d)
  8. L64
    specialize prime_field_polynomial_left_pad_transport (e)
  9. L65
    apply prime_field_polynomial_left_pad_transport
10Fix variables and assumptionsL66–69

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

  1. L66
    intro i
  2. L67
    intro a
  3. L68
    intro hi
  4. L69
    intro ha
11Use earlier factsL70–72

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

  1. L70
    exact ha
  2. L71
    exact hv
  3. L72
    exact hp_witness_witness

Library-wide reading audit

Original exact command ledger · 72 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro L
  4. 0004intro t
  5. 0005intro d
  6. 0006intro e
  7. 0007intro he
  8. 0008have hp : exists B C. (((forall pfp_repeat_index_converse_constructedzeros. (exists pfa_gap_converse_constructedzerosindex. pfa_gap_converse_constructedzerosindex + S (pfp_repeat_index_converse_constructedzeros) = (t)) -> (((exists ff_h_pfp_converse_constructedzerosentry. ff_h_pfp_converse_constructedzerosentry + S (0) = S ((S (pfp_repeat_index_converse_constructedzeros)) * C)) /\ exists ff_q_pfp_converse_constructedzerosentry. B = ff_q_pfp_converse_constructedzerosentry * S ((S (pfp_repeat_index_converse_constructedzeros)) * C) + (0)))) /\ ((forall pfrep_index_converse_constructed pfrep_value_converse_constructed. (exists pfa_gap_converse_constructedbound. pfa_gap_converse_constructedbound + S (pfrep_index_converse_constructed) = (L)) -> (((exists ff_h_pfp_converse_constructedinput. ff_h_pfp_converse_constructedinput + S (pfrep_value_converse_constructed) = S ((S (pfrep_index_converse_constructed)) * c)) /\ exists ff_q_pfp_converse_constructedinput. b = ff_q_pfp_converse_constructedinput * S ((S (pfrep_index_converse_constructed)) * c) + (pfrep_value_converse_constructed))) -> (((exists ff_h_pfp_converse_constructedoutput. ff_h_pfp_converse_constructedoutput + S (pfrep_value_converse_constructed) = S ((S ((t)+pfrep_index_converse_constructed)) * C)) /\ exists ff_q_pfp_converse_constructedoutput. B = ff_q_pfp_converse_constructedoutput * S ((S ((t)+pfrep_index_converse_constructed)) * C) + (pfrep_value_converse_constructed)))))))
  9. 0009specialize prime_field_polynomial_left_pad_exists (b)
  10. 0010specialize prime_field_polynomial_left_pad_exists (c)
  11. 0011specialize prime_field_polynomial_left_pad_exists (t)
  12. 0012specialize prime_field_polynomial_left_pad_exists (L)
  13. 0013apply prime_field_polynomial_left_pad_exists
  14. 0014cases hp
  15. 0015cases hp_witness
  16. 0016have hs : forall pfrep_power_converse_source pfrep_left_converse_source pfrep_right_converse_source. ((exists pfrep_position_converse_sourcefirst. ((pfrep_position_converse_sourcefirst+S (pfrep_power_converse_source)=(L)) /\ ((((exists ff_h_pfp_converse_sourcefirstentry. ff_h_pfp_converse_sourcefirstentry + S (pfrep_left_converse_source) = S ((S (pfrep_position_converse_sourcefirst)) * c)) /\ exists ff_q_pfp_converse_sourcefirstentry. b = ff_q_pfp_converse_sourcefirstentry * S ((S (pfrep_position_converse_sourcefirst)) * c) + (pfrep_left_converse_source)))))) \/ (((exists pfrep_gap_converse_sourcefirstoutside. pfrep_gap_converse_sourcefirstoutside+(L)=(pfrep_power_converse_source)) /\ (((pfrep_left_converse_source)=0))))) -> ((exists pfrep_position_converse_sourcesecond. ((pfrep_position_converse_sourcesecond+S (pfrep_power_converse_source)=(t+L)) /\ ((((exists ff_h_pfp_converse_sourcesecondentry. ff_h_pfp_converse_sourcesecondentry + S (pfrep_right_converse_source) = S ((S (pfrep_position_converse_sourcesecond)) * x1)) /\ exists ff_q_pfp_converse_sourcesecondentry. x = ff_q_pfp_converse_sourcesecondentry * S ((S (pfrep_position_converse_sourcesecond)) * x1) + (pfrep_right_converse_source)))))) \/ (((exists pfrep_gap_converse_sourcesecondoutside. pfrep_gap_converse_sourcesecondoutside+(t+L)=(pfrep_power_converse_source)) /\ (((pfrep_right_converse_source)=0))))) -> pfrep_left_converse_source=pfrep_right_converse_source
  17. 0017specialize prime_field_polynomial_left_pad_equivalent (b)
  18. 0018specialize prime_field_polynomial_left_pad_equivalent (c)
  19. 0019specialize prime_field_polynomial_left_pad_equivalent (L)
  20. 0020specialize prime_field_polynomial_left_pad_equivalent (t)
  21. 0021specialize prime_field_polynomial_left_pad_equivalent (x)
  22. 0022specialize prime_field_polynomial_left_pad_equivalent (x1)
  23. 0023apply prime_field_polynomial_left_pad_equivalent
  24. 0024exact hp_witness_witness
  25. 0025have hr : forall pfrep_power_converse_reverse pfrep_left_converse_reverse pfrep_right_converse_reverse. ((exists pfrep_position_converse_reversefirst. ((pfrep_position_converse_reversefirst+S (pfrep_power_converse_reverse)=(t+L)) /\ ((((exists ff_h_pfp_converse_reversefirstentry. ff_h_pfp_converse_reversefirstentry + S (pfrep_left_converse_reverse) = S ((S (pfrep_position_converse_reversefirst)) * x1)) /\ exists ff_q_pfp_converse_reversefirstentry. x = ff_q_pfp_converse_reversefirstentry * S ((S (pfrep_position_converse_reversefirst)) * x1) + (pfrep_left_converse_reverse)))))) \/ (((exists pfrep_gap_converse_reversefirstoutside. pfrep_gap_converse_reversefirstoutside+(t+L)=(pfrep_power_converse_reverse)) /\ (((pfrep_left_converse_reverse)=0))))) -> ((exists pfrep_position_converse_reversesecond. ((pfrep_position_converse_reversesecond+S (pfrep_power_converse_reverse)=(L)) /\ ((((exists ff_h_pfp_converse_reversesecondentry. ff_h_pfp_converse_reversesecondentry + S (pfrep_right_converse_reverse) = S ((S (pfrep_position_converse_reversesecond)) * c)) /\ exists ff_q_pfp_converse_reversesecondentry. b = ff_q_pfp_converse_reversesecondentry * S ((S (pfrep_position_converse_reversesecond)) * c) + (pfrep_right_converse_reverse)))))) \/ (((exists pfrep_gap_converse_reversesecondoutside. pfrep_gap_converse_reversesecondoutside+(L)=(pfrep_power_converse_reverse)) /\ (((pfrep_right_converse_reverse)=0))))) -> pfrep_left_converse_reverse=pfrep_right_converse_reverse
  26. 0026specialize prime_field_polynomial_equivalent_symmetric (b)
  27. 0027specialize prime_field_polynomial_equivalent_symmetric (c)
  28. 0028specialize prime_field_polynomial_equivalent_symmetric (L)
  29. 0029specialize prime_field_polynomial_equivalent_symmetric (x)
  30. 0030specialize prime_field_polynomial_equivalent_symmetric (x1)
  31. 0031specialize prime_field_polynomial_equivalent_symmetric (t+L)
  32. 0032apply prime_field_polynomial_equivalent_symmetric
  33. 0033exact hs
  34. 0034have ht : forall pfrep_power_converse_target pfrep_left_converse_target pfrep_right_converse_target. ((exists pfrep_position_converse_targetfirst. ((pfrep_position_converse_targetfirst+S (pfrep_power_converse_target)=(t+L)) /\ ((((exists ff_h_pfp_converse_targetfirstentry. ff_h_pfp_converse_targetfirstentry + S (pfrep_left_converse_target) = S ((S (pfrep_position_converse_targetfirst)) * x1)) /\ exists ff_q_pfp_converse_targetfirstentry. x = ff_q_pfp_converse_targetfirstentry * S ((S (pfrep_position_converse_targetfirst)) * x1) + (pfrep_left_converse_target)))))) \/ (((exists pfrep_gap_converse_targetfirstoutside. pfrep_gap_converse_targetfirstoutside+(t+L)=(pfrep_power_converse_target)) /\ (((pfrep_left_converse_target)=0))))) -> ((exists pfrep_position_converse_targetsecond. ((pfrep_position_converse_targetsecond+S (pfrep_power_converse_target)=(t+L)) /\ ((((exists ff_h_pfp_converse_targetsecondentry. ff_h_pfp_converse_targetsecondentry + S (pfrep_right_converse_target) = S ((S (pfrep_position_converse_targetsecond)) * e)) /\ exists ff_q_pfp_converse_targetsecondentry. d = ff_q_pfp_converse_targetsecondentry * S ((S (pfrep_position_converse_targetsecond)) * e) + (pfrep_right_converse_target)))))) \/ (((exists pfrep_gap_converse_targetsecondoutside. pfrep_gap_converse_targetsecondoutside+(t+L)=(pfrep_power_converse_target)) /\ (((pfrep_right_converse_target)=0))))) -> pfrep_left_converse_target=pfrep_right_converse_target
  35. 0035specialize prime_field_polynomial_equivalent_transitive (x)
  36. 0036specialize prime_field_polynomial_equivalent_transitive (x1)
  37. 0037specialize prime_field_polynomial_equivalent_transitive (t+L)
  38. 0038specialize prime_field_polynomial_equivalent_transitive (b)
  39. 0039specialize prime_field_polynomial_equivalent_transitive (c)
  40. 0040specialize prime_field_polynomial_equivalent_transitive (L)
  41. 0041specialize prime_field_polynomial_equivalent_transitive (d)
  42. 0042specialize prime_field_polynomial_equivalent_transitive (e)
  43. 0043specialize prime_field_polynomial_equivalent_transitive (t+L)
  44. 0044apply prime_field_polynomial_equivalent_transitive
  45. 0045exact hr
  46. 0046exact he
  47. 0047have hv : forall mdr_i_pfp_converse_values mdr_a_pfp_converse_values. (exists mdr_gap_pfp_converse_valuesb. mdr_gap_pfp_converse_valuesb + S (mdr_i_pfp_converse_values) = (t+L)) -> (((exists ff_h_mdr_pfp_converse_valueso. ff_h_mdr_pfp_converse_valueso + S (mdr_a_pfp_converse_values) = S ((S (mdr_i_pfp_converse_values)) * x1)) /\ exists ff_q_mdr_pfp_converse_valueso. x = ff_q_mdr_pfp_converse_valueso * S ((S (mdr_i_pfp_converse_values)) * x1) + (mdr_a_pfp_converse_values))) -> (((exists ff_h_mdr_pfp_converse_valuesn. ff_h_mdr_pfp_converse_valuesn + S (mdr_a_pfp_converse_values) = S ((S (mdr_i_pfp_converse_values)) * e)) /\ exists ff_q_mdr_pfp_converse_valuesn. d = ff_q_mdr_pfp_converse_valuesn * S ((S (mdr_i_pfp_converse_values)) * e) + (mdr_a_pfp_converse_values)))
  48. 0048specialize prime_field_polynomial_equivalent_implies_equal_same_length (x)
  49. 0049specialize prime_field_polynomial_equivalent_implies_equal_same_length (x1)
  50. 0050specialize prime_field_polynomial_equivalent_implies_equal_same_length (d)
  51. 0051specialize prime_field_polynomial_equivalent_implies_equal_same_length (e)
  52. 0052specialize prime_field_polynomial_equivalent_implies_equal_same_length (t+L)
  53. 0053apply prime_field_polynomial_equivalent_implies_equal_same_length
  54. 0054exact ht
  55. 0055specialize prime_field_polynomial_left_pad_transport (b)
  56. 0056specialize prime_field_polynomial_left_pad_transport (c)
  57. 0057specialize prime_field_polynomial_left_pad_transport (b)
  58. 0058specialize prime_field_polynomial_left_pad_transport (c)
  59. 0059specialize prime_field_polynomial_left_pad_transport (L)
  60. 0060specialize prime_field_polynomial_left_pad_transport (t)
  61. 0061specialize prime_field_polynomial_left_pad_transport (x)
  62. 0062specialize prime_field_polynomial_left_pad_transport (x1)
  63. 0063specialize prime_field_polynomial_left_pad_transport (d)
  64. 0064specialize prime_field_polynomial_left_pad_transport (e)
  65. 0065apply prime_field_polynomial_left_pad_transport
  66. 0066intro i
  67. 0067intro a
  68. 0068intro hi
  69. 0069intro ha
  70. 0070exact ha
  71. 0071exact hv
  72. 0072exact hp_witness_witness