PQ0040

prime_field_polynomial_monic_normalization_transport

Reencode both actual coefficient prefixes while retaining the same genuine leading inverse and scale relation.

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. ∀ AB. ∀ AC. ∀ BB. ∀ BC. ∀ L. (∀ x. ∀ y. Lt(x,L) → BetaAt(ab,ac,x,y) → BetaAt(AB,AC,x,y)) → (∀ x. ∀ y. Lt(x,L) → BetaAt(bb,bc,x,y) → BetaAt(BB,BC,x,y)) → FpMonicNormalization(p,k,ab,ac,bb,bc,L) → FpMonicNormalization(p,k,AB,AC,BB,BC,L)

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

Definition DAG

FpMonicNormalization(p,k,ab,ac,bb,bc,L) · 2Lt(a,b) · 2BetaAt(b,c,i,x) · 4

Actual proof prerequisites

one_le_of_ne_zero · checked external prerequisiteprime_field_polynomial_scale_transport · checked external prerequisite
Original expanded first-order statement 
forall p k ab ac bb bc AB AC BB BC L. (forall mdr_i_pfp_normalization_recode_input mdr_a_pfp_normalization_recode_input. (exists mdr_gap_pfp_normalization_recode_inputb. mdr_gap_pfp_normalization_recode_inputb + S (mdr_i_pfp_normalization_recode_input) = (L)) -> (((exists ff_h_mdr_pfp_normalization_recode_inputo. ff_h_mdr_pfp_normalization_recode_inputo + S (mdr_a_pfp_normalization_recode_input) = S ((S (mdr_i_pfp_normalization_recode_input)) * ac)) /\ exists ff_q_mdr_pfp_normalization_recode_inputo. ab = ff_q_mdr_pfp_normalization_recode_inputo * S ((S (mdr_i_pfp_normalization_recode_input)) * ac) + (mdr_a_pfp_normalization_recode_input))) -> (((exists ff_h_mdr_pfp_normalization_recode_inputn. ff_h_mdr_pfp_normalization_recode_inputn + S (mdr_a_pfp_normalization_recode_input) = S ((S (mdr_i_pfp_normalization_recode_input)) * AC)) /\ exists ff_q_mdr_pfp_normalization_recode_inputn. AB = ff_q_mdr_pfp_normalization_recode_inputn * S ((S (mdr_i_pfp_normalization_recode_input)) * AC) + (mdr_a_pfp_normalization_recode_input)))) -> (forall mdr_i_pfp_normalization_recode_output mdr_a_pfp_normalization_recode_output. (exists mdr_gap_pfp_normalization_recode_outputb. mdr_gap_pfp_normalization_recode_outputb + S (mdr_i_pfp_normalization_recode_output) = (L)) -> (((exists ff_h_mdr_pfp_normalization_recode_outputo. ff_h_mdr_pfp_normalization_recode_outputo + S (mdr_a_pfp_normalization_recode_output) = S ((S (mdr_i_pfp_normalization_recode_output)) * bc)) /\ exists ff_q_mdr_pfp_normalization_recode_outputo. bb = ff_q_mdr_pfp_normalization_recode_outputo * S ((S (mdr_i_pfp_normalization_recode_output)) * bc) + (mdr_a_pfp_normalization_recode_output))) -> (((exists ff_h_mdr_pfp_normalization_recode_outputn. ff_h_mdr_pfp_normalization_recode_outputn + S (mdr_a_pfp_normalization_recode_output) = S ((S (mdr_i_pfp_normalization_recode_output)) * BC)) /\ exists ff_q_mdr_pfp_normalization_recode_outputn. BB = ff_q_mdr_pfp_normalization_recode_outputn * S ((S (mdr_i_pfp_normalization_recode_output)) * BC) + (mdr_a_pfp_normalization_recode_output)))) -> (((~((L) = 0)) /\ (((exists pfm_leading_normalization_recode_old. ((((exists ff_h_pfp_normalization_recode_oldsource. ff_h_pfp_normalization_recode_oldsource + S (pfm_leading_normalization_recode_old) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_recode_oldsource. ab = ff_q_pfp_normalization_recode_oldsource * S ((S (0)) * ac) + (pfm_leading_normalization_recode_old))) /\ ((((~((pfm_leading_normalization_recode_old) = 0)) /\ ((((exists pfa_gap_normalization_recode_oldinversemultiplicationleft. pfa_gap_normalization_recode_oldinversemultiplicationleft + S (pfm_leading_normalization_recode_old) = (p)) /\ (((exists pfa_gap_normalization_recode_oldinversemultiplicationright. pfa_gap_normalization_recode_oldinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_recode_oldinversemultiplicationresultbound. pfa_gap_normalization_recode_oldinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_recode_oldinversemultiplicationresultcongruence pfa_offset_right_normalization_recode_oldinversemultiplicationresultcongruence. ((pfm_leading_normalization_recode_old) * (k)) + (p) * pfa_offset_left_normalization_recode_oldinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_recode_oldinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_recode_oldscalescalar. pfa_gap_normalization_recode_oldscalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_recode_oldscale. (exists pfa_gap_normalization_recode_oldscaleindex. pfa_gap_normalization_recode_oldscaleindex + S (pfp_index_normalization_recode_oldscale) = (L)) -> exists pfp_source_normalization_recode_oldscale pfp_value_normalization_recode_oldscale. ((((exists ff_h_pfp_normalization_recode_oldscalesource. ff_h_pfp_normalization_recode_oldscalesource + S (pfp_source_normalization_recode_oldscale) = S ((S (pfp_index_normalization_recode_oldscale)) * ac)) /\ exists ff_q_pfp_normalization_recode_oldscalesource. ab = ff_q_pfp_normalization_recode_oldscalesource * S ((S (pfp_index_normalization_recode_oldscale)) * ac) + (pfp_source_normalization_recode_oldscale))) /\ (((((exists ff_h_pfp_normalization_recode_oldscaletarget. ff_h_pfp_normalization_recode_oldscaletarget + S (pfp_value_normalization_recode_oldscale) = S ((S (pfp_index_normalization_recode_oldscale)) * bc)) /\ exists ff_q_pfp_normalization_recode_oldscaletarget. bb = ff_q_pfp_normalization_recode_oldscaletarget * S ((S (pfp_index_normalization_recode_oldscale)) * bc) + (pfp_value_normalization_recode_oldscale))) /\ ((((exists pfa_gap_normalization_recode_oldscaleoperationleft. pfa_gap_normalization_recode_oldscaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_recode_oldscaleoperationright. pfa_gap_normalization_recode_oldscaleoperationright + S (pfp_source_normalization_recode_oldscale) = (p)) /\ ((((exists pfa_gap_normalization_recode_oldscaleoperationresultbound. pfa_gap_normalization_recode_oldscaleoperationresultbound + S (pfp_value_normalization_recode_oldscale) = (p)) /\ ((exists pfa_offset_left_normalization_recode_oldscaleoperationresultcongruence pfa_offset_right_normalization_recode_oldscaleoperationresultcongruence. ((k) * (pfp_source_normalization_recode_oldscale)) + (p) * pfa_offset_left_normalization_recode_oldscaleoperationresultcongruence = (pfp_value_normalization_recode_oldscale) + (p) * pfa_offset_right_normalization_recode_oldscaleoperationresultcongruence)))))))))))))))))))))) -> (((~((L) = 0)) /\ (((exists pfm_leading_normalization_recode_new. ((((exists ff_h_pfp_normalization_recode_newsource. ff_h_pfp_normalization_recode_newsource + S (pfm_leading_normalization_recode_new) = S ((S (0)) * AC)) /\ exists ff_q_pfp_normalization_recode_newsource. AB = ff_q_pfp_normalization_recode_newsource * S ((S (0)) * AC) + (pfm_leading_normalization_recode_new))) /\ ((((~((pfm_leading_normalization_recode_new) = 0)) /\ ((((exists pfa_gap_normalization_recode_newinversemultiplicationleft. pfa_gap_normalization_recode_newinversemultiplicationleft + S (pfm_leading_normalization_recode_new) = (p)) /\ (((exists pfa_gap_normalization_recode_newinversemultiplicationright. pfa_gap_normalization_recode_newinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_recode_newinversemultiplicationresultbound. pfa_gap_normalization_recode_newinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_recode_newinversemultiplicationresultcongruence pfa_offset_right_normalization_recode_newinversemultiplicationresultcongruence. ((pfm_leading_normalization_recode_new) * (k)) + (p) * pfa_offset_left_normalization_recode_newinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_recode_newinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_recode_newscalescalar. pfa_gap_normalization_recode_newscalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_recode_newscale. (exists pfa_gap_normalization_recode_newscaleindex. pfa_gap_normalization_recode_newscaleindex + S (pfp_index_normalization_recode_newscale) = (L)) -> exists pfp_source_normalization_recode_newscale pfp_value_normalization_recode_newscale. ((((exists ff_h_pfp_normalization_recode_newscalesource. ff_h_pfp_normalization_recode_newscalesource + S (pfp_source_normalization_recode_newscale) = S ((S (pfp_index_normalization_recode_newscale)) * AC)) /\ exists ff_q_pfp_normalization_recode_newscalesource. AB = ff_q_pfp_normalization_recode_newscalesource * S ((S (pfp_index_normalization_recode_newscale)) * AC) + (pfp_source_normalization_recode_newscale))) /\ (((((exists ff_h_pfp_normalization_recode_newscaletarget. ff_h_pfp_normalization_recode_newscaletarget + S (pfp_value_normalization_recode_newscale) = S ((S (pfp_index_normalization_recode_newscale)) * BC)) /\ exists ff_q_pfp_normalization_recode_newscaletarget. BB = ff_q_pfp_normalization_recode_newscaletarget * S ((S (pfp_index_normalization_recode_newscale)) * BC) + (pfp_value_normalization_recode_newscale))) /\ ((((exists pfa_gap_normalization_recode_newscaleoperationleft. pfa_gap_normalization_recode_newscaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_recode_newscaleoperationright. pfa_gap_normalization_recode_newscaleoperationright + S (pfp_source_normalization_recode_newscale) = (p)) /\ ((((exists pfa_gap_normalization_recode_newscaleoperationresultbound. pfa_gap_normalization_recode_newscaleoperationresultbound + S (pfp_value_normalization_recode_newscale) = (p)) /\ ((exists pfa_offset_left_normalization_recode_newscaleoperationresultcongruence pfa_offset_right_normalization_recode_newscaleoperationresultcongruence. ((k) * (pfp_source_normalization_recode_newscale)) + (p) * pfa_offset_left_normalization_recode_newscaleoperationresultcongruence = (pfp_value_normalization_recode_newscale) + (p) * pfa_offset_right_normalization_recode_newscaleoperationresultcongruence))))))))))))))))))))))

Complete tactic proof in conservative notation

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

46 script commands · 10 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–10

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 AB
  8. L8
    intro AC
  9. L9
    intro BB
  10. L10
    intro BC
02Fix variables and assumptionsL11–14

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro L
  2. L12
    intro hin
  3. L13
    intro hout
  4. L14
    intro h
03Separate the logical casesL15–17

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

  1. L15
    cases h
  2. L16
    cases h_right
  3. L17
    split
04Use earlier factsL18–18

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

  1. L18
    exact h_left
05Separate the logical casesL19–21

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

  1. L19
    split
  2. L20
    cases h_right_left
  3. L21
    cases h_right_left_witness
06Construct an explicit witnessL22–22

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

  1. L22
    exists x
07Separate the logical casesL23–23

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

  1. L23
    split
08Use earlier factsL24–33

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

  1. L24
    specialize hin (0)
  2. L25
    specialize hin (x)
  3. L26
    apply hin
  4. L27
    specialize one_le_of_ne_zero (L)
  5. L28
    apply one_le_of_ne_zero
  6. L29
    exact h_left
  7. L30
    exact h_right_left_witness_left
  8. L31
    exact h_right_left_witness_right
  9. L32
    specialize prime_field_polynomial_scale_transport (p)
  10. L33
    specialize prime_field_polynomial_scale_transport (k)
09Use earlier factsL34–43

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

  1. L34
    specialize prime_field_polynomial_scale_transport (ab)
  2. L35
    specialize prime_field_polynomial_scale_transport (ac)
  3. L36
    specialize prime_field_polynomial_scale_transport (bb)
  4. L37
    specialize prime_field_polynomial_scale_transport (bc)
  5. L38
    specialize prime_field_polynomial_scale_transport (AB)
  6. L39
    specialize prime_field_polynomial_scale_transport (AC)
  7. L40
    specialize prime_field_polynomial_scale_transport (BB)
  8. L41
    specialize prime_field_polynomial_scale_transport (BC)
  9. L42
    specialize prime_field_polynomial_scale_transport (L)
  10. L43
    apply prime_field_polynomial_scale_transport
10Use earlier factsL44–46

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

  1. L44
    exact hin
  2. L45
    exact hout
  3. L46
    exact h_right_right

Library-wide reading audit

Original defined command ledger · 46 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro AB
  8. 0008intro AC
  9. 0009intro BB
  10. 0010intro BC
  11. 0011intro L
  12. 0012intro hin
  13. 0013intro hout
  14. 0014intro h
  15. 0015cases h
  16. 0016cases h_right
  17. 0017split
  18. 0018exact h_left
  19. 0019split
  20. 0020cases h_right_left
  21. 0021cases h_right_left_witness
  22. 0022exists x
  23. 0023split
  24. 0024specialize hin (0)
  25. 0025specialize hin (x)
  26. 0026apply hin
  27. 0027specialize one_le_of_ne_zero (L)
  28. 0028apply one_le_of_ne_zero
  29. 0029exact h_left
  30. 0030exact h_right_left_witness_left
  31. 0031exact h_right_left_witness_right
  32. 0032specialize prime_field_polynomial_scale_transport (p)
  33. 0033specialize prime_field_polynomial_scale_transport (k)
  34. 0034specialize prime_field_polynomial_scale_transport (ab)
  35. 0035specialize prime_field_polynomial_scale_transport (ac)
  36. 0036specialize prime_field_polynomial_scale_transport (bb)
  37. 0037specialize prime_field_polynomial_scale_transport (bc)
  38. 0038specialize prime_field_polynomial_scale_transport (AB)
  39. 0039specialize prime_field_polynomial_scale_transport (AC)
  40. 0040specialize prime_field_polynomial_scale_transport (BB)
  41. 0041specialize prime_field_polynomial_scale_transport (BC)
  42. 0042specialize prime_field_polynomial_scale_transport (L)
  43. 0043apply prime_field_polynomial_scale_transport
  44. 0044exact hin
  45. 0045exact hout
  46. 0046exact h_right_right