sbh_saturation_uniqueness
plain-language theorem explainer
The theorem asserts that for any positive Schwarzschild radius Rs the Bekenstein-Hawking entropy saturation value is the unique real number equal to the horizon area divided by four times ell0 squared. Researchers deriving black-hole thermodynamics from information or ledger constraints would cite it when establishing uniqueness of the area-law entropy. The proof is a direct term-mode construction that exhibits the candidate value, confirms equality by reflexivity, and discharges uniqueness by substitution.
Claim. For every real number $R_s > 0$ there exists a unique real number $S$ such that $S = A(R_s)/(4 ell_0^2)$, where $A(R_s) = 4 pi R_s^2$ is the event-horizon area.
background
The module derives the Bekenstein-Hawking entropy from the ledger capacity limit under the Recognition Science framework. HorizonArea(Rs) is defined as the classical Schwarzschild horizon area 4 pi Rs squared. ell0 is the fundamental length unit (voxel size) fixed to 1 in RS-native units, obtained from the relation ell0 = c tau0 with tau0 squared equal to hbar G over pi c to the fifth. Upstream results supply the entropy definition as total defect of a configuration and the maximum-recognition-flux bound that saturates at this area-law value.
proof idea
The term-mode proof constructs the explicit candidate HorizonArea Rs divided by 4 ell0 squared, applies rfl to witness the equality, and uses exact substitution to show that any other S prime satisfying the same equality must coincide with the candidate.
why it matters
The result certifies that the saturation entropy is uniquely fixed by the horizon area once ell0 is given, closing the definitional step in the derivation of S_BH = A / 4 ell_p squared from maximum recognition flux. It sits inside the chain that begins from the UniversalForcingSelfReference structure and the entropy-as-defect definition, and supplies the uniqueness needed for downstream ledger-capacity statements such as bh_entropy_from_ledger. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.