The original source-to-row bridge
Abstract
Original physical source rows supply the LOWER arithmetic and inventory.
OriginalSource, Coordinates and sourceCoordinates retain the OriginalLowerFullBank namespace. OriginalSource states all original hypotheses on the actual Fin(k) labels, with m>=5 and m LARGE labels of each sign. It includes the literal negative SMALL nonET tail witness and both source power branches. No selector or gate is an input to the computed coordinates.
Sorting the actual LARGE offsets partitions all k physical labels into 2m half-open rows, excluding only the repeated boundary x. The signed row formulas and the seed recurrence give N=Hz+b=Hb+n, z=n+(H-1)Delta, b=n+HDelta and b1=n+H^2*Delta. The original extrema and hard inequalities supply PrefixArithmetic without an a0<=z assumption.
The physical occurrence map is injective on that complete inventory and has image all Fin(k). sourceData supplies RowData naturalRows from the actual source lengths, bases and values, retaining length-zero rows and the original capacity C. OriginalLowerFullBank consumes these helpers for its least shifted-c full-bank selection, exact physical complement and conditional residual w support. This bridge does not assert tail completion or original normalization.
References
- Dependency: D5/S3/Combinatorics/Circle/M5SourceRows
- Dependency: D5/S3/Combinatorics/Circle/SourcePrefixInventory