PP0015

prime_field_polynomial_scale_exists

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 51 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_repeat_exists Stable theorem; checked-use authorized beta_pointwise_mul_prefix_exists Alpha theorem; checked-use authorized PP0002 prime_field_polynomial_normalization_exists PP0014 prime_field_polynomial_scale_from_normalization

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

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.

Named ingredients (2)
prime field polynomial normalization existsprime field polynomial scale from normalization

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–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 : exists kb kc. (forall pfp_repeat_index_scale_exists_repeat. (exists pfa_gap_scale_exists_repeatindex. pfa_gap_scale_exists_repeatindex + S (pfp_repeat_index_scale_exists_repeat) = (l)) -> (((exists ff_h_pfp_scale_exists_repeatentry. ff_h_pfp_scale_exists_repeatentry + S (k) = S ((S (pfp_repeat_index_scale_exists_repeat)) * kc)) /\ exists ff_q_pfp_scale_exists_repeatentry. kb = ff_q_pfp_scale_exists_repeatentry * S ((S (pfp_repeat_index_scale_exists_repeat)) * kc) + (k))))
  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: LtBetaAt
  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
  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 exact 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 : exists kb kc. (forall pfp_repeat_index_scale_exists_repeat. (exists pfa_gap_scale_exists_repeatindex. pfa_gap_scale_exists_repeatindex + S (pfp_repeat_index_scale_exists_repeat) = (l)) -> (((exists ff_h_pfp_scale_exists_repeatentry. ff_h_pfp_scale_exists_repeatentry + S (k) = S ((S (pfp_repeat_index_scale_exists_repeat)) * kc)) /\ exists ff_q_pfp_scale_exists_repeatentry. kb = ff_q_pfp_scale_exists_repeatentry * S ((S (pfp_repeat_index_scale_exists_repeat)) * kc) + (k))))
  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 : exists rb rc. (forall fpmp_index_pfp_scale_exists_raw fpmp_left_pfp_scale_exists_raw fpmp_right_pfp_scale_exists_raw fpmp_target_pfp_scale_exists_raw. (exists fpmp_gap_pfp_scale_exists_raw. fpmp_gap_pfp_scale_exists_raw + S fpmp_index_pfp_scale_exists_raw = l) -> (((exists ff_h_fpmp_pfp_scale_exists_raw_left. ff_h_fpmp_pfp_scale_exists_raw_left + S (fpmp_left_pfp_scale_exists_raw) = S ((S (fpmp_index_pfp_scale_exists_raw)) * x1)) /\ exists ff_q_fpmp_pfp_scale_exists_raw_left. x = ff_q_fpmp_pfp_scale_exists_raw_left * S ((S (fpmp_index_pfp_scale_exists_raw)) * x1) + (fpmp_left_pfp_scale_exists_raw))) -> (((exists ff_h_fpmp_pfp_scale_exists_raw_right. ff_h_fpmp_pfp_scale_exists_raw_right + S (fpmp_right_pfp_scale_exists_raw) = S ((S (fpmp_index_pfp_scale_exists_raw)) * ac)) /\ exists ff_q_fpmp_pfp_scale_exists_raw_right. ab = ff_q_fpmp_pfp_scale_exists_raw_right * S ((S (fpmp_index_pfp_scale_exists_raw)) * ac) + (fpmp_right_pfp_scale_exists_raw))) -> (((exists ff_h_fpmp_pfp_scale_exists_raw_target. ff_h_fpmp_pfp_scale_exists_raw_target + S (fpmp_target_pfp_scale_exists_raw) = S ((S (fpmp_index_pfp_scale_exists_raw)) * rc)) /\ exists ff_q_fpmp_pfp_scale_exists_raw_target. rb = ff_q_fpmp_pfp_scale_exists_raw_target * S ((S (fpmp_index_pfp_scale_exists_raw)) * rc) + (fpmp_target_pfp_scale_exists_raw))) -> fpmp_target_pfp_scale_exists_raw = fpmp_left_pfp_scale_exists_raw * fpmp_right_pfp_scale_exists_raw)
  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 : exists bb bc. (forall pfp_index_scale_exists_normalization. (exists pfa_gap_scale_exists_normalizationindex. pfa_gap_scale_exists_normalizationindex + S (pfp_index_scale_exists_normalization) = (l)) -> exists pfp_source_scale_exists_normalization pfp_residue_scale_exists_normalization. ((((exists ff_h_pfp_scale_exists_normalizationsource. ff_h_pfp_scale_exists_normalizationsource + S (pfp_source_scale_exists_normalization) = S ((S (pfp_index_scale_exists_normalization)) * x3)) /\ exists ff_q_pfp_scale_exists_normalizationsource. x2 = ff_q_pfp_scale_exists_normalizationsource * S ((S (pfp_index_scale_exists_normalization)) * x3) + (pfp_source_scale_exists_normalization))) /\ (((((exists ff_h_pfp_scale_exists_normalizationtarget. ff_h_pfp_scale_exists_normalizationtarget + S (pfp_residue_scale_exists_normalization) = S ((S (pfp_index_scale_exists_normalization)) * bc)) /\ exists ff_q_pfp_scale_exists_normalizationtarget. bb = ff_q_pfp_scale_exists_normalizationtarget * S ((S (pfp_index_scale_exists_normalization)) * bc) + (pfp_residue_scale_exists_normalization))) /\ ((((exists pfa_gap_scale_exists_normalizationresiduebound. pfa_gap_scale_exists_normalizationresiduebound + S (pfp_residue_scale_exists_normalization) = (p)) /\ ((exists pfa_offset_left_scale_exists_normalizationresiduecongruence pfa_offset_right_scale_exists_normalizationresiduecongruence. (pfp_source_scale_exists_normalization) + (p) * pfa_offset_left_scale_exists_normalizationresiduecongruence = (pfp_residue_scale_exists_normalization) + (p) * pfa_offset_right_scale_exists_normalizationresiduecongruence)))))))))
  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