blackHoleEntropyFromLedgerCert
plain-language theorem explainer
The definition constructs an instance of the BlackHoleEntropyFromLedgerCert structure by direct record assembly. A researcher comparing discrete ledger models to semiclassical gravity would cite it to confirm the RS entropy formula and its coefficient distinctions. The construction is a one-line record that supplies each required field from the supporting sibling theorems.
Claim. The structure requiring that the leading ledger entropy term $S_{lead}$ is positive for positive horizon area $A$, that $S_{lead}(A) = A/4$, that the RS log coefficient $c_{RS} = -\log\phi/2$ is negative, and that $c_{RS}$ differs from both the LQG value $-1/2$ and the string-theory value $-3/2$ is inhabited.
background
The module recovers the Bekenstein-Hawking entropy from the discrete RS ledger as the count of admissible horizon states. It defines the leading term $S_{lead}(A) = A/4$ (in units with $\ell_P = 1$) and the coefficient $c_{RS} = -\log\phi/2 \approx -0.241$. The structure BlackHoleEntropyFromLedgerCert packages the positivity of $S_{lead}$, the area-law equality, negativity of $c_{RS}$, and its strict inequality to the LQG and string values.
Upstream results supply the individual theorems: $S_{lead_pos}$ establishes positivity via linarith after unfolding the definition; $S_{lead_eq_BH}$ is the reflexivity $S_{lead}(A) = A/4$; $c_{RS_neg}$ uses the positivity of $\log\phi$; and the two inequality theorems invoke $\log\phi < 1$ to obtain contradictions with the target constants.
proof idea
This is a direct record construction that populates the five fields of BlackHoleEntropyFromLedgerCert by referencing the sibling theorems $S_{lead_pos}$, $S_{lead_eq_BH}$, $c_{RS_neg}$, $c_{RS_neq_LQG}$, and $c_{RS_neq_string}$. No further tactics or reductions are applied.
why it matters
The definition inhabits the master certificate for Track F6, which recovers the Bekenstein-Hawking leading term from the RS ledger and isolates the $\phi$-rational log correction. It supplies the algebraic structure asserted in the module documentation while leaving the empirical coefficient match as a hypothesis awaiting semiclassical adjudication. The result sits downstream of the phi-ladder constants and supports the one-statement theorem that packages the full RS entropy prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.