PX0052

prime_field_polynomial_quotient_step_functional

An actual triangular execution step has one decoded output, by beta and convolution functionality, additive cancellation, and product functionality.

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

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

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

Exact theorem in conservative defined notation

∀ p. ∀ k. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ M. ∀ qb. ∀ qc. ∀ i. ∀ q. ∀ r. FpPolynomialQuotientStep(p,k,ab,ac,bb,bc,M,qb,qc,i,q) → FpPolynomialQuotientStep(p,k,ab,ac,bb,bc,M,qb,qc,i,r) → q = r

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

Definition DAG

FpPolynomialQuotientStep(p,k,ab,ac,bb,bc,M,qb,qc,i,q) · 2

Actual proof prerequisites

beta_at_unique · checked external prerequisiteprime_field_convolution_coefficient_functional · checked external prerequisiteprime_field_add_cancel_left · checked external prerequisiteprime_field_multiply_functional · checked external prerequisite
Original expanded first-order statement 
forall p k ab ac bb bc M qb qc i q r. (exists pfd_input_step_unique_first pfd_previous_step_unique_first pfd_difference_step_unique_first. ((((exists ff_h_pfp_step_unique_firstinput. ff_h_pfp_step_unique_firstinput + S (pfd_input_step_unique_first) = S ((S (i)) * ac)) /\ exists ff_q_pfp_step_unique_firstinput. ab = ff_q_pfp_step_unique_firstinput * S ((S (i)) * ac) + (pfd_input_step_unique_first))) /\ (((exists pfc_terms_code_step_unique_firstprevious pfc_terms_scale_step_unique_firstprevious pfc_natural_sum_step_unique_firstprevious. ((forall pfc_index_step_unique_firstpreviousdiagonal. (exists pfa_gap_step_unique_firstpreviousdiagonalbound. pfa_gap_step_unique_firstpreviousdiagonalbound + S (pfc_index_step_unique_firstpreviousdiagonal) = (S (i))) -> exists pfc_value_step_unique_firstpreviousdiagonal. ((((exists ff_h_pfp_step_unique_firstpreviousdiagonalentry. ff_h_pfp_step_unique_firstpreviousdiagonalentry + S (pfc_value_step_unique_firstpreviousdiagonal) = S ((S (pfc_index_step_unique_firstpreviousdiagonal)) * pfc_terms_scale_step_unique_firstprevious)) /\ exists ff_q_pfp_step_unique_firstpreviousdiagonalentry. pfc_terms_code_step_unique_firstprevious = ff_q_pfp_step_unique_firstpreviousdiagonalentry * S ((S (pfc_index_step_unique_firstpreviousdiagonal)) * pfc_terms_scale_step_unique_firstprevious) + (pfc_value_step_unique_firstpreviousdiagonal))) /\ ((exists pfc_complement_step_unique_firstpreviousdiagonalterm pfc_left_step_unique_firstpreviousdiagonalterm pfc_right_step_unique_firstpreviousdiagonalterm. (((pfc_index_step_unique_firstpreviousdiagonal)+pfc_complement_step_unique_firstpreviousdiagonalterm=(i)) /\ ((((((exists pfa_gap_step_unique_firstpreviousdiagonaltermleftinside. pfa_gap_step_unique_firstpreviousdiagonaltermleftinside + S (pfc_index_step_unique_firstpreviousdiagonal) = (i)) /\ ((((exists ff_h_pfp_step_unique_firstpreviousdiagonaltermleftentry. ff_h_pfp_step_unique_firstpreviousdiagonaltermleftentry + S (pfc_left_step_unique_firstpreviousdiagonalterm) = S ((S (pfc_index_step_unique_firstpreviousdiagonal)) * qc)) /\ exists ff_q_pfp_step_unique_firstpreviousdiagonaltermleftentry. qb = ff_q_pfp_step_unique_firstpreviousdiagonaltermleftentry * S ((S (pfc_index_step_unique_firstpreviousdiagonal)) * qc) + (pfc_left_step_unique_firstpreviousdiagonalterm)))))) \/ (((exists pfc_gap_step_unique_firstpreviousdiagonaltermleftoutside. pfc_gap_step_unique_firstpreviousdiagonaltermleftoutside+(i)=(pfc_index_step_unique_firstpreviousdiagonal)) /\ (((pfc_left_step_unique_firstpreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_step_unique_firstpreviousdiagonaltermrightinside. pfa_gap_step_unique_firstpreviousdiagonaltermrightinside + S (pfc_complement_step_unique_firstpreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_step_unique_firstpreviousdiagonaltermrightentry. ff_h_pfp_step_unique_firstpreviousdiagonaltermrightentry + S (pfc_right_step_unique_firstpreviousdiagonalterm) = S ((S (pfc_complement_step_unique_firstpreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_step_unique_firstpreviousdiagonaltermrightentry. bb = ff_q_pfp_step_unique_firstpreviousdiagonaltermrightentry * S ((S (pfc_complement_step_unique_firstpreviousdiagonalterm)) * bc) + (pfc_right_step_unique_firstpreviousdiagonalterm)))))) \/ (((exists pfc_gap_step_unique_firstpreviousdiagonaltermrightoutside. pfc_gap_step_unique_firstpreviousdiagonaltermrightoutside+(M)=(pfc_complement_step_unique_firstpreviousdiagonalterm)) /\ (((pfc_right_step_unique_firstpreviousdiagonalterm)=0))))) /\ (((pfc_value_step_unique_firstpreviousdiagonal)=pfc_left_step_unique_firstpreviousdiagonalterm*pfc_right_step_unique_firstpreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_step_unique_firstprevioussum fs_v_pfc_step_unique_firstprevioussum. ((((exists fs_h_pfc_step_unique_firstprevioussum_body_start. fs_h_pfc_step_unique_firstprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_step_unique_firstprevioussum)) /\ exists fs_q_pfc_step_unique_firstprevioussum_body_start. fs_u_pfc_step_unique_firstprevioussum = fs_q_pfc_step_unique_firstprevioussum_body_start * S ((S (0)) * fs_v_pfc_step_unique_firstprevioussum) + (0))) /\ ((((exists fs_h_pfc_step_unique_firstprevioussum_body_terminal. fs_h_pfc_step_unique_firstprevioussum_body_terminal + S (pfc_natural_sum_step_unique_firstprevious) = S ((S (S (i))) * fs_v_pfc_step_unique_firstprevioussum)) /\ exists fs_q_pfc_step_unique_firstprevioussum_body_terminal. fs_u_pfc_step_unique_firstprevioussum = fs_q_pfc_step_unique_firstprevioussum_body_terminal * S ((S (S (i))) * fs_v_pfc_step_unique_firstprevioussum) + (pfc_natural_sum_step_unique_firstprevious))) /\ forall fs_i_pfc_step_unique_firstprevioussum_body_steps. (exists fs_lt_pfc_step_unique_firstprevioussum_body_steps_bound. fs_lt_pfc_step_unique_firstprevioussum_body_steps_bound + S fs_i_pfc_step_unique_firstprevioussum_body_steps = S (i)) -> exists fs_a_pfc_step_unique_firstprevioussum_body_steps fs_r_pfc_step_unique_firstprevioussum_body_steps fs_s_pfc_step_unique_firstprevioussum_body_steps. ((((exists fs_h_pfc_step_unique_firstprevioussum_body_steps_summand. fs_h_pfc_step_unique_firstprevioussum_body_steps_summand + S (fs_a_pfc_step_unique_firstprevioussum_body_steps) = S ((S (fs_i_pfc_step_unique_firstprevioussum_body_steps)) * pfc_terms_scale_step_unique_firstprevious)) /\ exists fs_q_pfc_step_unique_firstprevioussum_body_steps_summand. pfc_terms_code_step_unique_firstprevious = fs_q_pfc_step_unique_firstprevioussum_body_steps_summand * S ((S (fs_i_pfc_step_unique_firstprevioussum_body_steps)) * pfc_terms_scale_step_unique_firstprevious) + (fs_a_pfc_step_unique_firstprevioussum_body_steps))) /\ ((((exists fs_h_pfc_step_unique_firstprevioussum_body_steps_partial. fs_h_pfc_step_unique_firstprevioussum_body_steps_partial + S (fs_r_pfc_step_unique_firstprevioussum_body_steps) = S ((S (fs_i_pfc_step_unique_firstprevioussum_body_steps)) * fs_v_pfc_step_unique_firstprevioussum)) /\ exists fs_q_pfc_step_unique_firstprevioussum_body_steps_partial. fs_u_pfc_step_unique_firstprevioussum = fs_q_pfc_step_unique_firstprevioussum_body_steps_partial * S ((S (fs_i_pfc_step_unique_firstprevioussum_body_steps)) * fs_v_pfc_step_unique_firstprevioussum) + (fs_r_pfc_step_unique_firstprevioussum_body_steps))) /\ ((((exists fs_h_pfc_step_unique_firstprevioussum_body_steps_successor. fs_h_pfc_step_unique_firstprevioussum_body_steps_successor + S (fs_s_pfc_step_unique_firstprevioussum_body_steps) = S ((S (S fs_i_pfc_step_unique_firstprevioussum_body_steps)) * fs_v_pfc_step_unique_firstprevioussum)) /\ exists fs_q_pfc_step_unique_firstprevioussum_body_steps_successor. fs_u_pfc_step_unique_firstprevioussum = fs_q_pfc_step_unique_firstprevioussum_body_steps_successor * S ((S (S fs_i_pfc_step_unique_firstprevioussum_body_steps)) * fs_v_pfc_step_unique_firstprevioussum) + (fs_s_pfc_step_unique_firstprevioussum_body_steps))) /\ fs_s_pfc_step_unique_firstprevioussum_body_steps = fs_r_pfc_step_unique_firstprevioussum_body_steps + fs_a_pfc_step_unique_firstprevioussum_body_steps)))))) /\ ((((exists pfa_gap_step_unique_firstpreviousresiduebound. pfa_gap_step_unique_firstpreviousresiduebound + S (pfd_previous_step_unique_first) = (p)) /\ ((exists pfa_offset_left_step_unique_firstpreviousresiduecongruence pfa_offset_right_step_unique_firstpreviousresiduecongruence. (pfc_natural_sum_step_unique_firstprevious) + (p) * pfa_offset_left_step_unique_firstpreviousresiduecongruence = (pfd_previous_step_unique_first) + (p) * pfa_offset_right_step_unique_firstpreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_step_unique_firstsubtractleft. pfa_gap_step_unique_firstsubtractleft + S (pfd_previous_step_unique_first) = (p)) /\ (((exists pfa_gap_step_unique_firstsubtractright. pfa_gap_step_unique_firstsubtractright + S (pfd_difference_step_unique_first) = (p)) /\ ((((exists pfa_gap_step_unique_firstsubtractresultbound. pfa_gap_step_unique_firstsubtractresultbound + S (pfd_input_step_unique_first) = (p)) /\ ((exists pfa_offset_left_step_unique_firstsubtractresultcongruence pfa_offset_right_step_unique_firstsubtractresultcongruence. ((pfd_previous_step_unique_first) + (pfd_difference_step_unique_first)) + (p) * pfa_offset_left_step_unique_firstsubtractresultcongruence = (pfd_input_step_unique_first) + (p) * pfa_offset_right_step_unique_firstsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_step_unique_firstmultiplyleft. pfa_gap_step_unique_firstmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_step_unique_firstmultiplyright. pfa_gap_step_unique_firstmultiplyright + S (pfd_difference_step_unique_first) = (p)) /\ ((((exists pfa_gap_step_unique_firstmultiplyresultbound. pfa_gap_step_unique_firstmultiplyresultbound + S (q) = (p)) /\ ((exists pfa_offset_left_step_unique_firstmultiplyresultcongruence pfa_offset_right_step_unique_firstmultiplyresultcongruence. ((k) * (pfd_difference_step_unique_first)) + (p) * pfa_offset_left_step_unique_firstmultiplyresultcongruence = (q) + (p) * pfa_offset_right_step_unique_firstmultiplyresultcongruence)))))))))))))))) -> (exists pfd_input_step_unique_second pfd_previous_step_unique_second pfd_difference_step_unique_second. ((((exists ff_h_pfp_step_unique_secondinput. ff_h_pfp_step_unique_secondinput + S (pfd_input_step_unique_second) = S ((S (i)) * ac)) /\ exists ff_q_pfp_step_unique_secondinput. ab = ff_q_pfp_step_unique_secondinput * S ((S (i)) * ac) + (pfd_input_step_unique_second))) /\ (((exists pfc_terms_code_step_unique_secondprevious pfc_terms_scale_step_unique_secondprevious pfc_natural_sum_step_unique_secondprevious. ((forall pfc_index_step_unique_secondpreviousdiagonal. (exists pfa_gap_step_unique_secondpreviousdiagonalbound. pfa_gap_step_unique_secondpreviousdiagonalbound + S (pfc_index_step_unique_secondpreviousdiagonal) = (S (i))) -> exists pfc_value_step_unique_secondpreviousdiagonal. ((((exists ff_h_pfp_step_unique_secondpreviousdiagonalentry. ff_h_pfp_step_unique_secondpreviousdiagonalentry + S (pfc_value_step_unique_secondpreviousdiagonal) = S ((S (pfc_index_step_unique_secondpreviousdiagonal)) * pfc_terms_scale_step_unique_secondprevious)) /\ exists ff_q_pfp_step_unique_secondpreviousdiagonalentry. pfc_terms_code_step_unique_secondprevious = ff_q_pfp_step_unique_secondpreviousdiagonalentry * S ((S (pfc_index_step_unique_secondpreviousdiagonal)) * pfc_terms_scale_step_unique_secondprevious) + (pfc_value_step_unique_secondpreviousdiagonal))) /\ ((exists pfc_complement_step_unique_secondpreviousdiagonalterm pfc_left_step_unique_secondpreviousdiagonalterm pfc_right_step_unique_secondpreviousdiagonalterm. (((pfc_index_step_unique_secondpreviousdiagonal)+pfc_complement_step_unique_secondpreviousdiagonalterm=(i)) /\ ((((((exists pfa_gap_step_unique_secondpreviousdiagonaltermleftinside. pfa_gap_step_unique_secondpreviousdiagonaltermleftinside + S (pfc_index_step_unique_secondpreviousdiagonal) = (i)) /\ ((((exists ff_h_pfp_step_unique_secondpreviousdiagonaltermleftentry. ff_h_pfp_step_unique_secondpreviousdiagonaltermleftentry + S (pfc_left_step_unique_secondpreviousdiagonalterm) = S ((S (pfc_index_step_unique_secondpreviousdiagonal)) * qc)) /\ exists ff_q_pfp_step_unique_secondpreviousdiagonaltermleftentry. qb = ff_q_pfp_step_unique_secondpreviousdiagonaltermleftentry * S ((S (pfc_index_step_unique_secondpreviousdiagonal)) * qc) + (pfc_left_step_unique_secondpreviousdiagonalterm)))))) \/ (((exists pfc_gap_step_unique_secondpreviousdiagonaltermleftoutside. pfc_gap_step_unique_secondpreviousdiagonaltermleftoutside+(i)=(pfc_index_step_unique_secondpreviousdiagonal)) /\ (((pfc_left_step_unique_secondpreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_step_unique_secondpreviousdiagonaltermrightinside. pfa_gap_step_unique_secondpreviousdiagonaltermrightinside + S (pfc_complement_step_unique_secondpreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_step_unique_secondpreviousdiagonaltermrightentry. ff_h_pfp_step_unique_secondpreviousdiagonaltermrightentry + S (pfc_right_step_unique_secondpreviousdiagonalterm) = S ((S (pfc_complement_step_unique_secondpreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_step_unique_secondpreviousdiagonaltermrightentry. bb = ff_q_pfp_step_unique_secondpreviousdiagonaltermrightentry * S ((S (pfc_complement_step_unique_secondpreviousdiagonalterm)) * bc) + (pfc_right_step_unique_secondpreviousdiagonalterm)))))) \/ (((exists pfc_gap_step_unique_secondpreviousdiagonaltermrightoutside. pfc_gap_step_unique_secondpreviousdiagonaltermrightoutside+(M)=(pfc_complement_step_unique_secondpreviousdiagonalterm)) /\ (((pfc_right_step_unique_secondpreviousdiagonalterm)=0))))) /\ (((pfc_value_step_unique_secondpreviousdiagonal)=pfc_left_step_unique_secondpreviousdiagonalterm*pfc_right_step_unique_secondpreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_step_unique_secondprevioussum fs_v_pfc_step_unique_secondprevioussum. ((((exists fs_h_pfc_step_unique_secondprevioussum_body_start. fs_h_pfc_step_unique_secondprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_step_unique_secondprevioussum)) /\ exists fs_q_pfc_step_unique_secondprevioussum_body_start. fs_u_pfc_step_unique_secondprevioussum = fs_q_pfc_step_unique_secondprevioussum_body_start * S ((S (0)) * fs_v_pfc_step_unique_secondprevioussum) + (0))) /\ ((((exists fs_h_pfc_step_unique_secondprevioussum_body_terminal. fs_h_pfc_step_unique_secondprevioussum_body_terminal + S (pfc_natural_sum_step_unique_secondprevious) = S ((S (S (i))) * fs_v_pfc_step_unique_secondprevioussum)) /\ exists fs_q_pfc_step_unique_secondprevioussum_body_terminal. fs_u_pfc_step_unique_secondprevioussum = fs_q_pfc_step_unique_secondprevioussum_body_terminal * S ((S (S (i))) * fs_v_pfc_step_unique_secondprevioussum) + (pfc_natural_sum_step_unique_secondprevious))) /\ forall fs_i_pfc_step_unique_secondprevioussum_body_steps. (exists fs_lt_pfc_step_unique_secondprevioussum_body_steps_bound. fs_lt_pfc_step_unique_secondprevioussum_body_steps_bound + S fs_i_pfc_step_unique_secondprevioussum_body_steps = S (i)) -> exists fs_a_pfc_step_unique_secondprevioussum_body_steps fs_r_pfc_step_unique_secondprevioussum_body_steps fs_s_pfc_step_unique_secondprevioussum_body_steps. ((((exists fs_h_pfc_step_unique_secondprevioussum_body_steps_summand. fs_h_pfc_step_unique_secondprevioussum_body_steps_summand + S (fs_a_pfc_step_unique_secondprevioussum_body_steps) = S ((S (fs_i_pfc_step_unique_secondprevioussum_body_steps)) * pfc_terms_scale_step_unique_secondprevious)) /\ exists fs_q_pfc_step_unique_secondprevioussum_body_steps_summand. pfc_terms_code_step_unique_secondprevious = fs_q_pfc_step_unique_secondprevioussum_body_steps_summand * S ((S (fs_i_pfc_step_unique_secondprevioussum_body_steps)) * pfc_terms_scale_step_unique_secondprevious) + (fs_a_pfc_step_unique_secondprevioussum_body_steps))) /\ ((((exists fs_h_pfc_step_unique_secondprevioussum_body_steps_partial. fs_h_pfc_step_unique_secondprevioussum_body_steps_partial + S (fs_r_pfc_step_unique_secondprevioussum_body_steps) = S ((S (fs_i_pfc_step_unique_secondprevioussum_body_steps)) * fs_v_pfc_step_unique_secondprevioussum)) /\ exists fs_q_pfc_step_unique_secondprevioussum_body_steps_partial. fs_u_pfc_step_unique_secondprevioussum = fs_q_pfc_step_unique_secondprevioussum_body_steps_partial * S ((S (fs_i_pfc_step_unique_secondprevioussum_body_steps)) * fs_v_pfc_step_unique_secondprevioussum) + (fs_r_pfc_step_unique_secondprevioussum_body_steps))) /\ ((((exists fs_h_pfc_step_unique_secondprevioussum_body_steps_successor. fs_h_pfc_step_unique_secondprevioussum_body_steps_successor + S (fs_s_pfc_step_unique_secondprevioussum_body_steps) = S ((S (S fs_i_pfc_step_unique_secondprevioussum_body_steps)) * fs_v_pfc_step_unique_secondprevioussum)) /\ exists fs_q_pfc_step_unique_secondprevioussum_body_steps_successor. fs_u_pfc_step_unique_secondprevioussum = fs_q_pfc_step_unique_secondprevioussum_body_steps_successor * S ((S (S fs_i_pfc_step_unique_secondprevioussum_body_steps)) * fs_v_pfc_step_unique_secondprevioussum) + (fs_s_pfc_step_unique_secondprevioussum_body_steps))) /\ fs_s_pfc_step_unique_secondprevioussum_body_steps = fs_r_pfc_step_unique_secondprevioussum_body_steps + fs_a_pfc_step_unique_secondprevioussum_body_steps)))))) /\ ((((exists pfa_gap_step_unique_secondpreviousresiduebound. pfa_gap_step_unique_secondpreviousresiduebound + S (pfd_previous_step_unique_second) = (p)) /\ ((exists pfa_offset_left_step_unique_secondpreviousresiduecongruence pfa_offset_right_step_unique_secondpreviousresiduecongruence. (pfc_natural_sum_step_unique_secondprevious) + (p) * pfa_offset_left_step_unique_secondpreviousresiduecongruence = (pfd_previous_step_unique_second) + (p) * pfa_offset_right_step_unique_secondpreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_step_unique_secondsubtractleft. pfa_gap_step_unique_secondsubtractleft + S (pfd_previous_step_unique_second) = (p)) /\ (((exists pfa_gap_step_unique_secondsubtractright. pfa_gap_step_unique_secondsubtractright + S (pfd_difference_step_unique_second) = (p)) /\ ((((exists pfa_gap_step_unique_secondsubtractresultbound. pfa_gap_step_unique_secondsubtractresultbound + S (pfd_input_step_unique_second) = (p)) /\ ((exists pfa_offset_left_step_unique_secondsubtractresultcongruence pfa_offset_right_step_unique_secondsubtractresultcongruence. ((pfd_previous_step_unique_second) + (pfd_difference_step_unique_second)) + (p) * pfa_offset_left_step_unique_secondsubtractresultcongruence = (pfd_input_step_unique_second) + (p) * pfa_offset_right_step_unique_secondsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_step_unique_secondmultiplyleft. pfa_gap_step_unique_secondmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_step_unique_secondmultiplyright. pfa_gap_step_unique_secondmultiplyright + S (pfd_difference_step_unique_second) = (p)) /\ ((((exists pfa_gap_step_unique_secondmultiplyresultbound. pfa_gap_step_unique_secondmultiplyresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_step_unique_secondmultiplyresultcongruence pfa_offset_right_step_unique_secondmultiplyresultcongruence. ((k) * (pfd_difference_step_unique_second)) + (p) * pfa_offset_left_step_unique_secondmultiplyresultcongruence = (r) + (p) * pfa_offset_right_step_unique_secondmultiplyresultcongruence)))))))))))))))) -> q=r

Complete tactic proof in conservative notation

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

72 script commands · 11 reading checkpoints · 3 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.

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 i
02Fix variables and assumptionsL11–14

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

  1. L11
    intro q
  2. L12
    intro r
  3. L13
    intro hfirst
  4. L14
    intro hsecond
03Separate the logical casesL15–24

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

  1. L15
    cases hfirst
  2. L16
    cases hfirst_witness
  3. L17
    cases hfirst_witness_witness
  4. L18
    cases hfirst_witness_witness_witness
  5. L19
    cases hfirst_witness_witness_witness_right
  6. L20
    cases hfirst_witness_witness_witness_right_right
  7. L21
    cases hsecond
  8. L22
    cases hsecond_witness
  9. L23
    cases hsecond_witness_witness
  10. L24
    cases hsecond_witness_witness_witness
04Separate the logical casesL25–26

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

  1. L25
    cases hsecond_witness_witness_witness_right
  2. L26
    cases hsecond_witness_witness_witness_right_right
05Establish hinputL27–35

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

  1. L27
    have hinput : x=x3
  2. L28
    specialize beta_at_unique (ab)
  3. L29
    specialize beta_at_unique (ac)
  4. L30
    specialize beta_at_unique (i)
  5. L31
    specialize beta_at_unique (x)
  6. L32
    specialize beta_at_unique (x3)
  7. L33
    apply beta_at_unique
  8. L34
    exact hfirst_witness_witness_witness_left
  9. L35
    exact hsecond_witness_witness_witness_left
06Establish hpreviousL36–45

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

  1. L36
    have hprevious : x1=x4
  2. L37
    specialize prime_field_convolution_coefficient_functional (p)
  3. L38
    specialize prime_field_convolution_coefficient_functional (qb)
  4. L39
    specialize prime_field_convolution_coefficient_functional (qc)
  5. L40
    specialize prime_field_convolution_coefficient_functional (i)
  6. L41
    specialize prime_field_convolution_coefficient_functional (bb)
  7. L42
    specialize prime_field_convolution_coefficient_functional (bc)
  8. L43
    specialize prime_field_convolution_coefficient_functional (M)
  9. L44
    specialize prime_field_convolution_coefficient_functional (i)
  10. L45
    specialize prime_field_convolution_coefficient_functional (x1)
07Use earlier factsL46–49

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

  1. L46
    specialize prime_field_convolution_coefficient_functional (x4)
  2. L47
    apply prime_field_convolution_coefficient_functional
  3. L48
    exact hfirst_witness_witness_witness_right_left
  4. L49
    exact hsecond_witness_witness_witness_right_left
08Calculate and transport equalitiesL50–53

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

  1. L50
    rewrite hinput at hfirst_witness_witness_witness_right_right_left
  2. L51
    rewrite hinput at hfirst_witness_witness_witness_right_right_left
  3. L52
    rewrite hprevious at hfirst_witness_witness_witness_right_right_left
  4. L53
    rewrite hprevious at hfirst_witness_witness_witness_right_right_left
09Establish hdifferenceL54–63

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

  1. L54
    have hdifference : x2=x5
  2. L55
    specialize prime_field_add_cancel_left (p)
  3. L56
    specialize prime_field_add_cancel_left (x4)
  4. L57
    specialize prime_field_add_cancel_left (x2)
  5. L58
    specialize prime_field_add_cancel_left (x5)
  6. L59
    specialize prime_field_add_cancel_left (x3)
  7. L60
    apply prime_field_add_cancel_left
  8. L61
    exact hfirst_witness_witness_witness_right_right_left
  9. L62
    exact hsecond_witness_witness_witness_right_right_left
  10. L63
    rewrite hdifference at hfirst_witness_witness_witness_right_right_right
10Calculate and transport equalitiesL64–64

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

  1. L64
    rewrite hdifference at hfirst_witness_witness_witness_right_right_right
11Use earlier factsL65–72

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

  1. L65
    specialize prime_field_multiply_functional (p)
  2. L66
    specialize prime_field_multiply_functional (k)
  3. L67
    specialize prime_field_multiply_functional (x5)
  4. L68
    specialize prime_field_multiply_functional (q)
  5. L69
    specialize prime_field_multiply_functional (r)
  6. L70
    apply prime_field_multiply_functional
  7. L71
    exact hfirst_witness_witness_witness_right_right_right
  8. L72
    exact hsecond_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 72 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 i
  11. 0011intro q
  12. 0012intro r
  13. 0013intro hfirst
  14. 0014intro hsecond
  15. 0015cases hfirst
  16. 0016cases hfirst_witness
  17. 0017cases hfirst_witness_witness
  18. 0018cases hfirst_witness_witness_witness
  19. 0019cases hfirst_witness_witness_witness_right
  20. 0020cases hfirst_witness_witness_witness_right_right
  21. 0021cases hsecond
  22. 0022cases hsecond_witness
  23. 0023cases hsecond_witness_witness
  24. 0024cases hsecond_witness_witness_witness
  25. 0025cases hsecond_witness_witness_witness_right
  26. 0026cases hsecond_witness_witness_witness_right_right
  27. 0027have hinput : x=x3
  28. 0028specialize beta_at_unique (ab)
  29. 0029specialize beta_at_unique (ac)
  30. 0030specialize beta_at_unique (i)
  31. 0031specialize beta_at_unique (x)
  32. 0032specialize beta_at_unique (x3)
  33. 0033apply beta_at_unique
  34. 0034exact hfirst_witness_witness_witness_left
  35. 0035exact hsecond_witness_witness_witness_left
  36. 0036have hprevious : x1=x4
  37. 0037specialize prime_field_convolution_coefficient_functional (p)
  38. 0038specialize prime_field_convolution_coefficient_functional (qb)
  39. 0039specialize prime_field_convolution_coefficient_functional (qc)
  40. 0040specialize prime_field_convolution_coefficient_functional (i)
  41. 0041specialize prime_field_convolution_coefficient_functional (bb)
  42. 0042specialize prime_field_convolution_coefficient_functional (bc)
  43. 0043specialize prime_field_convolution_coefficient_functional (M)
  44. 0044specialize prime_field_convolution_coefficient_functional (i)
  45. 0045specialize prime_field_convolution_coefficient_functional (x1)
  46. 0046specialize prime_field_convolution_coefficient_functional (x4)
  47. 0047apply prime_field_convolution_coefficient_functional
  48. 0048exact hfirst_witness_witness_witness_right_left
  49. 0049exact hsecond_witness_witness_witness_right_left
  50. 0050rewrite hinput at hfirst_witness_witness_witness_right_right_left
  51. 0051rewrite hinput at hfirst_witness_witness_witness_right_right_left
  52. 0052rewrite hprevious at hfirst_witness_witness_witness_right_right_left
  53. 0053rewrite hprevious at hfirst_witness_witness_witness_right_right_left
  54. 0054have hdifference : x2=x5
  55. 0055specialize prime_field_add_cancel_left (p)
  56. 0056specialize prime_field_add_cancel_left (x4)
  57. 0057specialize prime_field_add_cancel_left (x2)
  58. 0058specialize prime_field_add_cancel_left (x5)
  59. 0059specialize prime_field_add_cancel_left (x3)
  60. 0060apply prime_field_add_cancel_left
  61. 0061exact hfirst_witness_witness_witness_right_right_left
  62. 0062exact hsecond_witness_witness_witness_right_right_left
  63. 0063rewrite hdifference at hfirst_witness_witness_witness_right_right_right
  64. 0064rewrite hdifference at hfirst_witness_witness_witness_right_right_right
  65. 0065specialize prime_field_multiply_functional (p)
  66. 0066specialize prime_field_multiply_functional (k)
  67. 0067specialize prime_field_multiply_functional (x5)
  68. 0068specialize prime_field_multiply_functional (q)
  69. 0069specialize prime_field_multiply_functional (r)
  70. 0070apply prime_field_multiply_functional
  71. 0071exact hfirst_witness_witness_witness_right_right_right
  72. 0072exact hsecond_witness_witness_witness_right_right_right