freeBits_eq_three
plain-language theorem explainer
The free-bit count (nullity of the ledger-closure map on a D=3 face) equals exactly 3. Holography and coefficient-bridge arguments cite this to pin the 3/4 density branch and the κ=4/3 alternative to Bekenstein. The proof is a one-line `decide` on the already-computed kernel cardinality 8=2³.
Claim. The free-bit nullity equals three: $\mathrm{freeBits} = \log_2|\ker(\mathrm{closed})| = 3$, where the kernel is the set of closed face configurations (cardinality $8 = 2^3$).
background
CoefficientBridge isolates GAP 1 in the holographic area law: the count-to-area coefficient $\kappa$ in $a_{\mathrm{pix}} = \kappa , H , \ell_P^2$ is not a number decide should invent, but a physical selector between two already-landed integers. The ledger-closure map PixelLocal.closed : FaceCfg → Bool has domain cardinality $|\mathrm{FaceCfg}| = 16 = 2^4$, image cardinality 2, and kernel cardinality 8.
freeBits is defined as $\mathrm{Nat.log2}$ of that kernel size: the nullity of the closure constraint. Companion quantities are the rank (closureRank = log2|image| = 1) and the total (rawBits = log2|domain| = 4). Rank-nullity and the first-isomorphism check $|\mathrm{image}|\cdot|\mathrm{kernel}| = |\mathrm{domain}|$ are verified independently from the actual sets, not by hand-typed subtraction.
Both candidate entropy attachments are then ratios against the landed sector count 4: rank/4 = 1/4 (Bekenstein) versus nullity/4 = 3/4 ($\kappa = 4/3$).
proof idea
One-line computational proof: by decide. Lean evaluates freeBits, which is Nat.log2 closedConfigs.card, against the concrete finite set of closed configurations (cardinality 8), and checks equality with 3. No algebraic lemmas are invoked beyond the definition of freeBits.
why it matters
This pins the nullity half of the coefficient bridge. Downstream, target_coefficient_bridge_holds packages it with closureRank_eq_one, rank-nullity additivity, and the image-kernel product into the full bridge statement. kappa_four_thirds_branch rewrites with this equality and the sector count to obtain $(\mathrm{freeBits})/4 = 3/4$, the $\kappa = 4/3$ alternative if entropy attaches to free-bit microstates rather than the closure event.
KeystoneFactorThree.density_ratio_is_three uses the same fact to show the nullity density is three times the rank density: $\mathrm{freeBits}/\mathrm{rawBits} = 3\cdot(\mathrm{closureRank}/\mathrm{rawBits})$. In the Recognition framework this is the D=3 plaquette side of the holographic coefficient; the remaining open input is the physical selector (multiplicity equals rank versus nullity), not the integer 3 itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.