target_coefficient_bridge_holds
plain-language theorem explainer
The pixel-local ledger-closure map obeys a genuine rank-nullity split: rank 1, free-bit nullity 3, total dimension 4, with the first-isomorphism check |im|·|ker|=|domain|. Both holographic candidate ratios against the four recognition sectors are proved exactly: 1/4 and 3/4. GAP-1 / Bekenstein-coefficient workers cite this as the landed arithmetic bridge. Proof assembles five prior equalities by refine and discharges the two ratio goals by rewrite plus norm_num.
Claim. The target coefficient bridge holds: the ledger-closure map on face configurations has closure rank $1$ and free-bit nullity $3$, these sum to the raw bit count $4$, the first-isomorphism identity $|\mathrm{im}|\cdot|\mathrm{ker}|=|\mathrm{domain}|$ holds, and both ratios against the recognition-sector count equal $1/4$ and $3/4$ respectively.
background
Module Holography.CoefficientBridge treats GAP 1 of the holographic panel: the count-to-area coefficient $\kappa$ in $a_{\mathrm{pix}}=\kappa,H,\ell_P^2$ (the "4" in Bekenstein-Hawking $S=A/4$). The landed lattice already supplies integers 1, 2, 3, 4; the coefficient is a physical selector, not a number for decide to pick. The selector asks whether per-plaquette recognition-event multiplicity attaches to the ledger-closure rank (1, ratio $1/4$) or to the free-bit nullity (3, ratio $3/4$, $\kappa=4/3$).
The one landed map is PixelLocal.closed : FaceCfg → Bool. Closure rank is $\mathrm{Nat.log2}$ of the image cardinality ($|\mathrm{im}|=2=2^1$), free bits are $\mathrm{Nat.log2}$ of the kernel ($|\mathrm{ker}|=8=2^3$, from EdgeSectorBridge.closed_free_bits), and raw bits are $\mathrm{Nat.log2}|\mathrm{FaceCfg}|$ ($16=2^4$). Recognition sector count is the landed admissibleSectors.card = 4. Both candidate ratios are then compared to that sector count.
Upstream edge-sector and recognition-event-capacity modules supply the concrete finite sets; this module only packages their rank-nullity arithmetic into one named bridge proposition.
proof idea
Term-mode refine builds the six-field bridge record. The first four fields are prior lemmas: closureRank_eq_one, freeBits_eq_three, rank_nullity_add (rank + nullity = raw bits), and closure_image_times_kernel (the first-isomorphism cardinality check $2\cdot 8=16$).
The last two goals are the ratio identities against recognition_sector_count. Each is a one-line rewrite of the corresponding rank/nullity lemma together with the sector-count fact, finished by norm_num ($1/4$ and $3/4$). No new set enumeration occurs here; the proof only wires already-proved equalities.
why it matters
This is the axiom-clean arithmetic core of GAP 1 in the holography panel. It shows both Bekenstein ($\kappa$ branch $1/4$) and the alternative $3/4$ ($\kappa=4/3$) are exact consequences of the landed ledger-closure map and the four recognition sectors; nothing is hand-typed as $4-3$.
Downstream, coefficient_of_multiplicity reduces the whole coefficient question to a single open integer multiplicity $m$ (pixel-to-sector ratio $m/4$), and bekenstein_branch / the selector hypothesis discharge the physical choice. The open crux named in the module is selector_multiplicity_is_closure_rank: whether one ledger-closed $D=3$ plaquette realizes exactly the closure rank's worth of recognition events (multiplicity 1). Affirming it yields Bekenstein-Hawking; taking multiplicity equal to nullity yields $\kappa=4/3$. The reduction always lands; the coefficient value is now a single crisp yes/no.
Framework contact: eight-tick / $D=3$ forcing (T7-T8) already fixed the plaquette combinatorics that produce raw bits 4 and free bits 3; this bridge converts that combinatorics into the holographic coefficient alternatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.