bitReadout
plain-language theorem explainer
Maps a cut entry in $\mathbb{Z}/2\mathbb{Z}$ to a posted Boolean bit: true exactly when the residue is $1$. Horizon and gravity record constructions cite it to turn discrete cut data into exterior-visible bit strings. The body is a one-line decidable equality check.
Claim. For $x \in \mathbb{Z}/2\mathbb{Z}$, the bit readout is $\mathsf{true}$ if $x = 1$ and $\mathsf{false}$ otherwise (equivalently, the Boolean value of the predicate $x = 1$).
background
The module builds local recognition horizon cuts by joining three audited legs on one shared context: one-sided horizon cuts that double-post the seam, exterior projection of closed cut configurations with discrete books balance and unit-temperature Clausius theorems, and a near-horizon Rindler-form rate model. A local cut is a closed cut configuration in that context; interior-private and rest-of-universe data are invisible to the exterior record.
Cut entries live in $\mathbb{Z}/2\mathbb{Z}$. This definition is the bridge from those residues to posted Boolean bits. Downstream, the exterior-accessible record is the list of exterior-private bits followed by seam bits, with interior and rest-of-universe entries traced out. No stress tensor, Ricci tensor, focusing law, or Einstein equation appears here.
proof idea
One-line definitional wrapper: apply Lean's decide to the decidable equality $x = 1$ on $\mathbb{Z}/2\mathbb{Z}$, yielding a Bool. No lemmas are invoked.
why it matters
This is the atomic conversion from discrete cut residues to posted bits used throughout the holography and gravity record stack. exteriorRecord builds the exterior-accessible bit list by reading every exterior-private and seam entry through this map. Gravity's channelBitReadout does the same per exterior cut channel (exterior-private or seam), feeding record-flux stress constructions.
In the Recognition framework it sits under the holography leg that prepares exterior records for Clausius and books-balance statements about horizon cuts. It does not itself touch T5–T8, the RCL, or the mass ladder; it only standardizes how $\mathbb{Z}/2\mathbb{Z}$ cut data become Boolean posts before those thermodynamic claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.