hair_cost
plain-language theorem explainer
The hair_cost definition assigns to each real field amplitude the J-cost of the shifted mode 1 plus amplitude. Physicists deriving black-hole uniqueness from cost minimization cite this as the explicit penalty on non-conserved perturbations. The definition is a direct wrapper around the Jcost function applied to the shifted argument.
Claim. For a real field amplitude $a$, the hair cost is defined by $J(1+a)$, where $J$ is the J-cost function induced by the multiplicative recognizer.
background
J-cost is the cost function induced by a multiplicative recognizer: the derived cost of its comparator on positive ratios. In the observer-forcing setting it is the cost of a recognition event, given by the J-cost of the underlying state. The module treats the stationary state of an asymptotically flat spacetime as the unique J-cost minimizer, so that only the three Noether charges (M, Q, J) forced by the RS voxel lattice can survive.
proof idea
This is a one-line wrapper that applies the Jcost function to the expression 1 + field_amplitude.
why it matters
The definition supplies the cost measure used by the downstream theorems hair_cost_nonneg, hair_cost_zero_iff and no_hair_field_decay. It encodes the RS mechanism that assigns positive J-cost to any field mode beyond the three conserved charges, forcing decay under J-cost minimization. The parent results close the structural no-hair statement that only (M, Q, J) remain in the stationary limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.