BHCharges
plain-language theorem explainer
BHCharges records the three conserved charges (mass from time symmetry, charge from U(1) gauge, angular momentum from rotations) that label stationary black holes in Recognition Science. Researchers proving uniqueness of J-cost minimizers or deriving Bekenstein-Hawking entropy would cite this structure when reducing the problem to these quantities. The declaration is a direct record structure with no computational content.
Claim. A black hole in RS is specified by its mass $M$, charge $Q$, and angular momentum $J$, the three quantities conserved by time-translation, U(1) gauge, and SO(3) rotational symmetries of the voxel lattice.
background
Recognition Science works in native units where one tick is the fundamental time quantum and one voxel is the fundamental length quantum, with speed of light set to 1. The eight-tick phase supplies the discrete angles $kπ/4$ that govern periodic evolution, while the active edge count $A=1$ enters the φ-power balance identity at three spatial dimensions. The module states that any stationary state is the unique J-cost minimizer, so that only the three charges forced by the lattice symmetries survive in asymptotically flat spacetimes.
proof idea
The declaration is a structure definition with an empty proof body. It simply assembles three real numbers whose physical meanings are supplied by the upstream constants tick, voxel, U, phase, and A.
why it matters
BHCharges supplies the data type for BHState and thereby feeds the no-hair results hair_cost_nonneg, hair_cost_zero_iff, and bekenstein_hawking_entropy. It realizes the module claim that exactly three charges survive J-cost minimization, closing the step from the eight-tick octave and D=3 forcing to the classical black-hole uniqueness statement in RS_No_Hair_Theorem.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.