bh_state_eq_of_charges_eq
plain-language theorem explainer
Black hole states in the Recognition Science model coincide exactly when their mass, charge, and angular momentum match. A researcher deriving uniqueness from J-cost minimization in asymptotically flat spacetimes would cite this result to close the classical no-hair argument. The proof is a direct one-line application of the lemma that BHState is fixed by its three conserved charges.
Claim. Let $s_1$ and $s_2$ be black hole states, each fully specified by its conserved charges. If the mass, electric charge, and angular momentum of $s_1$ equal those of $s_2$, then $s_1 = s_2$.
background
In the module, a black hole state is defined as BHState := BHCharges, the triple of conserved quantities (M, Q, J) that survive in D = 3 + 1 dimensions. The local setting is J-cost minimization: the stationary configuration is the unique global minimizer of the convex functional J(x) = (x + x^{-1})/2 - 1. Upstream results supply the convexity (PhysicsComplexityStructure.of) and the forcing of exactly three symmetries (SpectralEmergence.of together with PhiForcingDerived.of). The IntegrationGap.A and LedgerFactorization.of structures calibrate the discrete tick count and the J-bit ledger that underlie the cost.
proof idea
The proof is a one-line wrapper that applies the sibling lemma bh_state_determined_by_charges. No further tactics or reductions are required; the term simply invokes the prior result that any two BHState objects agreeing on the three charges are identical.
why it matters
This declaration supplies the uniqueness step inside the no-hair theorem constructed from J-cost minimization. It directly implements the DOC_COMMENT claim that only the three asymptotic symmetries (time translation, U(1) gauge, SO(3) rotation) remain unbroken in D = 3 + 1. The result sits immediately before the Bekenstein-Hawking entropy definitions and feeds the larger chain that equates entropy to horizon area in Planck units. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.