rank_nullity_add
plain-language theorem explainer
Additive rank-nullity for the ledger-closure map on face configurations: total bit count equals closure rank plus free-bit nullity (4 = 1 + 3), each side from independent set cardinalities. Anyone assembling the holographic coefficient bridge cites it. The proof is a one-line decide on three concrete naturals already fixed by the actual image, kernel, and domain.
Claim. For the ledger-closure map on face configurations, the base-2 log of the domain cardinality equals the sum of the base-2 logs of the image and kernel cardinalities: $4 = 1 + 3$. Equivalently, total raw bits equal closure rank plus free bits, with each integer computed independently from the actual finite sets (no hand-typed subtraction).
background
CoefficientBridge isolates GAP 1 of the holographic area law: the count-to-area factor $\kappa$ in $a_{\mathrm{pix}} = \kappa , H , \ell_P^2$ (the "4" in Bekenstein-Hawking $S = A/4$) is a physical selector, not a number for decide to invent. The landed map is the Boolean closure predicate on face configurations (domain size $16 = 2^4$). Its image has size $2 = 2^1$ (rank 1: a nonzero parity functional); its kernel has size $8 = 2^3$ (nullity 3, the closed free-bit count from EdgeSectorBridge).
The three integers raw bits, closure rank, and free bits are defined as those base-2 logs of domain, image, and kernel. The module also records the multiplicative first-isomorphism check $|\mathrm{image}| \cdot |\mathrm{kernel}| = |\mathrm{domain}|$ ($2 \cdot 8 = 16$). Both candidate ratios against the four admissible recognition sectors are then exact: rank$/4 = 1/4$ and nullity$/4 = 3/4$.
proof idea
One-line tactic proof: decide. The three sides are closed natural-number definitions already evaluated from finite-set cardinalities (domain $16$, image $2$, kernel $8$), so equality $4 = 1 + 3$ is a pure computational fact with no algebraic rewriting or external lemmas required.
why it matters
This is one of the four conjuncts that discharge target_coefficient_bridge_holds, the axiom-clean rank-nullity package for the single landed ledger-closure map. Together with independent proofs that rank is 1, nullity is 3, and the multiplicative isomorphism $2 \cdot 8 = 16$, it shows both Bekenstein ($\kappa$ from rank $\to 1/4$) and the free-bit branch ($\kappa = 4/3$) are exact against the sector count of 4; nothing is baked by hand subtraction.
Framework role: it sits under the holography coefficient bridge that reduces GAP 1 to one named selector (does per-plaquette recognition multiplicity attach to closure rank or to free-bit nullity?). Downstream, supplying the selector yields Bekenstein-Hawking; refuting it yields $\kappa = 4/3$. The eight-tick / $D=3$ forcing chain (T7-T8) supplies the ambient discrete geometry in which the face configuration space is $2^4$, but this lemma itself is pure finite linear algebra of the closed map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.