closureRank
plain-language theorem explainer
The rank of the ledger-closure map on face configurations is the base-2 log of the size of its image. For the parity functional that map is, the image has two values, so the rank is 1. Anyone citing the holographic coefficient bridge or the Bekenstein vs κ=4/3 fork uses this integer. It is a direct definition from the image cardinality, not a subtraction of free bits from raw bits.
Claim. Define the closure rank of the ledger-closure map $\mathrm{closed}:\mathrm{FaceCfg}\to\{\mathrm{true},\mathrm{false}\}$ by $\mathrm{rank}=\log_2|\mathrm{im}(\mathrm{closed})|$. Equivalently, if $I=\{\mathrm{closed}(c):c\in\mathrm{FaceCfg}\}$, then the rank is $\log_2|I|$.
background
CoefficientBridge isolates GAP 1 in the holographic count-to-area story: the coefficient $\kappa$ in $a_{\mathrm{pix}}=\kappa,H,\ell_P^2$ (the "4" in Bekenstein–Hawking $S=A/4$) is not a number for decide to pick among baked labels. It is a physical selector: does per-plaquette recognition-event multiplicity attach to the ledger-closure rank (1, ratio $1/4$) or to the free-bit nullity (3, ratio $3/4$, $\kappa=4/3$)?
The domain is FaceCfg, the 16 raw edge-bit configurations of a face ($|\mathrm{FaceCfg}|=2^4$). The map closed is the landed parity (ledger-closure) constraint on those bits. Its kernel is closedConfigs: the eight configurations with even parity, already counted in EdgeSectorBridge as $8=2^3$ free bits after the constraint. The image of a Boolean parity functional that is non-constant has size 2.
Rank here means $\log_2$ of image cardinality; nullity means $\log_2$ of kernel cardinality. Both are read from the actual sets of the one landed map, not typed as $4-3$.
proof idea
Pure definition: evaluate the image of closed over the finite universe of face configurations, take its cardinality, and apply Nat.log2. No lemma chain and no subtraction. Downstream, closureRank_eq_one discharges the value by decide once the image is known to have two elements. The companion free-bit and raw-bit definitions play the same role for nullity and domain dimension.
why it matters
This integer is the rank half of the genuine rank-nullity package that target_coefficient_bridge assembles: rank 1, nullity 3, total 4, and the first-isomorphism check $|\mathrm{im}|\cdot|\ker|=|\mathrm{domain}|$ ($2\cdot 8=16$). rank_nullity_add and rawBits_eq_four cite it; bekenstein_branch divides it by the landed sector count 4 to get exactly $1/4$.
The open selector selector_multiplicity_is_closure_rank is the claim that one ledger-closed $D=3$ plaquette realizes multiplicity equal to this rank (one T9 recognition event). Accepting that selector yields Bekenstein–Hawking via bekenstein_of_selector; rejecting it (multiplicity = nullity = 3) yields the $\kappa=4/3$ branch. KeystoneFactorThree also consumes the rank in the density-ratio argument. Framework-wise this sits in the holography layer that turns the eight-tick / $D=3$ ledger geometry into an area coefficient, without baking which branch is physical.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.