135theorem info_scales_subvolume (L : ℝ) (hL : 6 < L) : 136 6 * L ^ 2 < L ^ 3 := by
proof body
Tactic-mode proof.
137 have hL_pos : 0 < L := by linarith 138 have : 6 < L := hL 139 nlinarith [sq_nonneg (L - 6), sq_nonneg L] 140 141/-- The surface-to-volume ratio goes to zero: for large enough regions, 142 the boundary is negligible compared to the volume. This IS the content 143 of the holographic principle — bulk has more degrees of freedom than 144 the boundary can encode. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.