PP0018

prime_field_polynomial_scale_functional

The scalar product has a unique decoded coefficient prefix, not a unique raw beta code.

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. ∀ cb. ∀ cc. ∀ l. FpPolyScale(p,k,ab,ac,bb,bc,l) → FpPolyScale(p,k,ab,ac,cb,cc,l) → BetaPrefixEqual(bb,bc,cb,cc,l)

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

Definition DAG

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

Actual proof prerequisites

beta_at_exists · checked external prerequisiteprime_field_polynomial_scale_entryprime_field_multiply_functional · checked external prerequisite
Original expanded first-order statement 
forall p k ab ac bb bc cb cc l. (((exists pfa_gap_scale_functional_firstscalar. pfa_gap_scale_functional_firstscalar + S (k) = (p)) /\ ((forall pfp_index_scale_functional_first. (exists pfa_gap_scale_functional_firstindex. pfa_gap_scale_functional_firstindex + S (pfp_index_scale_functional_first) = (l)) -> exists pfp_source_scale_functional_first pfp_value_scale_functional_first. ((((exists ff_h_pfp_scale_functional_firstsource. ff_h_pfp_scale_functional_firstsource + S (pfp_source_scale_functional_first) = S ((S (pfp_index_scale_functional_first)) * ac)) /\ exists ff_q_pfp_scale_functional_firstsource. ab = ff_q_pfp_scale_functional_firstsource * S ((S (pfp_index_scale_functional_first)) * ac) + (pfp_source_scale_functional_first))) /\ (((((exists ff_h_pfp_scale_functional_firsttarget. ff_h_pfp_scale_functional_firsttarget + S (pfp_value_scale_functional_first) = S ((S (pfp_index_scale_functional_first)) * bc)) /\ exists ff_q_pfp_scale_functional_firsttarget. bb = ff_q_pfp_scale_functional_firsttarget * S ((S (pfp_index_scale_functional_first)) * bc) + (pfp_value_scale_functional_first))) /\ ((((exists pfa_gap_scale_functional_firstoperationleft. pfa_gap_scale_functional_firstoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scale_functional_firstoperationright. pfa_gap_scale_functional_firstoperationright + S (pfp_source_scale_functional_first) = (p)) /\ ((((exists pfa_gap_scale_functional_firstoperationresultbound. pfa_gap_scale_functional_firstoperationresultbound + S (pfp_value_scale_functional_first) = (p)) /\ ((exists pfa_offset_left_scale_functional_firstoperationresultcongruence pfa_offset_right_scale_functional_firstoperationresultcongruence. ((k) * (pfp_source_scale_functional_first)) + (p) * pfa_offset_left_scale_functional_firstoperationresultcongruence = (pfp_value_scale_functional_first) + (p) * pfa_offset_right_scale_functional_firstoperationresultcongruence))))))))))))))))) -> (((exists pfa_gap_scale_functional_secondscalar. pfa_gap_scale_functional_secondscalar + S (k) = (p)) /\ ((forall pfp_index_scale_functional_second. (exists pfa_gap_scale_functional_secondindex. pfa_gap_scale_functional_secondindex + S (pfp_index_scale_functional_second) = (l)) -> exists pfp_source_scale_functional_second pfp_value_scale_functional_second. ((((exists ff_h_pfp_scale_functional_secondsource. ff_h_pfp_scale_functional_secondsource + S (pfp_source_scale_functional_second) = S ((S (pfp_index_scale_functional_second)) * ac)) /\ exists ff_q_pfp_scale_functional_secondsource. ab = ff_q_pfp_scale_functional_secondsource * S ((S (pfp_index_scale_functional_second)) * ac) + (pfp_source_scale_functional_second))) /\ (((((exists ff_h_pfp_scale_functional_secondtarget. ff_h_pfp_scale_functional_secondtarget + S (pfp_value_scale_functional_second) = S ((S (pfp_index_scale_functional_second)) * cc)) /\ exists ff_q_pfp_scale_functional_secondtarget. cb = ff_q_pfp_scale_functional_secondtarget * S ((S (pfp_index_scale_functional_second)) * cc) + (pfp_value_scale_functional_second))) /\ ((((exists pfa_gap_scale_functional_secondoperationleft. pfa_gap_scale_functional_secondoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scale_functional_secondoperationright. pfa_gap_scale_functional_secondoperationright + S (pfp_source_scale_functional_second) = (p)) /\ ((((exists pfa_gap_scale_functional_secondoperationresultbound. pfa_gap_scale_functional_secondoperationresultbound + S (pfp_value_scale_functional_second) = (p)) /\ ((exists pfa_offset_left_scale_functional_secondoperationresultcongruence pfa_offset_right_scale_functional_secondoperationresultcongruence. ((k) * (pfp_source_scale_functional_second)) + (p) * pfa_offset_left_scale_functional_secondoperationresultcongruence = (pfp_value_scale_functional_second) + (p) * pfa_offset_right_scale_functional_secondoperationresultcongruence))))))))))))))))) -> (forall mdr_i_pfp_scale_functional_result mdr_a_pfp_scale_functional_result. (exists mdr_gap_pfp_scale_functional_resultb. mdr_gap_pfp_scale_functional_resultb + S (mdr_i_pfp_scale_functional_result) = (l)) -> (((exists ff_h_mdr_pfp_scale_functional_resulto. ff_h_mdr_pfp_scale_functional_resulto + S (mdr_a_pfp_scale_functional_result) = S ((S (mdr_i_pfp_scale_functional_result)) * bc)) /\ exists ff_q_mdr_pfp_scale_functional_resulto. bb = ff_q_mdr_pfp_scale_functional_resulto * S ((S (mdr_i_pfp_scale_functional_result)) * bc) + (mdr_a_pfp_scale_functional_result))) -> (((exists ff_h_mdr_pfp_scale_functional_resultn. ff_h_mdr_pfp_scale_functional_resultn + S (mdr_a_pfp_scale_functional_result) = S ((S (mdr_i_pfp_scale_functional_result)) * cc)) /\ exists ff_q_mdr_pfp_scale_functional_resultn. cb = ff_q_mdr_pfp_scale_functional_resultn * S ((S (mdr_i_pfp_scale_functional_result)) * cc) + (mdr_a_pfp_scale_functional_result))))

Complete tactic proof in conservative notation

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

67 script commands · 12 reading checkpoints · 3 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 scale entry
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 cb
  8. L8
    intro cc
  9. L9
    intro l
  10. L10
    intro hb
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hc
  2. L12
    intro i
  3. L13
    intro r
  4. L14
    intro hi
  5. L15
    intro hr
03Establish haL16–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at exists.

  1. L16
    have ha : ∃ a. BetaAt(ab,ac,i,a)Definitions: BetaAt(ab,ac,i,a)Original native command in the exact edition
  2. L17
    specialize beta_at_exists (ab)
  3. L18
    specialize beta_at_exists (ac)
  4. L19
    specialize beta_at_exists (i)
  5. L20
    apply beta_at_exists
04Separate the logical casesL21–21

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

  1. L21
    cases ha
05Establish hsL22–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at exists.

  1. L22
    have hs : ∃ s. BetaAt(cb,cc,i,s)Definitions: BetaAt(cb,cc,i,s)Original native command in the exact edition
  2. L23
    specialize beta_at_exists (cb)
  3. L24
    specialize beta_at_exists (cc)
  4. L25
    specialize beta_at_exists (i)
  5. L26
    apply beta_at_exists
06Separate the logical casesL27–27

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

  1. L27
    cases hs
07Establish heqL28–37

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

  1. L28
    have heq : r=x1
  2. L29
    specialize prime_field_multiply_functional (p)
  3. L30
    specialize prime_field_multiply_functional (k)
  4. L31
    specialize prime_field_multiply_functional (x)
  5. L32
    specialize prime_field_multiply_functional (r)
  6. L33
    specialize prime_field_multiply_functional (x1)
  7. L34
    apply prime_field_multiply_functional
  8. L35
    specialize prime_field_polynomial_scale_entry (p)
  9. L36
    specialize prime_field_polynomial_scale_entry (k)
  10. L37
    specialize prime_field_polynomial_scale_entry (ab)
08Use earlier factsL38–47

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

  1. L38
    specialize prime_field_polynomial_scale_entry (ac)
  2. L39
    specialize prime_field_polynomial_scale_entry (bb)
  3. L40
    specialize prime_field_polynomial_scale_entry (bc)
  4. L41
    specialize prime_field_polynomial_scale_entry (l)
  5. L42
    specialize prime_field_polynomial_scale_entry (i)
  6. L43
    specialize prime_field_polynomial_scale_entry (x)
  7. L44
    specialize prime_field_polynomial_scale_entry (r)
  8. L45
    apply prime_field_polynomial_scale_entry
  9. L46
    exact hb
  10. L47
    exact hi
09Use earlier factsL48–57

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

  1. L48
    exact ha_witness
  2. L49
    exact hr
  3. L50
    specialize prime_field_polynomial_scale_entry (p)
  4. L51
    specialize prime_field_polynomial_scale_entry (k)
  5. L52
    specialize prime_field_polynomial_scale_entry (ab)
  6. L53
    specialize prime_field_polynomial_scale_entry (ac)
  7. L54
    specialize prime_field_polynomial_scale_entry (cb)
  8. L55
    specialize prime_field_polynomial_scale_entry (cc)
  9. L56
    specialize prime_field_polynomial_scale_entry (l)
  10. L57
    specialize prime_field_polynomial_scale_entry (i)
10Use earlier factsL58–64

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

  1. L58
    specialize prime_field_polynomial_scale_entry (x)
  2. L59
    specialize prime_field_polynomial_scale_entry (x1)
  3. L60
    apply prime_field_polynomial_scale_entry
  4. L61
    exact hc
  5. L62
    exact hi
  6. L63
    exact ha_witness
  7. L64
    exact hs_witness
11Calculate and transport equalitiesL65–66

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

  1. L65
    rewrite heq
  2. L66
    rewrite heq
12Use earlier factsL67–67

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

  1. L67
    exact hs_witness

Library-wide reading audit

Original defined command ledger · 67 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro cb
  8. 0008intro cc
  9. 0009intro l
  10. 0010intro hb
  11. 0011intro hc
  12. 0012intro i
  13. 0013intro r
  14. 0014intro hi
  15. 0015intro hr
  16. 0016have ha : ∃ a. BetaAt(ab,ac,i,a)
  17. 0017specialize beta_at_exists (ab)
  18. 0018specialize beta_at_exists (ac)
  19. 0019specialize beta_at_exists (i)
  20. 0020apply beta_at_exists
  21. 0021cases ha
  22. 0022have hs : ∃ s. BetaAt(cb,cc,i,s)
  23. 0023specialize beta_at_exists (cb)
  24. 0024specialize beta_at_exists (cc)
  25. 0025specialize beta_at_exists (i)
  26. 0026apply beta_at_exists
  27. 0027cases hs
  28. 0028have heq : r=x1
  29. 0029specialize prime_field_multiply_functional (p)
  30. 0030specialize prime_field_multiply_functional (k)
  31. 0031specialize prime_field_multiply_functional (x)
  32. 0032specialize prime_field_multiply_functional (r)
  33. 0033specialize prime_field_multiply_functional (x1)
  34. 0034apply prime_field_multiply_functional
  35. 0035specialize prime_field_polynomial_scale_entry (p)
  36. 0036specialize prime_field_polynomial_scale_entry (k)
  37. 0037specialize prime_field_polynomial_scale_entry (ab)
  38. 0038specialize prime_field_polynomial_scale_entry (ac)
  39. 0039specialize prime_field_polynomial_scale_entry (bb)
  40. 0040specialize prime_field_polynomial_scale_entry (bc)
  41. 0041specialize prime_field_polynomial_scale_entry (l)
  42. 0042specialize prime_field_polynomial_scale_entry (i)
  43. 0043specialize prime_field_polynomial_scale_entry (x)
  44. 0044specialize prime_field_polynomial_scale_entry (r)
  45. 0045apply prime_field_polynomial_scale_entry
  46. 0046exact hb
  47. 0047exact hi
  48. 0048exact ha_witness
  49. 0049exact hr
  50. 0050specialize prime_field_polynomial_scale_entry (p)
  51. 0051specialize prime_field_polynomial_scale_entry (k)
  52. 0052specialize prime_field_polynomial_scale_entry (ab)
  53. 0053specialize prime_field_polynomial_scale_entry (ac)
  54. 0054specialize prime_field_polynomial_scale_entry (cb)
  55. 0055specialize prime_field_polynomial_scale_entry (cc)
  56. 0056specialize prime_field_polynomial_scale_entry (l)
  57. 0057specialize prime_field_polynomial_scale_entry (i)
  58. 0058specialize prime_field_polynomial_scale_entry (x)
  59. 0059specialize prime_field_polynomial_scale_entry (x1)
  60. 0060apply prime_field_polynomial_scale_entry
  61. 0061exact hc
  62. 0062exact hi
  63. 0063exact ha_witness
  64. 0064exact hs_witness
  65. 0065rewrite heq
  66. 0066rewrite heq
  67. 0067exact hs_witness