S_lead
plain-language theorem explainer
S_lead supplies the leading term of black-hole entropy recovered from the RS ledger as horizon area divided by four in native units. Quantum-gravity researchers comparing discrete state counts to semiclassical thermodynamics cite it to anchor the Bekenstein-Hawking match before adding logarithmic corrections. The declaration is a direct algebraic assignment with no lemmas or reductions required.
Claim. The leading-order black-hole entropy in Recognition Science is given by $S(A) = A/4$, where $A$ is the horizon area in RS-native units with Planck length set to 1.
background
The Black-Hole Entropy from the Ledger module recovers the Bekenstein-Hawking formula $S_{BH} = A/(4 ell_P^2)$ from the discrete ledger of admissible horizon states modulo sigma-equivalence. All work occurs in RS-native units where ell_P = 1, so the leading term reduces to A/4. Upstream results fix the active-edge count per tick and the coherence energy unit that set the dimensional conventions for the ledger.
proof idea
The declaration is a direct definition that performs the assignment A/4 with no lemmas, tactics, or reductions. It serves as the base term for all subsequent entropy statements in the module.
why it matters
S_lead supplies the leading term required by BlackHoleEntropyFromLedgerCert and black_hole_entropy_one_statement, which certify agreement with the classical A/4 result while distinguishing the RS log coefficient from LQG and string-theory values. It realizes the module claim that the ledger state count reproduces the Bekenstein-Hawking leading term in native units and sits inside the Recognition Science forcing chain at D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.