PG0055

prime_field_polynomial_scale_implies_right_divides

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic 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)))))))

Constructive proof overview

Generated structural guide

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.

The unchanged tactic script uses 5 declared prerequisites and contains 76 exact native proof lines.

Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

prime_field_polynomial_scale_bounded Alpha theorem; checked-use authorized PG0052 prime_field_polynomial_left_constant_product_exists prime_field_polynomial_scale_functional Alpha theorem; checked-use authorized PG0026 prime_field_polynomial_right_divides_from_product prime_field_polynomial_equal_implies_equivalent Alpha theorem; checked-use authorized

Direct dependents

PG0056 prime_field_polynomial_monic_normalization_right_associates

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (2)
prime field polynomial left constant product existsprime field polynomial right divides from product

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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
  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
  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: BetaPrefixIntoFpPolyScaleFpPolyProductBetaAt
  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
  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 exact 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 : ((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))))))))))))))))
  11. 0011exact hs
  12. 0012cases hcopy
  13. 0013have hbounds : ((forall fom_index_pfp_normalization_scale_A. (exists fom_gap_pfp_normalization_scale_A_index_bound. fom_gap_pfp_normalization_scale_A_index_bound + S (fom_index_pfp_normalization_scale_A) = L) -> exists fom_value_pfp_normalization_scale_A. ((((exists fom_beta_height_pfp_normalization_scale_A_entry. fom_beta_height_pfp_normalization_scale_A_entry + S (fom_value_pfp_normalization_scale_A) = S ((S (fom_index_pfp_normalization_scale_A)) * ac)) /\ exists fom_beta_quotient_pfp_normalization_scale_A_entry. ab = fom_beta_quotient_pfp_normalization_scale_A_entry * S ((S (fom_index_pfp_normalization_scale_A)) * ac) + (fom_value_pfp_normalization_scale_A))) /\ (exists fom_gap_pfp_normalization_scale_A_value_bound. fom_gap_pfp_normalization_scale_A_value_bound + S (fom_value_pfp_normalization_scale_A) = p))) /\ ((forall fom_index_pfp_normalization_scale_H. (exists fom_gap_pfp_normalization_scale_H_index_bound. fom_gap_pfp_normalization_scale_H_index_bound + S (fom_index_pfp_normalization_scale_H) = L) -> exists fom_value_pfp_normalization_scale_H. ((((exists fom_beta_height_pfp_normalization_scale_H_entry. fom_beta_height_pfp_normalization_scale_H_entry + S (fom_value_pfp_normalization_scale_H) = S ((S (fom_index_pfp_normalization_scale_H)) * hc)) /\ exists fom_beta_quotient_pfp_normalization_scale_H_entry. hb = fom_beta_quotient_pfp_normalization_scale_H_entry * S ((S (fom_index_pfp_normalization_scale_H)) * hc) + (fom_value_pfp_normalization_scale_H))) /\ (exists fom_gap_pfp_normalization_scale_H_value_bound. fom_gap_pfp_normalization_scale_H_value_bound + S (fom_value_pfp_normalization_scale_H) = 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 : exists ub uc vb vc. ((forall fom_index_pfp_normalization_scale_singleton. (exists fom_gap_pfp_normalization_scale_singleton_index_bound. fom_gap_pfp_normalization_scale_singleton_index_bound + S (fom_index_pfp_normalization_scale_singleton) = 1) -> exists fom_value_pfp_normalization_scale_singleton. ((((exists fom_beta_height_pfp_normalization_scale_singleton_entry. fom_beta_height_pfp_normalization_scale_singleton_entry + S (fom_value_pfp_normalization_scale_singleton) = S ((S (fom_index_pfp_normalization_scale_singleton)) * uc)) /\ exists fom_beta_quotient_pfp_normalization_scale_singleton_entry. ub = fom_beta_quotient_pfp_normalization_scale_singleton_entry * S ((S (fom_index_pfp_normalization_scale_singleton)) * uc) + (fom_value_pfp_normalization_scale_singleton))) /\ (exists fom_gap_pfp_normalization_scale_singleton_value_bound. fom_gap_pfp_normalization_scale_singleton_value_bound + S (fom_value_pfp_normalization_scale_singleton) = p))) /\ (((((exists ff_h_pfp_normalization_scale_head. ff_h_pfp_normalization_scale_head + S (k) = S ((S (0)) * uc)) /\ exists ff_q_pfp_normalization_scale_head. ub = ff_q_pfp_normalization_scale_head * S ((S (0)) * uc) + (k))) /\ (((((exists pfa_gap_normalization_scale_constructedscalar. pfa_gap_normalization_scale_constructedscalar + S (k) = (p)) /\ ((forall pfp_index_normalization_scale_constructed. (exists pfa_gap_normalization_scale_constructedindex. pfa_gap_normalization_scale_constructedindex + S (pfp_index_normalization_scale_constructed) = (L)) -> exists pfp_source_normalization_scale_constructed pfp_value_normalization_scale_constructed. ((((exists ff_h_pfp_normalization_scale_constructedsource. ff_h_pfp_normalization_scale_constructedsource + S (pfp_source_normalization_scale_constructed) = S ((S (pfp_index_normalization_scale_constructed)) * ac)) /\ exists ff_q_pfp_normalization_scale_constructedsource. ab = ff_q_pfp_normalization_scale_constructedsource * S ((S (pfp_index_normalization_scale_constructed)) * ac) + (pfp_source_normalization_scale_constructed))) /\ (((((exists ff_h_pfp_normalization_scale_constructedtarget. ff_h_pfp_normalization_scale_constructedtarget + S (pfp_value_normalization_scale_constructed) = S ((S (pfp_index_normalization_scale_constructed)) * vc)) /\ exists ff_q_pfp_normalization_scale_constructedtarget. vb = ff_q_pfp_normalization_scale_constructedtarget * S ((S (pfp_index_normalization_scale_constructed)) * vc) + (pfp_value_normalization_scale_constructed))) /\ ((((exists pfa_gap_normalization_scale_constructedoperationleft. pfa_gap_normalization_scale_constructedoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_scale_constructedoperationright. pfa_gap_normalization_scale_constructedoperationright + S (pfp_source_normalization_scale_constructed) = (p)) /\ ((((exists pfa_gap_normalization_scale_constructedoperationresultbound. pfa_gap_normalization_scale_constructedoperationresultbound + S (pfp_value_normalization_scale_constructed) = (p)) /\ ((exists pfa_offset_left_normalization_scale_constructedoperationresultcongruence pfa_offset_right_normalization_scale_constructedoperationresultcongruence. ((k) * (pfp_source_normalization_scale_constructed)) + (p) * pfa_offset_left_normalization_scale_constructedoperationresultcongruence = (pfp_value_normalization_scale_constructed) + (p) * pfa_offset_right_normalization_scale_constructedoperationresultcongruence))))))))))))))))) /\ ((((forall fom_index_pfp_normalization_scale_productleft. (exists fom_gap_pfp_normalization_scale_productleft_index_bound. fom_gap_pfp_normalization_scale_productleft_index_bound + S (fom_index_pfp_normalization_scale_productleft) = 1) -> exists fom_value_pfp_normalization_scale_productleft. ((((exists fom_beta_height_pfp_normalization_scale_productleft_entry. fom_beta_height_pfp_normalization_scale_productleft_entry + S (fom_value_pfp_normalization_scale_productleft) = S ((S (fom_index_pfp_normalization_scale_productleft)) * uc)) /\ exists fom_beta_quotient_pfp_normalization_scale_productleft_entry. ub = fom_beta_quotient_pfp_normalization_scale_productleft_entry * S ((S (fom_index_pfp_normalization_scale_productleft)) * uc) + (fom_value_pfp_normalization_scale_productleft))) /\ (exists fom_gap_pfp_normalization_scale_productleft_value_bound. fom_gap_pfp_normalization_scale_productleft_value_bound + S (fom_value_pfp_normalization_scale_productleft) = p))) /\ (((forall fom_index_pfp_normalization_scale_productright. (exists fom_gap_pfp_normalization_scale_productright_index_bound. fom_gap_pfp_normalization_scale_productright_index_bound + S (fom_index_pfp_normalization_scale_productright) = L) -> exists fom_value_pfp_normalization_scale_productright. ((((exists fom_beta_height_pfp_normalization_scale_productright_entry. fom_beta_height_pfp_normalization_scale_productright_entry + S (fom_value_pfp_normalization_scale_productright) = S ((S (fom_index_pfp_normalization_scale_productright)) * ac)) /\ exists fom_beta_quotient_pfp_normalization_scale_productright_entry. ab = fom_beta_quotient_pfp_normalization_scale_productright_entry * S ((S (fom_index_pfp_normalization_scale_productright)) * ac) + (fom_value_pfp_normalization_scale_productright))) /\ (exists fom_gap_pfp_normalization_scale_productright_value_bound. fom_gap_pfp_normalization_scale_productright_value_bound + S (fom_value_pfp_normalization_scale_productright) = p))) /\ (((((((1)=0 \/ (L)=0) /\ (((L)=0)))) \/ (((~((1)=0)) /\ (((~((L)=0)) /\ (((1)+(L)=S (L)))))))) /\ ((forall pfc_index_normalization_scale_productcoefficients. (exists pfa_gap_normalization_scale_productcoefficientsbound. pfa_gap_normalization_scale_productcoefficientsbound + S (pfc_index_normalization_scale_productcoefficients) = (L)) -> exists pfc_value_normalization_scale_productcoefficients. ((((exists ff_h_pfp_normalization_scale_productcoefficientsentry. ff_h_pfp_normalization_scale_productcoefficientsentry + S (pfc_value_normalization_scale_productcoefficients) = S ((S (pfc_index_normalization_scale_productcoefficients)) * vc)) /\ exists ff_q_pfp_normalization_scale_productcoefficientsentry. vb = ff_q_pfp_normalization_scale_productcoefficientsentry * S ((S (pfc_index_normalization_scale_productcoefficients)) * vc) + (pfc_value_normalization_scale_productcoefficients))) /\ ((exists pfc_terms_code_normalization_scale_productcoefficientscoefficient pfc_terms_scale_normalization_scale_productcoefficientscoefficient pfc_natural_sum_normalization_scale_productcoefficientscoefficient. ((forall pfc_index_normalization_scale_productcoefficientscoefficientdiagonal. (exists pfa_gap_normalization_scale_productcoefficientscoefficientdiagonalbound. pfa_gap_normalization_scale_productcoefficientscoefficientdiagonalbound + S (pfc_index_normalization_scale_productcoefficientscoefficientdiagonal) = (S (pfc_index_normalization_scale_productcoefficients))) -> exists pfc_value_normalization_scale_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalization_scale_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normalization_scale_productcoefficientscoefficientdiagonalentry + S (pfc_value_normalization_scale_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalization_scale_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalization_scale_productcoefficientscoefficient)) /\ exists ff_q_pfp_normalization_scale_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normalization_scale_productcoefficientscoefficient = ff_q_pfp_normalization_scale_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalization_scale_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalization_scale_productcoefficientscoefficient) + (pfc_value_normalization_scale_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalization_scale_productcoefficientscoefficientdiagonalterm pfc_left_normalization_scale_productcoefficientscoefficientdiagonalterm pfc_right_normalization_scale_productcoefficientscoefficientdiagonalterm. (((pfc_index_normalization_scale_productcoefficientscoefficientdiagonal)+pfc_complement_normalization_scale_productcoefficientscoefficientdiagonalterm=(pfc_index_normalization_scale_productcoefficients)) /\ ((((((exists pfa_gap_normalization_scale_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalization_scale_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalization_scale_productcoefficientscoefficientdiagonal) = (1)) /\ ((((exists ff_h_pfp_normalization_scale_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalization_scale_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalization_scale_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalization_scale_productcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_normalization_scale_productcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_normalization_scale_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalization_scale_productcoefficientscoefficientdiagonal)) * uc) + (pfc_left_normalization_scale_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalization_scale_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalization_scale_productcoefficientscoefficientdiagonaltermleftoutside+(1)=(pfc_index_normalization_scale_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalization_scale_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalization_scale_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalization_scale_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalization_scale_productcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_normalization_scale_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalization_scale_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalization_scale_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalization_scale_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_normalization_scale_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_normalization_scale_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalization_scale_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_normalization_scale_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalization_scale_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalization_scale_productcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_normalization_scale_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalization_scale_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalization_scale_productcoefficientscoefficientdiagonal)=pfc_left_normalization_scale_productcoefficientscoefficientdiagonalterm*pfc_right_normalization_scale_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalization_scale_productcoefficientscoefficientsum fs_v_pfc_normalization_scale_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normalization_scale_productcoefficientscoefficientsum_body_start. fs_h_pfc_normalization_scale_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalization_scale_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_scale_productcoefficientscoefficientsum_body_start. fs_u_pfc_normalization_scale_productcoefficientscoefficientsum = fs_q_pfc_normalization_scale_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalization_scale_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalization_scale_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalization_scale_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalization_scale_productcoefficientscoefficient) = S ((S (S (pfc_index_normalization_scale_productcoefficients))) * fs_v_pfc_normalization_scale_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_scale_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalization_scale_productcoefficientscoefficientsum = fs_q_pfc_normalization_scale_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalization_scale_productcoefficients))) * fs_v_pfc_normalization_scale_productcoefficientscoefficientsum) + (pfc_natural_sum_normalization_scale_productcoefficientscoefficient))) /\ forall fs_i_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps = S (pfc_index_normalization_scale_productcoefficients)) -> exists fs_a_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps fs_r_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps fs_s_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalization_scale_productcoefficientscoefficient)) /\ exists fs_q_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalization_scale_productcoefficientscoefficient = fs_q_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalization_scale_productcoefficientscoefficient) + (fs_a_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_scale_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalization_scale_productcoefficientscoefficientsum = fs_q_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_scale_productcoefficientscoefficientsum) + (fs_r_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_scale_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalization_scale_productcoefficientscoefficientsum = fs_q_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_scale_productcoefficientscoefficientsum) + (fs_s_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normalization_scale_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalization_scale_productcoefficientscoefficientresiduebound. pfa_gap_normalization_scale_productcoefficientscoefficientresiduebound + S (pfc_value_normalization_scale_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normalization_scale_productcoefficientscoefficientresiduecongruence pfa_offset_right_normalization_scale_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalization_scale_productcoefficientscoefficient) + (p) * pfa_offset_left_normalization_scale_productcoefficientscoefficientresiduecongruence = (pfc_value_normalization_scale_productcoefficients) + (p) * pfa_offset_right_normalization_scale_productcoefficientscoefficientresiduecongruence)))))))))))))))))))))))))
  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 : forall mdr_i_pfp_normalization_scale_recode mdr_a_pfp_normalization_scale_recode. (exists mdr_gap_pfp_normalization_scale_recodeb. mdr_gap_pfp_normalization_scale_recodeb + S (mdr_i_pfp_normalization_scale_recode) = (L)) -> (((exists ff_h_mdr_pfp_normalization_scale_recodeo. ff_h_mdr_pfp_normalization_scale_recodeo + S (mdr_a_pfp_normalization_scale_recode) = S ((S (mdr_i_pfp_normalization_scale_recode)) * x3)) /\ exists ff_q_mdr_pfp_normalization_scale_recodeo. x2 = ff_q_mdr_pfp_normalization_scale_recodeo * S ((S (mdr_i_pfp_normalization_scale_recode)) * x3) + (mdr_a_pfp_normalization_scale_recode))) -> (((exists ff_h_mdr_pfp_normalization_scale_recoden. ff_h_mdr_pfp_normalization_scale_recoden + S (mdr_a_pfp_normalization_scale_recode) = S ((S (mdr_i_pfp_normalization_scale_recode)) * hc)) /\ exists ff_q_mdr_pfp_normalization_scale_recoden. hb = ff_q_mdr_pfp_normalization_scale_recoden * S ((S (mdr_i_pfp_normalization_scale_recode)) * hc) + (mdr_a_pfp_normalization_scale_recode)))
  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