PG0033

prime_field_polynomial_convolution_left_unit_exists

Construct an actual canonical length-one unit and its actual length-L left product, formally equal to A. The proper length is zero when A is empty.

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. ∀ ab. ∀ ac. ∀ L. Prime(p) → BetaPrefixInto(ab,ac,L,p) → ∃ x. ∃ y. ∃ z. ∃ n. BetaPrefixInto(x,y,1,p) ∧ (BetaAt(x,y,0,1) ∧ (FpPolyProduct(p,x,y,1,ab,ac,L,z,n,L) ∧ PolynomialEquivalent(z,n,L,ab,ac,L)))

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 3FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 2PolynomialEquivalent(b,c,L,d,e,M) · 1Prime(p) · 1BetaAt(b,c,i,x) · 2Repeat(b,c,a,l) · 1

Actual proof prerequisites

prime_nonzero · checked external prerequisiteprime_field_polynomial_repeat_exists · checked external prerequisiteprime_two_le · checked external prerequisitezero_add · checked external prerequisiteprime_field_polynomial_convolution_at_length_exists · checked external prerequisiteeq_decidable · checked external prerequisitesucc_ne_zero · checked external prerequisiteadd_succ_left · checked external prerequisiteprime_field_polynomial_convolution_left_unit_equivalent
Original expanded first-order statement 
forall p ab ac L. (~((p) = 1) /\ forall pfa_factor_left_unit_exists_prime pfa_factor_right_unit_exists_prime. (p) = pfa_factor_left_unit_exists_prime * pfa_factor_right_unit_exists_prime -> pfa_factor_left_unit_exists_prime = 1 \/ pfa_factor_right_unit_exists_prime = 1) -> (forall fom_index_pfp_unit_exists_A. (exists fom_gap_pfp_unit_exists_A_index_bound. fom_gap_pfp_unit_exists_A_index_bound + S (fom_index_pfp_unit_exists_A) = L) -> exists fom_value_pfp_unit_exists_A. ((((exists fom_beta_height_pfp_unit_exists_A_entry. fom_beta_height_pfp_unit_exists_A_entry + S (fom_value_pfp_unit_exists_A) = S ((S (fom_index_pfp_unit_exists_A)) * ac)) /\ exists fom_beta_quotient_pfp_unit_exists_A_entry. ab = fom_beta_quotient_pfp_unit_exists_A_entry * S ((S (fom_index_pfp_unit_exists_A)) * ac) + (fom_value_pfp_unit_exists_A))) /\ (exists fom_gap_pfp_unit_exists_A_value_bound. fom_gap_pfp_unit_exists_A_value_bound + S (fom_value_pfp_unit_exists_A) = p))) -> (exists ub uc cb cc. ((forall fom_index_pfp_unit_exists_result_unit_bound. (exists fom_gap_pfp_unit_exists_result_unit_bound_index_bound. fom_gap_pfp_unit_exists_result_unit_bound_index_bound + S (fom_index_pfp_unit_exists_result_unit_bound) = 1) -> exists fom_value_pfp_unit_exists_result_unit_bound. ((((exists fom_beta_height_pfp_unit_exists_result_unit_bound_entry. fom_beta_height_pfp_unit_exists_result_unit_bound_entry + S (fom_value_pfp_unit_exists_result_unit_bound) = S ((S (fom_index_pfp_unit_exists_result_unit_bound)) * uc)) /\ exists fom_beta_quotient_pfp_unit_exists_result_unit_bound_entry. ub = fom_beta_quotient_pfp_unit_exists_result_unit_bound_entry * S ((S (fom_index_pfp_unit_exists_result_unit_bound)) * uc) + (fom_value_pfp_unit_exists_result_unit_bound))) /\ (exists fom_gap_pfp_unit_exists_result_unit_bound_value_bound. fom_gap_pfp_unit_exists_result_unit_bound_value_bound + S (fom_value_pfp_unit_exists_result_unit_bound) = p))) /\ (((((exists ff_h_pfp_unit_exists_result_unit_value. ff_h_pfp_unit_exists_result_unit_value + S (1) = S ((S (0)) * uc)) /\ exists ff_q_pfp_unit_exists_result_unit_value. ub = ff_q_pfp_unit_exists_result_unit_value * S ((S (0)) * uc) + (1))) /\ (((((forall fom_index_pfp_unit_exists_result_productleft. (exists fom_gap_pfp_unit_exists_result_productleft_index_bound. fom_gap_pfp_unit_exists_result_productleft_index_bound + S (fom_index_pfp_unit_exists_result_productleft) = 1) -> exists fom_value_pfp_unit_exists_result_productleft. ((((exists fom_beta_height_pfp_unit_exists_result_productleft_entry. fom_beta_height_pfp_unit_exists_result_productleft_entry + S (fom_value_pfp_unit_exists_result_productleft) = S ((S (fom_index_pfp_unit_exists_result_productleft)) * uc)) /\ exists fom_beta_quotient_pfp_unit_exists_result_productleft_entry. ub = fom_beta_quotient_pfp_unit_exists_result_productleft_entry * S ((S (fom_index_pfp_unit_exists_result_productleft)) * uc) + (fom_value_pfp_unit_exists_result_productleft))) /\ (exists fom_gap_pfp_unit_exists_result_productleft_value_bound. fom_gap_pfp_unit_exists_result_productleft_value_bound + S (fom_value_pfp_unit_exists_result_productleft) = p))) /\ (((forall fom_index_pfp_unit_exists_result_productright. (exists fom_gap_pfp_unit_exists_result_productright_index_bound. fom_gap_pfp_unit_exists_result_productright_index_bound + S (fom_index_pfp_unit_exists_result_productright) = L) -> exists fom_value_pfp_unit_exists_result_productright. ((((exists fom_beta_height_pfp_unit_exists_result_productright_entry. fom_beta_height_pfp_unit_exists_result_productright_entry + S (fom_value_pfp_unit_exists_result_productright) = S ((S (fom_index_pfp_unit_exists_result_productright)) * ac)) /\ exists fom_beta_quotient_pfp_unit_exists_result_productright_entry. ab = fom_beta_quotient_pfp_unit_exists_result_productright_entry * S ((S (fom_index_pfp_unit_exists_result_productright)) * ac) + (fom_value_pfp_unit_exists_result_productright))) /\ (exists fom_gap_pfp_unit_exists_result_productright_value_bound. fom_gap_pfp_unit_exists_result_productright_value_bound + S (fom_value_pfp_unit_exists_result_productright) = p))) /\ (((((((1)=0 \/ (L)=0) /\ (((L)=0)))) \/ (((~((1)=0)) /\ (((~((L)=0)) /\ (((1)+(L)=S (L)))))))) /\ ((forall pfc_index_unit_exists_result_productcoefficients. (exists pfa_gap_unit_exists_result_productcoefficientsbound. pfa_gap_unit_exists_result_productcoefficientsbound + S (pfc_index_unit_exists_result_productcoefficients) = (L)) -> exists pfc_value_unit_exists_result_productcoefficients. ((((exists ff_h_pfp_unit_exists_result_productcoefficientsentry. ff_h_pfp_unit_exists_result_productcoefficientsentry + S (pfc_value_unit_exists_result_productcoefficients) = S ((S (pfc_index_unit_exists_result_productcoefficients)) * cc)) /\ exists ff_q_pfp_unit_exists_result_productcoefficientsentry. cb = ff_q_pfp_unit_exists_result_productcoefficientsentry * S ((S (pfc_index_unit_exists_result_productcoefficients)) * cc) + (pfc_value_unit_exists_result_productcoefficients))) /\ ((exists pfc_terms_code_unit_exists_result_productcoefficientscoefficient pfc_terms_scale_unit_exists_result_productcoefficientscoefficient pfc_natural_sum_unit_exists_result_productcoefficientscoefficient. ((forall pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal. (exists pfa_gap_unit_exists_result_productcoefficientscoefficientdiagonalbound. pfa_gap_unit_exists_result_productcoefficientscoefficientdiagonalbound + S (pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal) = (S (pfc_index_unit_exists_result_productcoefficients))) -> exists pfc_value_unit_exists_result_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_unit_exists_result_productcoefficientscoefficientdiagonalentry. ff_h_pfp_unit_exists_result_productcoefficientscoefficientdiagonalentry + S (pfc_value_unit_exists_result_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_exists_result_productcoefficientscoefficient)) /\ exists ff_q_pfp_unit_exists_result_productcoefficientscoefficientdiagonalentry. pfc_terms_code_unit_exists_result_productcoefficientscoefficient = ff_q_pfp_unit_exists_result_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_exists_result_productcoefficientscoefficient) + (pfc_value_unit_exists_result_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_unit_exists_result_productcoefficientscoefficientdiagonalterm pfc_left_unit_exists_result_productcoefficientscoefficientdiagonalterm pfc_right_unit_exists_result_productcoefficientscoefficientdiagonalterm. (((pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal)+pfc_complement_unit_exists_result_productcoefficientscoefficientdiagonalterm=(pfc_index_unit_exists_result_productcoefficients)) /\ ((((((exists pfa_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal) = (1)) /\ ((((exists ff_h_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_unit_exists_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal)) * uc) + (pfc_left_unit_exists_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermleftoutside+(1)=(pfc_index_unit_exists_result_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_unit_exists_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_unit_exists_result_productcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_unit_exists_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_unit_exists_result_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_unit_exists_result_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_unit_exists_result_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_unit_exists_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_unit_exists_result_productcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_unit_exists_result_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_unit_exists_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_unit_exists_result_productcoefficientscoefficientdiagonal)=pfc_left_unit_exists_result_productcoefficientscoefficientdiagonalterm*pfc_right_unit_exists_result_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_unit_exists_result_productcoefficientscoefficientsum fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum. ((((exists fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_start. fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_start. fs_u_pfc_unit_exists_result_productcoefficientscoefficientsum = fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_unit_exists_result_productcoefficientscoefficient) = S ((S (S (pfc_index_unit_exists_result_productcoefficients))) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_unit_exists_result_productcoefficientscoefficientsum = fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_unit_exists_result_productcoefficients))) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum) + (pfc_natural_sum_unit_exists_result_productcoefficientscoefficient))) /\ forall fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps = S (pfc_index_unit_exists_result_productcoefficients)) -> exists fs_a_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps fs_r_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps fs_s_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_exists_result_productcoefficientscoefficient)) /\ exists fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_unit_exists_result_productcoefficientscoefficient = fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_exists_result_productcoefficientscoefficient) + (fs_a_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_unit_exists_result_productcoefficientscoefficientsum = fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum) + (fs_r_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_unit_exists_result_productcoefficientscoefficientsum = fs_q_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_exists_result_productcoefficientscoefficientsum) + (fs_s_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps = fs_r_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps + fs_a_pfc_unit_exists_result_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_unit_exists_result_productcoefficientscoefficientresiduebound. pfa_gap_unit_exists_result_productcoefficientscoefficientresiduebound + S (pfc_value_unit_exists_result_productcoefficients) = (p)) /\ ((exists pfa_offset_left_unit_exists_result_productcoefficientscoefficientresiduecongruence pfa_offset_right_unit_exists_result_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_unit_exists_result_productcoefficientscoefficient) + (p) * pfa_offset_left_unit_exists_result_productcoefficientscoefficientresiduecongruence = (pfc_value_unit_exists_result_productcoefficients) + (p) * pfa_offset_right_unit_exists_result_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_unit_exists_result_equivalent pfrep_left_unit_exists_result_equivalent pfrep_right_unit_exists_result_equivalent. ((exists pfrep_position_unit_exists_result_equivalentfirst. ((pfrep_position_unit_exists_result_equivalentfirst+S (pfrep_power_unit_exists_result_equivalent)=(L)) /\ ((((exists ff_h_pfp_unit_exists_result_equivalentfirstentry. ff_h_pfp_unit_exists_result_equivalentfirstentry + S (pfrep_left_unit_exists_result_equivalent) = S ((S (pfrep_position_unit_exists_result_equivalentfirst)) * cc)) /\ exists ff_q_pfp_unit_exists_result_equivalentfirstentry. cb = ff_q_pfp_unit_exists_result_equivalentfirstentry * S ((S (pfrep_position_unit_exists_result_equivalentfirst)) * cc) + (pfrep_left_unit_exists_result_equivalent)))))) \/ (((exists pfrep_gap_unit_exists_result_equivalentfirstoutside. pfrep_gap_unit_exists_result_equivalentfirstoutside+(L)=(pfrep_power_unit_exists_result_equivalent)) /\ (((pfrep_left_unit_exists_result_equivalent)=0))))) -> ((exists pfrep_position_unit_exists_result_equivalentsecond. ((pfrep_position_unit_exists_result_equivalentsecond+S (pfrep_power_unit_exists_result_equivalent)=(L)) /\ ((((exists ff_h_pfp_unit_exists_result_equivalentsecondentry. ff_h_pfp_unit_exists_result_equivalentsecondentry + S (pfrep_right_unit_exists_result_equivalent) = S ((S (pfrep_position_unit_exists_result_equivalentsecond)) * ac)) /\ exists ff_q_pfp_unit_exists_result_equivalentsecondentry. ab = ff_q_pfp_unit_exists_result_equivalentsecondentry * S ((S (pfrep_position_unit_exists_result_equivalentsecond)) * ac) + (pfrep_right_unit_exists_result_equivalent)))))) \/ (((exists pfrep_gap_unit_exists_result_equivalentsecondoutside. pfrep_gap_unit_exists_result_equivalentsecondoutside+(L)=(pfrep_power_unit_exists_result_equivalent)) /\ (((pfrep_right_unit_exists_result_equivalent)=0))))) -> pfrep_left_unit_exists_result_equivalent=pfrep_right_unit_exists_result_equivalent))))))))

Complete tactic proof in conservative notation

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

81 script commands · 26 reading checkpoints · 5 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 convolution left unit equivalent
01Fix variables and assumptionsL1–6

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 hp
  6. L6
    intro hA
02Establish hp0L7–12

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

  1. L7
    have hp0 : ~(p=0)
  2. L8
    intro hz
  3. L9
    specialize prime_nonzero (p)
  4. L10
    apply prime_nonzero
  5. L11
    exact hp
  6. L12
    exact hz
03Establish huL13–20

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

  1. L13
    have hu : ∃ ub. ∃ uc. BetaPrefixInto(ub,uc,1,p) ∧ Repeat(ub,uc,1,1)Definitions: BetaPrefixInto(ub,uc,1,p)Repeat(ub,uc,1,1)Original native command in the exact edition
  2. L14
    specialize prime_field_polynomial_repeat_exists (p)
  3. L15
    specialize prime_field_polynomial_repeat_exists (1)
  4. L16
    specialize prime_field_polynomial_repeat_exists (1)
  5. L17
    apply prime_field_polynomial_repeat_exists
  6. L18
    specialize prime_two_le (p)
  7. L19
    apply prime_two_le
  8. L20
    exact hp
04Separate the logical casesL21–23

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

  1. L21
    cases hu
  2. L22
    cases hu_witness
  3. L23
    cases hu_witness_witness
05Establish honeL24–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hu witness witness right.

  1. L24
    have hone : BetaAt(x,x1,0,1)Definitions: BetaAt(x,x1,0,1)Original native command in the exact edition
  2. L25
    specialize hu_witness_witness_right (0)
  3. L26
    apply hu_witness_witness_right
06Construct an explicit witnessL27–27

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

  1. L27
    exists 0
07Use earlier factsL28–28

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

  1. L28
    apply zero_add
08Establish hcL29–38

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

  1. L29
    have hc : ∃ cb. ∃ cc. FpPolyProduct(p,x,x1,1,ab,ac,L,cb,cc,L)Definitions: FpPolyProduct(p,x,x1,1,ab,ac,L,cb,cc,L)Original native command in the exact edition
  2. L30
    specialize prime_field_polynomial_convolution_at_length_exists (p)
  3. L31
    specialize prime_field_polynomial_convolution_at_length_exists (x)
  4. L32
    specialize prime_field_polynomial_convolution_at_length_exists (x1)
  5. L33
    specialize prime_field_polynomial_convolution_at_length_exists (1)
  6. L34
    specialize prime_field_polynomial_convolution_at_length_exists (ab)
  7. L35
    specialize prime_field_polynomial_convolution_at_length_exists (ac)
  8. L36
    specialize prime_field_polynomial_convolution_at_length_exists (L)
  9. L37
    specialize prime_field_polynomial_convolution_at_length_exists (L)
  10. L38
    apply prime_field_polynomial_convolution_at_length_exists
09Use earlier factsL39–41

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

  1. L39
    exact hp0
  2. L40
    exact hu_witness_witness_left
  3. L41
    exact hA
10Establish hzeroL42–45

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

  1. L42
    have hzero : L=0 \/ ~(L=0)
  2. L43
    specialize eq_decidable (L)
  3. L44
    specialize eq_decidable (0)
  4. L45
    apply eq_decidable
11Separate the logical casesL46–49

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

  1. L46
    cases hzero
  2. L47
    left
  3. L48
    split
  4. L49
    right
12Use earlier factsL50–51

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

  1. L50
    exact hzero_left
  2. L51
    exact hzero_left
13Separate the logical casesL52–53

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

  1. L52
    right
  2. L53
    split
14Use earlier factsL54–55

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

  1. L54
    specialize succ_ne_zero (0)
  2. L55
    apply succ_ne_zero
15Separate the logical casesL56–56

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

  1. L56
    split
16Use earlier factsL57–57

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

  1. L57
    exact hzero_right
17Calculate and transport equalitiesL58–58

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

  1. L58
    simp [add_succ_left,zero_add]
18Separate the logical casesL59–60

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

  1. L59
    cases hc
  2. L60
    cases hc_witness
19Construct an explicit witnessL61–64

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

  1. L61
    exists x
  2. L62
    exists x1
  3. L63
    exists x2
  4. L64
    exists x3
20Separate the logical casesL65–65

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

  1. L65
    split
21Use earlier factsL66–66

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

  1. L66
    exact hu_witness_witness_left
22Separate the logical casesL67–67

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

  1. L67
    split
23Use earlier factsL68–68

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

  1. L68
    exact hone
24Separate the logical casesL69–69

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

  1. L69
    split
25Use earlier factsL70–79

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

  1. L70
    exact hc_witness_witness
  2. L71
    specialize prime_field_polynomial_convolution_left_unit_equivalent (p)
  3. L72
    specialize prime_field_polynomial_convolution_left_unit_equivalent (x)
  4. L73
    specialize prime_field_polynomial_convolution_left_unit_equivalent (x1)
  5. L74
    specialize prime_field_polynomial_convolution_left_unit_equivalent (ab)
  6. L75
    specialize prime_field_polynomial_convolution_left_unit_equivalent (ac)
  7. L76
    specialize prime_field_polynomial_convolution_left_unit_equivalent (L)
  8. L77
    specialize prime_field_polynomial_convolution_left_unit_equivalent (x2)
  9. L78
    specialize prime_field_polynomial_convolution_left_unit_equivalent (x3)
  10. L79
    apply prime_field_polynomial_convolution_left_unit_equivalent
26Use earlier factsL80–81

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

  1. L80
    exact hone
  2. L81
    exact hc_witness_witness

Library-wide reading audit

Original defined command ledger · 81 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro hp
  6. 0006intro hA
  7. 0007have hp0 : ~(p=0)
  8. 0008intro hz
  9. 0009specialize prime_nonzero (p)
  10. 0010apply prime_nonzero
  11. 0011exact hp
  12. 0012exact hz
  13. 0013have hu : ∃ ub. ∃ uc. BetaPrefixInto(ub,uc,1,p) ∧ Repeat(ub,uc,1,1)
  14. 0014specialize prime_field_polynomial_repeat_exists (p)
  15. 0015specialize prime_field_polynomial_repeat_exists (1)
  16. 0016specialize prime_field_polynomial_repeat_exists (1)
  17. 0017apply prime_field_polynomial_repeat_exists
  18. 0018specialize prime_two_le (p)
  19. 0019apply prime_two_le
  20. 0020exact hp
  21. 0021cases hu
  22. 0022cases hu_witness
  23. 0023cases hu_witness_witness
  24. 0024have hone : BetaAt(x,x1,0,1)
  25. 0025specialize hu_witness_witness_right (0)
  26. 0026apply hu_witness_witness_right
  27. 0027exists 0
  28. 0028apply zero_add
  29. 0029have hc : ∃ cb. ∃ cc. FpPolyProduct(p,x,x1,1,ab,ac,L,cb,cc,L)
  30. 0030specialize prime_field_polynomial_convolution_at_length_exists (p)
  31. 0031specialize prime_field_polynomial_convolution_at_length_exists (x)
  32. 0032specialize prime_field_polynomial_convolution_at_length_exists (x1)
  33. 0033specialize prime_field_polynomial_convolution_at_length_exists (1)
  34. 0034specialize prime_field_polynomial_convolution_at_length_exists (ab)
  35. 0035specialize prime_field_polynomial_convolution_at_length_exists (ac)
  36. 0036specialize prime_field_polynomial_convolution_at_length_exists (L)
  37. 0037specialize prime_field_polynomial_convolution_at_length_exists (L)
  38. 0038apply prime_field_polynomial_convolution_at_length_exists
  39. 0039exact hp0
  40. 0040exact hu_witness_witness_left
  41. 0041exact hA
  42. 0042have hzero : L=0 \/ ~(L=0)
  43. 0043specialize eq_decidable (L)
  44. 0044specialize eq_decidable (0)
  45. 0045apply eq_decidable
  46. 0046cases hzero
  47. 0047left
  48. 0048split
  49. 0049right
  50. 0050exact hzero_left
  51. 0051exact hzero_left
  52. 0052right
  53. 0053split
  54. 0054specialize succ_ne_zero (0)
  55. 0055apply succ_ne_zero
  56. 0056split
  57. 0057exact hzero_right
  58. 0058simp [add_succ_left,zero_add]
  59. 0059cases hc
  60. 0060cases hc_witness
  61. 0061exists x
  62. 0062exists x1
  63. 0063exists x2
  64. 0064exists x3
  65. 0065split
  66. 0066exact hu_witness_witness_left
  67. 0067split
  68. 0068exact hone
  69. 0069split
  70. 0070exact hc_witness_witness
  71. 0071specialize prime_field_polynomial_convolution_left_unit_equivalent (p)
  72. 0072specialize prime_field_polynomial_convolution_left_unit_equivalent (x)
  73. 0073specialize prime_field_polynomial_convolution_left_unit_equivalent (x1)
  74. 0074specialize prime_field_polynomial_convolution_left_unit_equivalent (ab)
  75. 0075specialize prime_field_polynomial_convolution_left_unit_equivalent (ac)
  76. 0076specialize prime_field_polynomial_convolution_left_unit_equivalent (L)
  77. 0077specialize prime_field_polynomial_convolution_left_unit_equivalent (x2)
  78. 0078specialize prime_field_polynomial_convolution_left_unit_equivalent (x3)
  79. 0079apply prime_field_polynomial_convolution_left_unit_equivalent
  80. 0080exact hone
  81. 0081exact hc_witness_witness