dominoRank
plain-language theorem explainer
Rank of the two-face domino is the base-2 logarithm of the image size of the local domino map on paired face configurations. Holography and ledger-multiplicity arguments cite it when comparing rank to nullity on the glued pair. The definition simply takes log₂ of that finite image cardinality (documented as 4 = 2², both parities independently achievable).
Claim. The rank of the two-face domino is $\log_2$ of the cardinality of the image of the local domino map on the full finite configuration space (both faces closed).
background
In RecognitionMultiplicity, a cell is built from $k$ unit faces (minimal closed recognition loops in $D=3$). Three quantities are tracked separately: ledger multiplicity (cost of one posted distinction per face from the T-1 free ledger floor), closure rank (log₂ of the image of the local closed map), and nullity (log₂ of the kernel). The module is a rank-consistency check under the modeling choice that posts one generator per face, not a derivation of the Bekenstein 1/4 selector.
The two-face domino is the first place rank and nullity split. The local domino map sends paired face configurations to an observable pair of closedness bits. Its image size is the number of independently achievable parity outcomes; the doc records $|\mathrm{image}|=4=2^2$. Rank is defined as the log₂ of that image; the companion nullity is log₂ of the kernel (16 = 2⁴ free configs when both faces are closed).
proof idea
Pure definition, not a proof. Evaluate the image of the local domino map over the universe of configurations, take the finite cardinality of that image Finset, and return Nat.log2 of the card. No lemmas are applied at the definition site; the numerical identity rank = 2 is discharged later by decide in the companion theorem.
why it matters
This is the rank side of the domino divergence witness. Downstream, dominoRank_eq_two pins the value at 2; multiplicity_eq_rank_two then shows ledger multiplicity at two faces equals that rank (both 2), while multiplicity differs from nullity (2 ≠ 4). The bundle target_recognition_multiplicity packages those equalities and the inequality as the scoped consistency check under the rank reading of T-1.
RecordCostAsymmetry.recordCost_closed reuses the same rank for the two-face record cost. In the broader holography story the module no longer claims to force the Bekenstein selector; it only shows that if one encodes one distinction per face, multiplicity tracks rank and diverges from nullity on the domino. The live candidate forcing is gluing extensivity in the quad plaquette module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.