ND0291

BetaZeroExtend(b,c,L,i,a)

Decode the genuine beta entry when i<L and return zero when L<=i. This explicitly length-annotated zero extension imposes no false condition on raw beta values beyond the represented prefix.

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

Lt(i,L) ∧ BetaAt(b,c,i,a) ∨ Le(L,i) ∧ a = 0

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

Hygienic expanded first-order definition 
(((exists pfa_gap_lowercontinuationinside. pfa_gap_lowercontinuationinside + S ((i)) = ((L))) /\ ((((exists ff_h_pfp_lowercontinuationentry. ff_h_pfp_lowercontinuationentry + S ((a)) = S ((S ((i))) * (c))) /\ exists ff_q_pfp_lowercontinuationentry. (b) = ff_q_pfp_lowercontinuationentry * S ((S ((i))) * (c)) + ((a))))))) \/ (((exists pfc_gap_lowercontinuationoutside. pfc_gap_lowercontinuationoutside+((L))=((i))) /\ ((((a))=0))))

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)Le(a,b)BetaAt(b,c,i,x)

Definitions depending on this notation

PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t)

Checked theorems using this definition

PG0005 · polynomial_zero_extended_shift_forwardPG0006 · polynomial_zero_extended_shift_reversePG0011 · polynomial_zero_extended_scale_congruent