recognitionMultiplicity_eq
plain-language theorem explainer
The free recognition ledger cost of a cell with k unit faces equals the real number k. Holography bridges that equate floor multiplicity to closure rank, domino rank, or record cost all rewrite through this identity. The proof is induction on k, using unconditional ledger-cost additivity and the unit cost of a single posted distinction, with no appeal to any closure map.
Claim. For every natural number $k$, the recognition ledger multiplicity of a cell built from $k$ faces equals $k$ as a real: if one posts one primitive double-entry distinction per face into the free defect ledger (unit weights), the total ledger cost is exactly the face count.
background
In the Recognition Multiplicity module, a cell of $k$ D=3-forced unit faces carries a free defect ledger with one posted generator per face. The recognition multiplicity is the unit-weight ledger cost of that ledger, computed entirely at the T-1/T0 free ledger floor and never mentioning a closure map.
The floor supplies unconditional additivity: the cost of a sum of ledgers is the sum of the costs (ledgerCost_add), and a single posted distinction has unit cost (ledgerCost_single). These are the free-ledger generalizations of independent same-defect accounting; they need no independence side-condition.
Local setting (module audit): the construction encodes the rank reading of T-1 by fiat (one generator per face). A mirror nullity ledger is equally T-1-clean. The theorems remain true as a rank-consistency check: under that posting convention, multiplicity tracks rank and diverges from nullity on the two-face domino.
proof idea
Induction on the face count $k$.
Base $k=0$: the empty cell ledger has cost $0$ by unfolding the multiplicity and ledger definitions, matching $0:\mathbb{R}$.
Successor: the $(n+1)$-face ledger is the $n$-face ledger plus one single-entry ledger. Rewrite the cost by ledgerCost_add, evaluate the single entry by ledgerCost_single, substitute the inductive hypothesis, then push_cast and ring to obtain $n+1$ on the reals.
No geometric or map-side lemma appears; the argument is pure free-ledger arithmetic.
why it matters
This identity is the floor-side half of every rank bridge in the module. Downstream, multiplicity_eq_rank_one and multiplicity_eq_rank_two rewrite multiplicity to closure rank ($=1$) and domino rank ($=2$); multiplicity_ne_nullity_two turns the same rewrite into the scoped divergence $2\neq 4$ against domino nullity. Record-cost asymmetry reuses it to equate map-side record cost with floor multiplicity at one and two faces, and packages both into selector_forced.
Framework role: it anchors the three independent quantities (ledger multiplicity, closure rank, nullity) so the rank reading is internally consistent. It does not force the Bekenstein $1/4$ selector; the module audit retagged that claim as a modeling choice. The live candidate forcing is gluing extensivity in the quad-plaquette development (rank stays one per face under gluing; nullity does not). Landmark contact is the free ledger floor beneath holography, not T5–T8 directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.