PG0075

prime_field_polynomial_empty_right_divisor_implies_equivalent_zero

An empty right divisor has only formally zero multiples, at any target representation length. The actual product length is zero; no zero-degree assertion or prime hypothesis is used.

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. ∀ db. ∀ dc. ∀ ab. ∀ ac. ∀ L. FpPolynomialRightDivides(p,db,dc,0,ab,ac,L) → PolynomialEquivalent(ab,ac,L,db,dc,0)

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

Definition DAG

PolynomialProductLength(L,M,N) · 1PolynomialEquivalent(b,c,L,d,e,M) · 2FpPolynomialRightDivides(p,db,dc,D,ab,ac,L) · 1

Actual proof prerequisites

prime_field_polynomial_equivalent_transitive · checked external prerequisiteprime_field_polynomial_equivalent_symmetric · checked external prerequisiteprime_field_polynomial_equal_implies_equivalent · checked external prerequisitelt_not_le · checked external prerequisitezero_le · checked external prerequisite
Original expanded first-order statement 
forall p db dc ab ac L. (((forall fom_index_pfp_empty_divisor_canonical. (exists fom_gap_pfp_empty_divisor_canonical_index_bound. fom_gap_pfp_empty_divisor_canonical_index_bound + S (fom_index_pfp_empty_divisor_canonical) = L) -> exists fom_value_pfp_empty_divisor_canonical. ((((exists fom_beta_height_pfp_empty_divisor_canonical_entry. fom_beta_height_pfp_empty_divisor_canonical_entry + S (fom_value_pfp_empty_divisor_canonical) = S ((S (fom_index_pfp_empty_divisor_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_empty_divisor_canonical_entry. ab = fom_beta_quotient_pfp_empty_divisor_canonical_entry * S ((S (fom_index_pfp_empty_divisor_canonical)) * ac) + (fom_value_pfp_empty_divisor_canonical))) /\ (exists fom_gap_pfp_empty_divisor_canonical_value_bound. fom_gap_pfp_empty_divisor_canonical_value_bound + S (fom_value_pfp_empty_divisor_canonical) = p))) /\ ((exists pfgu_qb_empty_divisor pfgu_qc_empty_divisor pfgu_Q_empty_divisor pfgu_pb_empty_divisor pfgu_pc_empty_divisor pfgu_P_empty_divisor. ((((forall fom_index_pfp_empty_divisor_productleft. (exists fom_gap_pfp_empty_divisor_productleft_index_bound. fom_gap_pfp_empty_divisor_productleft_index_bound + S (fom_index_pfp_empty_divisor_productleft) = pfgu_Q_empty_divisor) -> exists fom_value_pfp_empty_divisor_productleft. ((((exists fom_beta_height_pfp_empty_divisor_productleft_entry. fom_beta_height_pfp_empty_divisor_productleft_entry + S (fom_value_pfp_empty_divisor_productleft) = S ((S (fom_index_pfp_empty_divisor_productleft)) * pfgu_qc_empty_divisor)) /\ exists fom_beta_quotient_pfp_empty_divisor_productleft_entry. pfgu_qb_empty_divisor = fom_beta_quotient_pfp_empty_divisor_productleft_entry * S ((S (fom_index_pfp_empty_divisor_productleft)) * pfgu_qc_empty_divisor) + (fom_value_pfp_empty_divisor_productleft))) /\ (exists fom_gap_pfp_empty_divisor_productleft_value_bound. fom_gap_pfp_empty_divisor_productleft_value_bound + S (fom_value_pfp_empty_divisor_productleft) = p))) /\ (((forall fom_index_pfp_empty_divisor_productright. (exists fom_gap_pfp_empty_divisor_productright_index_bound. fom_gap_pfp_empty_divisor_productright_index_bound + S (fom_index_pfp_empty_divisor_productright) = 0) -> exists fom_value_pfp_empty_divisor_productright. ((((exists fom_beta_height_pfp_empty_divisor_productright_entry. fom_beta_height_pfp_empty_divisor_productright_entry + S (fom_value_pfp_empty_divisor_productright) = S ((S (fom_index_pfp_empty_divisor_productright)) * dc)) /\ exists fom_beta_quotient_pfp_empty_divisor_productright_entry. db = fom_beta_quotient_pfp_empty_divisor_productright_entry * S ((S (fom_index_pfp_empty_divisor_productright)) * dc) + (fom_value_pfp_empty_divisor_productright))) /\ (exists fom_gap_pfp_empty_divisor_productright_value_bound. fom_gap_pfp_empty_divisor_productright_value_bound + S (fom_value_pfp_empty_divisor_productright) = p))) /\ (((((((pfgu_Q_empty_divisor)=0 \/ (0)=0) /\ (((pfgu_P_empty_divisor)=0)))) \/ (((~((pfgu_Q_empty_divisor)=0)) /\ (((~((0)=0)) /\ (((pfgu_Q_empty_divisor)+(0)=S (pfgu_P_empty_divisor)))))))) /\ ((forall pfc_index_empty_divisor_productcoefficients. (exists pfa_gap_empty_divisor_productcoefficientsbound. pfa_gap_empty_divisor_productcoefficientsbound + S (pfc_index_empty_divisor_productcoefficients) = (pfgu_P_empty_divisor)) -> exists pfc_value_empty_divisor_productcoefficients. ((((exists ff_h_pfp_empty_divisor_productcoefficientsentry. ff_h_pfp_empty_divisor_productcoefficientsentry + S (pfc_value_empty_divisor_productcoefficients) = S ((S (pfc_index_empty_divisor_productcoefficients)) * pfgu_pc_empty_divisor)) /\ exists ff_q_pfp_empty_divisor_productcoefficientsentry. pfgu_pb_empty_divisor = ff_q_pfp_empty_divisor_productcoefficientsentry * S ((S (pfc_index_empty_divisor_productcoefficients)) * pfgu_pc_empty_divisor) + (pfc_value_empty_divisor_productcoefficients))) /\ ((exists pfc_terms_code_empty_divisor_productcoefficientscoefficient pfc_terms_scale_empty_divisor_productcoefficientscoefficient pfc_natural_sum_empty_divisor_productcoefficientscoefficient. ((forall pfc_index_empty_divisor_productcoefficientscoefficientdiagonal. (exists pfa_gap_empty_divisor_productcoefficientscoefficientdiagonalbound. pfa_gap_empty_divisor_productcoefficientscoefficientdiagonalbound + S (pfc_index_empty_divisor_productcoefficientscoefficientdiagonal) = (S (pfc_index_empty_divisor_productcoefficients))) -> exists pfc_value_empty_divisor_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_empty_divisor_productcoefficientscoefficientdiagonalentry. ff_h_pfp_empty_divisor_productcoefficientscoefficientdiagonalentry + S (pfc_value_empty_divisor_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_empty_divisor_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_empty_divisor_productcoefficientscoefficient)) /\ exists ff_q_pfp_empty_divisor_productcoefficientscoefficientdiagonalentry. pfc_terms_code_empty_divisor_productcoefficientscoefficient = ff_q_pfp_empty_divisor_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_empty_divisor_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_empty_divisor_productcoefficientscoefficient) + (pfc_value_empty_divisor_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_empty_divisor_productcoefficientscoefficientdiagonalterm pfc_left_empty_divisor_productcoefficientscoefficientdiagonalterm pfc_right_empty_divisor_productcoefficientscoefficientdiagonalterm. (((pfc_index_empty_divisor_productcoefficientscoefficientdiagonal)+pfc_complement_empty_divisor_productcoefficientscoefficientdiagonalterm=(pfc_index_empty_divisor_productcoefficients)) /\ ((((((exists pfa_gap_empty_divisor_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_empty_divisor_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_empty_divisor_productcoefficientscoefficientdiagonal) = (pfgu_Q_empty_divisor)) /\ ((((exists ff_h_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_empty_divisor_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_empty_divisor_productcoefficientscoefficientdiagonal)) * pfgu_qc_empty_divisor)) /\ exists ff_q_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_empty_divisor = ff_q_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_empty_divisor_productcoefficientscoefficientdiagonal)) * pfgu_qc_empty_divisor) + (pfc_left_empty_divisor_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_empty_divisor_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_empty_divisor_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_empty_divisor)=(pfc_index_empty_divisor_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_empty_divisor_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_empty_divisor_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_empty_divisor_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_empty_divisor_productcoefficientscoefficientdiagonalterm) = (0)) /\ ((((exists ff_h_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_empty_divisor_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_empty_divisor_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_empty_divisor_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_empty_divisor_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_empty_divisor_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_empty_divisor_productcoefficientscoefficientdiagonaltermrightoutside+(0)=(pfc_complement_empty_divisor_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_empty_divisor_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_empty_divisor_productcoefficientscoefficientdiagonal)=pfc_left_empty_divisor_productcoefficientscoefficientdiagonalterm*pfc_right_empty_divisor_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_empty_divisor_productcoefficientscoefficientsum fs_v_pfc_empty_divisor_productcoefficientscoefficientsum. ((((exists fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_start. fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_start. fs_u_pfc_empty_divisor_productcoefficientscoefficientsum = fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_empty_divisor_productcoefficientscoefficient) = S ((S (S (pfc_index_empty_divisor_productcoefficients))) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_empty_divisor_productcoefficientscoefficientsum = fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_empty_divisor_productcoefficients))) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum) + (pfc_natural_sum_empty_divisor_productcoefficientscoefficient))) /\ forall fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps = S (pfc_index_empty_divisor_productcoefficients)) -> exists fs_a_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps fs_r_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps fs_s_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_empty_divisor_productcoefficientscoefficient)) /\ exists fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_empty_divisor_productcoefficientscoefficient = fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_empty_divisor_productcoefficientscoefficient) + (fs_a_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_empty_divisor_productcoefficientscoefficientsum = fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum) + (fs_r_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_empty_divisor_productcoefficientscoefficientsum = fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum) + (fs_s_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps = fs_r_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps + fs_a_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_empty_divisor_productcoefficientscoefficientresiduebound. pfa_gap_empty_divisor_productcoefficientscoefficientresiduebound + S (pfc_value_empty_divisor_productcoefficients) = (p)) /\ ((exists pfa_offset_left_empty_divisor_productcoefficientscoefficientresiduecongruence pfa_offset_right_empty_divisor_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_empty_divisor_productcoefficientscoefficient) + (p) * pfa_offset_left_empty_divisor_productcoefficientscoefficientresiduecongruence = (pfc_value_empty_divisor_productcoefficients) + (p) * pfa_offset_right_empty_divisor_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_empty_divisor_target pfrep_left_empty_divisor_target pfrep_right_empty_divisor_target. ((exists pfrep_position_empty_divisor_targetfirst. ((pfrep_position_empty_divisor_targetfirst+S (pfrep_power_empty_divisor_target)=(pfgu_P_empty_divisor)) /\ ((((exists ff_h_pfp_empty_divisor_targetfirstentry. ff_h_pfp_empty_divisor_targetfirstentry + S (pfrep_left_empty_divisor_target) = S ((S (pfrep_position_empty_divisor_targetfirst)) * pfgu_pc_empty_divisor)) /\ exists ff_q_pfp_empty_divisor_targetfirstentry. pfgu_pb_empty_divisor = ff_q_pfp_empty_divisor_targetfirstentry * S ((S (pfrep_position_empty_divisor_targetfirst)) * pfgu_pc_empty_divisor) + (pfrep_left_empty_divisor_target)))))) \/ (((exists pfrep_gap_empty_divisor_targetfirstoutside. pfrep_gap_empty_divisor_targetfirstoutside+(pfgu_P_empty_divisor)=(pfrep_power_empty_divisor_target)) /\ (((pfrep_left_empty_divisor_target)=0))))) -> ((exists pfrep_position_empty_divisor_targetsecond. ((pfrep_position_empty_divisor_targetsecond+S (pfrep_power_empty_divisor_target)=(L)) /\ ((((exists ff_h_pfp_empty_divisor_targetsecondentry. ff_h_pfp_empty_divisor_targetsecondentry + S (pfrep_right_empty_divisor_target) = S ((S (pfrep_position_empty_divisor_targetsecond)) * ac)) /\ exists ff_q_pfp_empty_divisor_targetsecondentry. ab = ff_q_pfp_empty_divisor_targetsecondentry * S ((S (pfrep_position_empty_divisor_targetsecond)) * ac) + (pfrep_right_empty_divisor_target)))))) \/ (((exists pfrep_gap_empty_divisor_targetsecondoutside. pfrep_gap_empty_divisor_targetsecondoutside+(L)=(pfrep_power_empty_divisor_target)) /\ (((pfrep_right_empty_divisor_target)=0))))) -> pfrep_left_empty_divisor_target=pfrep_right_empty_divisor_target))))))) -> (forall pfrep_power_empty_divisor_result pfrep_left_empty_divisor_result pfrep_right_empty_divisor_result. ((exists pfrep_position_empty_divisor_resultfirst. ((pfrep_position_empty_divisor_resultfirst+S (pfrep_power_empty_divisor_result)=(L)) /\ ((((exists ff_h_pfp_empty_divisor_resultfirstentry. ff_h_pfp_empty_divisor_resultfirstentry + S (pfrep_left_empty_divisor_result) = S ((S (pfrep_position_empty_divisor_resultfirst)) * ac)) /\ exists ff_q_pfp_empty_divisor_resultfirstentry. ab = ff_q_pfp_empty_divisor_resultfirstentry * S ((S (pfrep_position_empty_divisor_resultfirst)) * ac) + (pfrep_left_empty_divisor_result)))))) \/ (((exists pfrep_gap_empty_divisor_resultfirstoutside. pfrep_gap_empty_divisor_resultfirstoutside+(L)=(pfrep_power_empty_divisor_result)) /\ (((pfrep_left_empty_divisor_result)=0))))) -> ((exists pfrep_position_empty_divisor_resultsecond. ((pfrep_position_empty_divisor_resultsecond+S (pfrep_power_empty_divisor_result)=(0)) /\ ((((exists ff_h_pfp_empty_divisor_resultsecondentry. ff_h_pfp_empty_divisor_resultsecondentry + S (pfrep_right_empty_divisor_result) = S ((S (pfrep_position_empty_divisor_resultsecond)) * dc)) /\ exists ff_q_pfp_empty_divisor_resultsecondentry. db = ff_q_pfp_empty_divisor_resultsecondentry * S ((S (pfrep_position_empty_divisor_resultsecond)) * dc) + (pfrep_right_empty_divisor_result)))))) \/ (((exists pfrep_gap_empty_divisor_resultsecondoutside. pfrep_gap_empty_divisor_resultsecondoutside+(0)=(pfrep_power_empty_divisor_result)) /\ (((pfrep_right_empty_divisor_result)=0))))) -> pfrep_left_empty_divisor_result=pfrep_right_empty_divisor_result)

Complete tactic proof in conservative notation

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

66 script commands · 16 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.

01Fix variables and assumptionsL1–7

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

  1. L1
    intro p
  2. L2
    intro db
  3. L3
    intro dc
  4. L4
    intro ab
  5. L5
    intro ac
  6. L6
    intro L
  7. L7
    intro hrd
02Separate the logical casesL8–15

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

  1. L8
    cases hrd
  2. L9
    cases hrd_right
  3. L10
    cases hrd_right_witness
  4. L11
    cases hrd_right_witness_witness
  5. L12
    cases hrd_right_witness_witness_witness
  6. L13
    cases hrd_right_witness_witness_witness_witness
  7. L14
    cases hrd_right_witness_witness_witness_witness_witness
  8. L15
    cases hrd_right_witness_witness_witness_witness_witness_witness
03Establish hlengthL16–16

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

  1. L16
    have hlength : PolynomialProductLength(x2,0,x5)Definitions: PolynomialProductLength(x2,0,x5)Original native command in the exact edition
04Separate the logical casesL17–19

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

  1. L17
    cases hrd_right_witness_witness_witness_witness_witness_witness_left
  2. L18
    cases hrd_right_witness_witness_witness_witness_witness_witness_left_right
  3. L19
    cases hrd_right_witness_witness_witness_witness_witness_witness_left_right_right
05Use earlier factsL20–20

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

  1. L20
    exact hrd_right_witness_witness_witness_witness_witness_witness_left_right_right_left
06Separate the logical casesL21–22

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

  1. L21
    cases hlength
  2. L22
    cases hlength_left
07Use earlier factsL23–32

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

  1. L23
    specialize prime_field_polynomial_equivalent_transitive (ab)
  2. L24
    specialize prime_field_polynomial_equivalent_transitive (ac)
  3. L25
    specialize prime_field_polynomial_equivalent_transitive (L)
  4. L26
    specialize prime_field_polynomial_equivalent_transitive (x3)
  5. L27
    specialize prime_field_polynomial_equivalent_transitive (x4)
  6. L28
    specialize prime_field_polynomial_equivalent_transitive (0)
  7. L29
    specialize prime_field_polynomial_equivalent_transitive (db)
  8. L30
    specialize prime_field_polynomial_equivalent_transitive (dc)
  9. L31
    specialize prime_field_polynomial_equivalent_transitive (0)
  10. L32
    apply prime_field_polynomial_equivalent_transitive
08Use earlier factsL33–39

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

  1. L33
    specialize prime_field_polynomial_equivalent_symmetric (x3)
  2. L34
    specialize prime_field_polynomial_equivalent_symmetric (x4)
  3. L35
    specialize prime_field_polynomial_equivalent_symmetric (0)
  4. L36
    specialize prime_field_polynomial_equivalent_symmetric (ab)
  5. L37
    specialize prime_field_polynomial_equivalent_symmetric (ac)
  6. L38
    specialize prime_field_polynomial_equivalent_symmetric (L)
  7. L39
    apply prime_field_polynomial_equivalent_symmetric
09Establish hcopyL40–49

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

  1. L40
    have hcopy : PolynomialEquivalent(x3,x4,x5,ab,ac,L)Definitions: PolynomialEquivalent(x3,x4,x5,ab,ac,L)Original native command in the exact edition
  2. L41
    exact hrd_right_witness_witness_witness_witness_witness_witness_right
  3. L42
    rewrite hlength_left_right at hcopy
  4. L43
    rewrite hlength_left_right at hcopy
  5. L44
    exact hcopy
  6. L45
    specialize prime_field_polynomial_equal_implies_equivalent (x3)
  7. L46
    specialize prime_field_polynomial_equal_implies_equivalent (x4)
  8. L47
    specialize prime_field_polynomial_equal_implies_equivalent (db)
  9. L48
    specialize prime_field_polynomial_equal_implies_equivalent (dc)
  10. L49
    specialize prime_field_polynomial_equal_implies_equivalent (0)
10Use earlier factsL50–50

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

  1. L50
    apply prime_field_polynomial_equal_implies_equivalent
11Fix variables and assumptionsL51–54

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

  1. L51
    intro i
  2. L52
    intro a
  3. L53
    intro hi
  4. L54
    intro ha
12Separate the logical casesL55–55

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

  1. L55
    exfalso
13Use earlier factsL56–61

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

  1. L56
    specialize lt_not_le (i)
  2. L57
    specialize lt_not_le (0)
  3. L58
    apply lt_not_le
  4. L59
    exact hi
  5. L60
    specialize zero_le (i)
  6. L61
    apply zero_le
14Separate the logical casesL62–64

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

  1. L62
    cases hlength_right
  2. L63
    cases hlength_right_right
  3. L64
    exfalso
15Use earlier factsL65–65

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

  1. L65
    apply hlength_right_right_left
16Calculate and transport equalitiesL66–66

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

  1. L66
    refl

Library-wide reading audit

Original defined command ledger · 66 lines
  1. 0001intro p
  2. 0002intro db
  3. 0003intro dc
  4. 0004intro ab
  5. 0005intro ac
  6. 0006intro L
  7. 0007intro hrd
  8. 0008cases hrd
  9. 0009cases hrd_right
  10. 0010cases hrd_right_witness
  11. 0011cases hrd_right_witness_witness
  12. 0012cases hrd_right_witness_witness_witness
  13. 0013cases hrd_right_witness_witness_witness_witness
  14. 0014cases hrd_right_witness_witness_witness_witness_witness
  15. 0015cases hrd_right_witness_witness_witness_witness_witness_witness
  16. 0016have hlength : PolynomialProductLength(x2,0,x5)
  17. 0017cases hrd_right_witness_witness_witness_witness_witness_witness_left
  18. 0018cases hrd_right_witness_witness_witness_witness_witness_witness_left_right
  19. 0019cases hrd_right_witness_witness_witness_witness_witness_witness_left_right_right
  20. 0020exact hrd_right_witness_witness_witness_witness_witness_witness_left_right_right_left
  21. 0021cases hlength
  22. 0022cases hlength_left
  23. 0023specialize prime_field_polynomial_equivalent_transitive (ab)
  24. 0024specialize prime_field_polynomial_equivalent_transitive (ac)
  25. 0025specialize prime_field_polynomial_equivalent_transitive (L)
  26. 0026specialize prime_field_polynomial_equivalent_transitive (x3)
  27. 0027specialize prime_field_polynomial_equivalent_transitive (x4)
  28. 0028specialize prime_field_polynomial_equivalent_transitive (0)
  29. 0029specialize prime_field_polynomial_equivalent_transitive (db)
  30. 0030specialize prime_field_polynomial_equivalent_transitive (dc)
  31. 0031specialize prime_field_polynomial_equivalent_transitive (0)
  32. 0032apply prime_field_polynomial_equivalent_transitive
  33. 0033specialize prime_field_polynomial_equivalent_symmetric (x3)
  34. 0034specialize prime_field_polynomial_equivalent_symmetric (x4)
  35. 0035specialize prime_field_polynomial_equivalent_symmetric (0)
  36. 0036specialize prime_field_polynomial_equivalent_symmetric (ab)
  37. 0037specialize prime_field_polynomial_equivalent_symmetric (ac)
  38. 0038specialize prime_field_polynomial_equivalent_symmetric (L)
  39. 0039apply prime_field_polynomial_equivalent_symmetric
  40. 0040have hcopy : PolynomialEquivalent(x3,x4,x5,ab,ac,L)
  41. 0041exact hrd_right_witness_witness_witness_witness_witness_witness_right
  42. 0042rewrite hlength_left_right at hcopy
  43. 0043rewrite hlength_left_right at hcopy
  44. 0044exact hcopy
  45. 0045specialize prime_field_polynomial_equal_implies_equivalent (x3)
  46. 0046specialize prime_field_polynomial_equal_implies_equivalent (x4)
  47. 0047specialize prime_field_polynomial_equal_implies_equivalent (db)
  48. 0048specialize prime_field_polynomial_equal_implies_equivalent (dc)
  49. 0049specialize prime_field_polynomial_equal_implies_equivalent (0)
  50. 0050apply prime_field_polynomial_equal_implies_equivalent
  51. 0051intro i
  52. 0052intro a
  53. 0053intro hi
  54. 0054intro ha
  55. 0055exfalso
  56. 0056specialize lt_not_le (i)
  57. 0057specialize lt_not_le (0)
  58. 0058apply lt_not_le
  59. 0059exact hi
  60. 0060specialize zero_le (i)
  61. 0061apply zero_le
  62. 0062cases hlength_right
  63. 0063cases hlength_right_right
  64. 0064exfalso
  65. 0065apply hlength_right_right_left
  66. 0066refl