PX0029

prime_field_polynomial_quotient_prefix_empty

The actual empty quotient execution exists for all encodings and makes no assertion about an unused scalar or entry.

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. FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,qb,qc,0)

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

Definition DAG

FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,qb,qc,N) · 1

Actual proof prerequisites

lt_not_le · checked external prerequisitezero_le · checked external prerequisite
Original expanded first-order statement 
forall p k ab ac bb bc M qb qc. forall pfd_index_division_empty. (exists pfa_gap_division_emptybound. pfa_gap_division_emptybound + S (pfd_index_division_empty) = (0)) -> exists pfd_value_division_empty. ((((exists ff_h_pfp_division_emptyentry. ff_h_pfp_division_emptyentry + S (pfd_value_division_empty) = S ((S (pfd_index_division_empty)) * qc)) /\ exists ff_q_pfp_division_emptyentry. qb = ff_q_pfp_division_emptyentry * S ((S (pfd_index_division_empty)) * qc) + (pfd_value_division_empty))) /\ ((exists pfd_input_division_emptystep pfd_previous_division_emptystep pfd_difference_division_emptystep. ((((exists ff_h_pfp_division_emptystepinput. ff_h_pfp_division_emptystepinput + S (pfd_input_division_emptystep) = S ((S (pfd_index_division_empty)) * ac)) /\ exists ff_q_pfp_division_emptystepinput. ab = ff_q_pfp_division_emptystepinput * S ((S (pfd_index_division_empty)) * ac) + (pfd_input_division_emptystep))) /\ (((exists pfc_terms_code_division_emptystepprevious pfc_terms_scale_division_emptystepprevious pfc_natural_sum_division_emptystepprevious. ((forall pfc_index_division_emptysteppreviousdiagonal. (exists pfa_gap_division_emptysteppreviousdiagonalbound. pfa_gap_division_emptysteppreviousdiagonalbound + S (pfc_index_division_emptysteppreviousdiagonal) = (S (pfd_index_division_empty))) -> exists pfc_value_division_emptysteppreviousdiagonal. ((((exists ff_h_pfp_division_emptysteppreviousdiagonalentry. ff_h_pfp_division_emptysteppreviousdiagonalentry + S (pfc_value_division_emptysteppreviousdiagonal) = S ((S (pfc_index_division_emptysteppreviousdiagonal)) * pfc_terms_scale_division_emptystepprevious)) /\ exists ff_q_pfp_division_emptysteppreviousdiagonalentry. pfc_terms_code_division_emptystepprevious = ff_q_pfp_division_emptysteppreviousdiagonalentry * S ((S (pfc_index_division_emptysteppreviousdiagonal)) * pfc_terms_scale_division_emptystepprevious) + (pfc_value_division_emptysteppreviousdiagonal))) /\ ((exists pfc_complement_division_emptysteppreviousdiagonalterm pfc_left_division_emptysteppreviousdiagonalterm pfc_right_division_emptysteppreviousdiagonalterm. (((pfc_index_division_emptysteppreviousdiagonal)+pfc_complement_division_emptysteppreviousdiagonalterm=(pfd_index_division_empty)) /\ ((((((exists pfa_gap_division_emptysteppreviousdiagonaltermleftinside. pfa_gap_division_emptysteppreviousdiagonaltermleftinside + S (pfc_index_division_emptysteppreviousdiagonal) = (pfd_index_division_empty)) /\ ((((exists ff_h_pfp_division_emptysteppreviousdiagonaltermleftentry. ff_h_pfp_division_emptysteppreviousdiagonaltermleftentry + S (pfc_left_division_emptysteppreviousdiagonalterm) = S ((S (pfc_index_division_emptysteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_emptysteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_emptysteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_emptysteppreviousdiagonal)) * qc) + (pfc_left_division_emptysteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_emptysteppreviousdiagonaltermleftoutside. pfc_gap_division_emptysteppreviousdiagonaltermleftoutside+(pfd_index_division_empty)=(pfc_index_division_emptysteppreviousdiagonal)) /\ (((pfc_left_division_emptysteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_emptysteppreviousdiagonaltermrightinside. pfa_gap_division_emptysteppreviousdiagonaltermrightinside + S (pfc_complement_division_emptysteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_emptysteppreviousdiagonaltermrightentry. ff_h_pfp_division_emptysteppreviousdiagonaltermrightentry + S (pfc_right_division_emptysteppreviousdiagonalterm) = S ((S (pfc_complement_division_emptysteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_emptysteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_emptysteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_emptysteppreviousdiagonalterm)) * bc) + (pfc_right_division_emptysteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_emptysteppreviousdiagonaltermrightoutside. pfc_gap_division_emptysteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_emptysteppreviousdiagonalterm)) /\ (((pfc_right_division_emptysteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_emptysteppreviousdiagonal)=pfc_left_division_emptysteppreviousdiagonalterm*pfc_right_division_emptysteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_emptystepprevioussum fs_v_pfc_division_emptystepprevioussum. ((((exists fs_h_pfc_division_emptystepprevioussum_body_start. fs_h_pfc_division_emptystepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_emptystepprevioussum)) /\ exists fs_q_pfc_division_emptystepprevioussum_body_start. fs_u_pfc_division_emptystepprevioussum = fs_q_pfc_division_emptystepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_emptystepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_emptystepprevioussum_body_terminal. fs_h_pfc_division_emptystepprevioussum_body_terminal + S (pfc_natural_sum_division_emptystepprevious) = S ((S (S (pfd_index_division_empty))) * fs_v_pfc_division_emptystepprevioussum)) /\ exists fs_q_pfc_division_emptystepprevioussum_body_terminal. fs_u_pfc_division_emptystepprevioussum = fs_q_pfc_division_emptystepprevioussum_body_terminal * S ((S (S (pfd_index_division_empty))) * fs_v_pfc_division_emptystepprevioussum) + (pfc_natural_sum_division_emptystepprevious))) /\ forall fs_i_pfc_division_emptystepprevioussum_body_steps. (exists fs_lt_pfc_division_emptystepprevioussum_body_steps_bound. fs_lt_pfc_division_emptystepprevioussum_body_steps_bound + S fs_i_pfc_division_emptystepprevioussum_body_steps = S (pfd_index_division_empty)) -> exists fs_a_pfc_division_emptystepprevioussum_body_steps fs_r_pfc_division_emptystepprevioussum_body_steps fs_s_pfc_division_emptystepprevioussum_body_steps. ((((exists fs_h_pfc_division_emptystepprevioussum_body_steps_summand. fs_h_pfc_division_emptystepprevioussum_body_steps_summand + S (fs_a_pfc_division_emptystepprevioussum_body_steps) = S ((S (fs_i_pfc_division_emptystepprevioussum_body_steps)) * pfc_terms_scale_division_emptystepprevious)) /\ exists fs_q_pfc_division_emptystepprevioussum_body_steps_summand. pfc_terms_code_division_emptystepprevious = fs_q_pfc_division_emptystepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_emptystepprevioussum_body_steps)) * pfc_terms_scale_division_emptystepprevious) + (fs_a_pfc_division_emptystepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_emptystepprevioussum_body_steps_partial. fs_h_pfc_division_emptystepprevioussum_body_steps_partial + S (fs_r_pfc_division_emptystepprevioussum_body_steps) = S ((S (fs_i_pfc_division_emptystepprevioussum_body_steps)) * fs_v_pfc_division_emptystepprevioussum)) /\ exists fs_q_pfc_division_emptystepprevioussum_body_steps_partial. fs_u_pfc_division_emptystepprevioussum = fs_q_pfc_division_emptystepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_emptystepprevioussum_body_steps)) * fs_v_pfc_division_emptystepprevioussum) + (fs_r_pfc_division_emptystepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_emptystepprevioussum_body_steps_successor. fs_h_pfc_division_emptystepprevioussum_body_steps_successor + S (fs_s_pfc_division_emptystepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_emptystepprevioussum_body_steps)) * fs_v_pfc_division_emptystepprevioussum)) /\ exists fs_q_pfc_division_emptystepprevioussum_body_steps_successor. fs_u_pfc_division_emptystepprevioussum = fs_q_pfc_division_emptystepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_emptystepprevioussum_body_steps)) * fs_v_pfc_division_emptystepprevioussum) + (fs_s_pfc_division_emptystepprevioussum_body_steps))) /\ fs_s_pfc_division_emptystepprevioussum_body_steps = fs_r_pfc_division_emptystepprevioussum_body_steps + fs_a_pfc_division_emptystepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_emptysteppreviousresiduebound. pfa_gap_division_emptysteppreviousresiduebound + S (pfd_previous_division_emptystep) = (p)) /\ ((exists pfa_offset_left_division_emptysteppreviousresiduecongruence pfa_offset_right_division_emptysteppreviousresiduecongruence. (pfc_natural_sum_division_emptystepprevious) + (p) * pfa_offset_left_division_emptysteppreviousresiduecongruence = (pfd_previous_division_emptystep) + (p) * pfa_offset_right_division_emptysteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_emptystepsubtractleft. pfa_gap_division_emptystepsubtractleft + S (pfd_previous_division_emptystep) = (p)) /\ (((exists pfa_gap_division_emptystepsubtractright. pfa_gap_division_emptystepsubtractright + S (pfd_difference_division_emptystep) = (p)) /\ ((((exists pfa_gap_division_emptystepsubtractresultbound. pfa_gap_division_emptystepsubtractresultbound + S (pfd_input_division_emptystep) = (p)) /\ ((exists pfa_offset_left_division_emptystepsubtractresultcongruence pfa_offset_right_division_emptystepsubtractresultcongruence. ((pfd_previous_division_emptystep) + (pfd_difference_division_emptystep)) + (p) * pfa_offset_left_division_emptystepsubtractresultcongruence = (pfd_input_division_emptystep) + (p) * pfa_offset_right_division_emptystepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_emptystepmultiplyleft. pfa_gap_division_emptystepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_emptystepmultiplyright. pfa_gap_division_emptystepmultiplyright + S (pfd_difference_division_emptystep) = (p)) /\ ((((exists pfa_gap_division_emptystepmultiplyresultbound. pfa_gap_division_emptystepmultiplyresultbound + S (pfd_value_division_empty) = (p)) /\ ((exists pfa_offset_left_division_emptystepmultiplyresultcongruence pfa_offset_right_division_emptystepmultiplyresultcongruence. ((k) * (pfd_difference_division_emptystep)) + (p) * pfa_offset_left_division_emptystepmultiplyresultcongruence = (pfd_value_division_empty) + (p) * pfa_offset_right_division_emptystepmultiplyresultcongruence))))))))))))))))))

Complete tactic proof in conservative notation

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

18 script commands · 4 reading checkpoints · 0 local claims

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

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

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

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

  1. L11
    intro hi
03Separate the logical casesL12–12

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

  1. L12
    exfalso
04Use earlier factsL13–18

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

  1. L13
    specialize lt_not_le (i)
  2. L14
    specialize lt_not_le (0)
  3. L15
    apply lt_not_le
  4. L16
    exact hi
  5. L17
    specialize zero_le (i)
  6. L18
    apply zero_le

Library-wide reading audit

Original defined command ledger · 18 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 hi
  12. 0012exfalso
  13. 0013specialize lt_not_le (i)
  14. 0014specialize lt_not_le (0)
  15. 0015apply lt_not_le
  16. 0016exact hi
  17. 0017specialize zero_le (i)
  18. 0018apply zero_le