Free Rank

Definition

The free rank formalizes the completeness criterion for type resolution in the UOR framework. The ring R_n = Z/(2^n)Z admits an iterated Z/2Z fibration with exactly n binary sites. Each constraint applied during resolution pins one or more of these sites. When all n sites are pinned, the type is fully resolved and the partition is complete.

Site Indices

A SiteIndex represents a single binary degree of freedom in the ring's structure. Each site has a position within the fibration and a state indicating whether it has been determined:

PropertyRangeDescription
sitePositionxsd:nonNegativeIntegerZero-based position in the fibration (0 = LSB)
siteStatexsd:stringEither "pinned" or "free"

The Budget

A FreeRank tracks how many sites have been pinned versus how many remain free:

PropertyRangeDescription
totalSitesxsd:nonNegativeIntegerTotal sites (= Witt level n)
pinnedCountxsd:nonNegativeIntegerSites pinned by constraints
freeRankxsd:nonNegativeIntegerSites still free (= total - pinned)
isClosedxsd:booleanTrue when all sites are pinned
hasSiteSiteIndexA site in this budget
hasBindingSiteBindingA pinning record

A Partition links to its budget via siteBudget.

Site Binding

A SiteBinding records which constraint determined a specific site:

PropertyRangeDescription
pinnedByConstraintThe constraint that pinned this site
pinsCoordinateSiteIndexThe site that was pinned

Example: R_4 Budget

For R_4 (n=4), there are 4 sites. A residue constraint x ≡ 1 (mod 2) pins site 0 (the parity bit), leaving 3 free:

<https://uor.foundation/instance/budget-R4>
    a                       partition:FreeRank ;
    partition:totalSites    "4"^^xsd:nonNegativeInteger ;
    partition:pinnedCount   "1"^^xsd:nonNegativeInteger ;
    partition:freeRank      "3"^^xsd:nonNegativeInteger ;
    partition:isClosed      false .

Completeness

When isClosed is true, the free rank budget is closed and the resolution is complete. This corresponds to the resolver's isComplete flag and a siteDeficit of zero.