bekenstein_branch
plain-language theorem explainer
The Bekenstein branch of the holographic coefficient bridge: ledger-closure rank over admissible recognition-sector count equals exactly 1/4. Anyone deriving Bekenstein-Hawking from the plaquette ledger cites this once entropy is attached to closure rank rather than free-bit nullity. The proof rewrites by the landed facts rank = 1 and sector count = 4, then closes by arithmetic.
Claim. The ratio of the ledger-closure rank (cast to $\mathbb{Q}$) to the number of admissible recognition sectors equals $1/4$. Equivalently, if entropy attaches to the rank $m=1$ of the face-configuration closure map, the count-to-area coefficient is the classical Bekenstein value.
background
CoefficientBridge isolates GAP 1 of the holography program: the factor $\kappa$ in $a_{\mathrm{pix}}=\kappa\cdot H\cdot\ell_P^2$ (the "4" in Bekenstein-Hawking $S=A/4$) is not a number for decide to pick among landed integers. It is a physical selector: does per-plaquette recognition multiplicity attach to the ledger-closure rank or to the free-bit nullity?
The landed map is closed : FaceCfg → Bool. Its rank is $\mathrm{Nat.log2}$ of the image cardinality ($|\mathrm{image}|=2=2^1$), so rank $=1$, read from the map rather than as a hand subtraction. The domain has $16=2^4$ configurations and the kernel has $8=2^3$ closed configs; rank-nullity and the first-isomorphism check $2\cdot 8=16$ are verified independently. Admissible recognition sectors number exactly four.
Upstream, closureRank is that image-log definition. The companion nullity branch (free bits $=3$) yields ratio $3/4$ and coefficient $\kappa=4/3$. Both ratios are proved against the same sector count; only the selector remains open.
proof idea
Short tactic proof. Rewrite the numerator with closureRank_eq_one (rank equals $1$) and the denominator with recognition_sector_count (admissible sectors have cardinality $4$). The goal becomes $(1:\mathbb{Q})/(4:\mathbb{Q})=1/4$, discharged by norm_num. No further structure is unfolded.
why it matters
This is one of the two exact coefficient identities the module lands axiom-cleanly. Together with the free-bit (nullity) branch, it shows GAP 1 reduces to a single named physical input: whether one ledger-closed $D=3$ plaquette realizes multiplicity equal to the closure rank ($1$) or to the free-bit nullity ($3$).
The module header is explicit: supplying the selector (entropy attaches to the closure event) discharges Bekenstein-Hawking downstream; refuting it yields $\kappa=4/3$. Nothing numerical is baked. In the broader Recognition chain this sits under holography after the eight-tick / $D=3$ forcing (T7-T8): the plaquette ledger already carries rank $1$, nullity $3$, total $4$, and sector count $4$; the classical $1/4$ is the rank branch of that arithmetic.
No downstream consumers are wired yet (used_by empty). The open crux remains the unformalized identification of one closed plaquette with one T9 recognition event.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.