hair_cost_zero_iff
plain-language theorem explainer
The equivalence establishes that the J-cost associated to a black-hole hair amplitude vanishes precisely when the amplitude itself is zero, under the positivity constraint 1 + amplitude > 0. Researchers deriving the no-hair property from cost minimization would invoke this to rule out nonzero perturbations. The tactic proof rewrites the cost via the squared-ratio identity and reduces the resulting equation to amplitude squared equals zero by positivity of the denominator.
Claim. Let $a$ be a real number with $1 + a > 0$. Then the hair cost of amplitude $a$ equals zero if and only if $a = 0$, where the hair cost is the J-cost function evaluated at $1 + a$ and $J(x) = (x-1)^2 / (2x)$ for $x > 0$.
background
Black Hole No-Hair Theorem from J-Cost Minimization states that in RS the stationary state of any system is the unique J-cost minimizer. For asymptotically flat spacetime exactly three conserved charges survive (M, Q, J) corresponding to the three symmetries forced by the RS voxel lattice. All other classical information decays because it carries positive J-cost. The hair_cost function measures the cost of a perturbation with amplitude $a$ as $J(1 + a)$, where $J$ is the Recognition cost function. The upstream result Jcost_eq_sq rewrites $J(x) = (x-1)^2 / (2x)$ for $x ≠ 0$, while Jcost_unit0 records that $J(1) = 0$.
proof idea
The proof unfolds the definition of hair_cost then splits into the two directions of the biconditional. In the forward direction Jcost_eq_sq rewrites the cost as a ratio; the assumption that the ratio is zero together with the positivity of the denominator (derived from 1 + amplitude > 0) forces the numerator amplitude squared to be zero. The converse direction applies Jcost_unit0 after substituting amplitude = 0.
why it matters
This supplies the zero-cost characterization required by the downstream theorem no_hair_field_decay, which shows that nonzero hair amplitude produces strictly positive cost and therefore decays. It directly supports the structural no-hair statement that only the three conserved charges (M, Q, J) survive in stationary black holes. Within the framework it instantiates the J-uniqueness property that forces all non-fixed-point modes to carry positive cost, consistent with the eight-tick octave and D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.