PQ0039

prime_field_polynomial_monic_normalization_leading

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

The actual scaled leading coefficient equals one by the recorded inverse, not by a monic output premise.

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 L. (((~((L) = 0)) /\ (((exists pfm_leading_normalization_leading_source. ((((exists ff_h_pfp_normalization_leading_sourcesource. ff_h_pfp_normalization_leading_sourcesource + S (pfm_leading_normalization_leading_source) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_leading_sourcesource. ab = ff_q_pfp_normalization_leading_sourcesource * S ((S (0)) * ac) + (pfm_leading_normalization_leading_source))) /\ ((((~((pfm_leading_normalization_leading_source) = 0)) /\ ((((exists pfa_gap_normalization_leading_sourceinversemultiplicationleft. pfa_gap_normalization_leading_sourceinversemultiplicationleft + S (pfm_leading_normalization_leading_source) = (p)) /\ (((exists pfa_gap_normalization_leading_sourceinversemultiplicationright. pfa_gap_normalization_leading_sourceinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_leading_sourceinversemultiplicationresultbound. pfa_gap_normalization_leading_sourceinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_leading_sourceinversemultiplicationresultcongruence pfa_offset_right_normalization_leading_sourceinversemultiplicationresultcongruence. ((pfm_leading_normalization_leading_source) * (k)) + (p) * pfa_offset_left_normalization_leading_sourceinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_leading_sourceinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_leading_sourcescalescalar. pfa_gap_normalization_leading_sourcescalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_leading_sourcescale. (exists pfa_gap_normalization_leading_sourcescaleindex. pfa_gap_normalization_leading_sourcescaleindex + S (pfp_index_normalization_leading_sourcescale) = (L)) -> exists pfp_source_normalization_leading_sourcescale pfp_value_normalization_leading_sourcescale. ((((exists ff_h_pfp_normalization_leading_sourcescalesource. ff_h_pfp_normalization_leading_sourcescalesource + S (pfp_source_normalization_leading_sourcescale) = S ((S (pfp_index_normalization_leading_sourcescale)) * ac)) /\ exists ff_q_pfp_normalization_leading_sourcescalesource. ab = ff_q_pfp_normalization_leading_sourcescalesource * S ((S (pfp_index_normalization_leading_sourcescale)) * ac) + (pfp_source_normalization_leading_sourcescale))) /\ (((((exists ff_h_pfp_normalization_leading_sourcescaletarget. ff_h_pfp_normalization_leading_sourcescaletarget + S (pfp_value_normalization_leading_sourcescale) = S ((S (pfp_index_normalization_leading_sourcescale)) * bc)) /\ exists ff_q_pfp_normalization_leading_sourcescaletarget. bb = ff_q_pfp_normalization_leading_sourcescaletarget * S ((S (pfp_index_normalization_leading_sourcescale)) * bc) + (pfp_value_normalization_leading_sourcescale))) /\ ((((exists pfa_gap_normalization_leading_sourcescaleoperationleft. pfa_gap_normalization_leading_sourcescaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_leading_sourcescaleoperationright. pfa_gap_normalization_leading_sourcescaleoperationright + S (pfp_source_normalization_leading_sourcescale) = (p)) /\ ((((exists pfa_gap_normalization_leading_sourcescaleoperationresultbound. pfa_gap_normalization_leading_sourcescaleoperationresultbound + S (pfp_value_normalization_leading_sourcescale) = (p)) /\ ((exists pfa_offset_left_normalization_leading_sourcescaleoperationresultcongruence pfa_offset_right_normalization_leading_sourcescaleoperationresultcongruence. ((k) * (pfp_source_normalization_leading_sourcescale)) + (p) * pfa_offset_left_normalization_leading_sourcescaleoperationresultcongruence = (pfp_value_normalization_leading_sourcescale) + (p) * pfa_offset_right_normalization_leading_sourcescaleoperationresultcongruence)))))))))))))))))))))) -> (((exists ff_h_pfp_normalization_leading_result. ff_h_pfp_normalization_leading_result + S (1) = S ((S (0)) * bc)) /\ exists ff_q_pfp_normalization_leading_result. bb = ff_q_pfp_normalization_leading_result * S ((S (0)) * bc) + (1)))

Constructive proof overview

Generated structural guide

The actual scaled leading coefficient equals one by the recorded inverse, not by a monic output premise.

The unchanged tactic script uses 5 declared prerequisites and contains 60 exact native proof lines.

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

Proof neighborhood

Direct dependencies

one_le_of_ne_zero Stable theorem; checked-use authorized beta_at_exists Stable theorem; checked-use authorized PQ0037 prime_field_polynomial_monic_normalization_entry prime_field_multiply_commutative Alpha theorem; checked-use authorized prime_field_multiply_functional Alpha theorem; checked-use authorized

Direct dependents

PQ003A prime_field_polynomial_monic_normalization_monic

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

60 script commands · 12 reading checkpoints · 6 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 (1)
prime field polynomial monic normalization entry

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 bb
  6. L6
    intro bc
  7. L7
    intro L
  8. L8
    intro h
02Establish hcL9–10

Establish this local claim before using it. It is not an additional assumption.

  1. L9
    have hc : FpMonicNormalization(p,k,ab,ac,bb,bc,L)Definitions: FpMonicNormalization
  2. L10
    exact h
03Separate the logical casesL11–15

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

  1. L11
    cases hc
  2. L12
    cases hc_right
  3. L13
    cases hc_right_left
  4. L14
    cases hc_right_left_witness
  5. L15
    cases hc_right_left_witness_right
04Establish hzeroL16–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply one le of ne zero.

  1. L16
    have hzero : exists pfa_gap_normalization_leading_index. pfa_gap_normalization_leading_index + S (0) = (L)
  2. L17
    specialize one_le_of_ne_zero (L)
  3. L18
    apply one_le_of_ne_zero
  4. L19
    exact hc_left
05Establish hrL20–24

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

  1. L20
    have hr : exists r. (((exists ff_h_pfp_normalization_leading_decoding. ff_h_pfp_normalization_leading_decoding + S (r) = S ((S (0)) * bc)) /\ exists ff_q_pfp_normalization_leading_decoding. bb = ff_q_pfp_normalization_leading_decoding * S ((S (0)) * bc) + (r)))
  2. L21
    specialize beta_at_exists (bb)
  3. L22
    specialize beta_at_exists (bc)
  4. L23
    specialize beta_at_exists (0)
  5. L24
    apply beta_at_exists
06Separate the logical casesL25–25

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

  1. L25
    cases hr
07Establish hmL26–35

Establish this local claim before using it. It is not an additional assumption.

  1. L26
    have hm : FpMul(p,k,x,x1)Definitions: FpMul
  2. L27
    specialize prime_field_polynomial_monic_normalization_entry (p)
  3. L28
    specialize prime_field_polynomial_monic_normalization_entry (k)
  4. L29
    specialize prime_field_polynomial_monic_normalization_entry (ab)
  5. L30
    specialize prime_field_polynomial_monic_normalization_entry (ac)
  6. L31
    specialize prime_field_polynomial_monic_normalization_entry (bb)
  7. L32
    specialize prime_field_polynomial_monic_normalization_entry (bc)
  8. L33
    specialize prime_field_polynomial_monic_normalization_entry (L)
  9. L34
    specialize prime_field_polynomial_monic_normalization_entry (0)
  10. L35
    specialize prime_field_polynomial_monic_normalization_entry (x)
08Use earlier factsL36–41

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

  1. L36
    specialize prime_field_polynomial_monic_normalization_entry (x1)
  2. L37
    apply prime_field_polynomial_monic_normalization_entry
  3. L38
    exact h
  4. L39
    exact hzero
  5. L40
    exact hc_right_left_witness_left
  6. L41
    exact hr_witness
09Establish huL42–48

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

  1. L42
    have hu : FpMul(p,k,x,1)Definitions: FpMul
  2. L43
    specialize prime_field_multiply_commutative (p)
  3. L44
    specialize prime_field_multiply_commutative (x)
  4. L45
    specialize prime_field_multiply_commutative (k)
  5. L46
    specialize prime_field_multiply_commutative (1)
  6. L47
    apply prime_field_multiply_commutative
  7. L48
    exact hc_right_left_witness_right_right
10Establish heL49–58

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

  1. L49
    have he : x1=1
  2. L50
    specialize prime_field_multiply_functional (p)
  3. L51
    specialize prime_field_multiply_functional (k)
  4. L52
    specialize prime_field_multiply_functional (x)
  5. L53
    specialize prime_field_multiply_functional (x1)
  6. L54
    specialize prime_field_multiply_functional (1)
  7. L55
    apply prime_field_multiply_functional
  8. L56
    exact hm
  9. L57
    exact hu
  10. L58
    rewrite he at hr_witness
11Calculate and transport equalitiesL59–59

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

  1. L59
    rewrite he at hr_witness
12Use earlier factsL60–60

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

  1. L60
    exact hr_witness

Library-wide reading audit

Original exact command ledger · 60 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro L
  8. 0008intro h
  9. 0009have hc : ((~((L) = 0)) /\ (((exists pfm_leading_normalization_leading_copy. ((((exists ff_h_pfp_normalization_leading_copysource. ff_h_pfp_normalization_leading_copysource + S (pfm_leading_normalization_leading_copy) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_leading_copysource. ab = ff_q_pfp_normalization_leading_copysource * S ((S (0)) * ac) + (pfm_leading_normalization_leading_copy))) /\ ((((~((pfm_leading_normalization_leading_copy) = 0)) /\ ((((exists pfa_gap_normalization_leading_copyinversemultiplicationleft. pfa_gap_normalization_leading_copyinversemultiplicationleft + S (pfm_leading_normalization_leading_copy) = (p)) /\ (((exists pfa_gap_normalization_leading_copyinversemultiplicationright. pfa_gap_normalization_leading_copyinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_leading_copyinversemultiplicationresultbound. pfa_gap_normalization_leading_copyinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_leading_copyinversemultiplicationresultcongruence pfa_offset_right_normalization_leading_copyinversemultiplicationresultcongruence. ((pfm_leading_normalization_leading_copy) * (k)) + (p) * pfa_offset_left_normalization_leading_copyinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_leading_copyinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_leading_copyscalescalar. pfa_gap_normalization_leading_copyscalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_leading_copyscale. (exists pfa_gap_normalization_leading_copyscaleindex. pfa_gap_normalization_leading_copyscaleindex + S (pfp_index_normalization_leading_copyscale) = (L)) -> exists pfp_source_normalization_leading_copyscale pfp_value_normalization_leading_copyscale. ((((exists ff_h_pfp_normalization_leading_copyscalesource. ff_h_pfp_normalization_leading_copyscalesource + S (pfp_source_normalization_leading_copyscale) = S ((S (pfp_index_normalization_leading_copyscale)) * ac)) /\ exists ff_q_pfp_normalization_leading_copyscalesource. ab = ff_q_pfp_normalization_leading_copyscalesource * S ((S (pfp_index_normalization_leading_copyscale)) * ac) + (pfp_source_normalization_leading_copyscale))) /\ (((((exists ff_h_pfp_normalization_leading_copyscaletarget. ff_h_pfp_normalization_leading_copyscaletarget + S (pfp_value_normalization_leading_copyscale) = S ((S (pfp_index_normalization_leading_copyscale)) * bc)) /\ exists ff_q_pfp_normalization_leading_copyscaletarget. bb = ff_q_pfp_normalization_leading_copyscaletarget * S ((S (pfp_index_normalization_leading_copyscale)) * bc) + (pfp_value_normalization_leading_copyscale))) /\ ((((exists pfa_gap_normalization_leading_copyscaleoperationleft. pfa_gap_normalization_leading_copyscaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_leading_copyscaleoperationright. pfa_gap_normalization_leading_copyscaleoperationright + S (pfp_source_normalization_leading_copyscale) = (p)) /\ ((((exists pfa_gap_normalization_leading_copyscaleoperationresultbound. pfa_gap_normalization_leading_copyscaleoperationresultbound + S (pfp_value_normalization_leading_copyscale) = (p)) /\ ((exists pfa_offset_left_normalization_leading_copyscaleoperationresultcongruence pfa_offset_right_normalization_leading_copyscaleoperationresultcongruence. ((k) * (pfp_source_normalization_leading_copyscale)) + (p) * pfa_offset_left_normalization_leading_copyscaleoperationresultcongruence = (pfp_value_normalization_leading_copyscale) + (p) * pfa_offset_right_normalization_leading_copyscaleoperationresultcongruence)))))))))))))))))))))
  10. 0010exact h
  11. 0011cases hc
  12. 0012cases hc_right
  13. 0013cases hc_right_left
  14. 0014cases hc_right_left_witness
  15. 0015cases hc_right_left_witness_right
  16. 0016have hzero : exists pfa_gap_normalization_leading_index. pfa_gap_normalization_leading_index + S (0) = (L)
  17. 0017specialize one_le_of_ne_zero (L)
  18. 0018apply one_le_of_ne_zero
  19. 0019exact hc_left
  20. 0020have hr : exists r. (((exists ff_h_pfp_normalization_leading_decoding. ff_h_pfp_normalization_leading_decoding + S (r) = S ((S (0)) * bc)) /\ exists ff_q_pfp_normalization_leading_decoding. bb = ff_q_pfp_normalization_leading_decoding * S ((S (0)) * bc) + (r)))
  21. 0021specialize beta_at_exists (bb)
  22. 0022specialize beta_at_exists (bc)
  23. 0023specialize beta_at_exists (0)
  24. 0024apply beta_at_exists
  25. 0025cases hr
  26. 0026have hm : ((exists pfa_gap_normalization_leading_scaledleft. pfa_gap_normalization_leading_scaledleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_leading_scaledright. pfa_gap_normalization_leading_scaledright + S (x) = (p)) /\ ((((exists pfa_gap_normalization_leading_scaledresultbound. pfa_gap_normalization_leading_scaledresultbound + S (x1) = (p)) /\ ((exists pfa_offset_left_normalization_leading_scaledresultcongruence pfa_offset_right_normalization_leading_scaledresultcongruence. ((k) * (x)) + (p) * pfa_offset_left_normalization_leading_scaledresultcongruence = (x1) + (p) * pfa_offset_right_normalization_leading_scaledresultcongruence))))))))
  27. 0027specialize prime_field_polynomial_monic_normalization_entry (p)
  28. 0028specialize prime_field_polynomial_monic_normalization_entry (k)
  29. 0029specialize prime_field_polynomial_monic_normalization_entry (ab)
  30. 0030specialize prime_field_polynomial_monic_normalization_entry (ac)
  31. 0031specialize prime_field_polynomial_monic_normalization_entry (bb)
  32. 0032specialize prime_field_polynomial_monic_normalization_entry (bc)
  33. 0033specialize prime_field_polynomial_monic_normalization_entry (L)
  34. 0034specialize prime_field_polynomial_monic_normalization_entry (0)
  35. 0035specialize prime_field_polynomial_monic_normalization_entry (x)
  36. 0036specialize prime_field_polynomial_monic_normalization_entry (x1)
  37. 0037apply prime_field_polynomial_monic_normalization_entry
  38. 0038exact h
  39. 0039exact hzero
  40. 0040exact hc_right_left_witness_left
  41. 0041exact hr_witness
  42. 0042have hu : ((exists pfa_gap_normalization_leading_unitleft. pfa_gap_normalization_leading_unitleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_leading_unitright. pfa_gap_normalization_leading_unitright + S (x) = (p)) /\ ((((exists pfa_gap_normalization_leading_unitresultbound. pfa_gap_normalization_leading_unitresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_leading_unitresultcongruence pfa_offset_right_normalization_leading_unitresultcongruence. ((k) * (x)) + (p) * pfa_offset_left_normalization_leading_unitresultcongruence = (1) + (p) * pfa_offset_right_normalization_leading_unitresultcongruence))))))))
  43. 0043specialize prime_field_multiply_commutative (p)
  44. 0044specialize prime_field_multiply_commutative (x)
  45. 0045specialize prime_field_multiply_commutative (k)
  46. 0046specialize prime_field_multiply_commutative (1)
  47. 0047apply prime_field_multiply_commutative
  48. 0048exact hc_right_left_witness_right_right
  49. 0049have he : x1=1
  50. 0050specialize prime_field_multiply_functional (p)
  51. 0051specialize prime_field_multiply_functional (k)
  52. 0052specialize prime_field_multiply_functional (x)
  53. 0053specialize prime_field_multiply_functional (x1)
  54. 0054specialize prime_field_multiply_functional (1)
  55. 0055apply prime_field_multiply_functional
  56. 0056exact hm
  57. 0057exact hu
  58. 0058rewrite he at hr_witness
  59. 0059rewrite he at hr_witness
  60. 0060exact hr_witness