Pith. sign in
module module high

IndisputableMonolith.Holography.RecognitionMultiplicity

show as:
view Lean formalization →

Defines the defect ledger of a k-face cell as k primitive posted distinctions of multiplicity one (one per D=3 unit face). This is an explicit modeling choice encoding the rank reading, not forced by T-1. Holography results that attach the area coefficient to rank rather than nullity are conditional on it. The module is definitional, with elementary rank/nullity identities on the 2×1 domino.

claimFor a $k$-face cell the recognition multiplicity equals $k$: one primitive posted distinction per $D=3$ unit face, each of multiplicity one. On the $2\times 1$ domino the closed ledger has rank $2$ and nullity $4$, and the one-per-face multiplicity matches the rank reading.

background

Recognition holography must turn a discrete recognition-event count into the area coefficient $\kappa$ in $a_{\mathrm{pix}}=\kappa\cdot H\cdot\ell_P^2$ (the classical $4$ of Bekenstein-Hawking). CoefficientBridge isolates $\kappa$ as a named physical selector: attach per-plaquette multiplicity to ledger-closure rank (reading $1$) or to nullity (reading $3$ free bits). PixelGluedPlaquette already shows the recognition-sector count is not area-additive under edge-gluing of two faces into a $2\times 1$ domino.

The Recognition Ledger Floor supplies the free additive cost floor that closes the genuine T-1/T0 audit gaps. T-1 says a closed recognition loop posts distinctions, but does not fix how many per face. One-per-face encodes the rank reading; a mirror three-per-face ledger would encode nullity and is equally T-1-consistent. This module records the one-per-face choice as the defect ledger of a $k$-face cell. It knows only the face count, nothing about the closure map.

proof idea

Primarily definitional. It introduces the cell ledger and recognition multiplicity for a $k$-face cell, with an equality pinning the count to $k$. On the $2\times 1$ domino it defines left and right closed ledgers, the local map between them, and the associated rank and nullity. Elementary linear algebra then gives rank $=2$, nullity $=4$, an image-times-kernel decomposition, and the identity that multiplicity equals the rank-one contribution, confirming that the one-per-face modeling choice matches the rank reading on the glued plaquette.

why it matters in Recognition Science

RecordCostAsymmetry imports this module to fix the rank/nullity selector from the record-cost reading (panel verdict on unconditional holography; formerly framed as Landauer asymmetry). By locking multiplicity to one per face, downstream theorems become conditional on the rank reading rather than a three-per-face nullity ledger. The module sits between PixelGluedPlaquette's non-additivity result and the coefficient selection that feeds the holographic area law. D=3 forcing (T8) supplies the unit-face geometry that makes "one per face" well-defined. The audit note holo_mult_fable_20260702 flags that this is modeling, not a T-1 consequence.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (19)