ND0334

PolynomialLeftPad(b,c,L,t,d,e)

The target has t actual leading zero entries and then copies the L decoded source entries. It has annotated length t+L. This is left padding in highest-degree-first order, not right padding or multiplication by X. Canonical coefficients, a field modulus and formal polynomial equality are not assumptions of this graph.

Conservative notation; not a theorem, primitive, or axiom.

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

Definition in prerequisite notation

(∀ x. Lt(x,t) → BetaAt(d,e,x,0)) ∧ (∀ x. ∀ y. Lt(x,L) → BetaAt(b,c,x,y) → BetaAt(d,e,t + x,y))

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
((forall pfp_repeat_index_working_euclidean_definitionzeros. (exists pfa_gap_working_euclidean_definitionzerosindex. pfa_gap_working_euclidean_definitionzerosindex + S (pfp_repeat_index_working_euclidean_definitionzeros) = ((t))) -> (((exists ff_h_pfp_working_euclidean_definitionzerosentry. ff_h_pfp_working_euclidean_definitionzerosentry + S (0) = S ((S (pfp_repeat_index_working_euclidean_definitionzeros)) * (e))) /\ exists ff_q_pfp_working_euclidean_definitionzerosentry. (d) = ff_q_pfp_working_euclidean_definitionzerosentry * S ((S (pfp_repeat_index_working_euclidean_definitionzeros)) * (e)) + (0)))) /\ ((forall pfrep_index_working_euclidean_definition pfrep_value_working_euclidean_definition. (exists pfa_gap_working_euclidean_definitionbound. pfa_gap_working_euclidean_definitionbound + S (pfrep_index_working_euclidean_definition) = ((L))) -> (((exists ff_h_pfp_working_euclidean_definitioninput. ff_h_pfp_working_euclidean_definitioninput + S (pfrep_value_working_euclidean_definition) = S ((S (pfrep_index_working_euclidean_definition)) * (c))) /\ exists ff_q_pfp_working_euclidean_definitioninput. (b) = ff_q_pfp_working_euclidean_definitioninput * S ((S (pfrep_index_working_euclidean_definition)) * (c)) + (pfrep_value_working_euclidean_definition))) -> (((exists ff_h_pfp_working_euclidean_definitionoutput. ff_h_pfp_working_euclidean_definitionoutput + S (pfrep_value_working_euclidean_definition) = S ((S (((t))+pfrep_index_working_euclidean_definition)) * (e))) /\ exists ff_q_pfp_working_euclidean_definitionoutput. (d) = ff_q_pfp_working_euclidean_definitionoutput * S ((S (((t))+pfrep_index_working_euclidean_definition)) * (e)) + (pfrep_value_working_euclidean_definition))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Lt(a,b)BetaAt(b,c,i,x)

Definitions depending on this notation

none

Checked theorems using this definition

PG001A · prime_field_polynomial_append_shift_constant_addPG001B · prime_field_polynomial_append_shift_constant_decomposition_existsPG001C · prime_field_convolution_coefficient_right_append_addPG001D · prime_field_polynomial_shift_scale_aligned_sum_existsPG001E · prime_field_polynomial_convolution_right_append_equivalentPG001F · prime_field_polynomial_convolution_right_append_existsPG0021 · prime_field_polynomial_convolution_shift_scale_aligned_equivalentPG0022 · prime_field_polynomial_shift_scale_aligned_congruentPG0023 · prime_field_polynomial_convolution_associativity_append_stepPG0035 · prime_field_polynomial_bounded_representative_at_length_exists