firstBitScalarCost
plain-language theorem explainer
Defines a scalar cost on the two-bit toy space Bool × Bool that reads only the first coordinate: cost 1 if true, 0 if false. It is the concrete counterexample cost used to show that scalar-cost equality is not a complete physical quotient by default. Anyone citing the T0 Boolean-shadow completeness boundary or the one-bit incompleteness theorem uses this map. The body is a one-line piecewise definition.
Claim. Define a scalar cost $C_1 : \{0,1\}^2 \to \mathbb{R}$ by $C_1(b_1,b_2) = 1$ if $b_1$ is true and $C_1(b_1,b_2) = 0$ otherwise. Only the first Boolean coordinate enters the cost.
background
The module records the Lean correction from the T-1/T0 Boolean shadow audit: a single Boolean distinction is an atomic recognition floor, not a complete encoding of an arbitrary state space. Physical identification is equality of the full recognition signature; scalar-cost equality is a complete gauge invariant only under a separate completeness hypothesis.
PairBoolState is the toy space $\mathrm{Bool} \times \mathrm{Bool}$ built for the "one Boolean cannot encode everything" counterexample. The first-bit scalar cost is the real-valued map that collapses that space onto a single bit of cost, ignoring the second coordinate.
Upstream cost notions (J-cost on recognition events, multiplicative-recognizer derived cost, PRC quotient cost) motivate calling this a scalar cost, but the definition itself is purely combinatorial on the two-bit carrier.
proof idea
Definition, not a proof. The map is the anonymous function sending a pair $x$ to $1$ when the first projection $x.1$ is true and to $0$ otherwise. No lemmas are applied.
why it matters
Feeds the incompleteness theorem first_bit_scalar_cost_not_complete, which exhibits distinct two-bit states with equal first-bit scalar cost, and the audit structure BooleanShadowCompletenessBoundary, whose second clause records that scalar-cost equality is not complete in general.
In the Recognition framework this pins the T0 boundary: one Boolean coordinate (and its induced scalar cost) is not a complete physical quotient on $\mathrm{Bool} \times \mathrm{Bool}$, while a separating family of recognizers can be. It supports the module claim that scalar-cost equality requires a separate completeness hypothesis before it may replace full signature equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.