PP0019

prime_field_polynomial_scale_transport

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 0 declared prerequisites and contains 42 exact native proof lines.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

none

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

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.

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 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: FpMulBetaAt
  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 exact 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 : exists a r. ((((exists ff_h_pfp_scale_transport_a. ff_h_pfp_scale_transport_a + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_scale_transport_a. ab = ff_q_pfp_scale_transport_a * S ((S (i)) * ac) + (a))) /\ (((((exists ff_h_pfp_scale_transport_r. ff_h_pfp_scale_transport_r + S (r) = S ((S (i)) * bc)) /\ exists ff_q_pfp_scale_transport_r. bb = ff_q_pfp_scale_transport_r * S ((S (i)) * bc) + (r))) /\ ((((exists pfa_gap_scale_transport_operationleft. pfa_gap_scale_transport_operationleft + S (k) = (p)) /\ (((exists pfa_gap_scale_transport_operationright. pfa_gap_scale_transport_operationright + S (a) = (p)) /\ ((((exists pfa_gap_scale_transport_operationresultbound. pfa_gap_scale_transport_operationresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_scale_transport_operationresultcongruence pfa_offset_right_scale_transport_operationresultcongruence. ((k) * (a)) + (p) * pfa_offset_left_scale_transport_operationresultcongruence = (r) + (p) * pfa_offset_right_scale_transport_operationresultcongruence)))))))))))))
  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