ZS0001 signed_zero_window_emptyA half-open zero window with coinciding endpoints is genuinely empty.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableCurrent library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
ZS0002 signed_zero_window_restrictRestrict the upper endpoint of an actual zero window without changing any represented values.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableZS0003 signed_zero_window_raise_lowerRaise the lower endpoint of a zero window, retaining its actual pointwise meaning.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableZS0004 signed_prefix_sum_zero_tailOrdinary finite induction proves that a genuinely zero tail changes no actual canonical signed prefix sum.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableZS0005 signed_prefix_sum_zero_valueA genuinely all-zero represented prefix has canonical signed sum zero; the proof retains actual fold witnesses.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableZS0006 signed_prefix_sum_zero_existsConstruct the actual sum of a valid all-zero prefix and prove its value, without postulating a sum oracle.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableZS0007 signed_prefix_sum_last_valueIf a prefix is zero, its next actual sum is precisely the actual last entry, including the l=0 boundary.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StableZS0008 signed_prefix_sum_zero_padding_iffActually construct either fold from the other across a proved zero tail; both implications retain real finite-sum witnesses.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePD0001 Le(a,b)Witness-defined non-strict order on natural numbers.
Conservative definition · notation layer 0PD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0ND0058 MatrixMinorFourCode(z,up,us,un,ut)One canonical injective doubled-Cantor code for all four signed-minor beta-code parameters.
Conservative definition · notation layer 0PD0013 BetaAt(b,c,i,x)x is the bounded beta-decoded value at index i.
Conservative definition · notation layer 0ND0142 SignedDecode(z,p,n)The original canonical integer code: even 2p denotes p, and odd 2k+1 denotes −(k+1). The decoded positive and negative parts are normalized.
Conservative definition · notation layer 0ND0143 SignedBalance(z,p,n)The original canonical code z represents the integer difference p−n; these supplied components need not be normalized.
Conservative definition · notation layer 1ND0251 ArithTable(N,F)An actual packed signed table with canonical signed entries through index N, including index zero. It contains no divisor transform or inversion hypothesis.
Conservative definition · notation layer 2PD0015 Sum(b,c,l,z)z is the sum of a beta-coded prefix of length l.
Conservative definition · notation layer 1ND0253 SignedPrefixSum(F,l,z)The signed balance of two actual natural finite sums, at exactly the indices 0<=i<l. Existence, uniqueness and representation independence are proved separately.
Conservative definition · notation layer 2ND0144 SignedAdd(a,b,c)Actual addition of original canonical signed codes, witnessed by their decoders and balanced equality.
Conservative definition · notation layer 1ND0252 ArithAt(F,i,z)Two genuine beta entries of the packed table represent the unique canonical signed value z. Distinct component representations need not be equal.
Conservative definition · notation layer 2ND0300 SignedZeroWindow(F,k,l)Every actual signed lookup on the half-open interval k<=i<l has value zero. Table validity, existence of folds, and equality after padding are separate hypotheses or theorems, not part of this graph.
Conservative definition · notation layer 3Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.