PX0020

prime_field_polynomial_scale_left_pad_transport

Common actual leading-zero padding preserves the genuine aligned scale coefficient operation, including empty prefixes.

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

∀ p. ∀ k. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ L. ∀ t. ∀ AB. ∀ AC. ∀ BB. ∀ BC. Prime(p) → FpPolyScale(p,k,ab,ac,bb,bc,L) → PolynomialLeftPad(ab,ac,L,t,AB,AC) → PolynomialLeftPad(bb,bc,L,t,BB,BC) → FpPolyScale(p,k,AB,AC,BB,BC,t + L)

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

Definition DAG

FpMul(p,a,b,c) · 1FpPolyScale(p,k,ab,ac,bb,bc,l) · 2PolynomialLeftPad(b,c,L,t,d,e) · 2Lt(a,b) · 2Prime(p) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

prime_field_polynomial_left_pad_index_casesprime_field_multiply_zero_right · checked external prerequisite
Original expanded first-order statement 
forall p k ab ac bb bc L t AB AC BB BC. (~((p) = 1) /\ forall pfa_factor_left_pad_operation_prime pfa_factor_right_pad_operation_prime. (p) = pfa_factor_left_pad_operation_prime * pfa_factor_right_pad_operation_prime -> pfa_factor_left_pad_operation_prime = 1 \/ pfa_factor_right_pad_operation_prime = 1) -> (((exists pfa_gap_pad_operation_oldscalar. pfa_gap_pad_operation_oldscalar + S (k) = (p)) /\ ((forall pfp_index_pad_operation_old. (exists pfa_gap_pad_operation_oldindex. pfa_gap_pad_operation_oldindex + S (pfp_index_pad_operation_old) = (L)) -> exists pfp_source_pad_operation_old pfp_value_pad_operation_old. ((((exists ff_h_pfp_pad_operation_oldsource. ff_h_pfp_pad_operation_oldsource + S (pfp_source_pad_operation_old) = S ((S (pfp_index_pad_operation_old)) * ac)) /\ exists ff_q_pfp_pad_operation_oldsource. ab = ff_q_pfp_pad_operation_oldsource * S ((S (pfp_index_pad_operation_old)) * ac) + (pfp_source_pad_operation_old))) /\ (((((exists ff_h_pfp_pad_operation_oldtarget. ff_h_pfp_pad_operation_oldtarget + S (pfp_value_pad_operation_old) = S ((S (pfp_index_pad_operation_old)) * bc)) /\ exists ff_q_pfp_pad_operation_oldtarget. bb = ff_q_pfp_pad_operation_oldtarget * S ((S (pfp_index_pad_operation_old)) * bc) + (pfp_value_pad_operation_old))) /\ ((((exists pfa_gap_pad_operation_oldoperationleft. pfa_gap_pad_operation_oldoperationleft + S (k) = (p)) /\ (((exists pfa_gap_pad_operation_oldoperationright. pfa_gap_pad_operation_oldoperationright + S (pfp_source_pad_operation_old) = (p)) /\ ((((exists pfa_gap_pad_operation_oldoperationresultbound. pfa_gap_pad_operation_oldoperationresultbound + S (pfp_value_pad_operation_old) = (p)) /\ ((exists pfa_offset_left_pad_operation_oldoperationresultcongruence pfa_offset_right_pad_operation_oldoperationresultcongruence. ((k) * (pfp_source_pad_operation_old)) + (p) * pfa_offset_left_pad_operation_oldoperationresultcongruence = (pfp_value_pad_operation_old) + (p) * pfa_offset_right_pad_operation_oldoperationresultcongruence))))))))))))))))) -> (((forall pfp_repeat_index_pad_operation_abzeros. (exists pfa_gap_pad_operation_abzerosindex. pfa_gap_pad_operation_abzerosindex + S (pfp_repeat_index_pad_operation_abzeros) = (t)) -> (((exists ff_h_pfp_pad_operation_abzerosentry. ff_h_pfp_pad_operation_abzerosentry + S (0) = S ((S (pfp_repeat_index_pad_operation_abzeros)) * AC)) /\ exists ff_q_pfp_pad_operation_abzerosentry. AB = ff_q_pfp_pad_operation_abzerosentry * S ((S (pfp_repeat_index_pad_operation_abzeros)) * AC) + (0)))) /\ ((forall pfrep_index_pad_operation_ab pfrep_value_pad_operation_ab. (exists pfa_gap_pad_operation_abbound. pfa_gap_pad_operation_abbound + S (pfrep_index_pad_operation_ab) = (L)) -> (((exists ff_h_pfp_pad_operation_abinput. ff_h_pfp_pad_operation_abinput + S (pfrep_value_pad_operation_ab) = S ((S (pfrep_index_pad_operation_ab)) * ac)) /\ exists ff_q_pfp_pad_operation_abinput. ab = ff_q_pfp_pad_operation_abinput * S ((S (pfrep_index_pad_operation_ab)) * ac) + (pfrep_value_pad_operation_ab))) -> (((exists ff_h_pfp_pad_operation_aboutput. ff_h_pfp_pad_operation_aboutput + S (pfrep_value_pad_operation_ab) = S ((S ((t)+pfrep_index_pad_operation_ab)) * AC)) /\ exists ff_q_pfp_pad_operation_aboutput. AB = ff_q_pfp_pad_operation_aboutput * S ((S ((t)+pfrep_index_pad_operation_ab)) * AC) + (pfrep_value_pad_operation_ab))))))) -> (((forall pfp_repeat_index_pad_operation_bbzeros. (exists pfa_gap_pad_operation_bbzerosindex. pfa_gap_pad_operation_bbzerosindex + S (pfp_repeat_index_pad_operation_bbzeros) = (t)) -> (((exists ff_h_pfp_pad_operation_bbzerosentry. ff_h_pfp_pad_operation_bbzerosentry + S (0) = S ((S (pfp_repeat_index_pad_operation_bbzeros)) * BC)) /\ exists ff_q_pfp_pad_operation_bbzerosentry. BB = ff_q_pfp_pad_operation_bbzerosentry * S ((S (pfp_repeat_index_pad_operation_bbzeros)) * BC) + (0)))) /\ ((forall pfrep_index_pad_operation_bb pfrep_value_pad_operation_bb. (exists pfa_gap_pad_operation_bbbound. pfa_gap_pad_operation_bbbound + S (pfrep_index_pad_operation_bb) = (L)) -> (((exists ff_h_pfp_pad_operation_bbinput. ff_h_pfp_pad_operation_bbinput + S (pfrep_value_pad_operation_bb) = S ((S (pfrep_index_pad_operation_bb)) * bc)) /\ exists ff_q_pfp_pad_operation_bbinput. bb = ff_q_pfp_pad_operation_bbinput * S ((S (pfrep_index_pad_operation_bb)) * bc) + (pfrep_value_pad_operation_bb))) -> (((exists ff_h_pfp_pad_operation_bboutput. ff_h_pfp_pad_operation_bboutput + S (pfrep_value_pad_operation_bb) = S ((S ((t)+pfrep_index_pad_operation_bb)) * BC)) /\ exists ff_q_pfp_pad_operation_bboutput. BB = ff_q_pfp_pad_operation_bboutput * S ((S ((t)+pfrep_index_pad_operation_bb)) * BC) + (pfrep_value_pad_operation_bb))))))) -> (((exists pfa_gap_pad_operation_newscalar. pfa_gap_pad_operation_newscalar + S (k) = (p)) /\ ((forall pfp_index_pad_operation_new. (exists pfa_gap_pad_operation_newindex. pfa_gap_pad_operation_newindex + S (pfp_index_pad_operation_new) = (t+L)) -> exists pfp_source_pad_operation_new pfp_value_pad_operation_new. ((((exists ff_h_pfp_pad_operation_newsource. ff_h_pfp_pad_operation_newsource + S (pfp_source_pad_operation_new) = S ((S (pfp_index_pad_operation_new)) * AC)) /\ exists ff_q_pfp_pad_operation_newsource. AB = ff_q_pfp_pad_operation_newsource * S ((S (pfp_index_pad_operation_new)) * AC) + (pfp_source_pad_operation_new))) /\ (((((exists ff_h_pfp_pad_operation_newtarget. ff_h_pfp_pad_operation_newtarget + S (pfp_value_pad_operation_new) = S ((S (pfp_index_pad_operation_new)) * BC)) /\ exists ff_q_pfp_pad_operation_newtarget. BB = ff_q_pfp_pad_operation_newtarget * S ((S (pfp_index_pad_operation_new)) * BC) + (pfp_value_pad_operation_new))) /\ ((((exists pfa_gap_pad_operation_newoperationleft. pfa_gap_pad_operation_newoperationleft + S (k) = (p)) /\ (((exists pfa_gap_pad_operation_newoperationright. pfa_gap_pad_operation_newoperationright + S (pfp_source_pad_operation_new) = (p)) /\ ((((exists pfa_gap_pad_operation_newoperationresultbound. pfa_gap_pad_operation_newoperationresultbound + S (pfp_value_pad_operation_new) = (p)) /\ ((exists pfa_offset_left_pad_operation_newoperationresultcongruence pfa_offset_right_pad_operation_newoperationresultcongruence. ((k) * (pfp_source_pad_operation_new)) + (p) * pfa_offset_left_pad_operation_newoperationresultcongruence = (pfp_value_pad_operation_new) + (p) * pfa_offset_right_pad_operation_newoperationresultcongruence)))))))))))))))))

Complete tactic proof in conservative notation

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

74 script commands · 22 reading checkpoints · 2 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 p
  2. L2
    intro k
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro L
  8. L8
    intro t
  9. L9
    intro AB
  10. L10
    intro AC
02Fix variables and assumptionsL11–16

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

  1. L11
    intro BB
  2. L12
    intro BC
  3. L13
    intro hp
  4. L14
    intro hop
  5. L15
    intro h0
  6. L16
    intro h1
03Separate the logical casesL17–20

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

  1. L17
    cases h0
  2. L18
    cases h1
  3. L19
    cases hop
  4. L20
    split
04Use earlier factsL21–21

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

  1. L21
    exact hop_left
05Fix variables and assumptionsL22–23

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

  1. L22
    intro i
  2. L23
    intro hi
06Establish hcL24–29

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. L24
    have hc : 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. L25
    specialize prime_field_polynomial_left_pad_index_cases (t)
  3. L26
    specialize prime_field_polynomial_left_pad_index_cases (L)
  4. L27
    specialize prime_field_polynomial_left_pad_index_cases (i)
  5. L28
    apply prime_field_polynomial_left_pad_index_cases
  6. L29
    exact hi
07Separate the logical casesL30–30

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

  1. L30
    cases hc
08Construct an explicit witnessL31–32

Supply the displayed value, then prove that it has the required property.

  1. L31
    exists 0
  2. L32
    exists 0
09Separate the logical casesL33–33

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

  1. L33
    split
10Use earlier factsL34–36

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

  1. L34
    specialize h0_left (i)
  2. L35
    apply h0_left
  3. L36
    exact hc_left
11Separate the logical casesL37–37

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

  1. L37
    split
12Use earlier factsL38–45

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

  1. L38
    specialize h1_left (i)
  2. L39
    apply h1_left
  3. L40
    exact hc_left
  4. L41
    specialize prime_field_multiply_zero_right (p)
  5. L42
    specialize prime_field_multiply_zero_right (k)
  6. L43
    apply prime_field_multiply_zero_right
  7. L44
    exact hp
  8. L45
    exact hop_left
13Separate the logical casesL46–47

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

  1. L46
    cases hc_right
  2. L47
    cases hc_right_witness
14Establish hvL48–51

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hop right.

  1. L48
    have hv : ∃ a. ∃ r. BetaAt(ab,ac,x,a) ∧ (BetaAt(bb,bc,x,r) ∧ FpMul(p,k,a,r))Definitions: BetaAt(ab,ac,x,a)BetaAt(bb,bc,x,r)FpMul(p,k,a,r)Original native command in the exact edition
  2. L49
    specialize hop_right (x)
  3. L50
    apply hop_right
  4. L51
    exact hc_right_witness_left
15Separate the logical casesL52–55

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

  1. L52
    cases hv
  2. L53
    cases hv_witness
  3. L54
    cases hv_witness_witness
  4. L55
    cases hv_witness_witness_right
16Construct an explicit witnessL56–57

Supply the displayed value, then prove that it has the required property.

  1. L56
    exists x1
  2. L57
    exists x2
17Separate the logical casesL58–58

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

  1. L58
    split
18Calculate and transport equalitiesL59–60

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

  1. L59
    rewrite hc_right_witness_right
  2. L60
    rewrite hc_right_witness_right
19Use earlier factsL61–65

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

  1. L61
    specialize h0_right (x)
  2. L62
    specialize h0_right (x1)
  3. L63
    apply h0_right
  4. L64
    exact hc_right_witness_left
  5. L65
    exact hv_witness_witness_left
20Separate the logical casesL66–66

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

  1. L66
    split
21Calculate and transport equalitiesL67–68

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

  1. L67
    rewrite hc_right_witness_right
  2. L68
    rewrite hc_right_witness_right
22Use earlier factsL69–74

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

  1. L69
    specialize h1_right (x)
  2. L70
    specialize h1_right (x2)
  3. L71
    apply h1_right
  4. L72
    exact hc_right_witness_left
  5. L73
    exact hv_witness_witness_right_left
  6. L74
    exact hv_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 74 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro L
  8. 0008intro t
  9. 0009intro AB
  10. 0010intro AC
  11. 0011intro BB
  12. 0012intro BC
  13. 0013intro hp
  14. 0014intro hop
  15. 0015intro h0
  16. 0016intro h1
  17. 0017cases h0
  18. 0018cases h1
  19. 0019cases hop
  20. 0020split
  21. 0021exact hop_left
  22. 0022intro i
  23. 0023intro hi
  24. 0024have hc : Lt(i,t) ∨ (∃ x. Lt(x,L) ∧ i = t + x)
  25. 0025specialize prime_field_polynomial_left_pad_index_cases (t)
  26. 0026specialize prime_field_polynomial_left_pad_index_cases (L)
  27. 0027specialize prime_field_polynomial_left_pad_index_cases (i)
  28. 0028apply prime_field_polynomial_left_pad_index_cases
  29. 0029exact hi
  30. 0030cases hc
  31. 0031exists 0
  32. 0032exists 0
  33. 0033split
  34. 0034specialize h0_left (i)
  35. 0035apply h0_left
  36. 0036exact hc_left
  37. 0037split
  38. 0038specialize h1_left (i)
  39. 0039apply h1_left
  40. 0040exact hc_left
  41. 0041specialize prime_field_multiply_zero_right (p)
  42. 0042specialize prime_field_multiply_zero_right (k)
  43. 0043apply prime_field_multiply_zero_right
  44. 0044exact hp
  45. 0045exact hop_left
  46. 0046cases hc_right
  47. 0047cases hc_right_witness
  48. 0048have hv : ∃ a. ∃ r. BetaAt(ab,ac,x,a) ∧ (BetaAt(bb,bc,x,r) ∧ FpMul(p,k,a,r))
  49. 0049specialize hop_right (x)
  50. 0050apply hop_right
  51. 0051exact hc_right_witness_left
  52. 0052cases hv
  53. 0053cases hv_witness
  54. 0054cases hv_witness_witness
  55. 0055cases hv_witness_witness_right
  56. 0056exists x1
  57. 0057exists x2
  58. 0058split
  59. 0059rewrite hc_right_witness_right
  60. 0060rewrite hc_right_witness_right
  61. 0061specialize h0_right (x)
  62. 0062specialize h0_right (x1)
  63. 0063apply h0_right
  64. 0064exact hc_right_witness_left
  65. 0065exact hv_witness_witness_left
  66. 0066split
  67. 0067rewrite hc_right_witness_right
  68. 0068rewrite hc_right_witness_right
  69. 0069specialize h1_right (x)
  70. 0070specialize h1_right (x2)
  71. 0071apply h1_right
  72. 0072exact hc_right_witness_left
  73. 0073exact hv_witness_witness_right_left
  74. 0074exact hv_witness_witness_right_right