PP0015

prime_field_polynomial_scale_exists

Every canonical scalar has an actual finite coefficient-product table, including scalar zero and empty inputs.

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. ∀ l. ¬p = 0 → Lt(k,p) → BetaPrefixInto(ab,ac,l,p) → ∃ x. ∃ y. FpPolyScale(p,k,ab,ac,x,y,l)

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

Definition DAG

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

Actual proof prerequisites

beta_repeat_exists · checked external prerequisitebeta_pointwise_mul_prefix_exists · checked external prerequisiteprime_field_polynomial_normalization_existsprime_field_polynomial_scale_from_normalization
Original expanded first-order statement 
forall p k ab ac l. ~(p=0) -> (exists pfa_gap_scale_exists_scalar. pfa_gap_scale_exists_scalar + S (k) = (p)) -> (forall fom_index_pfp_scale_exists_source. (exists fom_gap_pfp_scale_exists_source_index_bound. fom_gap_pfp_scale_exists_source_index_bound + S (fom_index_pfp_scale_exists_source) = l) -> exists fom_value_pfp_scale_exists_source. ((((exists fom_beta_height_pfp_scale_exists_source_entry. fom_beta_height_pfp_scale_exists_source_entry + S (fom_value_pfp_scale_exists_source) = S ((S (fom_index_pfp_scale_exists_source)) * ac)) /\ exists fom_beta_quotient_pfp_scale_exists_source_entry. ab = fom_beta_quotient_pfp_scale_exists_source_entry * S ((S (fom_index_pfp_scale_exists_source)) * ac) + (fom_value_pfp_scale_exists_source))) /\ (exists fom_gap_pfp_scale_exists_source_value_bound. fom_gap_pfp_scale_exists_source_value_bound + S (fom_value_pfp_scale_exists_source) = p))) -> exists bb bc. (((exists pfa_gap_scale_exists_resultscalar. pfa_gap_scale_exists_resultscalar + S (k) = (p)) /\ ((forall pfp_index_scale_exists_result. (exists pfa_gap_scale_exists_resultindex. pfa_gap_scale_exists_resultindex + S (pfp_index_scale_exists_result) = (l)) -> exists pfp_source_scale_exists_result pfp_value_scale_exists_result. ((((exists ff_h_pfp_scale_exists_resultsource. ff_h_pfp_scale_exists_resultsource + S (pfp_source_scale_exists_result) = S ((S (pfp_index_scale_exists_result)) * ac)) /\ exists ff_q_pfp_scale_exists_resultsource. ab = ff_q_pfp_scale_exists_resultsource * S ((S (pfp_index_scale_exists_result)) * ac) + (pfp_source_scale_exists_result))) /\ (((((exists ff_h_pfp_scale_exists_resulttarget. ff_h_pfp_scale_exists_resulttarget + S (pfp_value_scale_exists_result) = S ((S (pfp_index_scale_exists_result)) * bc)) /\ exists ff_q_pfp_scale_exists_resulttarget. bb = ff_q_pfp_scale_exists_resulttarget * S ((S (pfp_index_scale_exists_result)) * bc) + (pfp_value_scale_exists_result))) /\ ((((exists pfa_gap_scale_exists_resultoperationleft. pfa_gap_scale_exists_resultoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scale_exists_resultoperationright. pfa_gap_scale_exists_resultoperationright + S (pfp_source_scale_exists_result) = (p)) /\ ((((exists pfa_gap_scale_exists_resultoperationresultbound. pfa_gap_scale_exists_resultoperationresultbound + S (pfp_value_scale_exists_result) = (p)) /\ ((exists pfa_offset_left_scale_exists_resultoperationresultcongruence pfa_offset_right_scale_exists_resultoperationresultcongruence. ((k) * (pfp_source_scale_exists_result)) + (p) * pfa_offset_left_scale_exists_resultoperationresultcongruence = (pfp_value_scale_exists_result) + (p) * pfa_offset_right_scale_exists_resultoperationresultcongruence)))))))))))))))))

Complete tactic proof in conservative notation

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

51 script commands · 10 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 (2)
prime field polynomial normalization existsprime field polynomial scale from normalization
01Fix variables and assumptionsL1–8

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 l
  6. L6
    intro hp
  7. L7
    intro hk
  8. L8
    intro hc
02Establish hrL9–12

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

  1. L9
    have hr : ∃ kb. ∃ kc. Repeat(kb,kc,k,l)Definitions: Repeat(kb,kc,k,l)Original native command in the exact edition
  2. L10
    specialize beta_repeat_exists (k)
  3. L11
    specialize beta_repeat_exists (l)
  4. L12
    apply beta_repeat_exists
03Separate the logical casesL13–14

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

  1. L13
    cases hr
  2. L14
    cases hr_witness
04Establish hmL15–21

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

  1. L15
    have hm : ∃ rb. ∃ rc. ∀ y. ∀ z. ∀ n. ∀ m. Lt(y,l) → BetaAt(x,x1,y,z) → BetaAt(ab,ac,y,n) → BetaAt(rb,rc,y,m) → m = z · nDefinitions: Lt(y,l)BetaAt(x,x1,y,z)BetaAt(ab,ac,y,n)BetaAt(rb,rc,y,m)Original native command in the exact edition
  2. L16
    specialize beta_pointwise_mul_prefix_exists (x)
  3. L17
    specialize beta_pointwise_mul_prefix_exists (x1)
  4. L18
    specialize beta_pointwise_mul_prefix_exists (ab)
  5. L19
    specialize beta_pointwise_mul_prefix_exists (ac)
  6. L20
    specialize beta_pointwise_mul_prefix_exists (l)
  7. L21
    apply beta_pointwise_mul_prefix_exists
05Separate the logical casesL22–23

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

  1. L22
    cases hm
  2. L23
    cases hm_witness
06Establish hnL24–30

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

  1. L24
    have hn : ∃ bb. ∃ bc. FpCoefficientReduction(p,x2,x3,bb,bc,l)Definitions: FpCoefficientReduction(p,x2,x3,bb,bc,l)Original native command in the exact edition
  2. L25
    specialize prime_field_polynomial_normalization_exists (p)
  3. L26
    specialize prime_field_polynomial_normalization_exists (x2)
  4. L27
    specialize prime_field_polynomial_normalization_exists (x3)
  5. L28
    specialize prime_field_polynomial_normalization_exists (l)
  6. L29
    apply prime_field_polynomial_normalization_exists
  7. L30
    exact hp
07Separate the logical casesL31–32

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

  1. L31
    cases hn
  2. L32
    cases hn_witness
08Construct an explicit witnessL33–34

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

  1. L33
    exists x4
  2. L34
    exists x5
09Use earlier factsL35–44

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

  1. L35
    specialize prime_field_polynomial_scale_from_normalization (p)
  2. L36
    specialize prime_field_polynomial_scale_from_normalization (k)
  3. L37
    specialize prime_field_polynomial_scale_from_normalization (x)
  4. L38
    specialize prime_field_polynomial_scale_from_normalization (x1)
  5. L39
    specialize prime_field_polynomial_scale_from_normalization (ab)
  6. L40
    specialize prime_field_polynomial_scale_from_normalization (ac)
  7. L41
    specialize prime_field_polynomial_scale_from_normalization (x2)
  8. L42
    specialize prime_field_polynomial_scale_from_normalization (x3)
  9. L43
    specialize prime_field_polynomial_scale_from_normalization (x4)
  10. L44
    specialize prime_field_polynomial_scale_from_normalization (x5)
10Use earlier factsL45–51

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

  1. L45
    specialize prime_field_polynomial_scale_from_normalization (l)
  2. L46
    apply prime_field_polynomial_scale_from_normalization
  3. L47
    exact hk
  4. L48
    exact hc
  5. L49
    exact hr_witness_witness
  6. L50
    exact hm_witness_witness
  7. L51
    exact hn_witness_witness

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro l
  6. 0006intro hp
  7. 0007intro hk
  8. 0008intro hc
  9. 0009have hr : ∃ kb. ∃ kc. Repeat(kb,kc,k,l)
  10. 0010specialize beta_repeat_exists (k)
  11. 0011specialize beta_repeat_exists (l)
  12. 0012apply beta_repeat_exists
  13. 0013cases hr
  14. 0014cases hr_witness
  15. 0015have hm : ∃ rb. ∃ rc. ∀ y. ∀ z. ∀ n. ∀ m. Lt(y,l) → BetaAt(x,x1,y,z) → BetaAt(ab,ac,y,n) → BetaAt(rb,rc,y,m) → m = z · n
  16. 0016specialize beta_pointwise_mul_prefix_exists (x)
  17. 0017specialize beta_pointwise_mul_prefix_exists (x1)
  18. 0018specialize beta_pointwise_mul_prefix_exists (ab)
  19. 0019specialize beta_pointwise_mul_prefix_exists (ac)
  20. 0020specialize beta_pointwise_mul_prefix_exists (l)
  21. 0021apply beta_pointwise_mul_prefix_exists
  22. 0022cases hm
  23. 0023cases hm_witness
  24. 0024have hn : ∃ bb. ∃ bc. FpCoefficientReduction(p,x2,x3,bb,bc,l)
  25. 0025specialize prime_field_polynomial_normalization_exists (p)
  26. 0026specialize prime_field_polynomial_normalization_exists (x2)
  27. 0027specialize prime_field_polynomial_normalization_exists (x3)
  28. 0028specialize prime_field_polynomial_normalization_exists (l)
  29. 0029apply prime_field_polynomial_normalization_exists
  30. 0030exact hp
  31. 0031cases hn
  32. 0032cases hn_witness
  33. 0033exists x4
  34. 0034exists x5
  35. 0035specialize prime_field_polynomial_scale_from_normalization (p)
  36. 0036specialize prime_field_polynomial_scale_from_normalization (k)
  37. 0037specialize prime_field_polynomial_scale_from_normalization (x)
  38. 0038specialize prime_field_polynomial_scale_from_normalization (x1)
  39. 0039specialize prime_field_polynomial_scale_from_normalization (ab)
  40. 0040specialize prime_field_polynomial_scale_from_normalization (ac)
  41. 0041specialize prime_field_polynomial_scale_from_normalization (x2)
  42. 0042specialize prime_field_polynomial_scale_from_normalization (x3)
  43. 0043specialize prime_field_polynomial_scale_from_normalization (x4)
  44. 0044specialize prime_field_polynomial_scale_from_normalization (x5)
  45. 0045specialize prime_field_polynomial_scale_from_normalization (l)
  46. 0046apply prime_field_polynomial_scale_from_normalization
  47. 0047exact hk
  48. 0048exact hc
  49. 0049exact hr_witness_witness
  50. 0050exact hm_witness_witness
  51. 0051exact hn_witness_witness