bh_state_determined_by_charges
plain-language theorem explainer
Black hole states in Recognition Science are identical whenever their mass, charge, and angular momentum match. Researchers deriving no-hair results from J-cost minimization would cite this uniqueness step. The proof is a direct term-mode argument that splits on the two state constructors and simplifies the charge equalities to structural identity.
Claim. Let $s_1$ and $s_2$ be black hole states. If the mass of $s_1$ equals the mass of $s_2$, the charge of $s_1$ equals the charge of $s_2$, and the angular momentum of $s_1$ equals the angular momentum of $s_2$, then $s_1 = s_2$.
background
A black hole state is defined as BHState := BHCharges, a structure fully characterized by its three conserved charges. The module sets the local theoretical setting as the no-hair theorem obtained from J-cost minimization: the stationary state of any system is the unique J-cost minimizer, and for asymptotically flat spacetimes exactly three conserved charges survive, corresponding to time translation (mass M), U(1) gauge (charge Q), and SO(3) rotation (angular momentum J). Upstream results supply the spatial independence semantics and RS-native units that fix the gauge and voxel lattice underlying charge conservation.
proof idea
The proof introduces the three hypotheses on mass, charge, and angular momentum equality. It performs case analysis on both BHState values, reducing them to their underlying charge records, then applies simplification to obtain structural equality.
why it matters
This theorem supplies the uniqueness link that feeds the downstream result bh_state_eq_of_charges_eq. It fills the key step in the no-hair theorem by showing that equal charges imply equal states via J-cost uniqueness. The result aligns with the framework's forcing chain to D = 3 spatial dimensions and the three independent asymptotic symmetries forced by the RS voxel lattice; all other would-be hair carries positive J-cost and decays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.