S_lead_pos
plain-language theorem explainer
The leading-order black-hole entropy in Recognition Science is strictly positive for any positive horizon area. Researchers modeling discrete gravity or ledger-based entropy would cite this to confirm the count of admissible states remains positive. The proof is a one-line wrapper that unfolds the definition S_lead(A) = A/4 and applies linear arithmetic.
Claim. If $A > 0$ then the leading entropy $S(A) = A/4$ is positive.
background
In the Black-Hole Entropy from the Ledger module the leading-order term is defined by S(A) = A/4 in RS-native units with Planck length set to 1. This recovers the classical Bekenstein-Hawking entropy at leading order while the module separately derives the logarithmic correction coefficient c_RS = -log phi / 2. The local setting treats black-hole entropy as the count of admissible horizon states modulo sigma-equivalence on the discrete ledger.
proof idea
The proof is a one-line wrapper. It unfolds the definition S(A) = A/4 and invokes the linarith tactic on the hypothesis 0 < A to conclude positivity.
why it matters
This result supplies the S_lead_pos field of the BlackHoleEntropyFromLedgerCert structure, the master certificate for Track F6. It closes the algebraic positivity requirement for the leading term A/4 while the module distinguishes the RS coefficient c_RS from the LQG value -1/2 and the string-theory value -3/2. The certificate remains a theorem on algebraic structure; the empirical match to semiclassical gravity is left as an open hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.