PQ0050 — prime_field_polynomial_synthetic_middle_coefficients

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

All coefficients retain the established highest-degree-first order. Trimming handles empty and all-zero prefixes; monic normalization requires a nonzero leading coefficient. Synthetic division has a nonempty input of length S n and a quotient of length n, unique in decoded values. Its coefficient recurrence, actual evaluation remainder and positive-degree drop are checked. General polynomial Euclidean division, gcd/Bezout, an arbitrary-convolution factor theorem, irreducible-polynomial existence and the full G091 prime-power-field endpoint remain open. These exact theorems are first admitted to Alpha v32; Stable remains unchanged.

Exact theorem in conservative defined notation

∀ p. ∀ b. ∀ c. ∀ a. ∀ n. ∀ qb. ∀ qc. ∀ r. ∀ i. ∀ h. ∀ j. ∀ v. Prime(p) → FpSyntheticDivision(p,b,c,a,S n,qb,qc,r) → Lt(i,n) → BetaAt(qb,qc,i,h) → BetaAt(qb,qc,S i,j) → BetaAt(b,c,S i,v) → ∃ x. FpMul(p,h,a,x) ∧ FpAdd(p,x,v,j)

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

Definition DAG

FpAdd(p,a,b,c) · 1 FpMul(p,a,b,c) · 1 FpSyntheticDivision(p,b,c,a,n,qb,qc,r) · 1 Lt(a,b) · 1 Prime(p) · 1 BetaAt(b,c,i,x) · 3

Actual proof prerequisites

prime_field_polynomial_horner_transition_values prime_field_polynomial_synthetic_quotient_entry le_succ · checked external prerequisite succ_le_succ · checked external prerequisite

Original expanded first-order statement

forall p b c a n qb qc r i h j v. (~((p) = 1) /\ forall pfa_factor_left_middle_prime pfa_factor_right_middle_prime. (p) = pfa_factor_left_middle_prime * pfa_factor_right_middle_prime -> pfa_factor_left_middle_prime = 1 \/ pfa_factor_right_middle_prime = 1) -> (exists pfs_history_code_middle_division pfs_history_scale_middle_division. ((((exists pfa_gap_middle_divisiontracebase. pfa_gap_middle_divisiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_middle_divisiontraceinitial. ff_h_pfp_middle_divisiontraceinitial + S (0) = S ((S (0)) * pfs_history_scale_middle_division)) /\ exists ff_q_pfp_middle_divisiontraceinitial. pfs_history_code_middle_division = ff_q_pfp_middle_divisiontraceinitial * S ((S (0)) * pfs_history_scale_middle_division) + (0))) /\ (((((exists ff_h_pfp_middle_divisiontraceterminal. ff_h_pfp_middle_divisiontraceterminal + S (r) = S ((S (S (S n))) * pfs_history_scale_middle_division)) /\ exists ff_q_pfp_middle_divisiontraceterminal. pfs_history_code_middle_division = ff_q_pfp_middle_divisiontraceterminal * S ((S (S (S n))) * pfs_history_scale_middle_division) + (r))) /\ ((forall pfh_index_middle_divisiontracesteps. (exists pfa_gap_middle_divisiontracestepsindex. pfa_gap_middle_divisiontracestepsindex + S (pfh_index_middle_divisiontracesteps) = (S (S n))) -> (exists pfh_coefficient_middle_divisiontracestepsstep pfh_before_middle_divisiontracestepsstep pfh_after_middle_divisiontracestepsstep pfh_product_middle_divisiontracestepsstep. ((((exists ff_h_pfp_middle_divisiontracestepsstepcoefficient. ff_h_pfp_middle_divisiontracestepsstepcoefficient + S (pfh_coefficient_middle_divisiontracestepsstep) = S ((S (pfh_index_middle_divisiontracesteps)) * c)) /\ exists ff_q_pfp_middle_divisiontracestepsstepcoefficient. b = ff_q_pfp_middle_divisiontracestepsstepcoefficient * S ((S (pfh_index_middle_divisiontracesteps)) * c) + (pfh_coefficient_middle_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_middle_divisiontracestepsstepbefore. ff_h_pfp_middle_divisiontracestepsstepbefore + S (pfh_before_middle_divisiontracestepsstep) = S ((S (pfh_index_middle_divisiontracesteps)) * pfs_history_scale_middle_division)) /\ exists ff_q_pfp_middle_divisiontracestepsstepbefore. pfs_history_code_middle_division = ff_q_pfp_middle_divisiontracestepsstepbefore * S ((S (pfh_index_middle_divisiontracesteps)) * pfs_history_scale_middle_division) + (pfh_before_middle_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_middle_divisiontracestepsstepafter. ff_h_pfp_middle_divisiontracestepsstepafter + S (pfh_after_middle_divisiontracestepsstep) = S ((S (S (pfh_index_middle_divisiontracesteps))) * pfs_history_scale_middle_division)) /\ exists ff_q_pfp_middle_divisiontracestepsstepafter. pfs_history_code_middle_division = ff_q_pfp_middle_divisiontracestepsstepafter * S ((S (S (pfh_index_middle_divisiontracesteps))) * pfs_history_scale_middle_division) + (pfh_after_middle_divisiontracestepsstep))) /\ (((((exists pfa_gap_middle_divisiontracestepsstepmultiplyleft. pfa_gap_middle_divisiontracestepsstepmultiplyleft + S (pfh_before_middle_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_middle_divisiontracestepsstepmultiplyright. pfa_gap_middle_divisiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_middle_divisiontracestepsstepmultiplyresultbound. pfa_gap_middle_divisiontracestepsstepmultiplyresultbound + S (pfh_product_middle_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_middle_divisiontracestepsstepmultiplyresultcongruence pfa_offset_right_middle_divisiontracestepsstepmultiplyresultcongruence. ((pfh_before_middle_divisiontracestepsstep) * (a)) + (p) * pfa_offset_left_middle_divisiontracestepsstepmultiplyresultcongruence = (pfh_product_middle_divisiontracestepsstep) + (p) * pfa_offset_right_middle_divisiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_middle_divisiontracestepsstepaddleft. pfa_gap_middle_divisiontracestepsstepaddleft + S (pfh_product_middle_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_middle_divisiontracestepsstepaddright. pfa_gap_middle_divisiontracestepsstepaddright + S (pfh_coefficient_middle_divisiontracestepsstep) = (p)) /\ ((((exists pfa_gap_middle_divisiontracestepsstepaddresultbound. pfa_gap_middle_divisiontracestepsstepaddresultbound + S (pfh_after_middle_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_middle_divisiontracestepsstepaddresultcongruence pfa_offset_right_middle_divisiontracestepsstepaddresultcongruence. ((pfh_product_middle_divisiontracestepsstep) + (pfh_coefficient_middle_divisiontracestepsstep)) + (p) * pfa_offset_left_middle_divisiontracestepsstepaddresultcongruence = (pfh_after_middle_divisiontracestepsstep) + (p) * pfa_offset_right_middle_divisiontracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_middle_divisionquotient ff_source_mcp_pfs_middle_divisionquotient ff_target_mcp_pfs_middle_divisionquotient. (exists mcp_gap_pfs_middle_divisionquotient_bound. mcp_gap_pfs_middle_divisionquotient_bound + S (ff_index_mcp_pfs_middle_divisionquotient) = (S n)) -> (((exists fs_h_mcp_pfs_middle_divisionquotient_source. fs_h_mcp_pfs_middle_divisionquotient_source + S (ff_source_mcp_pfs_middle_divisionquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_middle_divisionquotient)) * pfs_history_scale_middle_division)) /\ exists fs_q_mcp_pfs_middle_divisionquotient_source. pfs_history_code_middle_division = fs_q_mcp_pfs_middle_divisionquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_middle_divisionquotient)) * pfs_history_scale_middle_division) + (ff_source_mcp_pfs_middle_divisionquotient))) -> (((exists fs_h_mcp_pfs_middle_divisionquotient_target. fs_h_mcp_pfs_middle_divisionquotient_target + S (ff_target_mcp_pfs_middle_divisionquotient) = S ((S (ff_index_mcp_pfs_middle_divisionquotient)) * qc)) /\ exists fs_q_mcp_pfs_middle_divisionquotient_target. qb = fs_q_mcp_pfs_middle_divisionquotient_target * S ((S (ff_index_mcp_pfs_middle_divisionquotient)) * qc) + (ff_target_mcp_pfs_middle_divisionquotient))) -> ff_target_mcp_pfs_middle_divisionquotient = ff_source_mcp_pfs_middle_divisionquotient)))) -> (exists pfa_gap_middle_index. pfa_gap_middle_index + S (i) = (n)) -> (((exists ff_h_pfp_middle_previous. ff_h_pfp_middle_previous + S (h) = S ((S (i)) * qc)) /\ exists ff_q_pfp_middle_previous. qb = ff_q_pfp_middle_previous * S ((S (i)) * qc) + (h))) -> (((exists ff_h_pfp_middle_next. ff_h_pfp_middle_next + S (j) = S ((S (S i)) * qc)) /\ exists ff_q_pfp_middle_next. qb = ff_q_pfp_middle_next * S ((S (S i)) * qc) + (j))) -> (((exists ff_h_pfp_middle_input. ff_h_pfp_middle_input + S (v) = S ((S (S i)) * c)) /\ exists ff_q_pfp_middle_input. b = ff_q_pfp_middle_input * S ((S (S i)) * c) + (v))) -> exists k. ((((exists pfa_gap_middle_productleft. pfa_gap_middle_productleft + S (h) = (p)) /\ (((exists pfa_gap_middle_productright. pfa_gap_middle_productright + S (a) = (p)) /\ ((((exists pfa_gap_middle_productresultbound. pfa_gap_middle_productresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_middle_productresultcongruence pfa_offset_right_middle_productresultcongruence. ((h) * (a)) + (p) * pfa_offset_left_middle_productresultcongruence = (k) + (p) * pfa_offset_right_middle_productresultcongruence))))))))) /\ ((((exists pfa_gap_middle_sumleft. pfa_gap_middle_sumleft + S (k) = (p)) /\ (((exists pfa_gap_middle_sumright. pfa_gap_middle_sumright + S (v) = (p)) /\ ((((exists pfa_gap_middle_sumresultbound. pfa_gap_middle_sumresultbound + S (j) = (p)) /\ ((exists pfa_offset_left_middle_sumresultcongruence pfa_offset_right_middle_sumresultcongruence. ((k) + (v)) + (p) * pfa_offset_left_middle_sumresultcongruence = (j) + (p) * pfa_offset_right_middle_sumresultcongruence)))))))))))

Complete tactic proof in conservative notation

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

63 script commands · 7 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.

Named ingredients (2)

prime field polynomial horner transition values prime field polynomial synthetic quotient entry

01Fix variables and assumptionsL1–10

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

L1
intro p
L2
intro b
L3
intro c
L4
intro a
L5
intro n
L6
intro qb
L7
intro qc
L8
intro r
L9
intro i
L10
intro h

02Fix variables and assumptionsL11–18

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

L11
intro j
L12
intro v
L13
intro hp
L14
intro hs
L15
intro hi
L16
intro hh
L17
intro hj
L18
intro hv

03Use earlier factsL19–28