PG0029

prime_field_polynomial_right_divides_equivalent_target

Changing the canonical target by all-power formal coefficient equivalence preserves the same genuine quotient/product witnesses, independently of representation length.

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. ∀ D. ∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ M. BetaPrefixInto(bb,bc,M,p) → FpPolynomialRightDivides(p,db,dc,D,ab,ac,L) → PolynomialEquivalent(ab,ac,L,bb,bc,M) → FpPolynomialRightDivides(p,db,dc,D,bb,bc,M)

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

Definition DAG

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

Actual proof prerequisites

prime_field_polynomial_right_divides_from_productprime_field_polynomial_equivalent_transitive · checked external prerequisite
Original expanded first-order statement 
forall p db dc D ab ac L bb bc M. (forall fom_index_pfp_right_target_bound. (exists fom_gap_pfp_right_target_bound_index_bound. fom_gap_pfp_right_target_bound_index_bound + S (fom_index_pfp_right_target_bound) = M) -> exists fom_value_pfp_right_target_bound. ((((exists fom_beta_height_pfp_right_target_bound_entry. fom_beta_height_pfp_right_target_bound_entry + S (fom_value_pfp_right_target_bound) = S ((S (fom_index_pfp_right_target_bound)) * bc)) /\ exists fom_beta_quotient_pfp_right_target_bound_entry. bb = fom_beta_quotient_pfp_right_target_bound_entry * S ((S (fom_index_pfp_right_target_bound)) * bc) + (fom_value_pfp_right_target_bound))) /\ (exists fom_gap_pfp_right_target_bound_value_bound. fom_gap_pfp_right_target_bound_value_bound + S (fom_value_pfp_right_target_bound) = p))) -> (((forall fom_index_pfp_right_target_source_canonical. (exists fom_gap_pfp_right_target_source_canonical_index_bound. fom_gap_pfp_right_target_source_canonical_index_bound + S (fom_index_pfp_right_target_source_canonical) = L) -> exists fom_value_pfp_right_target_source_canonical. ((((exists fom_beta_height_pfp_right_target_source_canonical_entry. fom_beta_height_pfp_right_target_source_canonical_entry + S (fom_value_pfp_right_target_source_canonical) = S ((S (fom_index_pfp_right_target_source_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_right_target_source_canonical_entry. ab = fom_beta_quotient_pfp_right_target_source_canonical_entry * S ((S (fom_index_pfp_right_target_source_canonical)) * ac) + (fom_value_pfp_right_target_source_canonical))) /\ (exists fom_gap_pfp_right_target_source_canonical_value_bound. fom_gap_pfp_right_target_source_canonical_value_bound + S (fom_value_pfp_right_target_source_canonical) = p))) /\ ((exists pfrd_qb_right_target_source pfrd_qc_right_target_source pfrd_qlen_right_target_source pfrd_pb_right_target_source pfrd_pc_right_target_source pfrd_plen_right_target_source. ((((forall fom_index_pfp_right_target_source_productleft. (exists fom_gap_pfp_right_target_source_productleft_index_bound. fom_gap_pfp_right_target_source_productleft_index_bound + S (fom_index_pfp_right_target_source_productleft) = pfrd_qlen_right_target_source) -> exists fom_value_pfp_right_target_source_productleft. ((((exists fom_beta_height_pfp_right_target_source_productleft_entry. fom_beta_height_pfp_right_target_source_productleft_entry + S (fom_value_pfp_right_target_source_productleft) = S ((S (fom_index_pfp_right_target_source_productleft)) * pfrd_qc_right_target_source)) /\ exists fom_beta_quotient_pfp_right_target_source_productleft_entry. pfrd_qb_right_target_source = fom_beta_quotient_pfp_right_target_source_productleft_entry * S ((S (fom_index_pfp_right_target_source_productleft)) * pfrd_qc_right_target_source) + (fom_value_pfp_right_target_source_productleft))) /\ (exists fom_gap_pfp_right_target_source_productleft_value_bound. fom_gap_pfp_right_target_source_productleft_value_bound + S (fom_value_pfp_right_target_source_productleft) = p))) /\ (((forall fom_index_pfp_right_target_source_productright. (exists fom_gap_pfp_right_target_source_productright_index_bound. fom_gap_pfp_right_target_source_productright_index_bound + S (fom_index_pfp_right_target_source_productright) = D) -> exists fom_value_pfp_right_target_source_productright. ((((exists fom_beta_height_pfp_right_target_source_productright_entry. fom_beta_height_pfp_right_target_source_productright_entry + S (fom_value_pfp_right_target_source_productright) = S ((S (fom_index_pfp_right_target_source_productright)) * dc)) /\ exists fom_beta_quotient_pfp_right_target_source_productright_entry. db = fom_beta_quotient_pfp_right_target_source_productright_entry * S ((S (fom_index_pfp_right_target_source_productright)) * dc) + (fom_value_pfp_right_target_source_productright))) /\ (exists fom_gap_pfp_right_target_source_productright_value_bound. fom_gap_pfp_right_target_source_productright_value_bound + S (fom_value_pfp_right_target_source_productright) = p))) /\ (((((((pfrd_qlen_right_target_source)=0 \/ (D)=0) /\ (((pfrd_plen_right_target_source)=0)))) \/ (((~((pfrd_qlen_right_target_source)=0)) /\ (((~((D)=0)) /\ (((pfrd_qlen_right_target_source)+(D)=S (pfrd_plen_right_target_source)))))))) /\ ((forall pfc_index_right_target_source_productcoefficients. (exists pfa_gap_right_target_source_productcoefficientsbound. pfa_gap_right_target_source_productcoefficientsbound + S (pfc_index_right_target_source_productcoefficients) = (pfrd_plen_right_target_source)) -> exists pfc_value_right_target_source_productcoefficients. ((((exists ff_h_pfp_right_target_source_productcoefficientsentry. ff_h_pfp_right_target_source_productcoefficientsentry + S (pfc_value_right_target_source_productcoefficients) = S ((S (pfc_index_right_target_source_productcoefficients)) * pfrd_pc_right_target_source)) /\ exists ff_q_pfp_right_target_source_productcoefficientsentry. pfrd_pb_right_target_source = ff_q_pfp_right_target_source_productcoefficientsentry * S ((S (pfc_index_right_target_source_productcoefficients)) * pfrd_pc_right_target_source) + (pfc_value_right_target_source_productcoefficients))) /\ ((exists pfc_terms_code_right_target_source_productcoefficientscoefficient pfc_terms_scale_right_target_source_productcoefficientscoefficient pfc_natural_sum_right_target_source_productcoefficientscoefficient. ((forall pfc_index_right_target_source_productcoefficientscoefficientdiagonal. (exists pfa_gap_right_target_source_productcoefficientscoefficientdiagonalbound. pfa_gap_right_target_source_productcoefficientscoefficientdiagonalbound + S (pfc_index_right_target_source_productcoefficientscoefficientdiagonal) = (S (pfc_index_right_target_source_productcoefficients))) -> exists pfc_value_right_target_source_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_right_target_source_productcoefficientscoefficientdiagonalentry. ff_h_pfp_right_target_source_productcoefficientscoefficientdiagonalentry + S (pfc_value_right_target_source_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_right_target_source_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_target_source_productcoefficientscoefficient)) /\ exists ff_q_pfp_right_target_source_productcoefficientscoefficientdiagonalentry. pfc_terms_code_right_target_source_productcoefficientscoefficient = ff_q_pfp_right_target_source_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_right_target_source_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_target_source_productcoefficientscoefficient) + (pfc_value_right_target_source_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_right_target_source_productcoefficientscoefficientdiagonalterm pfc_left_right_target_source_productcoefficientscoefficientdiagonalterm pfc_right_right_target_source_productcoefficientscoefficientdiagonalterm. (((pfc_index_right_target_source_productcoefficientscoefficientdiagonal)+pfc_complement_right_target_source_productcoefficientscoefficientdiagonalterm=(pfc_index_right_target_source_productcoefficients)) /\ ((((((exists pfa_gap_right_target_source_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_right_target_source_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_right_target_source_productcoefficientscoefficientdiagonal) = (pfrd_qlen_right_target_source)) /\ ((((exists ff_h_pfp_right_target_source_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_right_target_source_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_right_target_source_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_right_target_source_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_target_source)) /\ exists ff_q_pfp_right_target_source_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_right_target_source = ff_q_pfp_right_target_source_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_right_target_source_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_target_source) + (pfc_left_right_target_source_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_target_source_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_right_target_source_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_right_target_source)=(pfc_index_right_target_source_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_right_target_source_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_right_target_source_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_right_target_source_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_right_target_source_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_right_target_source_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_right_target_source_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_right_target_source_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_right_target_source_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_right_target_source_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_right_target_source_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_right_target_source_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_right_target_source_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_target_source_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_right_target_source_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_right_target_source_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_right_target_source_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_right_target_source_productcoefficientscoefficientdiagonal)=pfc_left_right_target_source_productcoefficientscoefficientdiagonalterm*pfc_right_right_target_source_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_right_target_source_productcoefficientscoefficientsum fs_v_pfc_right_target_source_productcoefficientscoefficientsum. ((((exists fs_h_pfc_right_target_source_productcoefficientscoefficientsum_body_start. fs_h_pfc_right_target_source_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_right_target_source_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_target_source_productcoefficientscoefficientsum_body_start. fs_u_pfc_right_target_source_productcoefficientscoefficientsum = fs_q_pfc_right_target_source_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_right_target_source_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_right_target_source_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_right_target_source_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_right_target_source_productcoefficientscoefficient) = S ((S (S (pfc_index_right_target_source_productcoefficients))) * fs_v_pfc_right_target_source_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_target_source_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_right_target_source_productcoefficientscoefficientsum = fs_q_pfc_right_target_source_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_right_target_source_productcoefficients))) * fs_v_pfc_right_target_source_productcoefficientscoefficientsum) + (pfc_natural_sum_right_target_source_productcoefficientscoefficient))) /\ forall fs_i_pfc_right_target_source_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_right_target_source_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_right_target_source_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_right_target_source_productcoefficientscoefficientsum_body_steps = S (pfc_index_right_target_source_productcoefficients)) -> exists fs_a_pfc_right_target_source_productcoefficientscoefficientsum_body_steps fs_r_pfc_right_target_source_productcoefficientscoefficientsum_body_steps fs_s_pfc_right_target_source_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_right_target_source_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_right_target_source_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_right_target_source_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_target_source_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_target_source_productcoefficientscoefficient)) /\ exists fs_q_pfc_right_target_source_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_right_target_source_productcoefficientscoefficient = fs_q_pfc_right_target_source_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_right_target_source_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_target_source_productcoefficientscoefficient) + (fs_a_pfc_right_target_source_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_target_source_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_right_target_source_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_right_target_source_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_target_source_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_target_source_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_target_source_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_right_target_source_productcoefficientscoefficientsum = fs_q_pfc_right_target_source_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_right_target_source_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_target_source_productcoefficientscoefficientsum) + (fs_r_pfc_right_target_source_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_target_source_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_right_target_source_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_right_target_source_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_right_target_source_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_target_source_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_target_source_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_right_target_source_productcoefficientscoefficientsum = fs_q_pfc_right_target_source_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_right_target_source_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_target_source_productcoefficientscoefficientsum) + (fs_s_pfc_right_target_source_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_right_target_source_productcoefficientscoefficientsum_body_steps = fs_r_pfc_right_target_source_productcoefficientscoefficientsum_body_steps + fs_a_pfc_right_target_source_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_right_target_source_productcoefficientscoefficientresiduebound. pfa_gap_right_target_source_productcoefficientscoefficientresiduebound + S (pfc_value_right_target_source_productcoefficients) = (p)) /\ ((exists pfa_offset_left_right_target_source_productcoefficientscoefficientresiduecongruence pfa_offset_right_right_target_source_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_right_target_source_productcoefficientscoefficient) + (p) * pfa_offset_left_right_target_source_productcoefficientscoefficientresiduecongruence = (pfc_value_right_target_source_productcoefficients) + (p) * pfa_offset_right_right_target_source_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_right_target_source_target pfrep_left_right_target_source_target pfrep_right_right_target_source_target. ((exists pfrep_position_right_target_source_targetfirst. ((pfrep_position_right_target_source_targetfirst+S (pfrep_power_right_target_source_target)=(pfrd_plen_right_target_source)) /\ ((((exists ff_h_pfp_right_target_source_targetfirstentry. ff_h_pfp_right_target_source_targetfirstentry + S (pfrep_left_right_target_source_target) = S ((S (pfrep_position_right_target_source_targetfirst)) * pfrd_pc_right_target_source)) /\ exists ff_q_pfp_right_target_source_targetfirstentry. pfrd_pb_right_target_source = ff_q_pfp_right_target_source_targetfirstentry * S ((S (pfrep_position_right_target_source_targetfirst)) * pfrd_pc_right_target_source) + (pfrep_left_right_target_source_target)))))) \/ (((exists pfrep_gap_right_target_source_targetfirstoutside. pfrep_gap_right_target_source_targetfirstoutside+(pfrd_plen_right_target_source)=(pfrep_power_right_target_source_target)) /\ (((pfrep_left_right_target_source_target)=0))))) -> ((exists pfrep_position_right_target_source_targetsecond. ((pfrep_position_right_target_source_targetsecond+S (pfrep_power_right_target_source_target)=(L)) /\ ((((exists ff_h_pfp_right_target_source_targetsecondentry. ff_h_pfp_right_target_source_targetsecondentry + S (pfrep_right_right_target_source_target) = S ((S (pfrep_position_right_target_source_targetsecond)) * ac)) /\ exists ff_q_pfp_right_target_source_targetsecondentry. ab = ff_q_pfp_right_target_source_targetsecondentry * S ((S (pfrep_position_right_target_source_targetsecond)) * ac) + (pfrep_right_right_target_source_target)))))) \/ (((exists pfrep_gap_right_target_source_targetsecondoutside. pfrep_gap_right_target_source_targetsecondoutside+(L)=(pfrep_power_right_target_source_target)) /\ (((pfrep_right_right_target_source_target)=0))))) -> pfrep_left_right_target_source_target=pfrep_right_right_target_source_target))))))) -> (forall pfrep_power_right_target_equivalent pfrep_left_right_target_equivalent pfrep_right_right_target_equivalent. ((exists pfrep_position_right_target_equivalentfirst. ((pfrep_position_right_target_equivalentfirst+S (pfrep_power_right_target_equivalent)=(L)) /\ ((((exists ff_h_pfp_right_target_equivalentfirstentry. ff_h_pfp_right_target_equivalentfirstentry + S (pfrep_left_right_target_equivalent) = S ((S (pfrep_position_right_target_equivalentfirst)) * ac)) /\ exists ff_q_pfp_right_target_equivalentfirstentry. ab = ff_q_pfp_right_target_equivalentfirstentry * S ((S (pfrep_position_right_target_equivalentfirst)) * ac) + (pfrep_left_right_target_equivalent)))))) \/ (((exists pfrep_gap_right_target_equivalentfirstoutside. pfrep_gap_right_target_equivalentfirstoutside+(L)=(pfrep_power_right_target_equivalent)) /\ (((pfrep_left_right_target_equivalent)=0))))) -> ((exists pfrep_position_right_target_equivalentsecond. ((pfrep_position_right_target_equivalentsecond+S (pfrep_power_right_target_equivalent)=(M)) /\ ((((exists ff_h_pfp_right_target_equivalentsecondentry. ff_h_pfp_right_target_equivalentsecondentry + S (pfrep_right_right_target_equivalent) = S ((S (pfrep_position_right_target_equivalentsecond)) * bc)) /\ exists ff_q_pfp_right_target_equivalentsecondentry. bb = ff_q_pfp_right_target_equivalentsecondentry * S ((S (pfrep_position_right_target_equivalentsecond)) * bc) + (pfrep_right_right_target_equivalent)))))) \/ (((exists pfrep_gap_right_target_equivalentsecondoutside. pfrep_gap_right_target_equivalentsecondoutside+(M)=(pfrep_power_right_target_equivalent)) /\ (((pfrep_right_right_target_equivalent)=0))))) -> pfrep_left_right_target_equivalent=pfrep_right_right_target_equivalent) -> (((forall fom_index_pfp_right_target_result_canonical. (exists fom_gap_pfp_right_target_result_canonical_index_bound. fom_gap_pfp_right_target_result_canonical_index_bound + S (fom_index_pfp_right_target_result_canonical) = M) -> exists fom_value_pfp_right_target_result_canonical. ((((exists fom_beta_height_pfp_right_target_result_canonical_entry. fom_beta_height_pfp_right_target_result_canonical_entry + S (fom_value_pfp_right_target_result_canonical) = S ((S (fom_index_pfp_right_target_result_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_right_target_result_canonical_entry. bb = fom_beta_quotient_pfp_right_target_result_canonical_entry * S ((S (fom_index_pfp_right_target_result_canonical)) * bc) + (fom_value_pfp_right_target_result_canonical))) /\ (exists fom_gap_pfp_right_target_result_canonical_value_bound. fom_gap_pfp_right_target_result_canonical_value_bound + S (fom_value_pfp_right_target_result_canonical) = p))) /\ ((exists pfrd_qb_right_target_result pfrd_qc_right_target_result pfrd_qlen_right_target_result pfrd_pb_right_target_result pfrd_pc_right_target_result pfrd_plen_right_target_result. ((((forall fom_index_pfp_right_target_result_productleft. (exists fom_gap_pfp_right_target_result_productleft_index_bound. fom_gap_pfp_right_target_result_productleft_index_bound + S (fom_index_pfp_right_target_result_productleft) = pfrd_qlen_right_target_result) -> exists fom_value_pfp_right_target_result_productleft. ((((exists fom_beta_height_pfp_right_target_result_productleft_entry. fom_beta_height_pfp_right_target_result_productleft_entry + S (fom_value_pfp_right_target_result_productleft) = S ((S (fom_index_pfp_right_target_result_productleft)) * pfrd_qc_right_target_result)) /\ exists fom_beta_quotient_pfp_right_target_result_productleft_entry. pfrd_qb_right_target_result = fom_beta_quotient_pfp_right_target_result_productleft_entry * S ((S (fom_index_pfp_right_target_result_productleft)) * pfrd_qc_right_target_result) + (fom_value_pfp_right_target_result_productleft))) /\ (exists fom_gap_pfp_right_target_result_productleft_value_bound. fom_gap_pfp_right_target_result_productleft_value_bound + S (fom_value_pfp_right_target_result_productleft) = p))) /\ (((forall fom_index_pfp_right_target_result_productright. (exists fom_gap_pfp_right_target_result_productright_index_bound. fom_gap_pfp_right_target_result_productright_index_bound + S (fom_index_pfp_right_target_result_productright) = D) -> exists fom_value_pfp_right_target_result_productright. ((((exists fom_beta_height_pfp_right_target_result_productright_entry. fom_beta_height_pfp_right_target_result_productright_entry + S (fom_value_pfp_right_target_result_productright) = S ((S (fom_index_pfp_right_target_result_productright)) * dc)) /\ exists fom_beta_quotient_pfp_right_target_result_productright_entry. db = fom_beta_quotient_pfp_right_target_result_productright_entry * S ((S (fom_index_pfp_right_target_result_productright)) * dc) + (fom_value_pfp_right_target_result_productright))) /\ (exists fom_gap_pfp_right_target_result_productright_value_bound. fom_gap_pfp_right_target_result_productright_value_bound + S (fom_value_pfp_right_target_result_productright) = p))) /\ (((((((pfrd_qlen_right_target_result)=0 \/ (D)=0) /\ (((pfrd_plen_right_target_result)=0)))) \/ (((~((pfrd_qlen_right_target_result)=0)) /\ (((~((D)=0)) /\ (((pfrd_qlen_right_target_result)+(D)=S (pfrd_plen_right_target_result)))))))) /\ ((forall pfc_index_right_target_result_productcoefficients. (exists pfa_gap_right_target_result_productcoefficientsbound. pfa_gap_right_target_result_productcoefficientsbound + S (pfc_index_right_target_result_productcoefficients) = (pfrd_plen_right_target_result)) -> exists pfc_value_right_target_result_productcoefficients. ((((exists ff_h_pfp_right_target_result_productcoefficientsentry. ff_h_pfp_right_target_result_productcoefficientsentry + S (pfc_value_right_target_result_productcoefficients) = S ((S (pfc_index_right_target_result_productcoefficients)) * pfrd_pc_right_target_result)) /\ exists ff_q_pfp_right_target_result_productcoefficientsentry. pfrd_pb_right_target_result = ff_q_pfp_right_target_result_productcoefficientsentry * S ((S (pfc_index_right_target_result_productcoefficients)) * pfrd_pc_right_target_result) + (pfc_value_right_target_result_productcoefficients))) /\ ((exists pfc_terms_code_right_target_result_productcoefficientscoefficient pfc_terms_scale_right_target_result_productcoefficientscoefficient pfc_natural_sum_right_target_result_productcoefficientscoefficient. ((forall pfc_index_right_target_result_productcoefficientscoefficientdiagonal. (exists pfa_gap_right_target_result_productcoefficientscoefficientdiagonalbound. pfa_gap_right_target_result_productcoefficientscoefficientdiagonalbound + S (pfc_index_right_target_result_productcoefficientscoefficientdiagonal) = (S (pfc_index_right_target_result_productcoefficients))) -> exists pfc_value_right_target_result_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_right_target_result_productcoefficientscoefficientdiagonalentry. ff_h_pfp_right_target_result_productcoefficientscoefficientdiagonalentry + S (pfc_value_right_target_result_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_right_target_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_target_result_productcoefficientscoefficient)) /\ exists ff_q_pfp_right_target_result_productcoefficientscoefficientdiagonalentry. pfc_terms_code_right_target_result_productcoefficientscoefficient = ff_q_pfp_right_target_result_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_right_target_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_target_result_productcoefficientscoefficient) + (pfc_value_right_target_result_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_right_target_result_productcoefficientscoefficientdiagonalterm pfc_left_right_target_result_productcoefficientscoefficientdiagonalterm pfc_right_right_target_result_productcoefficientscoefficientdiagonalterm. (((pfc_index_right_target_result_productcoefficientscoefficientdiagonal)+pfc_complement_right_target_result_productcoefficientscoefficientdiagonalterm=(pfc_index_right_target_result_productcoefficients)) /\ ((((((exists pfa_gap_right_target_result_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_right_target_result_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_right_target_result_productcoefficientscoefficientdiagonal) = (pfrd_qlen_right_target_result)) /\ ((((exists ff_h_pfp_right_target_result_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_right_target_result_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_right_target_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_right_target_result_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_target_result)) /\ exists ff_q_pfp_right_target_result_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_right_target_result = ff_q_pfp_right_target_result_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_right_target_result_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_target_result) + (pfc_left_right_target_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_target_result_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_right_target_result_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_right_target_result)=(pfc_index_right_target_result_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_right_target_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_right_target_result_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_right_target_result_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_right_target_result_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_right_target_result_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_right_target_result_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_right_target_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_right_target_result_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_right_target_result_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_right_target_result_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_right_target_result_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_right_target_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_target_result_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_right_target_result_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_right_target_result_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_right_target_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_right_target_result_productcoefficientscoefficientdiagonal)=pfc_left_right_target_result_productcoefficientscoefficientdiagonalterm*pfc_right_right_target_result_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_right_target_result_productcoefficientscoefficientsum fs_v_pfc_right_target_result_productcoefficientscoefficientsum. ((((exists fs_h_pfc_right_target_result_productcoefficientscoefficientsum_body_start. fs_h_pfc_right_target_result_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_right_target_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_target_result_productcoefficientscoefficientsum_body_start. fs_u_pfc_right_target_result_productcoefficientscoefficientsum = fs_q_pfc_right_target_result_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_right_target_result_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_right_target_result_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_right_target_result_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_right_target_result_productcoefficientscoefficient) = S ((S (S (pfc_index_right_target_result_productcoefficients))) * fs_v_pfc_right_target_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_target_result_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_right_target_result_productcoefficientscoefficientsum = fs_q_pfc_right_target_result_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_right_target_result_productcoefficients))) * fs_v_pfc_right_target_result_productcoefficientscoefficientsum) + (pfc_natural_sum_right_target_result_productcoefficientscoefficient))) /\ forall fs_i_pfc_right_target_result_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_right_target_result_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_right_target_result_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_right_target_result_productcoefficientscoefficientsum_body_steps = S (pfc_index_right_target_result_productcoefficients)) -> exists fs_a_pfc_right_target_result_productcoefficientscoefficientsum_body_steps fs_r_pfc_right_target_result_productcoefficientscoefficientsum_body_steps fs_s_pfc_right_target_result_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_right_target_result_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_right_target_result_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_right_target_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_target_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_target_result_productcoefficientscoefficient)) /\ exists fs_q_pfc_right_target_result_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_right_target_result_productcoefficientscoefficient = fs_q_pfc_right_target_result_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_right_target_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_target_result_productcoefficientscoefficient) + (fs_a_pfc_right_target_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_target_result_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_right_target_result_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_right_target_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_target_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_target_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_target_result_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_right_target_result_productcoefficientscoefficientsum = fs_q_pfc_right_target_result_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_right_target_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_target_result_productcoefficientscoefficientsum) + (fs_r_pfc_right_target_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_target_result_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_right_target_result_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_right_target_result_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_right_target_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_target_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_target_result_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_right_target_result_productcoefficientscoefficientsum = fs_q_pfc_right_target_result_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_right_target_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_target_result_productcoefficientscoefficientsum) + (fs_s_pfc_right_target_result_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_right_target_result_productcoefficientscoefficientsum_body_steps = fs_r_pfc_right_target_result_productcoefficientscoefficientsum_body_steps + fs_a_pfc_right_target_result_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_right_target_result_productcoefficientscoefficientresiduebound. pfa_gap_right_target_result_productcoefficientscoefficientresiduebound + S (pfc_value_right_target_result_productcoefficients) = (p)) /\ ((exists pfa_offset_left_right_target_result_productcoefficientscoefficientresiduecongruence pfa_offset_right_right_target_result_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_right_target_result_productcoefficientscoefficient) + (p) * pfa_offset_left_right_target_result_productcoefficientscoefficientresiduecongruence = (pfc_value_right_target_result_productcoefficients) + (p) * pfa_offset_right_right_target_result_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_right_target_result_target pfrep_left_right_target_result_target pfrep_right_right_target_result_target. ((exists pfrep_position_right_target_result_targetfirst. ((pfrep_position_right_target_result_targetfirst+S (pfrep_power_right_target_result_target)=(pfrd_plen_right_target_result)) /\ ((((exists ff_h_pfp_right_target_result_targetfirstentry. ff_h_pfp_right_target_result_targetfirstentry + S (pfrep_left_right_target_result_target) = S ((S (pfrep_position_right_target_result_targetfirst)) * pfrd_pc_right_target_result)) /\ exists ff_q_pfp_right_target_result_targetfirstentry. pfrd_pb_right_target_result = ff_q_pfp_right_target_result_targetfirstentry * S ((S (pfrep_position_right_target_result_targetfirst)) * pfrd_pc_right_target_result) + (pfrep_left_right_target_result_target)))))) \/ (((exists pfrep_gap_right_target_result_targetfirstoutside. pfrep_gap_right_target_result_targetfirstoutside+(pfrd_plen_right_target_result)=(pfrep_power_right_target_result_target)) /\ (((pfrep_left_right_target_result_target)=0))))) -> ((exists pfrep_position_right_target_result_targetsecond. ((pfrep_position_right_target_result_targetsecond+S (pfrep_power_right_target_result_target)=(M)) /\ ((((exists ff_h_pfp_right_target_result_targetsecondentry. ff_h_pfp_right_target_result_targetsecondentry + S (pfrep_right_right_target_result_target) = S ((S (pfrep_position_right_target_result_targetsecond)) * bc)) /\ exists ff_q_pfp_right_target_result_targetsecondentry. bb = ff_q_pfp_right_target_result_targetsecondentry * S ((S (pfrep_position_right_target_result_targetsecond)) * bc) + (pfrep_right_right_target_result_target)))))) \/ (((exists pfrep_gap_right_target_result_targetsecondoutside. pfrep_gap_right_target_result_targetsecondoutside+(M)=(pfrep_power_right_target_result_target)) /\ (((pfrep_right_right_target_result_target)=0))))) -> pfrep_left_right_target_result_target=pfrep_right_right_target_result_target)))))))

Complete tactic proof in conservative notation

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

49 script commands · 6 reading checkpoints · 0 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 right divides from product
01Fix variables and assumptionsL1–10

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 D
  5. L5
    intro ab
  6. L6
    intro ac
  7. L7
    intro L
  8. L8
    intro bb
  9. L9
    intro bc
  10. L10
    intro M
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hB
  2. L12
    intro hdivides
  3. L13
    intro hequivalent
03Separate the logical casesL14–21

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

  1. L14
    cases hdivides
  2. L15
    cases hdivides_right
  3. L16
    cases hdivides_right_witness
  4. L17
    cases hdivides_right_witness_witness
  5. L18
    cases hdivides_right_witness_witness_witness
  6. L19
    cases hdivides_right_witness_witness_witness_witness
  7. L20
    cases hdivides_right_witness_witness_witness_witness_witness
  8. L21
    cases hdivides_right_witness_witness_witness_witness_witness_witness
04Use earlier factsL22–31

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

  1. L22
    specialize prime_field_polynomial_right_divides_from_product (p)
  2. L23
    specialize prime_field_polynomial_right_divides_from_product (db)
  3. L24
    specialize prime_field_polynomial_right_divides_from_product (dc)
  4. L25
    specialize prime_field_polynomial_right_divides_from_product (D)
  5. L26
    specialize prime_field_polynomial_right_divides_from_product (bb)
  6. L27
    specialize prime_field_polynomial_right_divides_from_product (bc)
  7. L28
    specialize prime_field_polynomial_right_divides_from_product (M)
  8. L29
    specialize prime_field_polynomial_right_divides_from_product (x)
  9. L30
    specialize prime_field_polynomial_right_divides_from_product (x1)
  10. L31
    specialize prime_field_polynomial_right_divides_from_product (x2)
05Use earlier factsL32–41

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

  1. L32
    specialize prime_field_polynomial_right_divides_from_product (x3)
  2. L33
    specialize prime_field_polynomial_right_divides_from_product (x4)
  3. L34
    specialize prime_field_polynomial_right_divides_from_product (x5)
  4. L35
    apply prime_field_polynomial_right_divides_from_product
  5. L36
    exact hB
  6. L37
    exact hdivides_right_witness_witness_witness_witness_witness_witness_left
  7. L38
    specialize prime_field_polynomial_equivalent_transitive (x3)
  8. L39
    specialize prime_field_polynomial_equivalent_transitive (x4)
  9. L40
    specialize prime_field_polynomial_equivalent_transitive (x5)
  10. L41
    specialize prime_field_polynomial_equivalent_transitive (ab)
06Use earlier factsL42–49

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

  1. L42
    specialize prime_field_polynomial_equivalent_transitive (ac)
  2. L43
    specialize prime_field_polynomial_equivalent_transitive (L)
  3. L44
    specialize prime_field_polynomial_equivalent_transitive (bb)
  4. L45
    specialize prime_field_polynomial_equivalent_transitive (bc)
  5. L46
    specialize prime_field_polynomial_equivalent_transitive (M)
  6. L47
    apply prime_field_polynomial_equivalent_transitive
  7. L48
    exact hdivides_right_witness_witness_witness_witness_witness_witness_right
  8. L49
    exact hequivalent

Library-wide reading audit

Original defined command ledger · 49 lines
  1. 0001intro p
  2. 0002intro db
  3. 0003intro dc
  4. 0004intro D
  5. 0005intro ab
  6. 0006intro ac
  7. 0007intro L
  8. 0008intro bb
  9. 0009intro bc
  10. 0010intro M
  11. 0011intro hB
  12. 0012intro hdivides
  13. 0013intro hequivalent
  14. 0014cases hdivides
  15. 0015cases hdivides_right
  16. 0016cases hdivides_right_witness
  17. 0017cases hdivides_right_witness_witness
  18. 0018cases hdivides_right_witness_witness_witness
  19. 0019cases hdivides_right_witness_witness_witness_witness
  20. 0020cases hdivides_right_witness_witness_witness_witness_witness
  21. 0021cases hdivides_right_witness_witness_witness_witness_witness_witness
  22. 0022specialize prime_field_polynomial_right_divides_from_product (p)
  23. 0023specialize prime_field_polynomial_right_divides_from_product (db)
  24. 0024specialize prime_field_polynomial_right_divides_from_product (dc)
  25. 0025specialize prime_field_polynomial_right_divides_from_product (D)
  26. 0026specialize prime_field_polynomial_right_divides_from_product (bb)
  27. 0027specialize prime_field_polynomial_right_divides_from_product (bc)
  28. 0028specialize prime_field_polynomial_right_divides_from_product (M)
  29. 0029specialize prime_field_polynomial_right_divides_from_product (x)
  30. 0030specialize prime_field_polynomial_right_divides_from_product (x1)
  31. 0031specialize prime_field_polynomial_right_divides_from_product (x2)
  32. 0032specialize prime_field_polynomial_right_divides_from_product (x3)
  33. 0033specialize prime_field_polynomial_right_divides_from_product (x4)
  34. 0034specialize prime_field_polynomial_right_divides_from_product (x5)
  35. 0035apply prime_field_polynomial_right_divides_from_product
  36. 0036exact hB
  37. 0037exact hdivides_right_witness_witness_witness_witness_witness_witness_left
  38. 0038specialize prime_field_polynomial_equivalent_transitive (x3)
  39. 0039specialize prime_field_polynomial_equivalent_transitive (x4)
  40. 0040specialize prime_field_polynomial_equivalent_transitive (x5)
  41. 0041specialize prime_field_polynomial_equivalent_transitive (ab)
  42. 0042specialize prime_field_polynomial_equivalent_transitive (ac)
  43. 0043specialize prime_field_polynomial_equivalent_transitive (L)
  44. 0044specialize prime_field_polynomial_equivalent_transitive (bb)
  45. 0045specialize prime_field_polynomial_equivalent_transitive (bc)
  46. 0046specialize prime_field_polynomial_equivalent_transitive (M)
  47. 0047apply prime_field_polynomial_equivalent_transitive
  48. 0048exact hdivides_right_witness_witness_witness_witness_witness_witness_right
  49. 0049exact hequivalent