PG0055

prime_field_polynomial_scale_implies_right_divides

A genuine scalar output is a right multiple of its source: construct an actual LEFT singleton quotient and actual product, then transport the independently encoded product to the supplied target by decoded-prefix equality. Empty inputs and scalar zero are included.

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. ∀ k. ∀ ab. ∀ ac. ∀ hb. ∀ hc. ∀ L. Prime(p) → FpPolyScale(p,k,ab,ac,hb,hc,L) → FpPolynomialRightDivides(p,ab,ac,L,hb,hc,L)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 3BetaPrefixEqual(b,c,d,e,l) · 1FpPolyScale(p,k,ab,ac,bb,bc,l) · 3FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 1FpPolynomialRightDivides(p,db,dc,D,ab,ac,L) · 1Prime(p) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

prime_field_polynomial_scale_bounded · checked external prerequisiteprime_field_polynomial_left_constant_product_existsprime_field_polynomial_scale_functional · checked external prerequisiteprime_field_polynomial_right_divides_from_productprime_field_polynomial_equal_implies_equivalent · checked external prerequisite
Original expanded first-order statement 
forall p k ab ac hb hc L. (~((p) = 1) /\ forall pfa_factor_left_normalization_scale_prime pfa_factor_right_normalization_scale_prime. (p) = pfa_factor_left_normalization_scale_prime * pfa_factor_right_normalization_scale_prime -> pfa_factor_left_normalization_scale_prime = 1 \/ pfa_factor_right_normalization_scale_prime = 1) -> (((exists pfa_gap_normalization_scale_sourcescalar. pfa_gap_normalization_scale_sourcescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_scale_source. (exists pfa_gap_normalization_scale_sourceindex. pfa_gap_normalization_scale_sourceindex + S (pfp_index_normalization_scale_source) = (L)) -> exists pfp_source_normalization_scale_source pfp_value_normalization_scale_source. ((((exists ff_h_pfp_normalization_scale_sourcesource. ff_h_pfp_normalization_scale_sourcesource + S (pfp_source_normalization_scale_source) = S ((S (pfp_index_normalization_scale_source)) * ac)) /\ exists ff_q_pfp_normalization_scale_sourcesource. ab = ff_q_pfp_normalization_scale_sourcesource * S ((S (pfp_index_normalization_scale_source)) * ac) + (pfp_source_normalization_scale_source))) /\ (((((exists ff_h_pfp_normalization_scale_sourcetarget. ff_h_pfp_normalization_scale_sourcetarget + S (pfp_value_normalization_scale_source) = S ((S (pfp_index_normalization_scale_source)) * hc)) /\ exists ff_q_pfp_normalization_scale_sourcetarget. hb = ff_q_pfp_normalization_scale_sourcetarget * S ((S (pfp_index_normalization_scale_source)) * hc) + (pfp_value_normalization_scale_source))) /\ ((((exists pfa_gap_normalization_scale_sourceoperationleft. pfa_gap_normalization_scale_sourceoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_scale_sourceoperationright. pfa_gap_normalization_scale_sourceoperationright + S (pfp_source_normalization_scale_source) = (p)) /\ ((((exists pfa_gap_normalization_scale_sourceoperationresultbound. pfa_gap_normalization_scale_sourceoperationresultbound + S (pfp_value_normalization_scale_source) = (p)) /\ ((exists pfa_offset_left_normalization_scale_sourceoperationresultcongruence pfa_offset_right_normalization_scale_sourceoperationresultcongruence. ((k) * (pfp_source_normalization_scale_source)) + (p) * pfa_offset_left_normalization_scale_sourceoperationresultcongruence = (pfp_value_normalization_scale_source) + (p) * pfa_offset_right_normalization_scale_sourceoperationresultcongruence))))))))))))))))) -> (((forall fom_index_pfp_normalization_scale_divides_canonical. (exists fom_gap_pfp_normalization_scale_divides_canonical_index_bound. fom_gap_pfp_normalization_scale_divides_canonical_index_bound + S (fom_index_pfp_normalization_scale_divides_canonical) = L) -> exists fom_value_pfp_normalization_scale_divides_canonical. ((((exists fom_beta_height_pfp_normalization_scale_divides_canonical_entry. fom_beta_height_pfp_normalization_scale_divides_canonical_entry + S (fom_value_pfp_normalization_scale_divides_canonical) = S ((S (fom_index_pfp_normalization_scale_divides_canonical)) * hc)) /\ exists fom_beta_quotient_pfp_normalization_scale_divides_canonical_entry. hb = fom_beta_quotient_pfp_normalization_scale_divides_canonical_entry * S ((S (fom_index_pfp_normalization_scale_divides_canonical)) * hc) + (fom_value_pfp_normalization_scale_divides_canonical))) /\ (exists fom_gap_pfp_normalization_scale_divides_canonical_value_bound. fom_gap_pfp_normalization_scale_divides_canonical_value_bound + S (fom_value_pfp_normalization_scale_divides_canonical) = p))) /\ ((exists pfen_qb_normalization_scale_divides pfen_qc_normalization_scale_divides pfen_qlen_normalization_scale_divides pfen_pb_normalization_scale_divides pfen_pc_normalization_scale_divides pfen_plen_normalization_scale_divides. ((((forall fom_index_pfp_normalization_scale_divides_productleft. (exists fom_gap_pfp_normalization_scale_divides_productleft_index_bound. fom_gap_pfp_normalization_scale_divides_productleft_index_bound + S (fom_index_pfp_normalization_scale_divides_productleft) = pfen_qlen_normalization_scale_divides) -> exists fom_value_pfp_normalization_scale_divides_productleft. ((((exists fom_beta_height_pfp_normalization_scale_divides_productleft_entry. fom_beta_height_pfp_normalization_scale_divides_productleft_entry + S (fom_value_pfp_normalization_scale_divides_productleft) = S ((S (fom_index_pfp_normalization_scale_divides_productleft)) * pfen_qc_normalization_scale_divides)) /\ exists fom_beta_quotient_pfp_normalization_scale_divides_productleft_entry. pfen_qb_normalization_scale_divides = fom_beta_quotient_pfp_normalization_scale_divides_productleft_entry * S ((S (fom_index_pfp_normalization_scale_divides_productleft)) * pfen_qc_normalization_scale_divides) + (fom_value_pfp_normalization_scale_divides_productleft))) /\ (exists fom_gap_pfp_normalization_scale_divides_productleft_value_bound. fom_gap_pfp_normalization_scale_divides_productleft_value_bound + S (fom_value_pfp_normalization_scale_divides_productleft) = p))) /\ (((forall fom_index_pfp_normalization_scale_divides_productright. (exists fom_gap_pfp_normalization_scale_divides_productright_index_bound. fom_gap_pfp_normalization_scale_divides_productright_index_bound + S (fom_index_pfp_normalization_scale_divides_productright) = L) -> exists fom_value_pfp_normalization_scale_divides_productright. ((((exists fom_beta_height_pfp_normalization_scale_divides_productright_entry. fom_beta_height_pfp_normalization_scale_divides_productright_entry + S (fom_value_pfp_normalization_scale_divides_productright) = S ((S (fom_index_pfp_normalization_scale_divides_productright)) * ac)) /\ exists fom_beta_quotient_pfp_normalization_scale_divides_productright_entry. ab = fom_beta_quotient_pfp_normalization_scale_divides_productright_entry * S ((S (fom_index_pfp_normalization_scale_divides_productright)) * ac) + (fom_value_pfp_normalization_scale_divides_productright))) /\ (exists fom_gap_pfp_normalization_scale_divides_productright_value_bound. fom_gap_pfp_normalization_scale_divides_productright_value_bound + S (fom_value_pfp_normalization_scale_divides_productright) = p))) /\ (((((((pfen_qlen_normalization_scale_divides)=0 \/ (L)=0) /\ (((pfen_plen_normalization_scale_divides)=0)))) \/ (((~((pfen_qlen_normalization_scale_divides)=0)) /\ (((~((L)=0)) /\ (((pfen_qlen_normalization_scale_divides)+(L)=S (pfen_plen_normalization_scale_divides)))))))) /\ ((forall pfc_index_normalization_scale_divides_productcoefficients. (exists pfa_gap_normalization_scale_divides_productcoefficientsbound. pfa_gap_normalization_scale_divides_productcoefficientsbound + S (pfc_index_normalization_scale_divides_productcoefficients) = (pfen_plen_normalization_scale_divides)) -> exists pfc_value_normalization_scale_divides_productcoefficients. ((((exists ff_h_pfp_normalization_scale_divides_productcoefficientsentry. ff_h_pfp_normalization_scale_divides_productcoefficientsentry + S (pfc_value_normalization_scale_divides_productcoefficients) = S ((S (pfc_index_normalization_scale_divides_productcoefficients)) * pfen_pc_normalization_scale_divides)) /\ exists ff_q_pfp_normalization_scale_divides_productcoefficientsentry. pfen_pb_normalization_scale_divides = ff_q_pfp_normalization_scale_divides_productcoefficientsentry * S ((S (pfc_index_normalization_scale_divides_productcoefficients)) * pfen_pc_normalization_scale_divides) + (pfc_value_normalization_scale_divides_productcoefficients))) /\ ((exists pfc_terms_code_normalization_scale_divides_productcoefficientscoefficient pfc_terms_scale_normalization_scale_divides_productcoefficientscoefficient pfc_natural_sum_normalization_scale_divides_productcoefficientscoefficient. ((forall pfc_index_normalization_scale_divides_productcoefficientscoefficientdiagonal. (exists pfa_gap_normalization_scale_divides_productcoefficientscoefficientdiagonalbound. pfa_gap_normalization_scale_divides_productcoefficientscoefficientdiagonalbound + S (pfc_index_normalization_scale_divides_productcoefficientscoefficientdiagonal) = (S (pfc_index_normalization_scale_divides_productcoefficients))) -> exists pfc_value_normalization_scale_divides_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalization_scale_divides_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normalization_scale_divides_productcoefficientscoefficientdiagonalentry + S (pfc_value_normalization_scale_divides_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalization_scale_divides_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalization_scale_divides_productcoefficientscoefficient)) /\ exists ff_q_pfp_normalization_scale_divides_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normalization_scale_divides_productcoefficientscoefficient = ff_q_pfp_normalization_scale_divides_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalization_scale_divides_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalization_scale_divides_productcoefficientscoefficient) + (pfc_value_normalization_scale_divides_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalization_scale_divides_productcoefficientscoefficientdiagonalterm pfc_left_normalization_scale_divides_productcoefficientscoefficientdiagonalterm pfc_right_normalization_scale_divides_productcoefficientscoefficientdiagonalterm. (((pfc_index_normalization_scale_divides_productcoefficientscoefficientdiagonal)+pfc_complement_normalization_scale_divides_productcoefficientscoefficientdiagonalterm=(pfc_index_normalization_scale_divides_productcoefficients)) /\ ((((((exists pfa_gap_normalization_scale_divides_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalization_scale_divides_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalization_scale_divides_productcoefficientscoefficientdiagonal) = (pfen_qlen_normalization_scale_divides)) /\ ((((exists ff_h_pfp_normalization_scale_divides_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalization_scale_divides_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalization_scale_divides_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalization_scale_divides_productcoefficientscoefficientdiagonal)) * pfen_qc_normalization_scale_divides)) /\ exists ff_q_pfp_normalization_scale_divides_productcoefficientscoefficientdiagonaltermleftentry. pfen_qb_normalization_scale_divides = ff_q_pfp_normalization_scale_divides_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalization_scale_divides_productcoefficientscoefficientdiagonal)) * pfen_qc_normalization_scale_divides) + (pfc_left_normalization_scale_divides_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalization_scale_divides_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalization_scale_divides_productcoefficientscoefficientdiagonaltermleftoutside+(pfen_qlen_normalization_scale_divides)=(pfc_index_normalization_scale_divides_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalization_scale_divides_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalization_scale_divides_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalization_scale_divides_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalization_scale_divides_productcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_normalization_scale_divides_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalization_scale_divides_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalization_scale_divides_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalization_scale_divides_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_normalization_scale_divides_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_normalization_scale_divides_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalization_scale_divides_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_normalization_scale_divides_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalization_scale_divides_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalization_scale_divides_productcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_normalization_scale_divides_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalization_scale_divides_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalization_scale_divides_productcoefficientscoefficientdiagonal)=pfc_left_normalization_scale_divides_productcoefficientscoefficientdiagonalterm*pfc_right_normalization_scale_divides_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalization_scale_divides_productcoefficientscoefficientsum fs_v_pfc_normalization_scale_divides_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_start. fs_h_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalization_scale_divides_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_start. fs_u_pfc_normalization_scale_divides_productcoefficientscoefficientsum = fs_q_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalization_scale_divides_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalization_scale_divides_productcoefficientscoefficient) = S ((S (S (pfc_index_normalization_scale_divides_productcoefficients))) * fs_v_pfc_normalization_scale_divides_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalization_scale_divides_productcoefficientscoefficientsum = fs_q_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalization_scale_divides_productcoefficients))) * fs_v_pfc_normalization_scale_divides_productcoefficientscoefficientsum) + (pfc_natural_sum_normalization_scale_divides_productcoefficientscoefficient))) /\ forall fs_i_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps = S (pfc_index_normalization_scale_divides_productcoefficients)) -> exists fs_a_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps fs_r_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps fs_s_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalization_scale_divides_productcoefficientscoefficient)) /\ exists fs_q_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalization_scale_divides_productcoefficientscoefficient = fs_q_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalization_scale_divides_productcoefficientscoefficient) + (fs_a_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_scale_divides_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalization_scale_divides_productcoefficientscoefficientsum = fs_q_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_scale_divides_productcoefficientscoefficientsum) + (fs_r_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_scale_divides_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalization_scale_divides_productcoefficientscoefficientsum = fs_q_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_scale_divides_productcoefficientscoefficientsum) + (fs_s_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normalization_scale_divides_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalization_scale_divides_productcoefficientscoefficientresiduebound. pfa_gap_normalization_scale_divides_productcoefficientscoefficientresiduebound + S (pfc_value_normalization_scale_divides_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normalization_scale_divides_productcoefficientscoefficientresiduecongruence pfa_offset_right_normalization_scale_divides_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalization_scale_divides_productcoefficientscoefficient) + (p) * pfa_offset_left_normalization_scale_divides_productcoefficientscoefficientresiduecongruence = (pfc_value_normalization_scale_divides_productcoefficients) + (p) * pfa_offset_right_normalization_scale_divides_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normalization_scale_divides_target pfrep_left_normalization_scale_divides_target pfrep_right_normalization_scale_divides_target. ((exists pfrep_position_normalization_scale_divides_targetfirst. ((pfrep_position_normalization_scale_divides_targetfirst+S (pfrep_power_normalization_scale_divides_target)=(pfen_plen_normalization_scale_divides)) /\ ((((exists ff_h_pfp_normalization_scale_divides_targetfirstentry. ff_h_pfp_normalization_scale_divides_targetfirstentry + S (pfrep_left_normalization_scale_divides_target) = S ((S (pfrep_position_normalization_scale_divides_targetfirst)) * pfen_pc_normalization_scale_divides)) /\ exists ff_q_pfp_normalization_scale_divides_targetfirstentry. pfen_pb_normalization_scale_divides = ff_q_pfp_normalization_scale_divides_targetfirstentry * S ((S (pfrep_position_normalization_scale_divides_targetfirst)) * pfen_pc_normalization_scale_divides) + (pfrep_left_normalization_scale_divides_target)))))) \/ (((exists pfrep_gap_normalization_scale_divides_targetfirstoutside. pfrep_gap_normalization_scale_divides_targetfirstoutside+(pfen_plen_normalization_scale_divides)=(pfrep_power_normalization_scale_divides_target)) /\ (((pfrep_left_normalization_scale_divides_target)=0))))) -> ((exists pfrep_position_normalization_scale_divides_targetsecond. ((pfrep_position_normalization_scale_divides_targetsecond+S (pfrep_power_normalization_scale_divides_target)=(L)) /\ ((((exists ff_h_pfp_normalization_scale_divides_targetsecondentry. ff_h_pfp_normalization_scale_divides_targetsecondentry + S (pfrep_right_normalization_scale_divides_target) = S ((S (pfrep_position_normalization_scale_divides_targetsecond)) * hc)) /\ exists ff_q_pfp_normalization_scale_divides_targetsecondentry. hb = ff_q_pfp_normalization_scale_divides_targetsecondentry * S ((S (pfrep_position_normalization_scale_divides_targetsecond)) * hc) + (pfrep_right_normalization_scale_divides_target)))))) \/ (((exists pfrep_gap_normalization_scale_divides_targetsecondoutside. pfrep_gap_normalization_scale_divides_targetsecondoutside+(L)=(pfrep_power_normalization_scale_divides_target)) /\ (((pfrep_right_normalization_scale_divides_target)=0))))) -> pfrep_left_normalization_scale_divides_target=pfrep_right_normalization_scale_divides_target)))))))

Complete tactic proof in conservative notation

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

76 script commands · 11 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
prime field polynomial left constant product existsprime field polynomial right divides from product
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro hb
  6. L6
    intro hc
  7. L7
    intro L
  8. L8
    intro hp
  9. L9
    intro hs
02Establish hcopyL10–11

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

  1. L10
    have hcopy : FpPolyScale(p,k,ab,ac,hb,hc,L)Definitions: FpPolyScale(p,k,ab,ac,hb,hc,L)Original native command in the exact edition
  2. L11
    exact hs
03Separate the logical casesL12–12

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

  1. L12
    cases hcopy
04Establish hboundsL13–22

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

  1. L13
    have hbounds : BetaPrefixInto(ab,ac,L,p) ∧ BetaPrefixInto(hb,hc,L,p)Definitions: BetaPrefixInto(ab,ac,L,p)BetaPrefixInto(hb,hc,L,p)Original native command in the exact edition
  2. L14
    specialize prime_field_polynomial_scale_bounded (p)
  3. L15
    specialize prime_field_polynomial_scale_bounded (k)
  4. L16
    specialize prime_field_polynomial_scale_bounded (ab)
  5. L17
    specialize prime_field_polynomial_scale_bounded (ac)
  6. L18
    specialize prime_field_polynomial_scale_bounded (hb)
  7. L19
    specialize prime_field_polynomial_scale_bounded (hc)
  8. L20
    specialize prime_field_polynomial_scale_bounded (L)
  9. L21
    apply prime_field_polynomial_scale_bounded
  10. L22
    exact hs
05Separate the logical casesL23–23

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

  1. L23
    cases hbounds
06Establish hactualL24–33

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

  1. L24
    have hactual : ∃ ub. ∃ uc. ∃ vb. ∃ vc. BetaPrefixInto(ub,uc,1,p) ∧ (BetaAt(ub,uc,0,k) ∧ (FpPolyScale(p,k,ab,ac,vb,vc,L) ∧ FpPolyProduct(p,ub,uc,1,ab,ac,L,vb,vc,L)))Definitions: BetaPrefixInto(ub,uc,1,p)BetaAt(ub,uc,0,k)FpPolyScale(p,k,ab,ac,vb,vc,L)FpPolyProduct(p,ub,uc,1,ab,ac,L,vb,vc,L)Original native command in the exact edition
  2. L25
    specialize prime_field_polynomial_left_constant_product_exists (p)
  3. L26
    specialize prime_field_polynomial_left_constant_product_exists (k)
  4. L27
    specialize prime_field_polynomial_left_constant_product_exists (ab)
  5. L28
    specialize prime_field_polynomial_left_constant_product_exists (ac)
  6. L29
    specialize prime_field_polynomial_left_constant_product_exists (L)
  7. L30
    apply prime_field_polynomial_left_constant_product_exists
  8. L31
    exact hp
  9. L32
    exact hcopy_left
  10. L33
    exact hbounds_left
07Separate the logical casesL34–40

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

  1. L34
    cases hactual
  2. L35
    cases hactual_witness
  3. L36
    cases hactual_witness_witness
  4. L37
    cases hactual_witness_witness_witness
  5. L38
    cases hactual_witness_witness_witness_witness
  6. L39
    cases hactual_witness_witness_witness_witness_right
  7. L40
    cases hactual_witness_witness_witness_witness_right_right
08Establish hequalL41–50

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

  1. L41
    have hequal : BetaPrefixEqual(x2,x3,hb,hc,L)Definitions: BetaPrefixEqual(x2,x3,hb,hc,L)Original native command in the exact edition
  2. L42
    specialize prime_field_polynomial_scale_functional (p)
  3. L43
    specialize prime_field_polynomial_scale_functional (k)
  4. L44
    specialize prime_field_polynomial_scale_functional (ab)
  5. L45
    specialize prime_field_polynomial_scale_functional (ac)
  6. L46
    specialize prime_field_polynomial_scale_functional (x2)
  7. L47
    specialize prime_field_polynomial_scale_functional (x3)
  8. L48
    specialize prime_field_polynomial_scale_functional (hb)
  9. L49
    specialize prime_field_polynomial_scale_functional (hc)
  10. L50
    specialize prime_field_polynomial_scale_functional (L)
09Use earlier factsL51–60

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

  1. L51
    apply prime_field_polynomial_scale_functional
  2. L52
    exact hactual_witness_witness_witness_witness_right_right_left
  3. L53
    exact hs
  4. L54
    specialize prime_field_polynomial_right_divides_from_product (p)
  5. L55
    specialize prime_field_polynomial_right_divides_from_product (ab)
  6. L56
    specialize prime_field_polynomial_right_divides_from_product (ac)
  7. L57
    specialize prime_field_polynomial_right_divides_from_product (L)
  8. L58
    specialize prime_field_polynomial_right_divides_from_product (hb)
  9. L59
    specialize prime_field_polynomial_right_divides_from_product (hc)
  10. L60
    specialize prime_field_polynomial_right_divides_from_product (L)
10Use earlier factsL61–70

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

  1. L61
    specialize prime_field_polynomial_right_divides_from_product (x)
  2. L62
    specialize prime_field_polynomial_right_divides_from_product (x1)
  3. L63
    specialize prime_field_polynomial_right_divides_from_product (1)
  4. L64
    specialize prime_field_polynomial_right_divides_from_product (x2)
  5. L65
    specialize prime_field_polynomial_right_divides_from_product (x3)
  6. L66
    specialize prime_field_polynomial_right_divides_from_product (L)
  7. L67
    apply prime_field_polynomial_right_divides_from_product
  8. L68
    exact hbounds_right
  9. L69
    exact hactual_witness_witness_witness_witness_right_right_right
  10. L70
    specialize prime_field_polynomial_equal_implies_equivalent (x2)
11Use earlier factsL71–76

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

  1. L71
    specialize prime_field_polynomial_equal_implies_equivalent (x3)
  2. L72
    specialize prime_field_polynomial_equal_implies_equivalent (hb)
  3. L73
    specialize prime_field_polynomial_equal_implies_equivalent (hc)
  4. L74
    specialize prime_field_polynomial_equal_implies_equivalent (L)
  5. L75
    apply prime_field_polynomial_equal_implies_equivalent
  6. L76
    exact hequal

Library-wide reading audit

Original defined command ledger · 76 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro hb
  6. 0006intro hc
  7. 0007intro L
  8. 0008intro hp
  9. 0009intro hs
  10. 0010have hcopy : FpPolyScale(p,k,ab,ac,hb,hc,L)
  11. 0011exact hs
  12. 0012cases hcopy
  13. 0013have hbounds : BetaPrefixInto(ab,ac,L,p) ∧ BetaPrefixInto(hb,hc,L,p)
  14. 0014specialize prime_field_polynomial_scale_bounded (p)
  15. 0015specialize prime_field_polynomial_scale_bounded (k)
  16. 0016specialize prime_field_polynomial_scale_bounded (ab)
  17. 0017specialize prime_field_polynomial_scale_bounded (ac)
  18. 0018specialize prime_field_polynomial_scale_bounded (hb)
  19. 0019specialize prime_field_polynomial_scale_bounded (hc)
  20. 0020specialize prime_field_polynomial_scale_bounded (L)
  21. 0021apply prime_field_polynomial_scale_bounded
  22. 0022exact hs
  23. 0023cases hbounds
  24. 0024have hactual : ∃ ub. ∃ uc. ∃ vb. ∃ vc. BetaPrefixInto(ub,uc,1,p) ∧ (BetaAt(ub,uc,0,k) ∧ (FpPolyScale(p,k,ab,ac,vb,vc,L) ∧ FpPolyProduct(p,ub,uc,1,ab,ac,L,vb,vc,L)))
  25. 0025specialize prime_field_polynomial_left_constant_product_exists (p)
  26. 0026specialize prime_field_polynomial_left_constant_product_exists (k)
  27. 0027specialize prime_field_polynomial_left_constant_product_exists (ab)
  28. 0028specialize prime_field_polynomial_left_constant_product_exists (ac)
  29. 0029specialize prime_field_polynomial_left_constant_product_exists (L)
  30. 0030apply prime_field_polynomial_left_constant_product_exists
  31. 0031exact hp
  32. 0032exact hcopy_left
  33. 0033exact hbounds_left
  34. 0034cases hactual
  35. 0035cases hactual_witness
  36. 0036cases hactual_witness_witness
  37. 0037cases hactual_witness_witness_witness
  38. 0038cases hactual_witness_witness_witness_witness
  39. 0039cases hactual_witness_witness_witness_witness_right
  40. 0040cases hactual_witness_witness_witness_witness_right_right
  41. 0041have hequal : BetaPrefixEqual(x2,x3,hb,hc,L)
  42. 0042specialize prime_field_polynomial_scale_functional (p)
  43. 0043specialize prime_field_polynomial_scale_functional (k)
  44. 0044specialize prime_field_polynomial_scale_functional (ab)
  45. 0045specialize prime_field_polynomial_scale_functional (ac)
  46. 0046specialize prime_field_polynomial_scale_functional (x2)
  47. 0047specialize prime_field_polynomial_scale_functional (x3)
  48. 0048specialize prime_field_polynomial_scale_functional (hb)
  49. 0049specialize prime_field_polynomial_scale_functional (hc)
  50. 0050specialize prime_field_polynomial_scale_functional (L)
  51. 0051apply prime_field_polynomial_scale_functional
  52. 0052exact hactual_witness_witness_witness_witness_right_right_left
  53. 0053exact hs
  54. 0054specialize prime_field_polynomial_right_divides_from_product (p)
  55. 0055specialize prime_field_polynomial_right_divides_from_product (ab)
  56. 0056specialize prime_field_polynomial_right_divides_from_product (ac)
  57. 0057specialize prime_field_polynomial_right_divides_from_product (L)
  58. 0058specialize prime_field_polynomial_right_divides_from_product (hb)
  59. 0059specialize prime_field_polynomial_right_divides_from_product (hc)
  60. 0060specialize prime_field_polynomial_right_divides_from_product (L)
  61. 0061specialize prime_field_polynomial_right_divides_from_product (x)
  62. 0062specialize prime_field_polynomial_right_divides_from_product (x1)
  63. 0063specialize prime_field_polynomial_right_divides_from_product (1)
  64. 0064specialize prime_field_polynomial_right_divides_from_product (x2)
  65. 0065specialize prime_field_polynomial_right_divides_from_product (x3)
  66. 0066specialize prime_field_polynomial_right_divides_from_product (L)
  67. 0067apply prime_field_polynomial_right_divides_from_product
  68. 0068exact hbounds_right
  69. 0069exact hactual_witness_witness_witness_witness_right_right_right
  70. 0070specialize prime_field_polynomial_equal_implies_equivalent (x2)
  71. 0071specialize prime_field_polynomial_equal_implies_equivalent (x3)
  72. 0072specialize prime_field_polynomial_equal_implies_equivalent (hb)
  73. 0073specialize prime_field_polynomial_equal_implies_equivalent (hc)
  74. 0074specialize prime_field_polynomial_equal_implies_equivalent (L)
  75. 0075apply prime_field_polynomial_equal_implies_equivalent
  76. 0076exact hequal