PX0072

prime_field_polynomial_equivalent_implies_left_pad

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.

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. PolynomialEquivalent(b,c,L,d,e,t + L) → 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) · 1PolynomialLeftPad(b,c,L,t,d,e) · 2PolynomialEquivalent(b,c,L,d,e,M) · 4

Actual proof prerequisites

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

Complete tactic proof in conservative notation

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

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.

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 (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
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(b,c,L,t,B,C)Original native command in the exact edition
  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(b,c,L,x,x1,t + L)Original native command in the exact edition
  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(x,x1,t + L,b,c,L)Original native command in the exact edition
  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(x,x1,t + L,d,e,t + L)Original native command in the exact edition
  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(x,x1,d,e,t + L)Original native command in the exact edition
  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 defined 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 : ∃ B. ∃ C. PolynomialLeftPad(b,c,L,t,B,C)
  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 : PolynomialEquivalent(b,c,L,x,x1,t + L)
  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 : PolynomialEquivalent(x,x1,t + L,b,c,L)
  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 : PolynomialEquivalent(x,x1,t + L,d,e,t + L)
  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 : BetaPrefixEqual(x,x1,d,e,t + L)
  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