target_coefficient_bridge
plain-language theorem explainer
Packages the rank-nullity arithmetic of the landed ledger-closure map on face configurations: rank 1, nullity 3, total 4 bits, first-isomorphism check, and both candidate ratios 1/4 and 3/4 against four admissible sectors. Holography workers cite it as the precise Prop that GAP 1 reduces to before choosing the physical selector. Pure definition of a six-conjunct proposition; the equalities are discharged later by decide-backed lemmas.
Claim. The coefficient-bridge target is the proposition that the ledger-closure map on face configurations has rank $1$ and nullity $3$, that total configuration bits equal rank plus nullity, that $|\mathrm{im}(\mathrm{closed})| \cdot |\ker(\mathrm{closed})| = |\mathrm{FaceCfg}|$, and that rank and nullity over the admissible-sector count equal $1/4$ and $3/4$ respectively.
background
Module CoefficientBridge isolates GAP 1 of the holography program: the count-to-area coefficient $\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 labelled integers, but a physical selector between two already-computed ratios.
The underlying map is ledger-closure closed : FaceCfg → Bool on the four raw edge bits of a unit face. Rank is Nat.log2 of the image cardinality (parity hits both values, so $|\mathrm{image}| = 2 = 2^1$). Nullity is Nat.log2 of the kernel closedConfigs (eight closed configs, $2^3$). Total bits are Nat.log2 of $|\mathrm{FaceCfg}| = 16 = 2^4$. Admissible sectors come from the landed pixel-local count of four recognition sectors.
Upstream, EdgeSectorBridge.closedConfigs supplies the pre-quotient closed edge substrate; the image and domain cardinalities are read off the actual closed map, not typed as hand subtractions.
proof idea
Definitional packaging only: the body is the six-way conjunction of (i) rank equals 1, (ii) nullity equals 3, (iii) total bits equal rank plus nullity, (iv) image-cardinality times kernel-cardinality equals domain cardinality, (v) rank over admissible-sector count equals $1/4$, (vi) nullity over that count equals $3/4$. No tactics; the named quantities closureRank, freeBits, rawBits are themselves Nat.log2 of the corresponding Finset cardinalities.
why it matters
This Prop is the single named target that target_coefficient_bridge_holds discharges by assembling closureRank_eq_one, freeBits_eq_three, rank_nullity_add, closure_image_times_kernel, and two norm_num ratio steps against recognition_sector_count. Per the module panel verdict, both branches (rank/4 = 1/4 Bekenstein; nullity/4 = 3/4 giving $\kappa = 4/3$) are then proven axiom-clean from the landed sets.
The open crux is not this arithmetic: it is the unformalized selector that one ledger-closed D=3 plaquette realizes the closure rank's worth of recognition events (multiplicity 1) rather than the free-bit microstates. Supplying that selector derives Bekenstein-Hawking; refuting it yields $\kappa = 4/3$. The reduction always lands; the coefficient becomes a crisp yes/no rather than a lattice-model war. Ties the holography coefficient to the eight-tick / D=3 forcing chain only through that remaining physical identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.