PP0019

prime_field_polynomial_scale_transport

Independent recoding of the source and target preserves actual scalar multiplication.

Alpha v34 checked-use · first admitted v31 · 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.

Length is representation length, not polynomial degree. Leading zeros and the empty zero polynomial are allowed; the canonical argument guard x<p also applies to the empty case. Evaluation is defined by actual field-operation steps, not an assumed residue invariant. Polynomial division, gcd, irreducibles and general prime-power extension fields remain open; this does not close G091.

Exact theorem in conservative defined notation

∀ p. ∀ k. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ AB. ∀ AC. ∀ BB. ∀ BC. ∀ l. BetaPrefixEqual(ab,ac,AB,AC,l) → BetaPrefixEqual(bb,bc,BB,BC,l) → FpPolyScale(p,k,ab,ac,bb,bc,l) → FpPolyScale(p,k,AB,AC,BB,BC,l)

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

Definition DAG

FpMul(p,a,b,c) · 1BetaPrefixEqual(b,c,d,e,l) · 2FpPolyScale(p,k,ab,ac,bb,bc,l) · 2BetaAt(b,c,i,x) · 2

Actual proof prerequisites

none
Original expanded first-order statement 
forall p k ab ac bb bc AB AC BB BC l. (forall mdr_i_pfp_scale_transport_source mdr_a_pfp_scale_transport_source. (exists mdr_gap_pfp_scale_transport_sourceb. mdr_gap_pfp_scale_transport_sourceb + S (mdr_i_pfp_scale_transport_source) = (l)) -> (((exists ff_h_mdr_pfp_scale_transport_sourceo. ff_h_mdr_pfp_scale_transport_sourceo + S (mdr_a_pfp_scale_transport_source) = S ((S (mdr_i_pfp_scale_transport_source)) * ac)) /\ exists ff_q_mdr_pfp_scale_transport_sourceo. ab = ff_q_mdr_pfp_scale_transport_sourceo * S ((S (mdr_i_pfp_scale_transport_source)) * ac) + (mdr_a_pfp_scale_transport_source))) -> (((exists ff_h_mdr_pfp_scale_transport_sourcen. ff_h_mdr_pfp_scale_transport_sourcen + S (mdr_a_pfp_scale_transport_source) = S ((S (mdr_i_pfp_scale_transport_source)) * AC)) /\ exists ff_q_mdr_pfp_scale_transport_sourcen. AB = ff_q_mdr_pfp_scale_transport_sourcen * S ((S (mdr_i_pfp_scale_transport_source)) * AC) + (mdr_a_pfp_scale_transport_source)))) -> (forall mdr_i_pfp_scale_transport_target mdr_a_pfp_scale_transport_target. (exists mdr_gap_pfp_scale_transport_targetb. mdr_gap_pfp_scale_transport_targetb + S (mdr_i_pfp_scale_transport_target) = (l)) -> (((exists ff_h_mdr_pfp_scale_transport_targeto. ff_h_mdr_pfp_scale_transport_targeto + S (mdr_a_pfp_scale_transport_target) = S ((S (mdr_i_pfp_scale_transport_target)) * bc)) /\ exists ff_q_mdr_pfp_scale_transport_targeto. bb = ff_q_mdr_pfp_scale_transport_targeto * S ((S (mdr_i_pfp_scale_transport_target)) * bc) + (mdr_a_pfp_scale_transport_target))) -> (((exists ff_h_mdr_pfp_scale_transport_targetn. ff_h_mdr_pfp_scale_transport_targetn + S (mdr_a_pfp_scale_transport_target) = S ((S (mdr_i_pfp_scale_transport_target)) * BC)) /\ exists ff_q_mdr_pfp_scale_transport_targetn. BB = ff_q_mdr_pfp_scale_transport_targetn * S ((S (mdr_i_pfp_scale_transport_target)) * BC) + (mdr_a_pfp_scale_transport_target)))) -> (((exists pfa_gap_scale_transport_oldscalar. pfa_gap_scale_transport_oldscalar + S (k) = (p)) /\ ((forall pfp_index_scale_transport_old. (exists pfa_gap_scale_transport_oldindex. pfa_gap_scale_transport_oldindex + S (pfp_index_scale_transport_old) = (l)) -> exists pfp_source_scale_transport_old pfp_value_scale_transport_old. ((((exists ff_h_pfp_scale_transport_oldsource. ff_h_pfp_scale_transport_oldsource + S (pfp_source_scale_transport_old) = S ((S (pfp_index_scale_transport_old)) * ac)) /\ exists ff_q_pfp_scale_transport_oldsource. ab = ff_q_pfp_scale_transport_oldsource * S ((S (pfp_index_scale_transport_old)) * ac) + (pfp_source_scale_transport_old))) /\ (((((exists ff_h_pfp_scale_transport_oldtarget. ff_h_pfp_scale_transport_oldtarget + S (pfp_value_scale_transport_old) = S ((S (pfp_index_scale_transport_old)) * bc)) /\ exists ff_q_pfp_scale_transport_oldtarget. bb = ff_q_pfp_scale_transport_oldtarget * S ((S (pfp_index_scale_transport_old)) * bc) + (pfp_value_scale_transport_old))) /\ ((((exists pfa_gap_scale_transport_oldoperationleft. pfa_gap_scale_transport_oldoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scale_transport_oldoperationright. pfa_gap_scale_transport_oldoperationright + S (pfp_source_scale_transport_old) = (p)) /\ ((((exists pfa_gap_scale_transport_oldoperationresultbound. pfa_gap_scale_transport_oldoperationresultbound + S (pfp_value_scale_transport_old) = (p)) /\ ((exists pfa_offset_left_scale_transport_oldoperationresultcongruence pfa_offset_right_scale_transport_oldoperationresultcongruence. ((k) * (pfp_source_scale_transport_old)) + (p) * pfa_offset_left_scale_transport_oldoperationresultcongruence = (pfp_value_scale_transport_old) + (p) * pfa_offset_right_scale_transport_oldoperationresultcongruence))))))))))))))))) -> (((exists pfa_gap_scale_transport_newscalar. pfa_gap_scale_transport_newscalar + S (k) = (p)) /\ ((forall pfp_index_scale_transport_new. (exists pfa_gap_scale_transport_newindex. pfa_gap_scale_transport_newindex + S (pfp_index_scale_transport_new) = (l)) -> exists pfp_source_scale_transport_new pfp_value_scale_transport_new. ((((exists ff_h_pfp_scale_transport_newsource. ff_h_pfp_scale_transport_newsource + S (pfp_source_scale_transport_new) = S ((S (pfp_index_scale_transport_new)) * AC)) /\ exists ff_q_pfp_scale_transport_newsource. AB = ff_q_pfp_scale_transport_newsource * S ((S (pfp_index_scale_transport_new)) * AC) + (pfp_source_scale_transport_new))) /\ (((((exists ff_h_pfp_scale_transport_newtarget. ff_h_pfp_scale_transport_newtarget + S (pfp_value_scale_transport_new) = S ((S (pfp_index_scale_transport_new)) * BC)) /\ exists ff_q_pfp_scale_transport_newtarget. BB = ff_q_pfp_scale_transport_newtarget * S ((S (pfp_index_scale_transport_new)) * BC) + (pfp_value_scale_transport_new))) /\ ((((exists pfa_gap_scale_transport_newoperationleft. pfa_gap_scale_transport_newoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scale_transport_newoperationright. pfa_gap_scale_transport_newoperationright + S (pfp_source_scale_transport_new) = (p)) /\ ((((exists pfa_gap_scale_transport_newoperationresultbound. pfa_gap_scale_transport_newoperationresultbound + S (pfp_value_scale_transport_new) = (p)) /\ ((exists pfa_offset_left_scale_transport_newoperationresultcongruence pfa_offset_right_scale_transport_newoperationresultcongruence. ((k) * (pfp_source_scale_transport_new)) + (p) * pfa_offset_left_scale_transport_newoperationresultcongruence = (pfp_value_scale_transport_new) + (p) * pfa_offset_right_scale_transport_newoperationresultcongruence)))))))))))))))))

Complete tactic proof in conservative notation

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

42 script commands · 12 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 p
  2. L2
    intro k
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro AB
  8. L8
    intro AC
  9. L9
    intro BB
  10. L10
    intro BC
02Fix variables and assumptionsL11–14

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

  1. L11
    intro l
  2. L12
    intro ha
  3. L13
    intro hb
  4. L14
    intro h
03Separate the logical casesL15–16

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

  1. L15
    cases h
  2. L16
    split
04Use earlier factsL17–17

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

  1. L17
    exact h_left
05Fix variables and assumptionsL18–19

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

  1. L18
    intro i
  2. L19
    intro hi
06Establish hvL20–23

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

  1. L20
    have hv : ∃ a. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(bb,bc,i,r) ∧ FpMul(p,k,a,r))Definitions: BetaAt(ab,ac,i,a)BetaAt(bb,bc,i,r)FpMul(p,k,a,r)Original native command in the exact edition
  2. L21
    specialize h_right (i)
  3. L22
    apply h_right
  4. L23
    exact hi
07Separate the logical casesL24–27

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

  1. L24
    cases hv
  2. L25
    cases hv_witness
  3. L26
    cases hv_witness_witness
  4. L27
    cases hv_witness_witness_right
08Construct an explicit witnessL28–29

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

  1. L28
    exists x
  2. L29
    exists x1
09Separate the logical casesL30–30

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

  1. L30
    split
10Use earlier factsL31–35

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

  1. L31
    specialize ha (i)
  2. L32
    specialize ha (x)
  3. L33
    apply ha
  4. L34
    exact hi
  5. L35
    exact hv_witness_witness_left
11Separate the logical casesL36–36

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

  1. L36
    split
12Use earlier factsL37–42

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

  1. L37
    specialize hb (i)
  2. L38
    specialize hb (x1)
  3. L39
    apply hb
  4. L40
    exact hi
  5. L41
    exact hv_witness_witness_right_left
  6. L42
    exact hv_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro AB
  8. 0008intro AC
  9. 0009intro BB
  10. 0010intro BC
  11. 0011intro l
  12. 0012intro ha
  13. 0013intro hb
  14. 0014intro h
  15. 0015cases h
  16. 0016split
  17. 0017exact h_left
  18. 0018intro i
  19. 0019intro hi
  20. 0020have hv : ∃ a. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(bb,bc,i,r) ∧ FpMul(p,k,a,r))
  21. 0021specialize h_right (i)
  22. 0022apply h_right
  23. 0023exact hi
  24. 0024cases hv
  25. 0025cases hv_witness
  26. 0026cases hv_witness_witness
  27. 0027cases hv_witness_witness_right
  28. 0028exists x
  29. 0029exists x1
  30. 0030split
  31. 0031specialize ha (i)
  32. 0032specialize ha (x)
  33. 0033apply ha
  34. 0034exact hi
  35. 0035exact hv_witness_witness_left
  36. 0036split
  37. 0037specialize hb (i)
  38. 0038specialize hb (x1)
  39. 0039apply hb
  40. 0040exact hi
  41. 0041exact hv_witness_witness_right_left
  42. 0042exact hv_witness_witness_right_right