PQ0043

prime_field_polynomial_monic_normalization_exists_unique

Construct a monic normalization of the same represented degree, with unique inverse scalar and unique decoded coefficient prefix.

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. ∀ ab. ∀ ac. ∀ L. ∀ d. Prime(p) → FpRepresentedDegree(p,ab,ac,L,d) → ∃ x. ∃ y. ∃ z. FpMonicNormalization(p,x,ab,ac,y,z,L) ∧ (FpMonic(p,y,z,L) ∧ (FpRepresentedDegree(p,y,z,L,d) ∧ (∀ n. ∀ m. ∀ k. FpMonicNormalization(p,n,ab,ac,m,k,L) → n = x ∧ (∀ i. ∀ j. Lt(i,L) → BetaAt(m,k,i,j) → BetaAt(y,z,i,j)))))

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

Definition DAG

FpRepresentedDegree(p,b,c,L,d) · 2FpMonic(p,b,c,L) · 1FpMonicNormalization(p,k,ab,ac,bb,bc,L) · 3Lt(a,b) · 1Prime(p) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

prime_field_polynomial_monic_normalization_existsprime_field_polynomial_monic_normalization_monicprime_field_polynomial_monic_normalization_represented_degreeprime_field_polynomial_monic_normalization_scalar_functionalprime_field_polynomial_monic_normalization_functional
Original expanded first-order statement 
forall p ab ac L d. (~((p) = 1) /\ forall pfa_factor_left_normalization_unique_prime pfa_factor_right_normalization_unique_prime. (p) = pfa_factor_left_normalization_unique_prime * pfa_factor_right_normalization_unique_prime -> pfa_factor_left_normalization_unique_prime = 1 \/ pfa_factor_right_normalization_unique_prime = 1) -> ((((L)=S (d)) /\ (((forall fom_index_pfp_normalization_unique_inputcoefficients. (exists fom_gap_pfp_normalization_unique_inputcoefficients_index_bound. fom_gap_pfp_normalization_unique_inputcoefficients_index_bound + S (fom_index_pfp_normalization_unique_inputcoefficients) = L) -> exists fom_value_pfp_normalization_unique_inputcoefficients. ((((exists fom_beta_height_pfp_normalization_unique_inputcoefficients_entry. fom_beta_height_pfp_normalization_unique_inputcoefficients_entry + S (fom_value_pfp_normalization_unique_inputcoefficients) = S ((S (fom_index_pfp_normalization_unique_inputcoefficients)) * ac)) /\ exists fom_beta_quotient_pfp_normalization_unique_inputcoefficients_entry. ab = fom_beta_quotient_pfp_normalization_unique_inputcoefficients_entry * S ((S (fom_index_pfp_normalization_unique_inputcoefficients)) * ac) + (fom_value_pfp_normalization_unique_inputcoefficients))) /\ (exists fom_gap_pfp_normalization_unique_inputcoefficients_value_bound. fom_gap_pfp_normalization_unique_inputcoefficients_value_bound + S (fom_value_pfp_normalization_unique_inputcoefficients) = p))) /\ ((exists pfd_leading_normalization_unique_input. ((((exists ff_h_pfp_normalization_unique_inputentry. ff_h_pfp_normalization_unique_inputentry + S (pfd_leading_normalization_unique_input) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_unique_inputentry. ab = ff_q_pfp_normalization_unique_inputentry * S ((S (0)) * ac) + (pfd_leading_normalization_unique_input))) /\ ((~(pfd_leading_normalization_unique_input=0)))))))))) -> exists k bb bc. (((((~((L) = 0)) /\ (((exists pfm_leading_normalization_unique_graph. ((((exists ff_h_pfp_normalization_unique_graphsource. ff_h_pfp_normalization_unique_graphsource + S (pfm_leading_normalization_unique_graph) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_unique_graphsource. ab = ff_q_pfp_normalization_unique_graphsource * S ((S (0)) * ac) + (pfm_leading_normalization_unique_graph))) /\ ((((~((pfm_leading_normalization_unique_graph) = 0)) /\ ((((exists pfa_gap_normalization_unique_graphinversemultiplicationleft. pfa_gap_normalization_unique_graphinversemultiplicationleft + S (pfm_leading_normalization_unique_graph) = (p)) /\ (((exists pfa_gap_normalization_unique_graphinversemultiplicationright. pfa_gap_normalization_unique_graphinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_unique_graphinversemultiplicationresultbound. pfa_gap_normalization_unique_graphinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_unique_graphinversemultiplicationresultcongruence pfa_offset_right_normalization_unique_graphinversemultiplicationresultcongruence. ((pfm_leading_normalization_unique_graph) * (k)) + (p) * pfa_offset_left_normalization_unique_graphinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_unique_graphinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_unique_graphscalescalar. pfa_gap_normalization_unique_graphscalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_unique_graphscale. (exists pfa_gap_normalization_unique_graphscaleindex. pfa_gap_normalization_unique_graphscaleindex + S (pfp_index_normalization_unique_graphscale) = (L)) -> exists pfp_source_normalization_unique_graphscale pfp_value_normalization_unique_graphscale. ((((exists ff_h_pfp_normalization_unique_graphscalesource. ff_h_pfp_normalization_unique_graphscalesource + S (pfp_source_normalization_unique_graphscale) = S ((S (pfp_index_normalization_unique_graphscale)) * ac)) /\ exists ff_q_pfp_normalization_unique_graphscalesource. ab = ff_q_pfp_normalization_unique_graphscalesource * S ((S (pfp_index_normalization_unique_graphscale)) * ac) + (pfp_source_normalization_unique_graphscale))) /\ (((((exists ff_h_pfp_normalization_unique_graphscaletarget. ff_h_pfp_normalization_unique_graphscaletarget + S (pfp_value_normalization_unique_graphscale) = S ((S (pfp_index_normalization_unique_graphscale)) * bc)) /\ exists ff_q_pfp_normalization_unique_graphscaletarget. bb = ff_q_pfp_normalization_unique_graphscaletarget * S ((S (pfp_index_normalization_unique_graphscale)) * bc) + (pfp_value_normalization_unique_graphscale))) /\ ((((exists pfa_gap_normalization_unique_graphscaleoperationleft. pfa_gap_normalization_unique_graphscaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_unique_graphscaleoperationright. pfa_gap_normalization_unique_graphscaleoperationright + S (pfp_source_normalization_unique_graphscale) = (p)) /\ ((((exists pfa_gap_normalization_unique_graphscaleoperationresultbound. pfa_gap_normalization_unique_graphscaleoperationresultbound + S (pfp_value_normalization_unique_graphscale) = (p)) /\ ((exists pfa_offset_left_normalization_unique_graphscaleoperationresultcongruence pfa_offset_right_normalization_unique_graphscaleoperationresultcongruence. ((k) * (pfp_source_normalization_unique_graphscale)) + (p) * pfa_offset_left_normalization_unique_graphscaleoperationresultcongruence = (pfp_value_normalization_unique_graphscale) + (p) * pfa_offset_right_normalization_unique_graphscaleoperationresultcongruence)))))))))))))))))))))) /\ (((((~((L) = 0)) /\ (((forall fom_index_pfp_normalization_unique_moniccoefficients. (exists fom_gap_pfp_normalization_unique_moniccoefficients_index_bound. fom_gap_pfp_normalization_unique_moniccoefficients_index_bound + S (fom_index_pfp_normalization_unique_moniccoefficients) = L) -> exists fom_value_pfp_normalization_unique_moniccoefficients. ((((exists fom_beta_height_pfp_normalization_unique_moniccoefficients_entry. fom_beta_height_pfp_normalization_unique_moniccoefficients_entry + S (fom_value_pfp_normalization_unique_moniccoefficients) = S ((S (fom_index_pfp_normalization_unique_moniccoefficients)) * bc)) /\ exists fom_beta_quotient_pfp_normalization_unique_moniccoefficients_entry. bb = fom_beta_quotient_pfp_normalization_unique_moniccoefficients_entry * S ((S (fom_index_pfp_normalization_unique_moniccoefficients)) * bc) + (fom_value_pfp_normalization_unique_moniccoefficients))) /\ (exists fom_gap_pfp_normalization_unique_moniccoefficients_value_bound. fom_gap_pfp_normalization_unique_moniccoefficients_value_bound + S (fom_value_pfp_normalization_unique_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_normalization_unique_monicleading. ff_h_pfp_normalization_unique_monicleading + S (1) = S ((S (0)) * bc)) /\ exists ff_q_pfp_normalization_unique_monicleading. bb = ff_q_pfp_normalization_unique_monicleading * S ((S (0)) * bc) + (1)))))))) /\ ((((((L)=S (d)) /\ (((forall fom_index_pfp_normalization_unique_degreecoefficients. (exists fom_gap_pfp_normalization_unique_degreecoefficients_index_bound. fom_gap_pfp_normalization_unique_degreecoefficients_index_bound + S (fom_index_pfp_normalization_unique_degreecoefficients) = L) -> exists fom_value_pfp_normalization_unique_degreecoefficients. ((((exists fom_beta_height_pfp_normalization_unique_degreecoefficients_entry. fom_beta_height_pfp_normalization_unique_degreecoefficients_entry + S (fom_value_pfp_normalization_unique_degreecoefficients) = S ((S (fom_index_pfp_normalization_unique_degreecoefficients)) * bc)) /\ exists fom_beta_quotient_pfp_normalization_unique_degreecoefficients_entry. bb = fom_beta_quotient_pfp_normalization_unique_degreecoefficients_entry * S ((S (fom_index_pfp_normalization_unique_degreecoefficients)) * bc) + (fom_value_pfp_normalization_unique_degreecoefficients))) /\ (exists fom_gap_pfp_normalization_unique_degreecoefficients_value_bound. fom_gap_pfp_normalization_unique_degreecoefficients_value_bound + S (fom_value_pfp_normalization_unique_degreecoefficients) = p))) /\ ((exists pfd_leading_normalization_unique_degree. ((((exists ff_h_pfp_normalization_unique_degreeentry. ff_h_pfp_normalization_unique_degreeentry + S (pfd_leading_normalization_unique_degree) = S ((S (0)) * bc)) /\ exists ff_q_pfp_normalization_unique_degreeentry. bb = ff_q_pfp_normalization_unique_degreeentry * S ((S (0)) * bc) + (pfd_leading_normalization_unique_degree))) /\ ((~(pfd_leading_normalization_unique_degree=0)))))))))) /\ ((forall j cb cc. (((~((L) = 0)) /\ (((exists pfm_leading_normalization_uniquecomparison. ((((exists ff_h_pfp_normalization_uniquecomparisonsource. ff_h_pfp_normalization_uniquecomparisonsource + S (pfm_leading_normalization_uniquecomparison) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_uniquecomparisonsource. ab = ff_q_pfp_normalization_uniquecomparisonsource * S ((S (0)) * ac) + (pfm_leading_normalization_uniquecomparison))) /\ ((((~((pfm_leading_normalization_uniquecomparison) = 0)) /\ ((((exists pfa_gap_normalization_uniquecomparisoninversemultiplicationleft. pfa_gap_normalization_uniquecomparisoninversemultiplicationleft + S (pfm_leading_normalization_uniquecomparison) = (p)) /\ (((exists pfa_gap_normalization_uniquecomparisoninversemultiplicationright. pfa_gap_normalization_uniquecomparisoninversemultiplicationright + S (j) = (p)) /\ ((((exists pfa_gap_normalization_uniquecomparisoninversemultiplicationresultbound. pfa_gap_normalization_uniquecomparisoninversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_uniquecomparisoninversemultiplicationresultcongruence pfa_offset_right_normalization_uniquecomparisoninversemultiplicationresultcongruence. ((pfm_leading_normalization_uniquecomparison) * (j)) + (p) * pfa_offset_left_normalization_uniquecomparisoninversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_uniquecomparisoninversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_uniquecomparisonscalescalar. pfa_gap_normalization_uniquecomparisonscalescalar + S (j) = (p)) /\ ((forall pfp_index_normalization_uniquecomparisonscale. (exists pfa_gap_normalization_uniquecomparisonscaleindex. pfa_gap_normalization_uniquecomparisonscaleindex + S (pfp_index_normalization_uniquecomparisonscale) = (L)) -> exists pfp_source_normalization_uniquecomparisonscale pfp_value_normalization_uniquecomparisonscale. ((((exists ff_h_pfp_normalization_uniquecomparisonscalesource. ff_h_pfp_normalization_uniquecomparisonscalesource + S (pfp_source_normalization_uniquecomparisonscale) = S ((S (pfp_index_normalization_uniquecomparisonscale)) * ac)) /\ exists ff_q_pfp_normalization_uniquecomparisonscalesource. ab = ff_q_pfp_normalization_uniquecomparisonscalesource * S ((S (pfp_index_normalization_uniquecomparisonscale)) * ac) + (pfp_source_normalization_uniquecomparisonscale))) /\ (((((exists ff_h_pfp_normalization_uniquecomparisonscaletarget. ff_h_pfp_normalization_uniquecomparisonscaletarget + S (pfp_value_normalization_uniquecomparisonscale) = S ((S (pfp_index_normalization_uniquecomparisonscale)) * cc)) /\ exists ff_q_pfp_normalization_uniquecomparisonscaletarget. cb = ff_q_pfp_normalization_uniquecomparisonscaletarget * S ((S (pfp_index_normalization_uniquecomparisonscale)) * cc) + (pfp_value_normalization_uniquecomparisonscale))) /\ ((((exists pfa_gap_normalization_uniquecomparisonscaleoperationleft. pfa_gap_normalization_uniquecomparisonscaleoperationleft + S (j) = (p)) /\ (((exists pfa_gap_normalization_uniquecomparisonscaleoperationright. pfa_gap_normalization_uniquecomparisonscaleoperationright + S (pfp_source_normalization_uniquecomparisonscale) = (p)) /\ ((((exists pfa_gap_normalization_uniquecomparisonscaleoperationresultbound. pfa_gap_normalization_uniquecomparisonscaleoperationresultbound + S (pfp_value_normalization_uniquecomparisonscale) = (p)) /\ ((exists pfa_offset_left_normalization_uniquecomparisonscaleoperationresultcongruence pfa_offset_right_normalization_uniquecomparisonscaleoperationresultcongruence. ((j) * (pfp_source_normalization_uniquecomparisonscale)) + (p) * pfa_offset_left_normalization_uniquecomparisonscaleoperationresultcongruence = (pfp_value_normalization_uniquecomparisonscale) + (p) * pfa_offset_right_normalization_uniquecomparisonscaleoperationresultcongruence)))))))))))))))))))))) -> ((j=(k)) /\ ((forall mdr_i_pfp_normalization_uniqueequal mdr_a_pfp_normalization_uniqueequal. (exists mdr_gap_pfp_normalization_uniqueequalb. mdr_gap_pfp_normalization_uniqueequalb + S (mdr_i_pfp_normalization_uniqueequal) = (L)) -> (((exists ff_h_mdr_pfp_normalization_uniqueequalo. ff_h_mdr_pfp_normalization_uniqueequalo + S (mdr_a_pfp_normalization_uniqueequal) = S ((S (mdr_i_pfp_normalization_uniqueequal)) * cc)) /\ exists ff_q_mdr_pfp_normalization_uniqueequalo. cb = ff_q_mdr_pfp_normalization_uniqueequalo * S ((S (mdr_i_pfp_normalization_uniqueequal)) * cc) + (mdr_a_pfp_normalization_uniqueequal))) -> (((exists ff_h_mdr_pfp_normalization_uniqueequaln. ff_h_mdr_pfp_normalization_uniqueequaln + S (mdr_a_pfp_normalization_uniqueequal) = S ((S (mdr_i_pfp_normalization_uniqueequal)) * bc)) /\ exists ff_q_mdr_pfp_normalization_uniqueequaln. bb = ff_q_mdr_pfp_normalization_uniqueequaln * S ((S (mdr_i_pfp_normalization_uniqueequal)) * bc) + (mdr_a_pfp_normalization_uniqueequal))))))))))))))

Complete tactic proof in conservative notation

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

77 script commands · 16 reading checkpoints · 1 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 (5)
prime field polynomial monic normalization existsprime field polynomial monic normalization monicprime field polynomial monic normalization represented degreeprime field polynomial monic normalization scalar functionalprime field polynomial monic normalization functional
01Fix variables and assumptionsL1–7

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

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro d
  6. L6
    intro hp
  7. L7
    intro hd
02Establish hL8–16

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

  1. L8
    have h : ∃ k. ∃ bb. ∃ bc. 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. L9
    specialize prime_field_polynomial_monic_normalization_exists (p)
  3. L10
    specialize prime_field_polynomial_monic_normalization_exists (ab)
  4. L11
    specialize prime_field_polynomial_monic_normalization_exists (ac)
  5. L12
    specialize prime_field_polynomial_monic_normalization_exists (L)
  6. L13
    specialize prime_field_polynomial_monic_normalization_exists (d)
  7. L14
    apply prime_field_polynomial_monic_normalization_exists
  8. L15
    exact hp
  9. L16
    exact hd
03Separate the logical casesL17–19

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

  1. L17
    cases h
  2. L18
    cases h_witness
  3. L19
    cases h_witness_witness
04Construct an explicit witnessL20–22

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

  1. L20
    exists x
  2. L21
    exists x1
  3. L22
    exists x2
05Separate the logical casesL23–23

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

  1. L23
    split
06Use earlier factsL24–24

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

  1. L24
    exact h_witness_witness_witness
07Separate the logical casesL25–25

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

  1. L25
    split
08Use earlier factsL26–34

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

  1. L26
    specialize prime_field_polynomial_monic_normalization_monic (p)
  2. L27
    specialize prime_field_polynomial_monic_normalization_monic (x)
  3. L28
    specialize prime_field_polynomial_monic_normalization_monic (ab)
  4. L29
    specialize prime_field_polynomial_monic_normalization_monic (ac)
  5. L30
    specialize prime_field_polynomial_monic_normalization_monic (x1)
  6. L31
    specialize prime_field_polynomial_monic_normalization_monic (x2)
  7. L32
    specialize prime_field_polynomial_monic_normalization_monic (L)
  8. L33
    apply prime_field_polynomial_monic_normalization_monic
  9. L34
    exact h_witness_witness_witness
09Separate the logical casesL35–35

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

  1. L35
    split
10Use earlier factsL36–45

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

  1. L36
    specialize prime_field_polynomial_monic_normalization_represented_degree (p)
  2. L37
    specialize prime_field_polynomial_monic_normalization_represented_degree (x)
  3. L38
    specialize prime_field_polynomial_monic_normalization_represented_degree (ab)
  4. L39
    specialize prime_field_polynomial_monic_normalization_represented_degree (ac)
  5. L40
    specialize prime_field_polynomial_monic_normalization_represented_degree (x1)
  6. L41
    specialize prime_field_polynomial_monic_normalization_represented_degree (x2)
  7. L42
    specialize prime_field_polynomial_monic_normalization_represented_degree (L)
  8. L43
    specialize prime_field_polynomial_monic_normalization_represented_degree (d)
  9. L44
    apply prime_field_polynomial_monic_normalization_represented_degree
  10. L45
    exact hd
11Use earlier factsL46–46

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

  1. L46
    exact h_witness_witness_witness
12Fix variables and assumptionsL47–50

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

  1. L47
    intro j
  2. L48
    intro cb
  3. L49
    intro cc
  4. L50
    intro hj
13Separate the logical casesL51–51

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

  1. L51
    split
14Use earlier factsL52–61

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

  1. L52
    specialize prime_field_polynomial_monic_normalization_scalar_functional (p)
  2. L53
    specialize prime_field_polynomial_monic_normalization_scalar_functional (j)
  3. L54
    specialize prime_field_polynomial_monic_normalization_scalar_functional (x)
  4. L55
    specialize prime_field_polynomial_monic_normalization_scalar_functional (ab)
  5. L56
    specialize prime_field_polynomial_monic_normalization_scalar_functional (ac)
  6. L57
    specialize prime_field_polynomial_monic_normalization_scalar_functional (cb)
  7. L58
    specialize prime_field_polynomial_monic_normalization_scalar_functional (cc)
  8. L59
    specialize prime_field_polynomial_monic_normalization_scalar_functional (x1)
  9. L60
    specialize prime_field_polynomial_monic_normalization_scalar_functional (x2)
  10. L61
    specialize prime_field_polynomial_monic_normalization_scalar_functional (L)
15Use earlier factsL62–71

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

  1. L62
    apply prime_field_polynomial_monic_normalization_scalar_functional
  2. L63
    exact hj
  3. L64
    exact h_witness_witness_witness
  4. L65
    specialize prime_field_polynomial_monic_normalization_functional (p)
  5. L66
    specialize prime_field_polynomial_monic_normalization_functional (j)
  6. L67
    specialize prime_field_polynomial_monic_normalization_functional (x)
  7. L68
    specialize prime_field_polynomial_monic_normalization_functional (ab)
  8. L69
    specialize prime_field_polynomial_monic_normalization_functional (ac)
  9. L70
    specialize prime_field_polynomial_monic_normalization_functional (cb)
  10. L71
    specialize prime_field_polynomial_monic_normalization_functional (cc)
16Use earlier factsL72–77

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

  1. L72
    specialize prime_field_polynomial_monic_normalization_functional (x1)
  2. L73
    specialize prime_field_polynomial_monic_normalization_functional (x2)
  3. L74
    specialize prime_field_polynomial_monic_normalization_functional (L)
  4. L75
    apply prime_field_polynomial_monic_normalization_functional
  5. L76
    exact hj
  6. L77
    exact h_witness_witness_witness

Library-wide reading audit

Original defined command ledger · 77 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro d
  6. 0006intro hp
  7. 0007intro hd
  8. 0008have h : ∃ k. ∃ bb. ∃ bc. FpMonicNormalization(p,k,ab,ac,bb,bc,L)
  9. 0009specialize prime_field_polynomial_monic_normalization_exists (p)
  10. 0010specialize prime_field_polynomial_monic_normalization_exists (ab)
  11. 0011specialize prime_field_polynomial_monic_normalization_exists (ac)
  12. 0012specialize prime_field_polynomial_monic_normalization_exists (L)
  13. 0013specialize prime_field_polynomial_monic_normalization_exists (d)
  14. 0014apply prime_field_polynomial_monic_normalization_exists
  15. 0015exact hp
  16. 0016exact hd
  17. 0017cases h
  18. 0018cases h_witness
  19. 0019cases h_witness_witness
  20. 0020exists x
  21. 0021exists x1
  22. 0022exists x2
  23. 0023split
  24. 0024exact h_witness_witness_witness
  25. 0025split
  26. 0026specialize prime_field_polynomial_monic_normalization_monic (p)
  27. 0027specialize prime_field_polynomial_monic_normalization_monic (x)
  28. 0028specialize prime_field_polynomial_monic_normalization_monic (ab)
  29. 0029specialize prime_field_polynomial_monic_normalization_monic (ac)
  30. 0030specialize prime_field_polynomial_monic_normalization_monic (x1)
  31. 0031specialize prime_field_polynomial_monic_normalization_monic (x2)
  32. 0032specialize prime_field_polynomial_monic_normalization_monic (L)
  33. 0033apply prime_field_polynomial_monic_normalization_monic
  34. 0034exact h_witness_witness_witness
  35. 0035split
  36. 0036specialize prime_field_polynomial_monic_normalization_represented_degree (p)
  37. 0037specialize prime_field_polynomial_monic_normalization_represented_degree (x)
  38. 0038specialize prime_field_polynomial_monic_normalization_represented_degree (ab)
  39. 0039specialize prime_field_polynomial_monic_normalization_represented_degree (ac)
  40. 0040specialize prime_field_polynomial_monic_normalization_represented_degree (x1)
  41. 0041specialize prime_field_polynomial_monic_normalization_represented_degree (x2)
  42. 0042specialize prime_field_polynomial_monic_normalization_represented_degree (L)
  43. 0043specialize prime_field_polynomial_monic_normalization_represented_degree (d)
  44. 0044apply prime_field_polynomial_monic_normalization_represented_degree
  45. 0045exact hd
  46. 0046exact h_witness_witness_witness
  47. 0047intro j
  48. 0048intro cb
  49. 0049intro cc
  50. 0050intro hj
  51. 0051split
  52. 0052specialize prime_field_polynomial_monic_normalization_scalar_functional (p)
  53. 0053specialize prime_field_polynomial_monic_normalization_scalar_functional (j)
  54. 0054specialize prime_field_polynomial_monic_normalization_scalar_functional (x)
  55. 0055specialize prime_field_polynomial_monic_normalization_scalar_functional (ab)
  56. 0056specialize prime_field_polynomial_monic_normalization_scalar_functional (ac)
  57. 0057specialize prime_field_polynomial_monic_normalization_scalar_functional (cb)
  58. 0058specialize prime_field_polynomial_monic_normalization_scalar_functional (cc)
  59. 0059specialize prime_field_polynomial_monic_normalization_scalar_functional (x1)
  60. 0060specialize prime_field_polynomial_monic_normalization_scalar_functional (x2)
  61. 0061specialize prime_field_polynomial_monic_normalization_scalar_functional (L)
  62. 0062apply prime_field_polynomial_monic_normalization_scalar_functional
  63. 0063exact hj
  64. 0064exact h_witness_witness_witness
  65. 0065specialize prime_field_polynomial_monic_normalization_functional (p)
  66. 0066specialize prime_field_polynomial_monic_normalization_functional (j)
  67. 0067specialize prime_field_polynomial_monic_normalization_functional (x)
  68. 0068specialize prime_field_polynomial_monic_normalization_functional (ab)
  69. 0069specialize prime_field_polynomial_monic_normalization_functional (ac)
  70. 0070specialize prime_field_polynomial_monic_normalization_functional (cb)
  71. 0071specialize prime_field_polynomial_monic_normalization_functional (cc)
  72. 0072specialize prime_field_polynomial_monic_normalization_functional (x1)
  73. 0073specialize prime_field_polynomial_monic_normalization_functional (x2)
  74. 0074specialize prime_field_polynomial_monic_normalization_functional (L)
  75. 0075apply prime_field_polynomial_monic_normalization_functional
  76. 0076exact hj
  77. 0077exact h_witness_witness_witness