bekenstein_selector_derived
plain-language theorem explainer
The Bekenstein selector identity holds in the rank reading: selector multiplicity equals closure rank, both equal to 1. Holography authors cite it when wiring the one-quarter coefficient bridge and the recognition-multiplicity target bundle. The proof is a two-step term: unfold the selector predicate, then rewrite by the known fact that closure rank is one. Audit note: the ledger construction is not load-bearing here; this instantiates the rank reading rather than forcing it from T-1.
Claim. The selector-multiplicity reading agrees with the closure rank at value one: the predicate "selector multiplicity is closure rank" holds for the unit cell, i.e. both quantities equal $1$.
background
This module sits in the holography stack as a rank-consistency check for the Bekenstein selector, not as a T-1 forcing. For a cell built of $k$ unit faces (each a minimal closed recognition loop in $D=3$), three independent counts are compared: recognition multiplicity (ledger cost with one posted distinction per face), closure rank (image dimension of the face-to-edge boundary map), and nullity (kernel dimension). Under the rank reading one posts one generator per face; under the nullity reading one posts three free bits per face. Bare T-1 underdetermines which ledger shape to use.
The selector predicate (from the coefficient bridge) asserts that multiplicity tracks closure rank rather than nullity. A sibling equality already records that the closure rank of the unit cell is exactly one. The module doc is explicit that the one-generator-per-face ledger is a modeling choice encoded into the types, equally T-1-consistent with a three-generator mirror that would witness the opposite branch.
Upstream scaffolding (forcing ranks, cost projectors, circle faces) supplies the ambient recognition calculus; none of those lemmas is invoked in the payoff term below.
proof idea
Term-mode, two steps. Unfold the coefficient-bridge predicate selector_multiplicity_is_closure_rank so the goal becomes the bare numerical claim that the closure rank equals one. Discharge that goal by rewriting with the already-proved bridge lemma that the unit-cell closure rank is one. No appeal to recognition multiplicity, the cell ledger, domino rank/nullity, or any T-1 floor lemma appears in the term.
why it matters
Parent consumers are local. The one-quarter coefficient theorem applies the bridge map bekenstein_of_selector at this selector fact to obtain the pixel-to-sector ratio $1/4$ under the rank reading. The bundled holography target packages this fact with the multiplicity-versus-rank and multiplicity-versus-nullity comparisons. Record-cost asymmetry re-exports the same selector identity under a performed-distinction grounding.
Framework role: this is the selector half of the classical Bekenstein-Hawking factor $A/4$ in RS units, conditional on choosing the rank reading of the ledger. The module audit (holo_mult_fable_20260702) retracted the stronger claim that T-1 alone forces the selector; GAP 1 (extensivity and gluing invariance of rank versus nullity on the quad plaquette) remains the live candidate for a non-circular force. The _derived suffix is retained only so downstream re-exports stay stable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.