freeBits
plain-language theorem explainer
Defines the free-bit count (nullity) of the ledger-closure map on face configurations as the base-2 log of the kernel size. Anyone citing the holographic rank-nullity split or the κ = 4/3 branch uses this integer. The body is a one-line abbreviation: log₂ of the closed-config Finset cardinality.
Claim. The free-bit nullity is $\log_2 |K|$, where $K$ is the set of ledger-closed face configurations (the kernel of the closure predicate on the $16$-element face configuration space).
background
CoefficientBridge isolates GAP 1 of the holographic area law: the count-to-area coefficient κ in $a_{\mathrm{pix}} = \kappa \cdot H \cdot \ell_P^2$ is not a number for decide to pick among labelled integers, but a physical selector between rank and nullity of one landed map.
The domain is FaceCfg, the $2^4 = 16$ raw four-edge bit patterns on a plaquette. Ledger closure is the Boolean parity map closed : FaceCfg → Bool. Its kernel is closedConfigs, the Finset of configurations with closed = true. Upstream, EdgeSectorBridge records that this kernel has eight elements before any $D_4$ quotient: the parity constraint removes exactly one of the four raw edge degrees of freedom.
Nullity is then the information-theoretic free-bit count on that kernel: base-2 log of its cardinality. The companion totals are closure rank (log of the image size) and raw bits (log of the full domain).
proof idea
Pure definition, not a proof. The body is Nat.log2 closedConfigs.card: apply Mathlib's natural log-base-2 to the cardinality of the already-filtered closed-configuration Finset. No tactics, no lemmas beyond the upstream definition of that Finset.
why it matters
This is the named nullity integer in the module's genuine rank-nullity of PixelLocal.closed. Downstream, freeBits_eq_three pins it to 3 by decide; rank_nullity_add checks $4 = 1 + 3$ against independently computed rank and total; target_coefficient_bridge packages rank = 1, nullity = 3, additive rank-nullity, and the first-isomorphism identity $|\mathrm{im}| \cdot |\ker| = |\mathrm{dom}|$.
The κ = 4/3 branch divides this nullity by the landed sector count 4 to get the ratio 3/4. KeystoneFactorThree reuses it for the density identity that nullity density is three times rank density. Framework-wise this sits under the D = 3, eight-tick holography stack: the open crux remains the selector (does entropy attach to closure rank 1 or free-bit nullity 3?), not the integer itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.