ND0015

MatrixPointwiseAdd(mb,mc,sb,sc,tb,tc,l)

The complete beta-coded pointwise sum of two exact bounded natural vector prefixes.

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. Exact original first-admission records.

Definition in prerequisite notation

∀ ff_index_mcp_add_advanced. ∀ ff_left_mcp_add_advanced. ∀ ff_right_mcp_add_advanced. ∀ ff_target_mcp_add_advanced. Lt(ff_index_mcp_add_advanced,l) → Beta(mb,mc,ff_index_mcp_add_advanced,ff_left_mcp_add_advanced) → Beta(sb,sc,ff_index_mcp_add_advanced,ff_right_mcp_add_advanced) → Beta(tb,tc,ff_index_mcp_add_advanced,ff_target_mcp_add_advanced) → ff_target_mcp_add_advanced = ff_left_mcp_add_advanced + ff_right_mcp_add_advanced

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

Hygienic expanded first-order definition 
forall ff_index_mcp_add_advanced ff_left_mcp_add_advanced ff_right_mcp_add_advanced ff_target_mcp_add_advanced. (exists mcp_gap_advanced_bound. mcp_gap_advanced_bound + S (ff_index_mcp_add_advanced) = (l)) -> (((exists fs_h_mcp_advanced_left. fs_h_mcp_advanced_left + S (ff_left_mcp_add_advanced) = S ((S (ff_index_mcp_add_advanced)) * mc)) /\ exists fs_q_mcp_advanced_left. mb = fs_q_mcp_advanced_left * S ((S (ff_index_mcp_add_advanced)) * mc) + (ff_left_mcp_add_advanced))) -> (((exists fs_h_mcp_advanced_right. fs_h_mcp_advanced_right + S (ff_right_mcp_add_advanced) = S ((S (ff_index_mcp_add_advanced)) * sc)) /\ exists fs_q_mcp_advanced_right. sb = fs_q_mcp_advanced_right * S ((S (ff_index_mcp_add_advanced)) * sc) + (ff_right_mcp_add_advanced))) -> (((exists fs_h_mcp_advanced_target. fs_h_mcp_advanced_target + S (ff_target_mcp_add_advanced) = S ((S (ff_index_mcp_add_advanced)) * tc)) /\ exists fs_q_mcp_advanced_target. tb = fs_q_mcp_advanced_target * S ((S (ff_index_mcp_add_advanced)) * tc) + (ff_target_mcp_add_advanced))) -> ff_target_mcp_add_advanced = ff_left_mcp_add_advanced + ff_right_mcp_add_advanced

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

Direct definition dependencies

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

Definitions depending on this notation

SignedMatrixProduct(ab,ac,db,dc,eb,ec,fb,fc,w,v,r,pb,pc,nb,nc)

Checked theorems using this definition

DL0065 · integer_span_natural_cell_add_rightDL0067 · integer_span_natural_product_add_rightDL0068 · integer_span_pointwise_add_interchangeDL006A · integer_span_signed_product_equal_coefficientsDL006B · integer_span_signed_product_add_rightDL0073 · integer_vector_add_from_component_sumsDL0074 · integer_vector_add_existsDL007B · integer_matrix_vector_add_coefficientsDL007C · integer_matrix_vector_add_constructiveDL0082 · integer_column_span_add_closedDL008A · matrix_integer_signed_sum_balance