recognitionMultiplicityCert
plain-language theorem explainer
Certificate that the holography recognition-multiplicity consistency bundle holds: ledger cost matches closure rank at one and two faces, diverges from domino nullity, and the rank-reading selector with coefficient 1/4 is assembled. Holography-loop auditors cite it as the `#print axioms`-gated verify-target. Proof is a one-line alias of the already-proved conjunction.
Claim. The recognition-multiplicity consistency package holds: ledger cost of one face equals the closure rank; ledger cost of two faces equals the domino rank and is unequal to the domino nullity; the domino local map factors as image cardinality times kernel cardinality; under the one-distinction-per-face (rank) reading the Bekenstein selector is available; and the holographic coefficient equals $1/4$.
background
This module sits in the holography stack as a rank-consistency check at the T-1 recognition ledger floor. For a cell of $k$ unit faces (each a minimal closed recognition loop in $D=3$), recognitionMultiplicity k is the unit-weight ledger cost of posting one primitive double-entry distinction per face. That cost is grounded outside holography in the free ledger floor and never mentions the closure map; the equality recognitionMultiplicity k = k is already proved.
Three independent quantities are compared: ledger multiplicity, closure rank (image dimension of the local face map), and nullity (kernel dimension). On a single face and on the two-face domino, multiplicity is checked against rank; on the domino it is also checked against nullity. The module header, after the holo_mult_fable_20260702 audit, stresses that posting one generator per face is a modeling choice: a three-generators-per-face nullity ledger is equally T-1-consistent. Bare T-1 underdetermines the shape, so the shape encodes the selector rather than deriving it.
The target proposition packages the surviving checks: multiplicity equals rank at one and two faces, multiplicity differs from nullity at two faces, the domino image-times-kernel identity, the selector under the rank reading, and the coefficient $1/4$.
proof idea
One-line term wrapper: the certificate is definitionally the already-proved conjunction target_recognition_multiplicity_holds. That theorem assembles six conjuncts by angle-bracket introduction: multiplicity equals rank at one face, multiplicity equals rank at two faces, multiplicity differs from nullity at two faces, the domino image-times-kernel card identity, the rank-reading Bekenstein selector, and the derived coefficient $1/4$. No new algebra is done here.
why it matters
This is the verify-target handle for the holography loop: a single named proposition that #print axioms can gate against. It does not force the Bekenstein $1/4$ selector from T-1; the module doc retracts that headline. What it certifies is mutual exclusivity of the rank and nullity readings once one posts one distinction per face, plus the coefficient under that reading.
Downstream use count is currently empty; the live candidate for non-circular selection is gluing-invariance/extensivity in PixelQuadPlaquette (rank stays 1 per face under gluing; nullity does not: $3\to 4\neq 6$ on the domino). In the broader RS chain this sits after T8 ($D=3$) and the eight-tick octave, at the holographic coefficient bridge, not at J-uniqueness or the RCL. The tag chain recorded in the module is: postulate (T9CarrierBridge) to modeling choice (here) to candidate consistency-forcing (quad extensivity, still open until landed).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.