PX002B

prime_field_polynomial_quotient_prefix_entry

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

Every actual bounded decoded quotient value has the exact subtraction-and-inverse-product execution witnesses.

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 bb bc M qb qc N i q. (forall pfd_index_division_entry_source. (exists pfa_gap_division_entry_sourcebound. pfa_gap_division_entry_sourcebound + S (pfd_index_division_entry_source) = (N)) -> exists pfd_value_division_entry_source. ((((exists ff_h_pfp_division_entry_sourceentry. ff_h_pfp_division_entry_sourceentry + S (pfd_value_division_entry_source) = S ((S (pfd_index_division_entry_source)) * qc)) /\ exists ff_q_pfp_division_entry_sourceentry. qb = ff_q_pfp_division_entry_sourceentry * S ((S (pfd_index_division_entry_source)) * qc) + (pfd_value_division_entry_source))) /\ ((exists pfd_input_division_entry_sourcestep pfd_previous_division_entry_sourcestep pfd_difference_division_entry_sourcestep. ((((exists ff_h_pfp_division_entry_sourcestepinput. ff_h_pfp_division_entry_sourcestepinput + S (pfd_input_division_entry_sourcestep) = S ((S (pfd_index_division_entry_source)) * ac)) /\ exists ff_q_pfp_division_entry_sourcestepinput. ab = ff_q_pfp_division_entry_sourcestepinput * S ((S (pfd_index_division_entry_source)) * ac) + (pfd_input_division_entry_sourcestep))) /\ (((exists pfc_terms_code_division_entry_sourcestepprevious pfc_terms_scale_division_entry_sourcestepprevious pfc_natural_sum_division_entry_sourcestepprevious. ((forall pfc_index_division_entry_sourcesteppreviousdiagonal. (exists pfa_gap_division_entry_sourcesteppreviousdiagonalbound. pfa_gap_division_entry_sourcesteppreviousdiagonalbound + S (pfc_index_division_entry_sourcesteppreviousdiagonal) = (S (pfd_index_division_entry_source))) -> exists pfc_value_division_entry_sourcesteppreviousdiagonal. ((((exists ff_h_pfp_division_entry_sourcesteppreviousdiagonalentry. ff_h_pfp_division_entry_sourcesteppreviousdiagonalentry + S (pfc_value_division_entry_sourcesteppreviousdiagonal) = S ((S (pfc_index_division_entry_sourcesteppreviousdiagonal)) * pfc_terms_scale_division_entry_sourcestepprevious)) /\ exists ff_q_pfp_division_entry_sourcesteppreviousdiagonalentry. pfc_terms_code_division_entry_sourcestepprevious = ff_q_pfp_division_entry_sourcesteppreviousdiagonalentry * S ((S (pfc_index_division_entry_sourcesteppreviousdiagonal)) * pfc_terms_scale_division_entry_sourcestepprevious) + (pfc_value_division_entry_sourcesteppreviousdiagonal))) /\ ((exists pfc_complement_division_entry_sourcesteppreviousdiagonalterm pfc_left_division_entry_sourcesteppreviousdiagonalterm pfc_right_division_entry_sourcesteppreviousdiagonalterm. (((pfc_index_division_entry_sourcesteppreviousdiagonal)+pfc_complement_division_entry_sourcesteppreviousdiagonalterm=(pfd_index_division_entry_source)) /\ ((((((exists pfa_gap_division_entry_sourcesteppreviousdiagonaltermleftinside. pfa_gap_division_entry_sourcesteppreviousdiagonaltermleftinside + S (pfc_index_division_entry_sourcesteppreviousdiagonal) = (pfd_index_division_entry_source)) /\ ((((exists ff_h_pfp_division_entry_sourcesteppreviousdiagonaltermleftentry. ff_h_pfp_division_entry_sourcesteppreviousdiagonaltermleftentry + S (pfc_left_division_entry_sourcesteppreviousdiagonalterm) = S ((S (pfc_index_division_entry_sourcesteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_entry_sourcesteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_entry_sourcesteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_entry_sourcesteppreviousdiagonal)) * qc) + (pfc_left_division_entry_sourcesteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_entry_sourcesteppreviousdiagonaltermleftoutside. pfc_gap_division_entry_sourcesteppreviousdiagonaltermleftoutside+(pfd_index_division_entry_source)=(pfc_index_division_entry_sourcesteppreviousdiagonal)) /\ (((pfc_left_division_entry_sourcesteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_entry_sourcesteppreviousdiagonaltermrightinside. pfa_gap_division_entry_sourcesteppreviousdiagonaltermrightinside + S (pfc_complement_division_entry_sourcesteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_entry_sourcesteppreviousdiagonaltermrightentry. ff_h_pfp_division_entry_sourcesteppreviousdiagonaltermrightentry + S (pfc_right_division_entry_sourcesteppreviousdiagonalterm) = S ((S (pfc_complement_division_entry_sourcesteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_entry_sourcesteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_entry_sourcesteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_entry_sourcesteppreviousdiagonalterm)) * bc) + (pfc_right_division_entry_sourcesteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_entry_sourcesteppreviousdiagonaltermrightoutside. pfc_gap_division_entry_sourcesteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_entry_sourcesteppreviousdiagonalterm)) /\ (((pfc_right_division_entry_sourcesteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_entry_sourcesteppreviousdiagonal)=pfc_left_division_entry_sourcesteppreviousdiagonalterm*pfc_right_division_entry_sourcesteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_entry_sourcestepprevioussum fs_v_pfc_division_entry_sourcestepprevioussum. ((((exists fs_h_pfc_division_entry_sourcestepprevioussum_body_start. fs_h_pfc_division_entry_sourcestepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_entry_sourcestepprevioussum)) /\ exists fs_q_pfc_division_entry_sourcestepprevioussum_body_start. fs_u_pfc_division_entry_sourcestepprevioussum = fs_q_pfc_division_entry_sourcestepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_entry_sourcestepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_entry_sourcestepprevioussum_body_terminal. fs_h_pfc_division_entry_sourcestepprevioussum_body_terminal + S (pfc_natural_sum_division_entry_sourcestepprevious) = S ((S (S (pfd_index_division_entry_source))) * fs_v_pfc_division_entry_sourcestepprevioussum)) /\ exists fs_q_pfc_division_entry_sourcestepprevioussum_body_terminal. fs_u_pfc_division_entry_sourcestepprevioussum = fs_q_pfc_division_entry_sourcestepprevioussum_body_terminal * S ((S (S (pfd_index_division_entry_source))) * fs_v_pfc_division_entry_sourcestepprevioussum) + (pfc_natural_sum_division_entry_sourcestepprevious))) /\ forall fs_i_pfc_division_entry_sourcestepprevioussum_body_steps. (exists fs_lt_pfc_division_entry_sourcestepprevioussum_body_steps_bound. fs_lt_pfc_division_entry_sourcestepprevioussum_body_steps_bound + S fs_i_pfc_division_entry_sourcestepprevioussum_body_steps = S (pfd_index_division_entry_source)) -> exists fs_a_pfc_division_entry_sourcestepprevioussum_body_steps fs_r_pfc_division_entry_sourcestepprevioussum_body_steps fs_s_pfc_division_entry_sourcestepprevioussum_body_steps. ((((exists fs_h_pfc_division_entry_sourcestepprevioussum_body_steps_summand. fs_h_pfc_division_entry_sourcestepprevioussum_body_steps_summand + S (fs_a_pfc_division_entry_sourcestepprevioussum_body_steps) = S ((S (fs_i_pfc_division_entry_sourcestepprevioussum_body_steps)) * pfc_terms_scale_division_entry_sourcestepprevious)) /\ exists fs_q_pfc_division_entry_sourcestepprevioussum_body_steps_summand. pfc_terms_code_division_entry_sourcestepprevious = fs_q_pfc_division_entry_sourcestepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_entry_sourcestepprevioussum_body_steps)) * pfc_terms_scale_division_entry_sourcestepprevious) + (fs_a_pfc_division_entry_sourcestepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_entry_sourcestepprevioussum_body_steps_partial. fs_h_pfc_division_entry_sourcestepprevioussum_body_steps_partial + S (fs_r_pfc_division_entry_sourcestepprevioussum_body_steps) = S ((S (fs_i_pfc_division_entry_sourcestepprevioussum_body_steps)) * fs_v_pfc_division_entry_sourcestepprevioussum)) /\ exists fs_q_pfc_division_entry_sourcestepprevioussum_body_steps_partial. fs_u_pfc_division_entry_sourcestepprevioussum = fs_q_pfc_division_entry_sourcestepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_entry_sourcestepprevioussum_body_steps)) * fs_v_pfc_division_entry_sourcestepprevioussum) + (fs_r_pfc_division_entry_sourcestepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_entry_sourcestepprevioussum_body_steps_successor. fs_h_pfc_division_entry_sourcestepprevioussum_body_steps_successor + S (fs_s_pfc_division_entry_sourcestepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_entry_sourcestepprevioussum_body_steps)) * fs_v_pfc_division_entry_sourcestepprevioussum)) /\ exists fs_q_pfc_division_entry_sourcestepprevioussum_body_steps_successor. fs_u_pfc_division_entry_sourcestepprevioussum = fs_q_pfc_division_entry_sourcestepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_entry_sourcestepprevioussum_body_steps)) * fs_v_pfc_division_entry_sourcestepprevioussum) + (fs_s_pfc_division_entry_sourcestepprevioussum_body_steps))) /\ fs_s_pfc_division_entry_sourcestepprevioussum_body_steps = fs_r_pfc_division_entry_sourcestepprevioussum_body_steps + fs_a_pfc_division_entry_sourcestepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_entry_sourcesteppreviousresiduebound. pfa_gap_division_entry_sourcesteppreviousresiduebound + S (pfd_previous_division_entry_sourcestep) = (p)) /\ ((exists pfa_offset_left_division_entry_sourcesteppreviousresiduecongruence pfa_offset_right_division_entry_sourcesteppreviousresiduecongruence. (pfc_natural_sum_division_entry_sourcestepprevious) + (p) * pfa_offset_left_division_entry_sourcesteppreviousresiduecongruence = (pfd_previous_division_entry_sourcestep) + (p) * pfa_offset_right_division_entry_sourcesteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_entry_sourcestepsubtractleft. pfa_gap_division_entry_sourcestepsubtractleft + S (pfd_previous_division_entry_sourcestep) = (p)) /\ (((exists pfa_gap_division_entry_sourcestepsubtractright. pfa_gap_division_entry_sourcestepsubtractright + S (pfd_difference_division_entry_sourcestep) = (p)) /\ ((((exists pfa_gap_division_entry_sourcestepsubtractresultbound. pfa_gap_division_entry_sourcestepsubtractresultbound + S (pfd_input_division_entry_sourcestep) = (p)) /\ ((exists pfa_offset_left_division_entry_sourcestepsubtractresultcongruence pfa_offset_right_division_entry_sourcestepsubtractresultcongruence. ((pfd_previous_division_entry_sourcestep) + (pfd_difference_division_entry_sourcestep)) + (p) * pfa_offset_left_division_entry_sourcestepsubtractresultcongruence = (pfd_input_division_entry_sourcestep) + (p) * pfa_offset_right_division_entry_sourcestepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_entry_sourcestepmultiplyleft. pfa_gap_division_entry_sourcestepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_entry_sourcestepmultiplyright. pfa_gap_division_entry_sourcestepmultiplyright + S (pfd_difference_division_entry_sourcestep) = (p)) /\ ((((exists pfa_gap_division_entry_sourcestepmultiplyresultbound. pfa_gap_division_entry_sourcestepmultiplyresultbound + S (pfd_value_division_entry_source) = (p)) /\ ((exists pfa_offset_left_division_entry_sourcestepmultiplyresultcongruence pfa_offset_right_division_entry_sourcestepmultiplyresultcongruence. ((k) * (pfd_difference_division_entry_sourcestep)) + (p) * pfa_offset_left_division_entry_sourcestepmultiplyresultcongruence = (pfd_value_division_entry_source) + (p) * pfa_offset_right_division_entry_sourcestepmultiplyresultcongruence))))))))))))))))))) -> (exists pfa_gap_division_entry_bound. pfa_gap_division_entry_bound + S (i) = (N)) -> (((exists ff_h_pfp_division_entry_given. ff_h_pfp_division_entry_given + S (q) = S ((S (i)) * qc)) /\ exists ff_q_pfp_division_entry_given. qb = ff_q_pfp_division_entry_given * S ((S (i)) * qc) + (q))) -> (exists pfd_input_division_entry_result pfd_previous_division_entry_result pfd_difference_division_entry_result. ((((exists ff_h_pfp_division_entry_resultinput. ff_h_pfp_division_entry_resultinput + S (pfd_input_division_entry_result) = S ((S (i)) * ac)) /\ exists ff_q_pfp_division_entry_resultinput. ab = ff_q_pfp_division_entry_resultinput * S ((S (i)) * ac) + (pfd_input_division_entry_result))) /\ (((exists pfc_terms_code_division_entry_resultprevious pfc_terms_scale_division_entry_resultprevious pfc_natural_sum_division_entry_resultprevious. ((forall pfc_index_division_entry_resultpreviousdiagonal. (exists pfa_gap_division_entry_resultpreviousdiagonalbound. pfa_gap_division_entry_resultpreviousdiagonalbound + S (pfc_index_division_entry_resultpreviousdiagonal) = (S (i))) -> exists pfc_value_division_entry_resultpreviousdiagonal. ((((exists ff_h_pfp_division_entry_resultpreviousdiagonalentry. ff_h_pfp_division_entry_resultpreviousdiagonalentry + S (pfc_value_division_entry_resultpreviousdiagonal) = S ((S (pfc_index_division_entry_resultpreviousdiagonal)) * pfc_terms_scale_division_entry_resultprevious)) /\ exists ff_q_pfp_division_entry_resultpreviousdiagonalentry. pfc_terms_code_division_entry_resultprevious = ff_q_pfp_division_entry_resultpreviousdiagonalentry * S ((S (pfc_index_division_entry_resultpreviousdiagonal)) * pfc_terms_scale_division_entry_resultprevious) + (pfc_value_division_entry_resultpreviousdiagonal))) /\ ((exists pfc_complement_division_entry_resultpreviousdiagonalterm pfc_left_division_entry_resultpreviousdiagonalterm pfc_right_division_entry_resultpreviousdiagonalterm. (((pfc_index_division_entry_resultpreviousdiagonal)+pfc_complement_division_entry_resultpreviousdiagonalterm=(i)) /\ ((((((exists pfa_gap_division_entry_resultpreviousdiagonaltermleftinside. pfa_gap_division_entry_resultpreviousdiagonaltermleftinside + S (pfc_index_division_entry_resultpreviousdiagonal) = (i)) /\ ((((exists ff_h_pfp_division_entry_resultpreviousdiagonaltermleftentry. ff_h_pfp_division_entry_resultpreviousdiagonaltermleftentry + S (pfc_left_division_entry_resultpreviousdiagonalterm) = S ((S (pfc_index_division_entry_resultpreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_entry_resultpreviousdiagonaltermleftentry. qb = ff_q_pfp_division_entry_resultpreviousdiagonaltermleftentry * S ((S (pfc_index_division_entry_resultpreviousdiagonal)) * qc) + (pfc_left_division_entry_resultpreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_entry_resultpreviousdiagonaltermleftoutside. pfc_gap_division_entry_resultpreviousdiagonaltermleftoutside+(i)=(pfc_index_division_entry_resultpreviousdiagonal)) /\ (((pfc_left_division_entry_resultpreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_entry_resultpreviousdiagonaltermrightinside. pfa_gap_division_entry_resultpreviousdiagonaltermrightinside + S (pfc_complement_division_entry_resultpreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_entry_resultpreviousdiagonaltermrightentry. ff_h_pfp_division_entry_resultpreviousdiagonaltermrightentry + S (pfc_right_division_entry_resultpreviousdiagonalterm) = S ((S (pfc_complement_division_entry_resultpreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_entry_resultpreviousdiagonaltermrightentry. bb = ff_q_pfp_division_entry_resultpreviousdiagonaltermrightentry * S ((S (pfc_complement_division_entry_resultpreviousdiagonalterm)) * bc) + (pfc_right_division_entry_resultpreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_entry_resultpreviousdiagonaltermrightoutside. pfc_gap_division_entry_resultpreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_entry_resultpreviousdiagonalterm)) /\ (((pfc_right_division_entry_resultpreviousdiagonalterm)=0))))) /\ (((pfc_value_division_entry_resultpreviousdiagonal)=pfc_left_division_entry_resultpreviousdiagonalterm*pfc_right_division_entry_resultpreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_entry_resultprevioussum fs_v_pfc_division_entry_resultprevioussum. ((((exists fs_h_pfc_division_entry_resultprevioussum_body_start. fs_h_pfc_division_entry_resultprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_entry_resultprevioussum)) /\ exists fs_q_pfc_division_entry_resultprevioussum_body_start. fs_u_pfc_division_entry_resultprevioussum = fs_q_pfc_division_entry_resultprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_entry_resultprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_entry_resultprevioussum_body_terminal. fs_h_pfc_division_entry_resultprevioussum_body_terminal + S (pfc_natural_sum_division_entry_resultprevious) = S ((S (S (i))) * fs_v_pfc_division_entry_resultprevioussum)) /\ exists fs_q_pfc_division_entry_resultprevioussum_body_terminal. fs_u_pfc_division_entry_resultprevioussum = fs_q_pfc_division_entry_resultprevioussum_body_terminal * S ((S (S (i))) * fs_v_pfc_division_entry_resultprevioussum) + (pfc_natural_sum_division_entry_resultprevious))) /\ forall fs_i_pfc_division_entry_resultprevioussum_body_steps. (exists fs_lt_pfc_division_entry_resultprevioussum_body_steps_bound. fs_lt_pfc_division_entry_resultprevioussum_body_steps_bound + S fs_i_pfc_division_entry_resultprevioussum_body_steps = S (i)) -> exists fs_a_pfc_division_entry_resultprevioussum_body_steps fs_r_pfc_division_entry_resultprevioussum_body_steps fs_s_pfc_division_entry_resultprevioussum_body_steps. ((((exists fs_h_pfc_division_entry_resultprevioussum_body_steps_summand. fs_h_pfc_division_entry_resultprevioussum_body_steps_summand + S (fs_a_pfc_division_entry_resultprevioussum_body_steps) = S ((S (fs_i_pfc_division_entry_resultprevioussum_body_steps)) * pfc_terms_scale_division_entry_resultprevious)) /\ exists fs_q_pfc_division_entry_resultprevioussum_body_steps_summand. pfc_terms_code_division_entry_resultprevious = fs_q_pfc_division_entry_resultprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_entry_resultprevioussum_body_steps)) * pfc_terms_scale_division_entry_resultprevious) + (fs_a_pfc_division_entry_resultprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_entry_resultprevioussum_body_steps_partial. fs_h_pfc_division_entry_resultprevioussum_body_steps_partial + S (fs_r_pfc_division_entry_resultprevioussum_body_steps) = S ((S (fs_i_pfc_division_entry_resultprevioussum_body_steps)) * fs_v_pfc_division_entry_resultprevioussum)) /\ exists fs_q_pfc_division_entry_resultprevioussum_body_steps_partial. fs_u_pfc_division_entry_resultprevioussum = fs_q_pfc_division_entry_resultprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_entry_resultprevioussum_body_steps)) * fs_v_pfc_division_entry_resultprevioussum) + (fs_r_pfc_division_entry_resultprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_entry_resultprevioussum_body_steps_successor. fs_h_pfc_division_entry_resultprevioussum_body_steps_successor + S (fs_s_pfc_division_entry_resultprevioussum_body_steps) = S ((S (S fs_i_pfc_division_entry_resultprevioussum_body_steps)) * fs_v_pfc_division_entry_resultprevioussum)) /\ exists fs_q_pfc_division_entry_resultprevioussum_body_steps_successor. fs_u_pfc_division_entry_resultprevioussum = fs_q_pfc_division_entry_resultprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_entry_resultprevioussum_body_steps)) * fs_v_pfc_division_entry_resultprevioussum) + (fs_s_pfc_division_entry_resultprevioussum_body_steps))) /\ fs_s_pfc_division_entry_resultprevioussum_body_steps = fs_r_pfc_division_entry_resultprevioussum_body_steps + fs_a_pfc_division_entry_resultprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_entry_resultpreviousresiduebound. pfa_gap_division_entry_resultpreviousresiduebound + S (pfd_previous_division_entry_result) = (p)) /\ ((exists pfa_offset_left_division_entry_resultpreviousresiduecongruence pfa_offset_right_division_entry_resultpreviousresiduecongruence. (pfc_natural_sum_division_entry_resultprevious) + (p) * pfa_offset_left_division_entry_resultpreviousresiduecongruence = (pfd_previous_division_entry_result) + (p) * pfa_offset_right_division_entry_resultpreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_entry_resultsubtractleft. pfa_gap_division_entry_resultsubtractleft + S (pfd_previous_division_entry_result) = (p)) /\ (((exists pfa_gap_division_entry_resultsubtractright. pfa_gap_division_entry_resultsubtractright + S (pfd_difference_division_entry_result) = (p)) /\ ((((exists pfa_gap_division_entry_resultsubtractresultbound. pfa_gap_division_entry_resultsubtractresultbound + S (pfd_input_division_entry_result) = (p)) /\ ((exists pfa_offset_left_division_entry_resultsubtractresultcongruence pfa_offset_right_division_entry_resultsubtractresultcongruence. ((pfd_previous_division_entry_result) + (pfd_difference_division_entry_result)) + (p) * pfa_offset_left_division_entry_resultsubtractresultcongruence = (pfd_input_division_entry_result) + (p) * pfa_offset_right_division_entry_resultsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_entry_resultmultiplyleft. pfa_gap_division_entry_resultmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_entry_resultmultiplyright. pfa_gap_division_entry_resultmultiplyright + S (pfd_difference_division_entry_result) = (p)) /\ ((((exists pfa_gap_division_entry_resultmultiplyresultbound. pfa_gap_division_entry_resultmultiplyresultbound + S (q) = (p)) /\ ((exists pfa_offset_left_division_entry_resultmultiplyresultcongruence pfa_offset_right_division_entry_resultmultiplyresultcongruence. ((k) * (pfd_difference_division_entry_result)) + (p) * pfa_offset_left_division_entry_resultmultiplyresultcongruence = (q) + (p) * pfa_offset_right_division_entry_resultmultiplyresultcongruence))))))))))))))))

Constructive proof overview

Generated structural guide

Every actual bounded decoded quotient value has the exact subtraction-and-inverse-product execution witnesses.

The unchanged tactic script uses 1 declared prerequisite and contains 33 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_unique Alpha theorem; checked-use authorized

Direct dependents

PX0054 prime_field_polynomial_quotient_prefix_functional

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

33 script commands · 7 reading checkpoints · 2 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.

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–10

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 bb
  6. L6
    intro bc
  7. L7
    intro M
  8. L8
    intro qb
  9. L9
    intro qc
  10. L10
    intro N
02Fix variables and assumptionsL11–15

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

  1. L11
    intro i
  2. L12
    intro q
  3. L13
    intro h
  4. L14
    intro hi
  5. L15
    intro hq
03Establish hvL16–19

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

  1. L16
    have hv : ∃ r. BetaAt(qb,qc,i,r) ∧ FpPolynomialQuotientStep(p,k,ab,ac,bb,bc,M,qb,qc,i,r)Definitions: FpPolynomialQuotientStepBetaAt
  2. L17
    specialize h (i)
  3. L18
    apply h
  4. L19
    exact hi
04Separate the logical casesL20–21

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

  1. L20
    cases hv
  2. L21
    cases hv_witness
05Establish heqL22–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L22
    have heq : x=q
  2. L23
    specialize beta_at_unique (qb)
  3. L24
    specialize beta_at_unique (qc)
  4. L25
    specialize beta_at_unique (i)
  5. L26
    specialize beta_at_unique (x)
  6. L27
    specialize beta_at_unique (q)
  7. L28
    apply beta_at_unique
  8. L29
    exact hv_witness_left
  9. L30
    exact hq
  10. L31
    rewrite heq at hv_witness_right
06Calculate and transport equalitiesL32–32

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

  1. L32
    rewrite heq at hv_witness_right
07Use earlier factsL33–33

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

  1. L33
    exact hv_witness_right

Library-wide reading audit

Original exact command ledger · 33 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro qb
  9. 0009intro qc
  10. 0010intro N
  11. 0011intro i
  12. 0012intro q
  13. 0013intro h
  14. 0014intro hi
  15. 0015intro hq
  16. 0016have hv : exists r. ((((exists ff_h_pfp_division_entry_chosen. ff_h_pfp_division_entry_chosen + S (r) = S ((S (i)) * qc)) /\ exists ff_q_pfp_division_entry_chosen. qb = ff_q_pfp_division_entry_chosen * S ((S (i)) * qc) + (r))) /\ ((exists pfd_input_division_entry_step pfd_previous_division_entry_step pfd_difference_division_entry_step. ((((exists ff_h_pfp_division_entry_stepinput. ff_h_pfp_division_entry_stepinput + S (pfd_input_division_entry_step) = S ((S (i)) * ac)) /\ exists ff_q_pfp_division_entry_stepinput. ab = ff_q_pfp_division_entry_stepinput * S ((S (i)) * ac) + (pfd_input_division_entry_step))) /\ (((exists pfc_terms_code_division_entry_stepprevious pfc_terms_scale_division_entry_stepprevious pfc_natural_sum_division_entry_stepprevious. ((forall pfc_index_division_entry_steppreviousdiagonal. (exists pfa_gap_division_entry_steppreviousdiagonalbound. pfa_gap_division_entry_steppreviousdiagonalbound + S (pfc_index_division_entry_steppreviousdiagonal) = (S (i))) -> exists pfc_value_division_entry_steppreviousdiagonal. ((((exists ff_h_pfp_division_entry_steppreviousdiagonalentry. ff_h_pfp_division_entry_steppreviousdiagonalentry + S (pfc_value_division_entry_steppreviousdiagonal) = S ((S (pfc_index_division_entry_steppreviousdiagonal)) * pfc_terms_scale_division_entry_stepprevious)) /\ exists ff_q_pfp_division_entry_steppreviousdiagonalentry. pfc_terms_code_division_entry_stepprevious = ff_q_pfp_division_entry_steppreviousdiagonalentry * S ((S (pfc_index_division_entry_steppreviousdiagonal)) * pfc_terms_scale_division_entry_stepprevious) + (pfc_value_division_entry_steppreviousdiagonal))) /\ ((exists pfc_complement_division_entry_steppreviousdiagonalterm pfc_left_division_entry_steppreviousdiagonalterm pfc_right_division_entry_steppreviousdiagonalterm. (((pfc_index_division_entry_steppreviousdiagonal)+pfc_complement_division_entry_steppreviousdiagonalterm=(i)) /\ ((((((exists pfa_gap_division_entry_steppreviousdiagonaltermleftinside. pfa_gap_division_entry_steppreviousdiagonaltermleftinside + S (pfc_index_division_entry_steppreviousdiagonal) = (i)) /\ ((((exists ff_h_pfp_division_entry_steppreviousdiagonaltermleftentry. ff_h_pfp_division_entry_steppreviousdiagonaltermleftentry + S (pfc_left_division_entry_steppreviousdiagonalterm) = S ((S (pfc_index_division_entry_steppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_entry_steppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_entry_steppreviousdiagonaltermleftentry * S ((S (pfc_index_division_entry_steppreviousdiagonal)) * qc) + (pfc_left_division_entry_steppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_entry_steppreviousdiagonaltermleftoutside. pfc_gap_division_entry_steppreviousdiagonaltermleftoutside+(i)=(pfc_index_division_entry_steppreviousdiagonal)) /\ (((pfc_left_division_entry_steppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_entry_steppreviousdiagonaltermrightinside. pfa_gap_division_entry_steppreviousdiagonaltermrightinside + S (pfc_complement_division_entry_steppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_entry_steppreviousdiagonaltermrightentry. ff_h_pfp_division_entry_steppreviousdiagonaltermrightentry + S (pfc_right_division_entry_steppreviousdiagonalterm) = S ((S (pfc_complement_division_entry_steppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_entry_steppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_entry_steppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_entry_steppreviousdiagonalterm)) * bc) + (pfc_right_division_entry_steppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_entry_steppreviousdiagonaltermrightoutside. pfc_gap_division_entry_steppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_entry_steppreviousdiagonalterm)) /\ (((pfc_right_division_entry_steppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_entry_steppreviousdiagonal)=pfc_left_division_entry_steppreviousdiagonalterm*pfc_right_division_entry_steppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_entry_stepprevioussum fs_v_pfc_division_entry_stepprevioussum. ((((exists fs_h_pfc_division_entry_stepprevioussum_body_start. fs_h_pfc_division_entry_stepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_entry_stepprevioussum)) /\ exists fs_q_pfc_division_entry_stepprevioussum_body_start. fs_u_pfc_division_entry_stepprevioussum = fs_q_pfc_division_entry_stepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_entry_stepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_entry_stepprevioussum_body_terminal. fs_h_pfc_division_entry_stepprevioussum_body_terminal + S (pfc_natural_sum_division_entry_stepprevious) = S ((S (S (i))) * fs_v_pfc_division_entry_stepprevioussum)) /\ exists fs_q_pfc_division_entry_stepprevioussum_body_terminal. fs_u_pfc_division_entry_stepprevioussum = fs_q_pfc_division_entry_stepprevioussum_body_terminal * S ((S (S (i))) * fs_v_pfc_division_entry_stepprevioussum) + (pfc_natural_sum_division_entry_stepprevious))) /\ forall fs_i_pfc_division_entry_stepprevioussum_body_steps. (exists fs_lt_pfc_division_entry_stepprevioussum_body_steps_bound. fs_lt_pfc_division_entry_stepprevioussum_body_steps_bound + S fs_i_pfc_division_entry_stepprevioussum_body_steps = S (i)) -> exists fs_a_pfc_division_entry_stepprevioussum_body_steps fs_r_pfc_division_entry_stepprevioussum_body_steps fs_s_pfc_division_entry_stepprevioussum_body_steps. ((((exists fs_h_pfc_division_entry_stepprevioussum_body_steps_summand. fs_h_pfc_division_entry_stepprevioussum_body_steps_summand + S (fs_a_pfc_division_entry_stepprevioussum_body_steps) = S ((S (fs_i_pfc_division_entry_stepprevioussum_body_steps)) * pfc_terms_scale_division_entry_stepprevious)) /\ exists fs_q_pfc_division_entry_stepprevioussum_body_steps_summand. pfc_terms_code_division_entry_stepprevious = fs_q_pfc_division_entry_stepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_entry_stepprevioussum_body_steps)) * pfc_terms_scale_division_entry_stepprevious) + (fs_a_pfc_division_entry_stepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_entry_stepprevioussum_body_steps_partial. fs_h_pfc_division_entry_stepprevioussum_body_steps_partial + S (fs_r_pfc_division_entry_stepprevioussum_body_steps) = S ((S (fs_i_pfc_division_entry_stepprevioussum_body_steps)) * fs_v_pfc_division_entry_stepprevioussum)) /\ exists fs_q_pfc_division_entry_stepprevioussum_body_steps_partial. fs_u_pfc_division_entry_stepprevioussum = fs_q_pfc_division_entry_stepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_entry_stepprevioussum_body_steps)) * fs_v_pfc_division_entry_stepprevioussum) + (fs_r_pfc_division_entry_stepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_entry_stepprevioussum_body_steps_successor. fs_h_pfc_division_entry_stepprevioussum_body_steps_successor + S (fs_s_pfc_division_entry_stepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_entry_stepprevioussum_body_steps)) * fs_v_pfc_division_entry_stepprevioussum)) /\ exists fs_q_pfc_division_entry_stepprevioussum_body_steps_successor. fs_u_pfc_division_entry_stepprevioussum = fs_q_pfc_division_entry_stepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_entry_stepprevioussum_body_steps)) * fs_v_pfc_division_entry_stepprevioussum) + (fs_s_pfc_division_entry_stepprevioussum_body_steps))) /\ fs_s_pfc_division_entry_stepprevioussum_body_steps = fs_r_pfc_division_entry_stepprevioussum_body_steps + fs_a_pfc_division_entry_stepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_entry_steppreviousresiduebound. pfa_gap_division_entry_steppreviousresiduebound + S (pfd_previous_division_entry_step) = (p)) /\ ((exists pfa_offset_left_division_entry_steppreviousresiduecongruence pfa_offset_right_division_entry_steppreviousresiduecongruence. (pfc_natural_sum_division_entry_stepprevious) + (p) * pfa_offset_left_division_entry_steppreviousresiduecongruence = (pfd_previous_division_entry_step) + (p) * pfa_offset_right_division_entry_steppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_entry_stepsubtractleft. pfa_gap_division_entry_stepsubtractleft + S (pfd_previous_division_entry_step) = (p)) /\ (((exists pfa_gap_division_entry_stepsubtractright. pfa_gap_division_entry_stepsubtractright + S (pfd_difference_division_entry_step) = (p)) /\ ((((exists pfa_gap_division_entry_stepsubtractresultbound. pfa_gap_division_entry_stepsubtractresultbound + S (pfd_input_division_entry_step) = (p)) /\ ((exists pfa_offset_left_division_entry_stepsubtractresultcongruence pfa_offset_right_division_entry_stepsubtractresultcongruence. ((pfd_previous_division_entry_step) + (pfd_difference_division_entry_step)) + (p) * pfa_offset_left_division_entry_stepsubtractresultcongruence = (pfd_input_division_entry_step) + (p) * pfa_offset_right_division_entry_stepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_entry_stepmultiplyleft. pfa_gap_division_entry_stepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_entry_stepmultiplyright. pfa_gap_division_entry_stepmultiplyright + S (pfd_difference_division_entry_step) = (p)) /\ ((((exists pfa_gap_division_entry_stepmultiplyresultbound. pfa_gap_division_entry_stepmultiplyresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_division_entry_stepmultiplyresultcongruence pfa_offset_right_division_entry_stepmultiplyresultcongruence. ((k) * (pfd_difference_division_entry_step)) + (p) * pfa_offset_left_division_entry_stepmultiplyresultcongruence = (r) + (p) * pfa_offset_right_division_entry_stepmultiplyresultcongruence))))))))))))))))))
  17. 0017specialize h (i)
  18. 0018apply h
  19. 0019exact hi
  20. 0020cases hv
  21. 0021cases hv_witness
  22. 0022have heq : x=q
  23. 0023specialize beta_at_unique (qb)
  24. 0024specialize beta_at_unique (qc)
  25. 0025specialize beta_at_unique (i)
  26. 0026specialize beta_at_unique (x)
  27. 0027specialize beta_at_unique (q)
  28. 0028apply beta_at_unique
  29. 0029exact hv_witness_left
  30. 0030exact hq
  31. 0031rewrite heq at hv_witness_right
  32. 0032rewrite heq at hv_witness_right
  33. 0033exact hv_witness_right