ledger_capacity_pos_of_area_pos
plain-language theorem explainer
Positive area A guarantees strictly positive ledger capacity A over ell0 squared in RS units. Researchers deriving black hole entropy from information capacity on horizons cite this for consistency of the positivity step. The proof is a direct term reduction that unfolds the capacity definition and applies the division positivity lemma to hA together with ell0 squared positivity.
Claim. If $A > 0$ then $A / ell_0^2 > 0$, where $ell_0 > 0$ is the fundamental length unit in RS-native units.
background
LedgerCapacityLimit is the definition $A / ell_0^2$, the maximum number of recognition bits storable on a surface of area A. The module derives the Bekenstein-Hawking entropy from this limit, showing that $S_{BH} = A / 4 ell_p^2$ arises from maximum recognition flux on the horizon. Upstream results establish ell0 as the RS voxel length (equal to 1 in native units) and prove ell0_pos by direct simplification.
proof idea
The term proof unfolds LedgerCapacityLimit to the quotient A / ell0^2. It then applies div_pos directly to the hypothesis hA and the positivity of ell0 squared, which is immediate from ell0_pos.
why it matters
The result supplies the required positivity for the ledger-capacity derivation of black hole entropy in the module. It supports downstream statements such as bh_entropy_from_ledger by ensuring the capacity expression remains positive whenever area is positive, consistent with the Recognition Science objective of maximum recognition flux. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.