theorem proved term proof

`bekenstein_positive`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 121theorem bekenstein_positive (A : ℝ) (hA : 0 < A) :
 122    0 < A / (4 * G_rs * hbar_rs) := by

proof body

Term-mode proof.

 123  rw [bekenstein_hawking_from_rs A hA]
 124  positivity
 125
 126/-! ## Part 4: Information Scales with Boundary (Not Volume) -/
 127
 128/-- **INFORMATION SCALES SUB-VOLUME**: In D=3, the information accessible from
 129    a region of volume V scales as V^{2/3} (surface area), NOT as V.
 130
 131    For a cube of side L: volume = L³, surface = 6L², so
 132    surface/volume = 6/L → 0 as L → ∞.
 133
 134    This proves the holographic scaling: info ∝ Area ∝ V^{2/3} ≪ V. -/

depends on (21)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
G_rs in IndisputableMonolith.Constants.GravitationalConstant decl_use
V in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost decl_use
G_rs in IndisputableMonolith.Foundation.ConstantDerivations decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
V in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
bekenstein_hawking_from_rs in IndisputableMonolith.Papers.GCIC.BekensteinFromLedger decl_use
G_rs in IndisputableMonolith.Papers.GCIC.BekensteinFromLedger decl_use
hbar_rs in IndisputableMonolith.Papers.GCIC.BekensteinFromLedger decl_use
volume in IndisputableMonolith.Papers.GCIC.BrainHolography decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
V in IndisputableMonolith.RRF.Core.Glossary decl_use