PP0014

prime_field_polynomial_scale_from_normalization

Normalize an actual pointwise product with a repeated scalar to obtain genuine canonical 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. ∀ kb. ∀ kc. ∀ ab. ∀ ac. ∀ rb. ∀ rc. ∀ bb. ∀ bc. ∀ l. Lt(k,p) → BetaPrefixInto(ab,ac,l,p) → Repeat(kb,kc,k,l) → (∀ x. ∀ y. ∀ z. ∀ n. Lt(x,l) → BetaAt(kb,kc,x,y) → BetaAt(ab,ac,x,z) → BetaAt(rb,rc,x,n) → n = y · z) → FpCoefficientReduction(p,rb,rc,bb,bc,l) → FpPolyScale(p,k,ab,ac,bb,bc,l)

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

Definition DAG

CanonicalModularResidue(m,a,r) · 1BetaPrefixInto(b,c,l,B) · 1FpCoefficientReduction(p,b,c,d,e,l) · 1FpPolyScale(p,k,ab,ac,bb,bc,l) · 1Lt(a,b) · 3BetaAt(b,c,i,x) · 6Repeat(b,c,a,l) · 1

Actual proof prerequisites

prime_field_residue_input_equal · checked external prerequisite
Original expanded first-order statement 
forall p k kb kc ab ac rb rc bb bc l. (exists pfa_gap_scale_scalar. pfa_gap_scale_scalar + S (k) = (p)) -> (forall fom_index_pfp_scale_source. (exists fom_gap_pfp_scale_source_index_bound. fom_gap_pfp_scale_source_index_bound + S (fom_index_pfp_scale_source) = l) -> exists fom_value_pfp_scale_source. ((((exists fom_beta_height_pfp_scale_source_entry. fom_beta_height_pfp_scale_source_entry + S (fom_value_pfp_scale_source) = S ((S (fom_index_pfp_scale_source)) * ac)) /\ exists fom_beta_quotient_pfp_scale_source_entry. ab = fom_beta_quotient_pfp_scale_source_entry * S ((S (fom_index_pfp_scale_source)) * ac) + (fom_value_pfp_scale_source))) /\ (exists fom_gap_pfp_scale_source_value_bound. fom_gap_pfp_scale_source_value_bound + S (fom_value_pfp_scale_source) = p))) -> (forall pfp_repeat_index_scale_repeated. (exists pfa_gap_scale_repeatedindex. pfa_gap_scale_repeatedindex + S (pfp_repeat_index_scale_repeated) = (l)) -> (((exists ff_h_pfp_scale_repeatedentry. ff_h_pfp_scale_repeatedentry + S (k) = S ((S (pfp_repeat_index_scale_repeated)) * kc)) /\ exists ff_q_pfp_scale_repeatedentry. kb = ff_q_pfp_scale_repeatedentry * S ((S (pfp_repeat_index_scale_repeated)) * kc) + (k)))) -> (forall fpmp_index_pfp_scale_raw fpmp_left_pfp_scale_raw fpmp_right_pfp_scale_raw fpmp_target_pfp_scale_raw. (exists fpmp_gap_pfp_scale_raw. fpmp_gap_pfp_scale_raw + S fpmp_index_pfp_scale_raw = l) -> (((exists ff_h_fpmp_pfp_scale_raw_left. ff_h_fpmp_pfp_scale_raw_left + S (fpmp_left_pfp_scale_raw) = S ((S (fpmp_index_pfp_scale_raw)) * kc)) /\ exists ff_q_fpmp_pfp_scale_raw_left. kb = ff_q_fpmp_pfp_scale_raw_left * S ((S (fpmp_index_pfp_scale_raw)) * kc) + (fpmp_left_pfp_scale_raw))) -> (((exists ff_h_fpmp_pfp_scale_raw_right. ff_h_fpmp_pfp_scale_raw_right + S (fpmp_right_pfp_scale_raw) = S ((S (fpmp_index_pfp_scale_raw)) * ac)) /\ exists ff_q_fpmp_pfp_scale_raw_right. ab = ff_q_fpmp_pfp_scale_raw_right * S ((S (fpmp_index_pfp_scale_raw)) * ac) + (fpmp_right_pfp_scale_raw))) -> (((exists ff_h_fpmp_pfp_scale_raw_target. ff_h_fpmp_pfp_scale_raw_target + S (fpmp_target_pfp_scale_raw) = S ((S (fpmp_index_pfp_scale_raw)) * rc)) /\ exists ff_q_fpmp_pfp_scale_raw_target. rb = ff_q_fpmp_pfp_scale_raw_target * S ((S (fpmp_index_pfp_scale_raw)) * rc) + (fpmp_target_pfp_scale_raw))) -> fpmp_target_pfp_scale_raw = fpmp_left_pfp_scale_raw * fpmp_right_pfp_scale_raw) -> (forall pfp_index_scale_normalize. (exists pfa_gap_scale_normalizeindex. pfa_gap_scale_normalizeindex + S (pfp_index_scale_normalize) = (l)) -> exists pfp_source_scale_normalize pfp_residue_scale_normalize. ((((exists ff_h_pfp_scale_normalizesource. ff_h_pfp_scale_normalizesource + S (pfp_source_scale_normalize) = S ((S (pfp_index_scale_normalize)) * rc)) /\ exists ff_q_pfp_scale_normalizesource. rb = ff_q_pfp_scale_normalizesource * S ((S (pfp_index_scale_normalize)) * rc) + (pfp_source_scale_normalize))) /\ (((((exists ff_h_pfp_scale_normalizetarget. ff_h_pfp_scale_normalizetarget + S (pfp_residue_scale_normalize) = S ((S (pfp_index_scale_normalize)) * bc)) /\ exists ff_q_pfp_scale_normalizetarget. bb = ff_q_pfp_scale_normalizetarget * S ((S (pfp_index_scale_normalize)) * bc) + (pfp_residue_scale_normalize))) /\ ((((exists pfa_gap_scale_normalizeresiduebound. pfa_gap_scale_normalizeresiduebound + S (pfp_residue_scale_normalize) = (p)) /\ ((exists pfa_offset_left_scale_normalizeresiduecongruence pfa_offset_right_scale_normalizeresiduecongruence. (pfp_source_scale_normalize) + (p) * pfa_offset_left_scale_normalizeresiduecongruence = (pfp_residue_scale_normalize) + (p) * pfa_offset_right_scale_normalizeresiduecongruence))))))))) -> (((exists pfa_gap_scale_resultscalar. pfa_gap_scale_resultscalar + S (k) = (p)) /\ ((forall pfp_index_scale_result. (exists pfa_gap_scale_resultindex. pfa_gap_scale_resultindex + S (pfp_index_scale_result) = (l)) -> exists pfp_source_scale_result pfp_value_scale_result. ((((exists ff_h_pfp_scale_resultsource. ff_h_pfp_scale_resultsource + S (pfp_source_scale_result) = S ((S (pfp_index_scale_result)) * ac)) /\ exists ff_q_pfp_scale_resultsource. ab = ff_q_pfp_scale_resultsource * S ((S (pfp_index_scale_result)) * ac) + (pfp_source_scale_result))) /\ (((((exists ff_h_pfp_scale_resulttarget. ff_h_pfp_scale_resulttarget + S (pfp_value_scale_result) = S ((S (pfp_index_scale_result)) * bc)) /\ exists ff_q_pfp_scale_resulttarget. bb = ff_q_pfp_scale_resulttarget * S ((S (pfp_index_scale_result)) * bc) + (pfp_value_scale_result))) /\ ((((exists pfa_gap_scale_resultoperationleft. pfa_gap_scale_resultoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scale_resultoperationright. pfa_gap_scale_resultoperationright + S (pfp_source_scale_result) = (p)) /\ ((((exists pfa_gap_scale_resultoperationresultbound. pfa_gap_scale_resultoperationresultbound + S (pfp_value_scale_result) = (p)) /\ ((exists pfa_offset_left_scale_resultoperationresultcongruence pfa_offset_right_scale_resultoperationresultcongruence. ((k) * (pfp_source_scale_result)) + (p) * pfa_offset_left_scale_resultoperationresultcongruence = (pfp_value_scale_result) + (p) * pfa_offset_right_scale_resultoperationresultcongruence)))))))))))))))))

Complete tactic proof in conservative notation

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

62 script commands · 21 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.

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 kb
  4. L4
    intro kc
  5. L5
    intro ab
  6. L6
    intro ac
  7. L7
    intro rb
  8. L8
    intro rc
  9. L9
    intro bb
  10. L10
    intro bc
02Fix variables and assumptionsL11–16

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

  1. L11
    intro l
  2. L12
    intro hk
  3. L13
    intro hc
  4. L14
    intro hr
  5. L15
    intro hm
  6. L16
    intro hn
03Separate the logical casesL17–17

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

  1. L17
    split
04Use earlier factsL18–18

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

  1. L18
    exact hk
05Fix variables and assumptionsL19–20

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

  1. L19
    intro i
  2. L20
    intro hi
06Establish haL21–24

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

  1. L21
    have ha : ∃ a. BetaAt(ab,ac,i,a) ∧ Lt(a,p)Definitions: BetaAt(ab,ac,i,a)Lt(a,p)Original native command in the exact edition
  2. L22
    specialize hc (i)
  3. L23
    apply hc
  4. L24
    exact hi
07Separate the logical casesL25–26

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

  1. L25
    cases ha
  2. L26
    cases ha_witness
08Establish hvnL27–30

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

  1. L27
    have hvn : ∃ n. ∃ r. BetaAt(rb,rc,i,n) ∧ (BetaAt(bb,bc,i,r) ∧ CanonicalModularResidue(p,n,r))Definitions: BetaAt(rb,rc,i,n)BetaAt(bb,bc,i,r)CanonicalModularResidue(p,n,r)Original native command in the exact edition
  2. L28
    specialize hn (i)
  3. L29
    apply hn
  4. L30
    exact hi
09Separate the logical casesL31–34

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

  1. L31
    cases hvn
  2. L32
    cases hvn_witness
  3. L33
    cases hvn_witness_witness
  4. L34
    cases hvn_witness_witness_right
10Construct an explicit witnessL35–36

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

  1. L35
    exists x
  2. L36
    exists x2
11Separate the logical casesL37–37

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

  1. L37
    split
12Use earlier factsL38–38

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

  1. L38
    exact ha_witness_left
13Separate the logical casesL39–39

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

  1. L39
    split
14Use earlier factsL40–40

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

  1. L40
    exact hvn_witness_witness_right_left
15Separate the logical casesL41–41

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

  1. L41
    split
16Use earlier factsL42–42

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

  1. L42
    exact hk
17Separate the logical casesL43–43

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

  1. L43
    split
18Use earlier factsL44–49

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

  1. L44
    exact ha_witness_right
  2. L45
    specialize prime_field_residue_input_equal (p)
  3. L46
    specialize prime_field_residue_input_equal (k*x)
  4. L47
    specialize prime_field_residue_input_equal (x1)
  5. L48
    specialize prime_field_residue_input_equal (x2)
  6. L49
    apply prime_field_residue_input_equal
19Calculate and transport equalitiesL50–50

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

  1. L50
    symm
20Use earlier factsL51–60

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

  1. L51
    specialize hm (i)
  2. L52
    specialize hm (k)
  3. L53
    specialize hm (x)
  4. L54
    specialize hm (x1)
  5. L55
    apply hm
  6. L56
    exact hi
  7. L57
    specialize hr (i)
  8. L58
    apply hr
  9. L59
    exact hi
  10. L60
    exact ha_witness_left
21Use earlier factsL61–62

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

  1. L61
    exact hvn_witness_witness_left
  2. L62
    exact hvn_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 62 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro kb
  4. 0004intro kc
  5. 0005intro ab
  6. 0006intro ac
  7. 0007intro rb
  8. 0008intro rc
  9. 0009intro bb
  10. 0010intro bc
  11. 0011intro l
  12. 0012intro hk
  13. 0013intro hc
  14. 0014intro hr
  15. 0015intro hm
  16. 0016intro hn
  17. 0017split
  18. 0018exact hk
  19. 0019intro i
  20. 0020intro hi
  21. 0021have ha : ∃ a. BetaAt(ab,ac,i,a) ∧ Lt(a,p)
  22. 0022specialize hc (i)
  23. 0023apply hc
  24. 0024exact hi
  25. 0025cases ha
  26. 0026cases ha_witness
  27. 0027have hvn : ∃ n. ∃ r. BetaAt(rb,rc,i,n) ∧ (BetaAt(bb,bc,i,r) ∧ CanonicalModularResidue(p,n,r))
  28. 0028specialize hn (i)
  29. 0029apply hn
  30. 0030exact hi
  31. 0031cases hvn
  32. 0032cases hvn_witness
  33. 0033cases hvn_witness_witness
  34. 0034cases hvn_witness_witness_right
  35. 0035exists x
  36. 0036exists x2
  37. 0037split
  38. 0038exact ha_witness_left
  39. 0039split
  40. 0040exact hvn_witness_witness_right_left
  41. 0041split
  42. 0042exact hk
  43. 0043split
  44. 0044exact ha_witness_right
  45. 0045specialize prime_field_residue_input_equal (p)
  46. 0046specialize prime_field_residue_input_equal (k*x)
  47. 0047specialize prime_field_residue_input_equal (x1)
  48. 0048specialize prime_field_residue_input_equal (x2)
  49. 0049apply prime_field_residue_input_equal
  50. 0050symm
  51. 0051specialize hm (i)
  52. 0052specialize hm (k)
  53. 0053specialize hm (x)
  54. 0054specialize hm (x1)
  55. 0055apply hm
  56. 0056exact hi
  57. 0057specialize hr (i)
  58. 0058apply hr
  59. 0059exact hi
  60. 0060exact ha_witness_left
  61. 0061exact hvn_witness_witness_left
  62. 0062exact hvn_witness_witness_right_right