multiplicity_ne_nullity_two
plain-language theorem explainer
Under the rank reading of the T-1 ledger, the recognition multiplicity of a two-face domino equals 2 while the domino nullity equals 4, so the two quantities diverge. Anyone auditing the holography selector or the mutual exclusivity of rank versus nullity readings cites this as the scoped divergence witness. The proof is a one-line rewrite of the two closed evaluations followed by numeric discharge.
Claim. The recognition multiplicity of a two-face cell is unequal to the real-valued nullity of the domino map: after the rank-reading evaluations, $2 \neq 4$.
background
This module is a rank-consistency check at the T-1 ledger floor, not a derivation of the Bekenstein selector. For a cell of $k$ unit faces (each a minimal closed recognition loop in $D=3$), three independent quantities are tracked: recognition multiplicity (ledger cost with one primitive double-entry distinction per face), closure rank of the gluing map, and nullity of that map.
Recognition multiplicity is grounded outside holography in the free ledger floor: with unit weight it evaluates to $k$ itself. On the two-face domino the siblings close rank $= 2$ and nullity $= 4$. The rank reading posts one generator per face by modeling choice; a mirror nullity reading (three generators per face) is equally T-1-clean and yields the opposite branch.
The local claim is only that, under the rank reading, multiplicity and nullity cannot agree on the domino. Mutual exclusivity of the two readings follows; selection between them does not.
proof idea
Term-mode one-liner. Rewrite the left side by the closed identity that recognition multiplicity of $k$ equals $k$, and the right side by the closed evaluation that domino nullity equals four. The goal reduces to $2 \neq 4$, discharged by norm_num. No gluing, no coefficient bridge, and no selector lemma is invoked.
why it matters
Feeds the package theorem target_recognition_multiplicity_holds, which bundles the multiplicity-rank matches, this divergence witness, the image-times-kernel factorization, and the (conditional) Bekenstein one-quarter selector into the holography verify-target certificate.
In the Recognition framework this is the scoped witness that rank and nullity readings of T-1 are mutually exclusive on the domino. It does not force the $1/4$ coefficient: the audit note and module doc retract the earlier "derived from the ledger floor" headline. The live candidate forcing is gluing-invariance/extensivity in the quad-plaquette module (rank stays one per face under gluing; nullity does not). Until that lands, the selector remains a modeling choice encoded as ledger shape, sitting downstream of the T9-carrier postulate and upstream of the open extensivity argument. Landmarks touched only indirectly: T-1 ledger floor, $D=3$ faces, eight-tick closure context.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.