closure_image_times_kernel
plain-language theorem explainer
Finite rank-nullity identity for the landed ledger-closure map on face configurations: |image| · |kernel| = |domain|, i.e. 2 · 8 = 16. Anyone citing the holographic coefficient bridge (GAP 1) needs this as the first-isomorphism check that the closure constraint is a genuine rank-1 parity functional. The proof is a single decide on the enumerated finite sets.
Claim. For the ledger-closure predicate $\mathrm{closed} : \mathrm{FaceCfg} \to \mathrm{Bool}$, the product of the cardinality of its image and the cardinality of its kernel equals the domain size: $|\mathrm{im}(\mathrm{closed})| \cdot |\{\,c \mid \mathrm{closed}(c)\,\}| = |\mathrm{FaceCfg}|$. Numerically this is $2 \cdot 8 = 16$.
background
CoefficientBridge isolates GAP 1 of the holography program: the count-to-area coefficient $\kappa$ in $a_{\mathrm{pix}} = \kappa , H , \ell_P^2$ (the "4" in Bekenstein-Hawking $S = A/4$) is not a number for decide to pick among pre-labelled integers, but a physical selector between two already-landed integers.
The underlying map is the one landed ledger-closure predicate on face configurations (PixelLocal.closed : FaceCfg → Bool). Its domain has 16 elements ($2^4$), its kernel (closed configurations) has 8 ($2^3$, the free-bit count from EdgeSectorBridge), and its image has 2 values (true/false). Rank and nullity are read as $\log_2$ of image and kernel cardinalities, not by hand-typed subtraction.
This declaration is the first-isomorphism form of rank-nullity for that actual map: image size times kernel size equals domain size. Together with the three independent $\log_2$ readings it certifies that the closure constraint is a nonzero parity functional of rank exactly 1.
proof idea
One-line finite check: by decide. Lean enumerates Finset.univ over FaceCfg, builds the image of closed, multiplies its cardinality by closedConfigs.card, and verifies equality with the domain cardinality. No algebraic lemmas are invoked; the identity is pure exhaustive computation on a 16-element type.
why it matters
Feeds directly into target_coefficient_bridge_holds, which packages the full GAP 1 bridge: rank = 1, nullity = 3, rank + nullity = 4, this image-kernel identity, and the two exact ratios $1/4$ and $3/4$ against the landed sector count of 4.
The module's point is that both Bekenstein ($\kappa$ from rank, ratio $1/4$) and the free-bit alternative ($\kappa = 4/3$ from nullity) are proved branches. The remaining open input is the physical selector selector_multiplicity_is_closure_rank: whether one closed D=3 plaquette realizes multiplicity 1 (closure rank) or 3 (free bits). This identity is the piece that stops the rank from being a hand-typed $4-3$, the failure mode the panel flagged.
In the broader RS chain this sits in the holography layer that turns eight-tick / D=3 ledger structure into an area-law coefficient, without baking the classical 4.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.