PQ003A

prime_field_polynomial_monic_normalization_monic

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

Alpha v34 checked-use · first admitted v32 · 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.

All coefficients retain the established highest-degree-first order. Trimming handles empty and all-zero prefixes; monic normalization requires a nonzero leading coefficient. Synthetic division has a nonempty input of length S n and a quotient of length n, unique in decoded values. Its coefficient recurrence, actual evaluation remainder and positive-degree drop are checked. General polynomial Euclidean division, gcd/Bezout, an arbitrary-convolution factor theorem, irreducible-polynomial existence and the full G091 prime-power-field endpoint remain open. These exact theorems are first admitted to Alpha v32; Stable remains unchanged.

Exact theorem in conservative defined notation

∀ p. ∀ k. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ L. FpMonicNormalization(p,k,ab,ac,bb,bc,L) → FpMonic(p,bb,bc,L)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 2FpMonic(p,b,c,L) · 1FpMonicNormalization(p,k,ab,ac,bb,bc,L) · 2Lt(a,b) · 1

Actual proof prerequisites

prime_field_polynomial_monic_normalization_boundedprime_field_polynomial_monic_normalization_leading
Original expanded first-order 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))))))))

Complete tactic proof in conservative notation

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

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.

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 monic normalization boundedprime field polynomial monic normalization leading
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(p,k,ab,ac,bb,bc,L)Original native command in the exact edition
  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: Lt(k,p)BetaPrefixInto(ab,ac,L,p)BetaPrefixInto(bb,bc,L,p)Original native command in the exact edition
  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 defined 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 : FpMonicNormalization(p,k,ab,ac,bb,bc,L)
  10. 0010exact h
  11. 0011cases hc
  12. 0012cases hc_right
  13. 0013split
  14. 0014exact hc_left
  15. 0015split
  16. 0016have hb : Lt(k,p) ∧ (BetaPrefixInto(ab,ac,L,p) ∧ BetaPrefixInto(bb,bc,L,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