closureRank_eq_one
plain-language theorem explainer
The ledger-closure map on a face configuration has rank exactly 1: the log2 of its image cardinality is 1. Anyone deriving the Bekenstein 1/4 ratio or the rank-nullity coefficient bridge cites this. The proof is a one-line `decide` on the finite image of the landed closed map.
Claim. The rank of the ledger-closure map $\mathrm{closed}:\mathrm{FaceCfg}\to\mathrm{Bool}$, defined as $\log_2$ of the cardinality of its image, equals $1$.
background
CoefficientBridge isolates GAP 1 in the holographic coefficient: the factor $\kappa$ in $a_{\mathrm{pix}}=\kappa,H,\ell_P^2$ (the "4" in Bekenstein-Hawking $S=A/4$) is not a number to bake, but a physical selector between two integers already present in the landed ledger. The map in play is the actual plaquette closure predicate $\mathrm{closed}:\mathrm{FaceCfg}\to\mathrm{Bool}$.
The rank is read off that map as $\mathrm{Nat.log2}$ of the cardinality of its image, not as a hand-typed subtraction of free bits from raw bits. Upstream, closureRank is defined exactly that way: the parity functional hits both Boolean values, so $|\mathrm{image}|=2=2^1$. Parallel quantities are the nullity (log2 of the kernel, free bits $=3$) and the domain dimension (raw bits $=4$), with the first-isomorphism check $|\mathrm{image}|\cdot|\mathrm{kernel}|=|\mathrm{domain}|$.
proof idea
One-line wrapper: decide evaluates the finite Finset image of closed over FaceCfg, takes its cardinality, applies Nat.log2, and confirms the result is 1. No algebraic lemmas are invoked; the computation is the definition of closureRank on a decidable finite type.
why it matters
This is the rank half of the genuine rank-nullity package that target_coefficient_bridge_holds assembles (rank 1, nullity 3, total 4, image-kernel product identity, and both candidate ratios against the four admissible sectors). Downstream, bekenstein_branch rewrites with this equality to get $(\mathrm{closureRank})/4=1/4$; bekenstein_of_selector does the same once the open selector identifies multiplicity with rank. KeystoneFactorThree uses it to show the nullity density is three times the rank density. RecognitionMultiplicity bridges ledger multiplicity at one face to this rank and instantiates the conditional Bekenstein selector as multiplicity $=1$.
In the framework, this pins the "1" side of the GAP 1 selector: entropy attaches either to closure rank (Bekenstein $1/4$) or to free-bit nullity ($\kappa=4/3$). The module does not close that selector; it only lands the integer that the rank branch needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.