sv_ratio_decreasing
plain-language theorem explainer
The surface-to-volume ratio 6/L for a cubic region of side L is strictly decreasing in L for L > 0. Researchers deriving holographic bounds from the RS ledger on Z^3 cite this step to show boundary information becomes negligible compared to bulk volume at macroscopic scales. The proof is a one-line term application of the library inequality for positive real quotients.
Claim. For real numbers $L_1, L_2 > 0$ with $L_1 < L_2$, the surface-to-volume ratio satisfies $6/L_2 < 6/L_1$.
background
The module derives the Bekenstein-Hawking bound from the RS ledger on Z^3. In this setting D = 3 is forced by the unified chain, each voxel carries one ledger unit, and boundary size scales as volume to the power (D-1)/D = 2/3. The surface-to-volume ratio for a cube is therefore 6/L, which tends to zero for large L. This fact is used to separate boundary-accessible information from bulk degrees of freedom. Upstream results supply the active-edge count A = 1 per tick and the G hbar product equal to one in RS units.
proof idea
The proof is a one-line term that applies the Mathlib lemma div_lt_div_of_pos_left to the positive constant 6, using the hypotheses that L1 is positive and L1 < L2.
why it matters
This lemma supplies the monotonicity step inside the area-not-volume certificate that closes Gap G3. It confirms that for L > 6 the ratio drops below unity, so information scales with boundary area rather than volume, matching the holographic content stated in the module doc-comment. The result sits inside the T8-forced D = 3 geometry and the G hbar = 1 normalization that yields S_BH = A/4.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.