PG006F

prime_field_polynomial_product_equivalent_nonzero_left_nonempty

An actual product formally equal to a nonzero-leading representation cannot have an empty left factor. No degree is assigned to empty factors.

Alpha v34 checked-use · first admitted v34 · 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 products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ p. ∀ qb. ∀ qc. ∀ Q. ∀ db. ∀ dc. ∀ D. ∀ pb. ∀ pc. ∀ P. ∀ ab. ∀ ac. ∀ L. ∀ a. FpRepresentedDegree(p,ab,ac,L,a) → FpPolyProduct(p,qb,qc,Q,db,dc,D,pb,pc,P) → PolynomialEquivalent(pb,pc,P,ab,ac,L) → ¬Q = 0

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

Definition DAG

PolynomialProductLength(L,M,N) · 1FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 1FpRepresentedDegree(p,b,c,L,d) · 1PolynomialEquivalent(b,c,L,d,e,M) · 2Lt(a,b) · 1

Actual proof prerequisites

prime_field_polynomial_nonzero_leading_equivalent_length_boundprime_field_polynomial_equivalent_symmetric · checked external prerequisitesucc_ne_zero · checked external prerequisitele_zero · checked external prerequisite
Original expanded first-order statement 
forall p qb qc Q db dc D pb pc P ab ac L a. ((((L)=S (a)) /\ (((forall fom_index_pfp_nonempty_targetcoefficients. (exists fom_gap_pfp_nonempty_targetcoefficients_index_bound. fom_gap_pfp_nonempty_targetcoefficients_index_bound + S (fom_index_pfp_nonempty_targetcoefficients) = L) -> exists fom_value_pfp_nonempty_targetcoefficients. ((((exists fom_beta_height_pfp_nonempty_targetcoefficients_entry. fom_beta_height_pfp_nonempty_targetcoefficients_entry + S (fom_value_pfp_nonempty_targetcoefficients) = S ((S (fom_index_pfp_nonempty_targetcoefficients)) * ac)) /\ exists fom_beta_quotient_pfp_nonempty_targetcoefficients_entry. ab = fom_beta_quotient_pfp_nonempty_targetcoefficients_entry * S ((S (fom_index_pfp_nonempty_targetcoefficients)) * ac) + (fom_value_pfp_nonempty_targetcoefficients))) /\ (exists fom_gap_pfp_nonempty_targetcoefficients_value_bound. fom_gap_pfp_nonempty_targetcoefficients_value_bound + S (fom_value_pfp_nonempty_targetcoefficients) = p))) /\ ((exists pfd_leading_nonempty_target. ((((exists ff_h_pfp_nonempty_targetentry. ff_h_pfp_nonempty_targetentry + S (pfd_leading_nonempty_target) = S ((S (0)) * ac)) /\ exists ff_q_pfp_nonempty_targetentry. ab = ff_q_pfp_nonempty_targetentry * S ((S (0)) * ac) + (pfd_leading_nonempty_target))) /\ ((~(pfd_leading_nonempty_target=0)))))))))) -> (((forall fom_index_pfp_nonempty_productleft. (exists fom_gap_pfp_nonempty_productleft_index_bound. fom_gap_pfp_nonempty_productleft_index_bound + S (fom_index_pfp_nonempty_productleft) = Q) -> exists fom_value_pfp_nonempty_productleft. ((((exists fom_beta_height_pfp_nonempty_productleft_entry. fom_beta_height_pfp_nonempty_productleft_entry + S (fom_value_pfp_nonempty_productleft) = S ((S (fom_index_pfp_nonempty_productleft)) * qc)) /\ exists fom_beta_quotient_pfp_nonempty_productleft_entry. qb = fom_beta_quotient_pfp_nonempty_productleft_entry * S ((S (fom_index_pfp_nonempty_productleft)) * qc) + (fom_value_pfp_nonempty_productleft))) /\ (exists fom_gap_pfp_nonempty_productleft_value_bound. fom_gap_pfp_nonempty_productleft_value_bound + S (fom_value_pfp_nonempty_productleft) = p))) /\ (((forall fom_index_pfp_nonempty_productright. (exists fom_gap_pfp_nonempty_productright_index_bound. fom_gap_pfp_nonempty_productright_index_bound + S (fom_index_pfp_nonempty_productright) = D) -> exists fom_value_pfp_nonempty_productright. ((((exists fom_beta_height_pfp_nonempty_productright_entry. fom_beta_height_pfp_nonempty_productright_entry + S (fom_value_pfp_nonempty_productright) = S ((S (fom_index_pfp_nonempty_productright)) * dc)) /\ exists fom_beta_quotient_pfp_nonempty_productright_entry. db = fom_beta_quotient_pfp_nonempty_productright_entry * S ((S (fom_index_pfp_nonempty_productright)) * dc) + (fom_value_pfp_nonempty_productright))) /\ (exists fom_gap_pfp_nonempty_productright_value_bound. fom_gap_pfp_nonempty_productright_value_bound + S (fom_value_pfp_nonempty_productright) = p))) /\ (((((((Q)=0 \/ (D)=0) /\ (((P)=0)))) \/ (((~((Q)=0)) /\ (((~((D)=0)) /\ (((Q)+(D)=S (P)))))))) /\ ((forall pfc_index_nonempty_productcoefficients. (exists pfa_gap_nonempty_productcoefficientsbound. pfa_gap_nonempty_productcoefficientsbound + S (pfc_index_nonempty_productcoefficients) = (P)) -> exists pfc_value_nonempty_productcoefficients. ((((exists ff_h_pfp_nonempty_productcoefficientsentry. ff_h_pfp_nonempty_productcoefficientsentry + S (pfc_value_nonempty_productcoefficients) = S ((S (pfc_index_nonempty_productcoefficients)) * pc)) /\ exists ff_q_pfp_nonempty_productcoefficientsentry. pb = ff_q_pfp_nonempty_productcoefficientsentry * S ((S (pfc_index_nonempty_productcoefficients)) * pc) + (pfc_value_nonempty_productcoefficients))) /\ ((exists pfc_terms_code_nonempty_productcoefficientscoefficient pfc_terms_scale_nonempty_productcoefficientscoefficient pfc_natural_sum_nonempty_productcoefficientscoefficient. ((forall pfc_index_nonempty_productcoefficientscoefficientdiagonal. (exists pfa_gap_nonempty_productcoefficientscoefficientdiagonalbound. pfa_gap_nonempty_productcoefficientscoefficientdiagonalbound + S (pfc_index_nonempty_productcoefficientscoefficientdiagonal) = (S (pfc_index_nonempty_productcoefficients))) -> exists pfc_value_nonempty_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_nonempty_productcoefficientscoefficientdiagonalentry. ff_h_pfp_nonempty_productcoefficientscoefficientdiagonalentry + S (pfc_value_nonempty_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_nonempty_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_productcoefficientscoefficient)) /\ exists ff_q_pfp_nonempty_productcoefficientscoefficientdiagonalentry. pfc_terms_code_nonempty_productcoefficientscoefficient = ff_q_pfp_nonempty_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_nonempty_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_productcoefficientscoefficient) + (pfc_value_nonempty_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_nonempty_productcoefficientscoefficientdiagonalterm pfc_left_nonempty_productcoefficientscoefficientdiagonalterm pfc_right_nonempty_productcoefficientscoefficientdiagonalterm. (((pfc_index_nonempty_productcoefficientscoefficientdiagonal)+pfc_complement_nonempty_productcoefficientscoefficientdiagonalterm=(pfc_index_nonempty_productcoefficients)) /\ ((((((exists pfa_gap_nonempty_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_nonempty_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_nonempty_productcoefficientscoefficientdiagonal) = (Q)) /\ ((((exists ff_h_pfp_nonempty_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_nonempty_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_nonempty_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_nonempty_productcoefficientscoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_nonempty_productcoefficientscoefficientdiagonaltermleftentry. qb = ff_q_pfp_nonempty_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_nonempty_productcoefficientscoefficientdiagonal)) * qc) + (pfc_left_nonempty_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_nonempty_productcoefficientscoefficientdiagonaltermleftoutside+(Q)=(pfc_index_nonempty_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_nonempty_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_nonempty_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_nonempty_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_nonempty_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_nonempty_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_nonempty_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_nonempty_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_nonempty_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_nonempty_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_nonempty_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_nonempty_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_nonempty_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_nonempty_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_nonempty_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_nonempty_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_nonempty_productcoefficientscoefficientdiagonal)=pfc_left_nonempty_productcoefficientscoefficientdiagonalterm*pfc_right_nonempty_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_nonempty_productcoefficientscoefficientsum fs_v_pfc_nonempty_productcoefficientscoefficientsum. ((((exists fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_start. fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_nonempty_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_start. fs_u_pfc_nonempty_productcoefficientscoefficientsum = fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_nonempty_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_nonempty_productcoefficientscoefficient) = S ((S (S (pfc_index_nonempty_productcoefficients))) * fs_v_pfc_nonempty_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_nonempty_productcoefficientscoefficientsum = fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_nonempty_productcoefficients))) * fs_v_pfc_nonempty_productcoefficientscoefficientsum) + (pfc_natural_sum_nonempty_productcoefficientscoefficient))) /\ forall fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_nonempty_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_nonempty_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps = S (pfc_index_nonempty_productcoefficients)) -> exists fs_a_pfc_nonempty_productcoefficientscoefficientsum_body_steps fs_r_pfc_nonempty_productcoefficientscoefficientsum_body_steps fs_s_pfc_nonempty_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_nonempty_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_productcoefficientscoefficient)) /\ exists fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_nonempty_productcoefficientscoefficient = fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_productcoefficientscoefficient) + (fs_a_pfc_nonempty_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_nonempty_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_nonempty_productcoefficientscoefficientsum = fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_productcoefficientscoefficientsum) + (fs_r_pfc_nonempty_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_nonempty_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_nonempty_productcoefficientscoefficientsum = fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_productcoefficientscoefficientsum) + (fs_s_pfc_nonempty_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_nonempty_productcoefficientscoefficientsum_body_steps = fs_r_pfc_nonempty_productcoefficientscoefficientsum_body_steps + fs_a_pfc_nonempty_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_nonempty_productcoefficientscoefficientresiduebound. pfa_gap_nonempty_productcoefficientscoefficientresiduebound + S (pfc_value_nonempty_productcoefficients) = (p)) /\ ((exists pfa_offset_left_nonempty_productcoefficientscoefficientresiduecongruence pfa_offset_right_nonempty_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_nonempty_productcoefficientscoefficient) + (p) * pfa_offset_left_nonempty_productcoefficientscoefficientresiduecongruence = (pfc_value_nonempty_productcoefficients) + (p) * pfa_offset_right_nonempty_productcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_nonempty_target_equivalent pfrep_left_nonempty_target_equivalent pfrep_right_nonempty_target_equivalent. ((exists pfrep_position_nonempty_target_equivalentfirst. ((pfrep_position_nonempty_target_equivalentfirst+S (pfrep_power_nonempty_target_equivalent)=(P)) /\ ((((exists ff_h_pfp_nonempty_target_equivalentfirstentry. ff_h_pfp_nonempty_target_equivalentfirstentry + S (pfrep_left_nonempty_target_equivalent) = S ((S (pfrep_position_nonempty_target_equivalentfirst)) * pc)) /\ exists ff_q_pfp_nonempty_target_equivalentfirstentry. pb = ff_q_pfp_nonempty_target_equivalentfirstentry * S ((S (pfrep_position_nonempty_target_equivalentfirst)) * pc) + (pfrep_left_nonempty_target_equivalent)))))) \/ (((exists pfrep_gap_nonempty_target_equivalentfirstoutside. pfrep_gap_nonempty_target_equivalentfirstoutside+(P)=(pfrep_power_nonempty_target_equivalent)) /\ (((pfrep_left_nonempty_target_equivalent)=0))))) -> ((exists pfrep_position_nonempty_target_equivalentsecond. ((pfrep_position_nonempty_target_equivalentsecond+S (pfrep_power_nonempty_target_equivalent)=(L)) /\ ((((exists ff_h_pfp_nonempty_target_equivalentsecondentry. ff_h_pfp_nonempty_target_equivalentsecondentry + S (pfrep_right_nonempty_target_equivalent) = S ((S (pfrep_position_nonempty_target_equivalentsecond)) * ac)) /\ exists ff_q_pfp_nonempty_target_equivalentsecondentry. ab = ff_q_pfp_nonempty_target_equivalentsecondentry * S ((S (pfrep_position_nonempty_target_equivalentsecond)) * ac) + (pfrep_right_nonempty_target_equivalent)))))) \/ (((exists pfrep_gap_nonempty_target_equivalentsecondoutside. pfrep_gap_nonempty_target_equivalentsecondoutside+(L)=(pfrep_power_nonempty_target_equivalent)) /\ (((pfrep_right_nonempty_target_equivalent)=0))))) -> pfrep_left_nonempty_target_equivalent=pfrep_right_nonempty_target_equivalent) -> (~(Q=0))

Complete tactic proof in conservative notation

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

64 script commands · 15 reading checkpoints · 4 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 (1)
prime field polynomial nonzero leading equivalent length bound
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro qb
  3. L3
    intro qc
  4. L4
    intro Q
  5. L5
    intro db
  6. L6
    intro dc
  7. L7
    intro D
  8. L8
    intro pb
  9. L9
    intro pc
  10. L10
    intro P
02Fix variables and assumptionsL11–18

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

  1. L11
    intro ab
  2. L12
    intro ac
  3. L13
    intro L
  4. L14
    intro a
  5. L15
    intro ha
  6. L16
    intro hc
  7. L17
    intro he
  8. L18
    intro hz
03Establish hlengthL19–19

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

  1. L19
    have hlength : PolynomialProductLength(Q,D,P)Definitions: PolynomialProductLength(Q,D,P)Original native command in the exact edition
04Separate the logical casesL20–22

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

  1. L20
    cases hc
  2. L21
    cases hc_right
  3. L22
    cases hc_right_right
05Use earlier factsL23–23

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

  1. L23
    exact hc_right_right_left
06Separate the logical casesL24–27

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

  1. L24
    cases ha
  2. L25
    cases ha_right
  3. L26
    cases ha_right_right
  4. L27
    cases ha_right_right_witness
07Establish hboundL28–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial nonzero leading equivalent length bound.

  1. L28
    have hbound : Lt(a,P)Definitions: Lt(a,P)Original native command in the exact edition
  2. L29
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (ab)
  3. L30
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (ac)
  4. L31
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (a)
  5. L32
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (pb)
  6. L33
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (pc)
  7. L34
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (P)
  8. L35
    specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (x)
  9. L36
    apply prime_field_polynomial_nonzero_leading_equivalent_length_bound
  10. L37
    exact ha_right_right_witness_left
08Use earlier factsL38–38

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

  1. L38
    exact ha_right_right_witness_right
09Establish hsameL39–48

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

  1. L39
    have hsame : PolynomialEquivalent(ab,ac,L,pb,pc,P)Definitions: PolynomialEquivalent(ab,ac,L,pb,pc,P)Original native command in the exact edition
  2. L40
    specialize prime_field_polynomial_equivalent_symmetric (pb)
  3. L41
    specialize prime_field_polynomial_equivalent_symmetric (pc)
  4. L42
    specialize prime_field_polynomial_equivalent_symmetric (P)
  5. L43
    specialize prime_field_polynomial_equivalent_symmetric (ab)
  6. L44
    specialize prime_field_polynomial_equivalent_symmetric (ac)
  7. L45
    specialize prime_field_polynomial_equivalent_symmetric (L)
  8. L46
    apply prime_field_polynomial_equivalent_symmetric
  9. L47
    exact he
  10. L48
    rewrite ha_left at hsame
10Calculate and transport equalitiesL49–49

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

  1. L49
    rewrite ha_left at hsame
11Use earlier factsL50–50

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

  1. L50
    exact hsame
12Separate the logical casesL51–52

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

  1. L51
    cases hlength
  2. L52
    cases hlength_left
13Establish hzeroL53–60

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

  1. L53
    have hzero : S a=0
  2. L54
    specialize le_zero (S a)
  3. L55
    apply le_zero
  4. L56
    rewrite <- hlength_left_right
  5. L57
    exact hbound
  6. L58
    specialize succ_ne_zero (a)
  7. L59
    apply succ_ne_zero
  8. L60
    exact hzero
14Separate the logical casesL61–62

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

  1. L61
    cases hlength_right
  2. L62
    cases hlength_right_right
15Use earlier factsL63–64

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

  1. L63
    apply hlength_right_left
  2. L64
    exact hz

Library-wide reading audit

Original defined command ledger · 64 lines
  1. 0001intro p
  2. 0002intro qb
  3. 0003intro qc
  4. 0004intro Q
  5. 0005intro db
  6. 0006intro dc
  7. 0007intro D
  8. 0008intro pb
  9. 0009intro pc
  10. 0010intro P
  11. 0011intro ab
  12. 0012intro ac
  13. 0013intro L
  14. 0014intro a
  15. 0015intro ha
  16. 0016intro hc
  17. 0017intro he
  18. 0018intro hz
  19. 0019have hlength : PolynomialProductLength(Q,D,P)
  20. 0020cases hc
  21. 0021cases hc_right
  22. 0022cases hc_right_right
  23. 0023exact hc_right_right_left
  24. 0024cases ha
  25. 0025cases ha_right
  26. 0026cases ha_right_right
  27. 0027cases ha_right_right_witness
  28. 0028have hbound : Lt(a,P)
  29. 0029specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (ab)
  30. 0030specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (ac)
  31. 0031specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (a)
  32. 0032specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (pb)
  33. 0033specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (pc)
  34. 0034specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (P)
  35. 0035specialize prime_field_polynomial_nonzero_leading_equivalent_length_bound (x)
  36. 0036apply prime_field_polynomial_nonzero_leading_equivalent_length_bound
  37. 0037exact ha_right_right_witness_left
  38. 0038exact ha_right_right_witness_right
  39. 0039have hsame : PolynomialEquivalent(ab,ac,L,pb,pc,P)
  40. 0040specialize prime_field_polynomial_equivalent_symmetric (pb)
  41. 0041specialize prime_field_polynomial_equivalent_symmetric (pc)
  42. 0042specialize prime_field_polynomial_equivalent_symmetric (P)
  43. 0043specialize prime_field_polynomial_equivalent_symmetric (ab)
  44. 0044specialize prime_field_polynomial_equivalent_symmetric (ac)
  45. 0045specialize prime_field_polynomial_equivalent_symmetric (L)
  46. 0046apply prime_field_polynomial_equivalent_symmetric
  47. 0047exact he
  48. 0048rewrite ha_left at hsame
  49. 0049rewrite ha_left at hsame
  50. 0050exact hsame
  51. 0051cases hlength
  52. 0052cases hlength_left
  53. 0053have hzero : S a=0
  54. 0054specialize le_zero (S a)
  55. 0055apply le_zero
  56. 0056rewrite <- hlength_left_right
  57. 0057exact hbound
  58. 0058specialize succ_ne_zero (a)
  59. 0059apply succ_ne_zero
  60. 0060exact hzero
  61. 0061cases hlength_right
  62. 0062cases hlength_right_right
  63. 0063apply hlength_right_left
  64. 0064exact hz