recognitionMultiplicity
plain-language theorem explainer
For each natural number k, recognition multiplicity is the unit-weight recognition ledger cost of a k-face cell. It counts posted primitive distinctions (one per face) from the T-1/T0 free ledger floor, with no reference to the holographic closure map. Holography workers cite it when bridging ledger cost to closure rank on plaquettes and the domino. The body is a one-line application of ledgerCost to the cell ledger under constant weight 1.
Claim. For $k \in \mathbb{N}$, the recognition multiplicity of a $k$-face cell is the recognition ledger cost of that cell's defect ledger under unit weight on every distinction index: $\mathrm{RM}(k) := \mathrm{ledgerCost}(w\equiv 1,\,\Gamma_k)$, where $\Gamma_k$ posts one primitive double-entry distinction per face.
background
In the free recognition ledger floor, a defect ledger $\Gamma$ on an index set $I$ is a finitely supported assignment of natural multiplicities. Its recognition cost under a weight $w:I\to\mathbb{R}$ is $\sum_i n_i,w(i)$: the total weighted multiplicity of performed distinctions. Unconditional additivity says the cost of a sum of ledgers is the sum of the costs, with no independence side-condition.
This module sits in holography as a rank-consistency check, not a derivation of the Bekenstein $1/4$ selector. A $k$-face cell is built from $k$ unit faces (minimal closed recognition loops forced by $D=3$). The cell ledger posts, by modeling choice, one generator per face. Recognition multiplicity is that ledger evaluated at unit weight, grounded outside holography in the T-1/T0 floor.
The module header is explicit: bare T-1 underdetermines ledger shape; a mirror nullity ledger (three generators per face) is equally consistent. What is checked here is only that, under the rank reading, multiplicity tracks closure rank and diverges from nullity on the domino.
proof idea
Definitional one-liner: unfold to ledgerCost of the constant weight $w\equiv 1$ on the cell ledger for $k$. No tactics, no lemmas in the body. Downstream equality $\mathrm{RM}(k)=k$ is proved separately by induction using ledger additivity and the single-defect cost lemma from the free floor, still without mentioning the closure map.
why it matters
This is the ledger-side quantity in the module's three-way split (multiplicity vs closure rank vs nullity). It feeds the bridges multiplicity_eq_rank_one and multiplicity_eq_rank_two (multiplicity equals rank at one and two faces), the scoped divergence witness multiplicity_ne_nullity_two ($2\neq 4$ on the domino under the rank reading), the equality theorem that multiplicity is exactly the face count, and the consistency-check bundle target_recognition_multiplicity. Record-cost asymmetry also rewrites record cost as this multiplicity at ranks one and two.
Framework role: it re-encodes the selector at the T-1 ledger floor after T9 carrier universality was only a postulate. The adversarial retag is load-bearing: the construction is a modeling choice (one distinction per face), not a forcing from T-1. Live candidate forcing is gluing extensivity in the quad-plaquette module (rank stays 1 per face; nullity does not). Landmarks touched: T-1/T0 ledger floor, $D=3$ unit faces, holographic rank vs nullity for the Bekenstein coefficient under a conditional rank reading.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.