cellLedger
plain-language theorem explainer
Builds the defect ledger of a k-face holographic cell as k unit-weight posted distinctions, one generator per face. Downstream multiplicity and rank-consistency theorems cite it as the rank-reading model of T-1. Defined by recursion: empty at zero, then add a fresh singleton defect at each successor.
Claim. The defect ledger of a $k$-face cell is the free finitely supported map $\mathbb{N}\to\mathbb{N}$ that places multiplicity one on each of the indices $0,\ldots,k-1$ (and zero elsewhere). Equivalently: $\mathrm{cellLedger}(0)=0$ and $\mathrm{cellLedger}(k+1)=\mathrm{cellLedger}(k)+\mathbf{1}_{\{k\}}$. This encodes one primitive posted distinction per $D=3$-forced unit face.
background
The module treats recognition multiplicity as a T-1 ledger construction used for a rank-consistency check in holography, not as a forced derivation of the Bekenstein selector. After the holo_mult_fable_20260702 audit, the headline claim that the 1/4 selector is derived from the ledger floor was retracted: bare T-1 underdetermines how many distinctions a closed face posts.
A defect ledger (from RecognitionLedgerFloor) is a finitely supported assignment of posted double-entry distinctions. Unit-weight ledger cost simply counts those postings. The present definition chooses one generator per face. A mirror three-per-face ledger (one per free bit) is equally T-1-consistent and would encode the nullity reading instead.
Upstream cost and count machinery (J-cost of recognition events, multiset event counts, multiplicative-recognizer costs) supplies the general language of recognition cost; this object stays purely combinatorial and never mentions the closure map.
proof idea
Definition by structural recursion on $\mathbb{N}$, not a proved theorem. Base case: the zero ledger. Successor: add the finitely supported singleton at index $k$ with multiplicity one (Finsupp.single k 1) to the ledger already built for $k$. The result is the characteristic sum of $k$ distinct unit defects.
why it matters
This is the modeling choice that encodes the rank reading of T-1 inside the holography stack. recognitionMultiplicity is defined as unit-weight ledger cost of this ledger, and recognitionMultiplicity_eq proves that cost equals the face count $k$ from the free ledger floor alone.
Parents use it for the divergence witness: at two faces, multiplicity equals domino rank ($2$) and differs from nullity ($4$), so the rank and nullity readings are mutually exclusive under this encoding (multiplicity_eq_rank_two, multiplicity_ne_nullity_two). RecordCostAsymmetry bridges record cost on the domino local map back to the same multiplicity.
Framework context: D=3 unit faces (T8) as minimal closed recognition loops; the live selector-forcing candidate is gluing extensivity in the quad/plaquette modules, still open. The ledger itself is not load-bearing in bekenstein_selector_derived, which closes $1=\mathrm{closureRank}$ directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.