dominoLocalMap
plain-language theorem explainer
Pairs a two-face domino configuration with its left and right face-closure parities in Bool×Bool. Holography and record-cost arguments cite it as the concrete local map whose image size is 4 and whose kernel (both faces closed) has size 16. The body is the obvious pairing of the two closedness predicates; rank and nullity are read off later via log2 of those cardinalities.
Claim. For a two-face domino configuration $c$, the local closure map is the pair of face parities $(\mathrm{left\text{-}closed}(c),\,\mathrm{right\text{-}closed}(c))\in\{\mathrm{true},\mathrm{false}\}^{2}$. Its image is all of $\mathrm{Bool}\times\mathrm{Bool}$ (the two constraints are independent), so the map has rank $2$.
background
The module treats recognition multiplicity as a rank-consistency check on a T-1 ledger, not as a derivation of the Bekenstein 1/4 selector. Under the modeling choice that one posts one distinction per face, ledger cost tracks closure rank and diverges from nullity on the two-face domino; bare T-1 underdetermines ledger shape, so the shape encodes rather than forces the selector.
A DominoCfg is a glued two-face plaquette configuration. The sibling predicates dominoLeftClosed and dominoRightClosed report whether each face is a closed recognition loop (parity true). The local map packages those two bits. Downstream, rank is $\log_2$ of the image cardinality and nullity is $\log_2$ of the kernel (both faces closed).
Separately, recognitionMultiplicity k is the free-ledger cost of $k$ unit faces (one posted double-entry distinction per face), grounded in the T-1/T0 ledger floor and independent of any closure map; one has recognitionMultiplicity k = k.
proof idea
Pure definition: evaluate the left- and right-closed predicates on c and return the pair. No lemmas, no tactics. Image/kernel cardinalities and the first-isomorphism identity $4\cdot 16=64$ are proved later by decide on the finite type of configurations.
why it matters
This is the concrete map that makes rank and nullity computable rather than stipulated. dominoRank is $\log_2$ of its image size (expected $2$); dominoNullity is $\log_2$ of the both-closed fiber (expected $4$). The theorem domino_image_times_kernel checks $|\mathrm{image}|\cdot|\mathrm{kernel}|=|\mathrm{domain}|$ on this map, pinning those numbers without hand subtraction.
The consistency bundle target_recognition_multiplicity equates multiplicity to rank at one and two faces, asserts multiplicity $\neq$ nullity on the domino, and reuses the image/kernel product. In RecordCostAsymmetry, recordCost_domino shows the record cost of this map equals $2$ (the rank), feeding the one- and two-face bridges that match floor-side multiplicity to map-side record cost and the selector-forcing arguments under the rank reading.
Framework role: supports the holography rank-vs-nullity divergence witness on the two-face cell (D=3 unit faces). It does not itself force the 1/4 selector; the live candidate forcing is gluing extensivity in the quad module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.