BHState
plain-language theorem explainer
BHState supplies the type of black hole configurations in Recognition Science, identified exactly with the triple of conserved charges (mass from time translation, charge from U(1) gauge, angular momentum from SO(3) rotation). Researchers deriving the no-hair property from J-cost minimization cite this when showing that stationary solutions are fixed by these three quantities alone. The declaration is a direct type alias to the BHCharges structure carrying no additional content or proof steps.
Claim. A black hole state is an element of the structure consisting of the triple $(M, Q, J)$ where $M$ is the mass arising from time-translation symmetry, $Q$ the charge from gauge invariance, and $J$ the angular momentum from rotational symmetry.
background
In the Recognition Science framework the stationary state of any system is the unique J-cost minimizer. For asymptotically flat spacetimes the voxel lattice forces exactly three asymptotic symmetries, producing three conserved charges: mass from the eight-tick clock, charge from ledger phase, and angular momentum from voxel rotation. The sibling structure BHCharges packages these fields as mass : ℝ, charge : ℝ, angular_momentum : ℝ. Upstream results supply the non-negative cost functions from ObserverForcing and MultiplicativeRecognizerL4 that drive the decay of all other modes.
proof idea
The declaration is a one-line abbreviation equating the identifier to the BHCharges structure. No lemmas are invoked and no tactics are used; the body consists solely of the alias.
why it matters
This definition supplies the type consumed by the uniqueness theorems bh_state_determined_by_charges and bh_state_eq_of_charges_eq, which prove that equal charges imply equal states. It realizes the three-charge characterization required by the RS no-hair theorem, consistent with the D = 3 spatial dimensions and eight-tick octave forced in UnifiedForcingChain. The parent paper proposition is that only (M, Q, J) survive because every other classical degree of freedom carries positive J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.