PX0037

prime_field_polynomial_division_quotient_data_exists

Construct the actual divisor head, inverse, quotient length and quotient table as one small independently checked construction stage.

Alpha v34 checked-use · first admitted v33 · 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.

Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ d. Prime(p) → BetaPrefixInto(ab,ac,L,p) → FpRepresentedDegree(p,bb,bc,S d,d) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. BetaAt(bb,bc,0,x) ∧ (FpInv(p,x,y) ∧ (PolynomialQuotientLength(L,d,z) ∧ FpPolynomialQuotientPrefix(p,y,ab,ac,bb,bc,S d,n,m,z)))

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

Definition DAG

FpInv(p,a,b) · 2BetaPrefixInto(b,c,l,B) · 1FpRepresentedDegree(p,b,c,L,d) · 1FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,qb,qc,N) · 2PolynomialQuotientLength(L,d,q) · 2Le(a,b) · 2Lt(a,b) · 1Prime(p) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

prime_field_inverse_exists · checked external prerequisitematrix_rank_bounded_prefix_value · checked external prerequisitepolynomial_quotient_length_existspolynomial_quotient_length_boundsprime_field_polynomial_quotient_prefix_existslt_of_lt_of_le · checked external prerequisite
Original expanded first-order statement 
forall p ab ac L bb bc d. (~((p) = 1) /\ forall pfa_factor_left_division_quotient_data_prime pfa_factor_right_division_quotient_data_prime. (p) = pfa_factor_left_division_quotient_data_prime * pfa_factor_right_division_quotient_data_prime -> pfa_factor_left_division_quotient_data_prime = 1 \/ pfa_factor_right_division_quotient_data_prime = 1) -> (forall fom_index_pfp_division_quotient_data_input. (exists fom_gap_pfp_division_quotient_data_input_index_bound. fom_gap_pfp_division_quotient_data_input_index_bound + S (fom_index_pfp_division_quotient_data_input) = L) -> exists fom_value_pfp_division_quotient_data_input. ((((exists fom_beta_height_pfp_division_quotient_data_input_entry. fom_beta_height_pfp_division_quotient_data_input_entry + S (fom_value_pfp_division_quotient_data_input) = S ((S (fom_index_pfp_division_quotient_data_input)) * ac)) /\ exists fom_beta_quotient_pfp_division_quotient_data_input_entry. ab = fom_beta_quotient_pfp_division_quotient_data_input_entry * S ((S (fom_index_pfp_division_quotient_data_input)) * ac) + (fom_value_pfp_division_quotient_data_input))) /\ (exists fom_gap_pfp_division_quotient_data_input_value_bound. fom_gap_pfp_division_quotient_data_input_value_bound + S (fom_value_pfp_division_quotient_data_input) = p))) -> ((((S d)=S (d)) /\ (((forall fom_index_pfp_division_quotient_data_divisorcoefficients. (exists fom_gap_pfp_division_quotient_data_divisorcoefficients_index_bound. fom_gap_pfp_division_quotient_data_divisorcoefficients_index_bound + S (fom_index_pfp_division_quotient_data_divisorcoefficients) = S d) -> exists fom_value_pfp_division_quotient_data_divisorcoefficients. ((((exists fom_beta_height_pfp_division_quotient_data_divisorcoefficients_entry. fom_beta_height_pfp_division_quotient_data_divisorcoefficients_entry + S (fom_value_pfp_division_quotient_data_divisorcoefficients) = S ((S (fom_index_pfp_division_quotient_data_divisorcoefficients)) * bc)) /\ exists fom_beta_quotient_pfp_division_quotient_data_divisorcoefficients_entry. bb = fom_beta_quotient_pfp_division_quotient_data_divisorcoefficients_entry * S ((S (fom_index_pfp_division_quotient_data_divisorcoefficients)) * bc) + (fom_value_pfp_division_quotient_data_divisorcoefficients))) /\ (exists fom_gap_pfp_division_quotient_data_divisorcoefficients_value_bound. fom_gap_pfp_division_quotient_data_divisorcoefficients_value_bound + S (fom_value_pfp_division_quotient_data_divisorcoefficients) = p))) /\ ((exists pfd_leading_division_quotient_data_divisor. ((((exists ff_h_pfp_division_quotient_data_divisorentry. ff_h_pfp_division_quotient_data_divisorentry + S (pfd_leading_division_quotient_data_divisor) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_quotient_data_divisorentry. bb = ff_q_pfp_division_quotient_data_divisorentry * S ((S (0)) * bc) + (pfd_leading_division_quotient_data_divisor))) /\ ((~(pfd_leading_division_quotient_data_divisor=0)))))))))) -> exists b k q qb qc. (((((exists ff_h_pfp_division_quotient_data_resulthead. ff_h_pfp_division_quotient_data_resulthead + S (b) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_quotient_data_resulthead. bb = ff_q_pfp_division_quotient_data_resulthead * S ((S (0)) * bc) + (b))) /\ (((((~((b) = 0)) /\ ((((exists pfa_gap_division_quotient_data_resultinversemultiplicationleft. pfa_gap_division_quotient_data_resultinversemultiplicationleft + S (b) = (p)) /\ (((exists pfa_gap_division_quotient_data_resultinversemultiplicationright. pfa_gap_division_quotient_data_resultinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_division_quotient_data_resultinversemultiplicationresultbound. pfa_gap_division_quotient_data_resultinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_quotient_data_resultinversemultiplicationresultcongruence pfa_offset_right_division_quotient_data_resultinversemultiplicationresultcongruence. ((b) * (k)) + (p) * pfa_offset_left_division_quotient_data_resultinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_quotient_data_resultinversemultiplicationresultcongruence)))))))))))) /\ (((((((q)=0) /\ ((exists pfc_gap_division_quotient_data_resultlengthshort. pfc_gap_division_quotient_data_resultlengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((forall pfd_index_division_quotient_data_resultexecution. (exists pfa_gap_division_quotient_data_resultexecutionbound. pfa_gap_division_quotient_data_resultexecutionbound + S (pfd_index_division_quotient_data_resultexecution) = (q)) -> exists pfd_value_division_quotient_data_resultexecution. ((((exists ff_h_pfp_division_quotient_data_resultexecutionentry. ff_h_pfp_division_quotient_data_resultexecutionentry + S (pfd_value_division_quotient_data_resultexecution) = S ((S (pfd_index_division_quotient_data_resultexecution)) * qc)) /\ exists ff_q_pfp_division_quotient_data_resultexecutionentry. qb = ff_q_pfp_division_quotient_data_resultexecutionentry * S ((S (pfd_index_division_quotient_data_resultexecution)) * qc) + (pfd_value_division_quotient_data_resultexecution))) /\ ((exists pfd_input_division_quotient_data_resultexecutionstep pfd_previous_division_quotient_data_resultexecutionstep pfd_difference_division_quotient_data_resultexecutionstep. ((((exists ff_h_pfp_division_quotient_data_resultexecutionstepinput. ff_h_pfp_division_quotient_data_resultexecutionstepinput + S (pfd_input_division_quotient_data_resultexecutionstep) = S ((S (pfd_index_division_quotient_data_resultexecution)) * ac)) /\ exists ff_q_pfp_division_quotient_data_resultexecutionstepinput. ab = ff_q_pfp_division_quotient_data_resultexecutionstepinput * S ((S (pfd_index_division_quotient_data_resultexecution)) * ac) + (pfd_input_division_quotient_data_resultexecutionstep))) /\ (((exists pfc_terms_code_division_quotient_data_resultexecutionstepprevious pfc_terms_scale_division_quotient_data_resultexecutionstepprevious pfc_natural_sum_division_quotient_data_resultexecutionstepprevious. ((forall pfc_index_division_quotient_data_resultexecutionsteppreviousdiagonal. (exists pfa_gap_division_quotient_data_resultexecutionsteppreviousdiagonalbound. pfa_gap_division_quotient_data_resultexecutionsteppreviousdiagonalbound + S (pfc_index_division_quotient_data_resultexecutionsteppreviousdiagonal) = (S (pfd_index_division_quotient_data_resultexecution))) -> exists pfc_value_division_quotient_data_resultexecutionsteppreviousdiagonal. ((((exists ff_h_pfp_division_quotient_data_resultexecutionsteppreviousdiagonalentry. ff_h_pfp_division_quotient_data_resultexecutionsteppreviousdiagonalentry + S (pfc_value_division_quotient_data_resultexecutionsteppreviousdiagonal) = S ((S (pfc_index_division_quotient_data_resultexecutionsteppreviousdiagonal)) * pfc_terms_scale_division_quotient_data_resultexecutionstepprevious)) /\ exists ff_q_pfp_division_quotient_data_resultexecutionsteppreviousdiagonalentry. pfc_terms_code_division_quotient_data_resultexecutionstepprevious = ff_q_pfp_division_quotient_data_resultexecutionsteppreviousdiagonalentry * S ((S (pfc_index_division_quotient_data_resultexecutionsteppreviousdiagonal)) * pfc_terms_scale_division_quotient_data_resultexecutionstepprevious) + (pfc_value_division_quotient_data_resultexecutionsteppreviousdiagonal))) /\ ((exists pfc_complement_division_quotient_data_resultexecutionsteppreviousdiagonalterm pfc_left_division_quotient_data_resultexecutionsteppreviousdiagonalterm pfc_right_division_quotient_data_resultexecutionsteppreviousdiagonalterm. (((pfc_index_division_quotient_data_resultexecutionsteppreviousdiagonal)+pfc_complement_division_quotient_data_resultexecutionsteppreviousdiagonalterm=(pfd_index_division_quotient_data_resultexecution)) /\ ((((((exists pfa_gap_division_quotient_data_resultexecutionsteppreviousdiagonaltermleftinside. pfa_gap_division_quotient_data_resultexecutionsteppreviousdiagonaltermleftinside + S (pfc_index_division_quotient_data_resultexecutionsteppreviousdiagonal) = (pfd_index_division_quotient_data_resultexecution)) /\ ((((exists ff_h_pfp_division_quotient_data_resultexecutionsteppreviousdiagonaltermleftentry. ff_h_pfp_division_quotient_data_resultexecutionsteppreviousdiagonaltermleftentry + S (pfc_left_division_quotient_data_resultexecutionsteppreviousdiagonalterm) = S ((S (pfc_index_division_quotient_data_resultexecutionsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_quotient_data_resultexecutionsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_quotient_data_resultexecutionsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_quotient_data_resultexecutionsteppreviousdiagonal)) * qc) + (pfc_left_division_quotient_data_resultexecutionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_quotient_data_resultexecutionsteppreviousdiagonaltermleftoutside. pfc_gap_division_quotient_data_resultexecutionsteppreviousdiagonaltermleftoutside+(pfd_index_division_quotient_data_resultexecution)=(pfc_index_division_quotient_data_resultexecutionsteppreviousdiagonal)) /\ (((pfc_left_division_quotient_data_resultexecutionsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_quotient_data_resultexecutionsteppreviousdiagonaltermrightinside. pfa_gap_division_quotient_data_resultexecutionsteppreviousdiagonaltermrightinside + S (pfc_complement_division_quotient_data_resultexecutionsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_quotient_data_resultexecutionsteppreviousdiagonaltermrightentry. ff_h_pfp_division_quotient_data_resultexecutionsteppreviousdiagonaltermrightentry + S (pfc_right_division_quotient_data_resultexecutionsteppreviousdiagonalterm) = S ((S (pfc_complement_division_quotient_data_resultexecutionsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_quotient_data_resultexecutionsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_quotient_data_resultexecutionsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_quotient_data_resultexecutionsteppreviousdiagonalterm)) * bc) + (pfc_right_division_quotient_data_resultexecutionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_quotient_data_resultexecutionsteppreviousdiagonaltermrightoutside. pfc_gap_division_quotient_data_resultexecutionsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_division_quotient_data_resultexecutionsteppreviousdiagonalterm)) /\ (((pfc_right_division_quotient_data_resultexecutionsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_quotient_data_resultexecutionsteppreviousdiagonal)=pfc_left_division_quotient_data_resultexecutionsteppreviousdiagonalterm*pfc_right_division_quotient_data_resultexecutionsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_quotient_data_resultexecutionstepprevioussum fs_v_pfc_division_quotient_data_resultexecutionstepprevioussum. ((((exists fs_h_pfc_division_quotient_data_resultexecutionstepprevioussum_body_start. fs_h_pfc_division_quotient_data_resultexecutionstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_quotient_data_resultexecutionstepprevioussum)) /\ exists fs_q_pfc_division_quotient_data_resultexecutionstepprevioussum_body_start. fs_u_pfc_division_quotient_data_resultexecutionstepprevioussum = fs_q_pfc_division_quotient_data_resultexecutionstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_quotient_data_resultexecutionstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_quotient_data_resultexecutionstepprevioussum_body_terminal. fs_h_pfc_division_quotient_data_resultexecutionstepprevioussum_body_terminal + S (pfc_natural_sum_division_quotient_data_resultexecutionstepprevious) = S ((S (S (pfd_index_division_quotient_data_resultexecution))) * fs_v_pfc_division_quotient_data_resultexecutionstepprevioussum)) /\ exists fs_q_pfc_division_quotient_data_resultexecutionstepprevioussum_body_terminal. fs_u_pfc_division_quotient_data_resultexecutionstepprevioussum = fs_q_pfc_division_quotient_data_resultexecutionstepprevioussum_body_terminal * S ((S (S (pfd_index_division_quotient_data_resultexecution))) * fs_v_pfc_division_quotient_data_resultexecutionstepprevioussum) + (pfc_natural_sum_division_quotient_data_resultexecutionstepprevious))) /\ forall fs_i_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps. (exists fs_lt_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps_bound. fs_lt_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps_bound + S fs_i_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps = S (pfd_index_division_quotient_data_resultexecution)) -> exists fs_a_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps fs_r_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps fs_s_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps. ((((exists fs_h_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps_summand. fs_h_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps_summand + S (fs_a_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps)) * pfc_terms_scale_division_quotient_data_resultexecutionstepprevious)) /\ exists fs_q_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps_summand. pfc_terms_code_division_quotient_data_resultexecutionstepprevious = fs_q_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps)) * pfc_terms_scale_division_quotient_data_resultexecutionstepprevious) + (fs_a_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps_partial. fs_h_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps_partial + S (fs_r_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps)) * fs_v_pfc_division_quotient_data_resultexecutionstepprevioussum)) /\ exists fs_q_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps_partial. fs_u_pfc_division_quotient_data_resultexecutionstepprevioussum = fs_q_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps)) * fs_v_pfc_division_quotient_data_resultexecutionstepprevioussum) + (fs_r_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps_successor. fs_h_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps_successor + S (fs_s_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps)) * fs_v_pfc_division_quotient_data_resultexecutionstepprevioussum)) /\ exists fs_q_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps_successor. fs_u_pfc_division_quotient_data_resultexecutionstepprevioussum = fs_q_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps)) * fs_v_pfc_division_quotient_data_resultexecutionstepprevioussum) + (fs_s_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps))) /\ fs_s_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps = fs_r_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps + fs_a_pfc_division_quotient_data_resultexecutionstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_quotient_data_resultexecutionsteppreviousresiduebound. pfa_gap_division_quotient_data_resultexecutionsteppreviousresiduebound + S (pfd_previous_division_quotient_data_resultexecutionstep) = (p)) /\ ((exists pfa_offset_left_division_quotient_data_resultexecutionsteppreviousresiduecongruence pfa_offset_right_division_quotient_data_resultexecutionsteppreviousresiduecongruence. (pfc_natural_sum_division_quotient_data_resultexecutionstepprevious) + (p) * pfa_offset_left_division_quotient_data_resultexecutionsteppreviousresiduecongruence = (pfd_previous_division_quotient_data_resultexecutionstep) + (p) * pfa_offset_right_division_quotient_data_resultexecutionsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_quotient_data_resultexecutionstepsubtractleft. pfa_gap_division_quotient_data_resultexecutionstepsubtractleft + S (pfd_previous_division_quotient_data_resultexecutionstep) = (p)) /\ (((exists pfa_gap_division_quotient_data_resultexecutionstepsubtractright. pfa_gap_division_quotient_data_resultexecutionstepsubtractright + S (pfd_difference_division_quotient_data_resultexecutionstep) = (p)) /\ ((((exists pfa_gap_division_quotient_data_resultexecutionstepsubtractresultbound. pfa_gap_division_quotient_data_resultexecutionstepsubtractresultbound + S (pfd_input_division_quotient_data_resultexecutionstep) = (p)) /\ ((exists pfa_offset_left_division_quotient_data_resultexecutionstepsubtractresultcongruence pfa_offset_right_division_quotient_data_resultexecutionstepsubtractresultcongruence. ((pfd_previous_division_quotient_data_resultexecutionstep) + (pfd_difference_division_quotient_data_resultexecutionstep)) + (p) * pfa_offset_left_division_quotient_data_resultexecutionstepsubtractresultcongruence = (pfd_input_division_quotient_data_resultexecutionstep) + (p) * pfa_offset_right_division_quotient_data_resultexecutionstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_quotient_data_resultexecutionstepmultiplyleft. pfa_gap_division_quotient_data_resultexecutionstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_quotient_data_resultexecutionstepmultiplyright. pfa_gap_division_quotient_data_resultexecutionstepmultiplyright + S (pfd_difference_division_quotient_data_resultexecutionstep) = (p)) /\ ((((exists pfa_gap_division_quotient_data_resultexecutionstepmultiplyresultbound. pfa_gap_division_quotient_data_resultexecutionstepmultiplyresultbound + S (pfd_value_division_quotient_data_resultexecution) = (p)) /\ ((exists pfa_offset_left_division_quotient_data_resultexecutionstepmultiplyresultcongruence pfa_offset_right_division_quotient_data_resultexecutionstepmultiplyresultcongruence. ((k) * (pfd_difference_division_quotient_data_resultexecutionstep)) + (p) * pfa_offset_left_division_quotient_data_resultexecutionstepmultiplyresultcongruence = (pfd_value_division_quotient_data_resultexecution) + (p) * pfa_offset_right_division_quotient_data_resultexecutionstepmultiplyresultcongruence))))))))))))))))))))))))))

Complete tactic proof in conservative notation

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

85 script commands · 27 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 (3)
polynomial quotient length existspolynomial quotient length boundsprime field polynomial quotient prefix exists
01Fix variables and assumptionsL1–10

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 bb
  6. L6
    intro bc
  7. L7
    intro d
  8. L8
    intro hp
  9. L9
    intro ha
  10. L10
    intro hb
02Separate the logical casesL11–14

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

  1. L11
    cases hb
  2. L12
    cases hb_right
  3. L13
    cases hb_right_right
  4. L14
    cases hb_right_right_witness
03Establish hiL15–24

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

  1. L15
    have hi : ∃ k. FpInv(p,x,k)Definitions: FpInv(p,x,k)Original native command in the exact edition
  2. L16
    specialize prime_field_inverse_exists (p)
  3. L17
    specialize prime_field_inverse_exists (x)
  4. L18
    apply prime_field_inverse_exists
  5. L19
    exact hp
  6. L20
    specialize matrix_rank_bounded_prefix_value (bb)
  7. L21
    specialize matrix_rank_bounded_prefix_value (bc)
  8. L22
    specialize matrix_rank_bounded_prefix_value (S d)
  9. L23
    specialize matrix_rank_bounded_prefix_value (p)
  10. L24
    specialize matrix_rank_bounded_prefix_value (0)
04Use earlier factsL25–27

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

  1. L25
    specialize matrix_rank_bounded_prefix_value (x)
  2. L26
    apply matrix_rank_bounded_prefix_value
  3. L27
    exact hb_right_left
05Construct an explicit witnessL28–28

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

  1. L28
    exists d
06Calculate and transport equalitiesL29–29

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

  1. L29
    simp
07Use earlier factsL30–31

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

  1. L30
    exact hb_right_right_witness_left
  2. L31
    exact hb_right_right_witness_right
08Separate the logical casesL32–32

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

  1. L32
    cases hi
09Establish hkL33–33

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

  1. L33
10Separate the logical casesL34–36

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

  1. L34
    cases hi_witness
  2. L35
    cases hi_witness_right
  3. L36
    cases hi_witness_right_right
11Use earlier factsL37–37

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

  1. L37
    exact hi_witness_right_right_left
12Establish hlengthL38–41

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

  1. L38
    have hlength : ∃ q. PolynomialQuotientLength(L,d,q)Definitions: PolynomialQuotientLength(L,d,q)Original native command in the exact edition
  2. L39
    specialize polynomial_quotient_length_exists (L)
  3. L40
    specialize polynomial_quotient_length_exists (d)
  4. L41
    apply polynomial_quotient_length_exists
13Separate the logical casesL42–42

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

  1. L42
    cases hlength
14Establish hboundsL43–48

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial quotient length bounds.

  1. L43
    have hbounds : Le(x2,L) ∧ Le(L,x2 + d)Definitions: Le(x2,L)Le(L,x2 + d)Original native command in the exact edition
  2. L44
    specialize polynomial_quotient_length_bounds (L)
  3. L45
    specialize polynomial_quotient_length_bounds (d)
  4. L46
    specialize polynomial_quotient_length_bounds (x2)
  5. L47
    apply polynomial_quotient_length_bounds
  6. L48
    exact hlength_witness
15Separate the logical casesL49–49

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

  1. L49
    cases hbounds
16Establish hquotientL50–59

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

  1. L50
    have hquotient : ∃ qb. ∃ qc. FpPolynomialQuotientPrefix(p,x1,ab,ac,bb,bc,S d,qb,qc,x2)Definitions: FpPolynomialQuotientPrefix(p,x1,ab,ac,bb,bc,S d,qb,qc,x2)Original native command in the exact edition
  2. L51
    specialize prime_field_polynomial_quotient_prefix_exists (p)
  3. L52
    specialize prime_field_polynomial_quotient_prefix_exists (x1)
  4. L53
    specialize prime_field_polynomial_quotient_prefix_exists (ab)
  5. L54
    specialize prime_field_polynomial_quotient_prefix_exists (ac)
  6. L55
    specialize prime_field_polynomial_quotient_prefix_exists (bb)
  7. L56
    specialize prime_field_polynomial_quotient_prefix_exists (bc)
  8. L57
    specialize prime_field_polynomial_quotient_prefix_exists (S d)
  9. L58
    specialize prime_field_polynomial_quotient_prefix_exists (x2)
  10. L59
    apply prime_field_polynomial_quotient_prefix_exists
17Use earlier factsL60–61

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

  1. L60
    exact hp
  2. L61
    exact hk
18Fix variables and assumptionsL62–63

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

  1. L62
    intro i
  2. L63
    intro hindex
19Use earlier factsL64–71

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

  1. L64
    specialize ha (i)
  2. L65
    apply ha
  3. L66
    specialize lt_of_lt_of_le (i)
  4. L67
    specialize lt_of_lt_of_le (x2)
  5. L68
    specialize lt_of_lt_of_le (L)
  6. L69
    apply lt_of_lt_of_le
  7. L70
    exact hindex
  8. L71
    exact hbounds_left
20Separate the logical casesL72–73

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

  1. L72
    cases hquotient
  2. L73
    cases hquotient_witness
21Construct an explicit witnessL74–78

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

  1. L74
    exists x
  2. L75
    exists x1
  3. L76
    exists x2
  4. L77
    exists x3
  5. L78
    exists x4
22Separate the logical casesL79–79

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

  1. L79
    split
23Use earlier factsL80–80

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

  1. L80
    exact hb_right_right_witness_left
24Separate the logical casesL81–81

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

  1. L81
    split
25Use earlier factsL82–82

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

  1. L82
    exact hi_witness
26Separate the logical casesL83–83

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

  1. L83
    split
27Use earlier factsL84–85

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

  1. L84
    exact hlength_witness
  2. L85
    exact hquotient_witness_witness

Library-wide reading audit

Original defined command ledger · 85 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro d
  8. 0008intro hp
  9. 0009intro ha
  10. 0010intro hb
  11. 0011cases hb
  12. 0012cases hb_right
  13. 0013cases hb_right_right
  14. 0014cases hb_right_right_witness
  15. 0015have hi : ∃ k. FpInv(p,x,k)
  16. 0016specialize prime_field_inverse_exists (p)
  17. 0017specialize prime_field_inverse_exists (x)
  18. 0018apply prime_field_inverse_exists
  19. 0019exact hp
  20. 0020specialize matrix_rank_bounded_prefix_value (bb)
  21. 0021specialize matrix_rank_bounded_prefix_value (bc)
  22. 0022specialize matrix_rank_bounded_prefix_value (S d)
  23. 0023specialize matrix_rank_bounded_prefix_value (p)
  24. 0024specialize matrix_rank_bounded_prefix_value (0)
  25. 0025specialize matrix_rank_bounded_prefix_value (x)
  26. 0026apply matrix_rank_bounded_prefix_value
  27. 0027exact hb_right_left
  28. 0028exists d
  29. 0029simp
  30. 0030exact hb_right_right_witness_left
  31. 0031exact hb_right_right_witness_right
  32. 0032cases hi
  33. 0033have hk : Lt(x1,p)
  34. 0034cases hi_witness
  35. 0035cases hi_witness_right
  36. 0036cases hi_witness_right_right
  37. 0037exact hi_witness_right_right_left
  38. 0038have hlength : ∃ q. PolynomialQuotientLength(L,d,q)
  39. 0039specialize polynomial_quotient_length_exists (L)
  40. 0040specialize polynomial_quotient_length_exists (d)
  41. 0041apply polynomial_quotient_length_exists
  42. 0042cases hlength
  43. 0043have hbounds : Le(x2,L) ∧ Le(L,x2 + d)
  44. 0044specialize polynomial_quotient_length_bounds (L)
  45. 0045specialize polynomial_quotient_length_bounds (d)
  46. 0046specialize polynomial_quotient_length_bounds (x2)
  47. 0047apply polynomial_quotient_length_bounds
  48. 0048exact hlength_witness
  49. 0049cases hbounds
  50. 0050have hquotient : ∃ qb. ∃ qc. FpPolynomialQuotientPrefix(p,x1,ab,ac,bb,bc,S d,qb,qc,x2)
  51. 0051specialize prime_field_polynomial_quotient_prefix_exists (p)
  52. 0052specialize prime_field_polynomial_quotient_prefix_exists (x1)
  53. 0053specialize prime_field_polynomial_quotient_prefix_exists (ab)
  54. 0054specialize prime_field_polynomial_quotient_prefix_exists (ac)
  55. 0055specialize prime_field_polynomial_quotient_prefix_exists (bb)
  56. 0056specialize prime_field_polynomial_quotient_prefix_exists (bc)
  57. 0057specialize prime_field_polynomial_quotient_prefix_exists (S d)
  58. 0058specialize prime_field_polynomial_quotient_prefix_exists (x2)
  59. 0059apply prime_field_polynomial_quotient_prefix_exists
  60. 0060exact hp
  61. 0061exact hk
  62. 0062intro i
  63. 0063intro hindex
  64. 0064specialize ha (i)
  65. 0065apply ha
  66. 0066specialize lt_of_lt_of_le (i)
  67. 0067specialize lt_of_lt_of_le (x2)
  68. 0068specialize lt_of_lt_of_le (L)
  69. 0069apply lt_of_lt_of_le
  70. 0070exact hindex
  71. 0071exact hbounds_left
  72. 0072cases hquotient
  73. 0073cases hquotient_witness
  74. 0074exists x
  75. 0075exists x1
  76. 0076exists x2
  77. 0077exists x3
  78. 0078exists x4
  79. 0079split
  80. 0080exact hb_right_right_witness_left
  81. 0081split
  82. 0082exact hi_witness
  83. 0083split
  84. 0084exact hlength_witness
  85. 0085exact hquotient_witness_witness