bit
plain-language theorem explainer
Maps a Boolean to its standard bit value in ℕ: false to 0 and true to 1. Geometry and constants code cite it whenever a Boolean flag must enter arithmetic (vertex offsets, bit costs, residual comparisons). The body is a two-clause pattern match with no proof obligations.
Claim. Define the function $\mathrm{bit}\colon\{\mathsf{false},\mathsf{true}\}\to\mathbb{N}$ by $\mathrm{bit}(\mathsf{false})=0$ and $\mathrm{bit}(\mathsf{true})=1$.
background
The module builds a typed periodic Freudenthal torus: a scalable target shape for an arbitrary periodic Freudenthal tiling. It isolates vertex, edge, and tetrahedron structure so that any finite triangulation encoding the model inherits the global incidence-edge-slot partition needed by the nonlinear Regge first-variation theorem. Concrete finite encoders into Fin nV, Fin nE, Fin nT remain future work.
Boolean flags appear throughout the vertex arithmetic (coordinate increments, bit displacements on the cube). Converting those flags to natural numbers is the role of this map. The same definition is re-exported from the 4D periodic torus module and is used far beyond geometry: constants code treats a single ledger bit as the unit whose cost is $\ln\varphi$.
proof idea
Pure definition by pattern match on Bool. No lemmas, tactics, or proof terms: false returns 0 and true returns 1. Downstream lemmas simply unfold or simp this definition when a Boolean enters an arithmetic expression.
why it matters
Although elementary, the map is a high-fan-in primitive: roughly forty use sites. In geometry it feeds addBit, addBits, dispBits, and vertexBits, which assemble periodic vertex offsets on the Freudenthal torus. In the constants layer it underwrites the ledger bit cost $J_{\mathrm{bit}}=\ln\varphi$ (T6), the locked lag constant $C_{\mathrm{lock}}=\varphi^{-5}$, the light-cone identity $\ell_0=c\cdot\tau_0$, Boltzmann-analog bounds $k_R\in(0.47,0.49)$, and the curvature-balance residual $J_{\mathrm{curv}}(\lambda)-J_{\mathrm{bit}}$ whose unique positive root fixes the recognition length. Without a uniform Boolean-to-ℕ coercion those identities would each reintroduce ad-hoc case splits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.