PQ003A

prime_field_polynomial_monic_normalization_monic

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

Normalization yields a nonempty canonical monic prefix; all three properties are proved.

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_monic_source. ((((exists ff_h_pfp_normalization_monic_sourcesource. ff_h_pfp_normalization_monic_sourcesource + S (pfm_leading_normalization_monic_source) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_monic_sourcesource. ab = ff_q_pfp_normalization_monic_sourcesource * S ((S (0)) * ac) + (pfm_leading_normalization_monic_source))) /\ ((((~((pfm_leading_normalization_monic_source) = 0)) /\ ((((exists pfa_gap_normalization_monic_sourceinversemultiplicationleft. pfa_gap_normalization_monic_sourceinversemultiplicationleft + S (pfm_leading_normalization_monic_source) = (p)) /\ (((exists pfa_gap_normalization_monic_sourceinversemultiplicationright. pfa_gap_normalization_monic_sourceinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_monic_sourceinversemultiplicationresultbound. pfa_gap_normalization_monic_sourceinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_monic_sourceinversemultiplicationresultcongruence pfa_offset_right_normalization_monic_sourceinversemultiplicationresultcongruence. ((pfm_leading_normalization_monic_source) * (k)) + (p) * pfa_offset_left_normalization_monic_sourceinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_monic_sourceinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_monic_sourcescalescalar. pfa_gap_normalization_monic_sourcescalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_monic_sourcescale. (exists pfa_gap_normalization_monic_sourcescaleindex. pfa_gap_normalization_monic_sourcescaleindex + S (pfp_index_normalization_monic_sourcescale) = (L)) -> exists pfp_source_normalization_monic_sourcescale pfp_value_normalization_monic_sourcescale. ((((exists ff_h_pfp_normalization_monic_sourcescalesource. ff_h_pfp_normalization_monic_sourcescalesource + S (pfp_source_normalization_monic_sourcescale) = S ((S (pfp_index_normalization_monic_sourcescale)) * ac)) /\ exists ff_q_pfp_normalization_monic_sourcescalesource. ab = ff_q_pfp_normalization_monic_sourcescalesource * S ((S (pfp_index_normalization_monic_sourcescale)) * ac) + (pfp_source_normalization_monic_sourcescale))) /\ (((((exists ff_h_pfp_normalization_monic_sourcescaletarget. ff_h_pfp_normalization_monic_sourcescaletarget + S (pfp_value_normalization_monic_sourcescale) = S ((S (pfp_index_normalization_monic_sourcescale)) * bc)) /\ exists ff_q_pfp_normalization_monic_sourcescaletarget. bb = ff_q_pfp_normalization_monic_sourcescaletarget * S ((S (pfp_index_normalization_monic_sourcescale)) * bc) + (pfp_value_normalization_monic_sourcescale))) /\ ((((exists pfa_gap_normalization_monic_sourcescaleoperationleft. pfa_gap_normalization_monic_sourcescaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_monic_sourcescaleoperationright. pfa_gap_normalization_monic_sourcescaleoperationright + S (pfp_source_normalization_monic_sourcescale) = (p)) /\ ((((exists pfa_gap_normalization_monic_sourcescaleoperationresultbound. pfa_gap_normalization_monic_sourcescaleoperationresultbound + S (pfp_value_normalization_monic_sourcescale) = (p)) /\ ((exists pfa_offset_left_normalization_monic_sourcescaleoperationresultcongruence pfa_offset_right_normalization_monic_sourcescaleoperationresultcongruence. ((k) * (pfp_source_normalization_monic_sourcescale)) + (p) * pfa_offset_left_normalization_monic_sourcescaleoperationresultcongruence = (pfp_value_normalization_monic_sourcescale) + (p) * pfa_offset_right_normalization_monic_sourcescaleoperationresultcongruence)))))))))))))))))))))) -> (((~((L) = 0)) /\ (((forall fom_index_pfp_normalization_monic_resultcoefficients. (exists fom_gap_pfp_normalization_monic_resultcoefficients_index_bound. fom_gap_pfp_normalization_monic_resultcoefficients_index_bound + S (fom_index_pfp_normalization_monic_resultcoefficients) = L) -> exists fom_value_pfp_normalization_monic_resultcoefficients. ((((exists fom_beta_height_pfp_normalization_monic_resultcoefficients_entry. fom_beta_height_pfp_normalization_monic_resultcoefficients_entry + S (fom_value_pfp_normalization_monic_resultcoefficients) = S ((S (fom_index_pfp_normalization_monic_resultcoefficients)) * bc)) /\ exists fom_beta_quotient_pfp_normalization_monic_resultcoefficients_entry. bb = fom_beta_quotient_pfp_normalization_monic_resultcoefficients_entry * S ((S (fom_index_pfp_normalization_monic_resultcoefficients)) * bc) + (fom_value_pfp_normalization_monic_resultcoefficients))) /\ (exists fom_gap_pfp_normalization_monic_resultcoefficients_value_bound. fom_gap_pfp_normalization_monic_resultcoefficients_value_bound + S (fom_value_pfp_normalization_monic_resultcoefficients) = p))) /\ ((((exists ff_h_pfp_normalization_monic_resultleading. ff_h_pfp_normalization_monic_resultleading + S (1) = S ((S (0)) * bc)) /\ exists ff_q_pfp_normalization_monic_resultleading. bb = ff_q_pfp_normalization_monic_resultleading * S ((S (0)) * bc) + (1))))))))

Constructive proof overview

Generated structural guide

Normalization yields a nonempty canonical monic prefix; all three properties are proved.

The unchanged tactic script uses 2 declared prerequisites and contains 37 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PQ0038 prime_field_polynomial_monic_normalization_bounded PQ0039 prime_field_polynomial_monic_normalization_leading

Direct dependents

PQ003B prime_field_polynomial_monic_normalization_represented_degree PQ0042 prime_field_polynomial_monic_normalization_constant PQ0043 prime_field_polynomial_monic_normalization_exists_unique

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

37 script commands · 8 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.

Named ingredients (2)
prime field polynomial monic normalization boundedprime field polynomial monic normalization leading

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–13

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

  1. L11
    cases hc
  2. L12
    cases hc_right
  3. L13
    split
04Use earlier factsL14–14

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

  1. L14
    exact hc_left
05Separate the logical casesL15–15

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

  1. L15
    split
06Establish hbL16–25

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

  1. L16
    have hb : Lt(k,p) ∧ (BetaPrefixInto(ab,ac,L,p) ∧ BetaPrefixInto(bb,bc,L,p))Definitions: BetaPrefixIntoLt
  2. L17
    specialize prime_field_polynomial_monic_normalization_bounded (p)
  3. L18
    specialize prime_field_polynomial_monic_normalization_bounded (k)
  4. L19
    specialize prime_field_polynomial_monic_normalization_bounded (ab)
  5. L20
    specialize prime_field_polynomial_monic_normalization_bounded (ac)
  6. L21
    specialize prime_field_polynomial_monic_normalization_bounded (bb)
  7. L22
    specialize prime_field_polynomial_monic_normalization_bounded (bc)
  8. L23
    specialize prime_field_polynomial_monic_normalization_bounded (L)
  9. L24
    apply prime_field_polynomial_monic_normalization_bounded
  10. L25
    exact h
07Separate the logical casesL26–27

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

  1. L26
    cases hb
  2. L27
    cases hb_right
08Use earlier factsL28–37

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

  1. L28
    exact hb_right_right
  2. L29
    specialize prime_field_polynomial_monic_normalization_leading (p)
  3. L30
    specialize prime_field_polynomial_monic_normalization_leading (k)
  4. L31
    specialize prime_field_polynomial_monic_normalization_leading (ab)
  5. L32
    specialize prime_field_polynomial_monic_normalization_leading (ac)
  6. L33
    specialize prime_field_polynomial_monic_normalization_leading (bb)
  7. L34
    specialize prime_field_polynomial_monic_normalization_leading (bc)
  8. L35
    specialize prime_field_polynomial_monic_normalization_leading (L)
  9. L36
    apply prime_field_polynomial_monic_normalization_leading
  10. L37
    exact h

Library-wide reading audit

Original exact command ledger · 37 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_monic_copy. ((((exists ff_h_pfp_normalization_monic_copysource. ff_h_pfp_normalization_monic_copysource + S (pfm_leading_normalization_monic_copy) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_monic_copysource. ab = ff_q_pfp_normalization_monic_copysource * S ((S (0)) * ac) + (pfm_leading_normalization_monic_copy))) /\ ((((~((pfm_leading_normalization_monic_copy) = 0)) /\ ((((exists pfa_gap_normalization_monic_copyinversemultiplicationleft. pfa_gap_normalization_monic_copyinversemultiplicationleft + S (pfm_leading_normalization_monic_copy) = (p)) /\ (((exists pfa_gap_normalization_monic_copyinversemultiplicationright. pfa_gap_normalization_monic_copyinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_monic_copyinversemultiplicationresultbound. pfa_gap_normalization_monic_copyinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_monic_copyinversemultiplicationresultcongruence pfa_offset_right_normalization_monic_copyinversemultiplicationresultcongruence. ((pfm_leading_normalization_monic_copy) * (k)) + (p) * pfa_offset_left_normalization_monic_copyinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_monic_copyinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_monic_copyscalescalar. pfa_gap_normalization_monic_copyscalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_monic_copyscale. (exists pfa_gap_normalization_monic_copyscaleindex. pfa_gap_normalization_monic_copyscaleindex + S (pfp_index_normalization_monic_copyscale) = (L)) -> exists pfp_source_normalization_monic_copyscale pfp_value_normalization_monic_copyscale. ((((exists ff_h_pfp_normalization_monic_copyscalesource. ff_h_pfp_normalization_monic_copyscalesource + S (pfp_source_normalization_monic_copyscale) = S ((S (pfp_index_normalization_monic_copyscale)) * ac)) /\ exists ff_q_pfp_normalization_monic_copyscalesource. ab = ff_q_pfp_normalization_monic_copyscalesource * S ((S (pfp_index_normalization_monic_copyscale)) * ac) + (pfp_source_normalization_monic_copyscale))) /\ (((((exists ff_h_pfp_normalization_monic_copyscaletarget. ff_h_pfp_normalization_monic_copyscaletarget + S (pfp_value_normalization_monic_copyscale) = S ((S (pfp_index_normalization_monic_copyscale)) * bc)) /\ exists ff_q_pfp_normalization_monic_copyscaletarget. bb = ff_q_pfp_normalization_monic_copyscaletarget * S ((S (pfp_index_normalization_monic_copyscale)) * bc) + (pfp_value_normalization_monic_copyscale))) /\ ((((exists pfa_gap_normalization_monic_copyscaleoperationleft. pfa_gap_normalization_monic_copyscaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_monic_copyscaleoperationright. pfa_gap_normalization_monic_copyscaleoperationright + S (pfp_source_normalization_monic_copyscale) = (p)) /\ ((((exists pfa_gap_normalization_monic_copyscaleoperationresultbound. pfa_gap_normalization_monic_copyscaleoperationresultbound + S (pfp_value_normalization_monic_copyscale) = (p)) /\ ((exists pfa_offset_left_normalization_monic_copyscaleoperationresultcongruence pfa_offset_right_normalization_monic_copyscaleoperationresultcongruence. ((k) * (pfp_source_normalization_monic_copyscale)) + (p) * pfa_offset_left_normalization_monic_copyscaleoperationresultcongruence = (pfp_value_normalization_monic_copyscale) + (p) * pfa_offset_right_normalization_monic_copyscaleoperationresultcongruence)))))))))))))))))))))
  10. 0010exact h
  11. 0011cases hc
  12. 0012cases hc_right
  13. 0013split
  14. 0014exact hc_left
  15. 0015split
  16. 0016have hb : ((exists pfa_gap_normalization_bound_scalar. pfa_gap_normalization_bound_scalar + S (k) = (p)) /\ (((forall fom_index_pfp_normalization_bound_input. (exists fom_gap_pfp_normalization_bound_input_index_bound. fom_gap_pfp_normalization_bound_input_index_bound + S (fom_index_pfp_normalization_bound_input) = L) -> exists fom_value_pfp_normalization_bound_input. ((((exists fom_beta_height_pfp_normalization_bound_input_entry. fom_beta_height_pfp_normalization_bound_input_entry + S (fom_value_pfp_normalization_bound_input) = S ((S (fom_index_pfp_normalization_bound_input)) * ac)) /\ exists fom_beta_quotient_pfp_normalization_bound_input_entry. ab = fom_beta_quotient_pfp_normalization_bound_input_entry * S ((S (fom_index_pfp_normalization_bound_input)) * ac) + (fom_value_pfp_normalization_bound_input))) /\ (exists fom_gap_pfp_normalization_bound_input_value_bound. fom_gap_pfp_normalization_bound_input_value_bound + S (fom_value_pfp_normalization_bound_input) = p))) /\ ((forall fom_index_pfp_normalization_bound_output. (exists fom_gap_pfp_normalization_bound_output_index_bound. fom_gap_pfp_normalization_bound_output_index_bound + S (fom_index_pfp_normalization_bound_output) = L) -> exists fom_value_pfp_normalization_bound_output. ((((exists fom_beta_height_pfp_normalization_bound_output_entry. fom_beta_height_pfp_normalization_bound_output_entry + S (fom_value_pfp_normalization_bound_output) = S ((S (fom_index_pfp_normalization_bound_output)) * bc)) /\ exists fom_beta_quotient_pfp_normalization_bound_output_entry. bb = fom_beta_quotient_pfp_normalization_bound_output_entry * S ((S (fom_index_pfp_normalization_bound_output)) * bc) + (fom_value_pfp_normalization_bound_output))) /\ (exists fom_gap_pfp_normalization_bound_output_value_bound. fom_gap_pfp_normalization_bound_output_value_bound + S (fom_value_pfp_normalization_bound_output) = p)))))))
  17. 0017specialize prime_field_polynomial_monic_normalization_bounded (p)
  18. 0018specialize prime_field_polynomial_monic_normalization_bounded (k)
  19. 0019specialize prime_field_polynomial_monic_normalization_bounded (ab)
  20. 0020specialize prime_field_polynomial_monic_normalization_bounded (ac)
  21. 0021specialize prime_field_polynomial_monic_normalization_bounded (bb)
  22. 0022specialize prime_field_polynomial_monic_normalization_bounded (bc)
  23. 0023specialize prime_field_polynomial_monic_normalization_bounded (L)
  24. 0024apply prime_field_polynomial_monic_normalization_bounded
  25. 0025exact h
  26. 0026cases hb
  27. 0027cases hb_right
  28. 0028exact hb_right_right
  29. 0029specialize prime_field_polynomial_monic_normalization_leading (p)
  30. 0030specialize prime_field_polynomial_monic_normalization_leading (k)
  31. 0031specialize prime_field_polynomial_monic_normalization_leading (ab)
  32. 0032specialize prime_field_polynomial_monic_normalization_leading (ac)
  33. 0033specialize prime_field_polynomial_monic_normalization_leading (bb)
  34. 0034specialize prime_field_polynomial_monic_normalization_leading (bc)
  35. 0035specialize prime_field_polynomial_monic_normalization_leading (L)
  36. 0036apply prime_field_polynomial_monic_normalization_leading
  37. 0037exact h