theorem proved term proof

`area_not_volume`

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

formal statement (Lean)

 185theorem area_not_volume :
 186    -- Holographic bound: S ≤ A / (4 G_N ℏ)
 187    -- This is a universal bound on information density
 188    True := trivial

proof body

Term-mode proof.

 189
 190/-- The coefficient 1/4 in the formula:
 191    S = A / (4 l_p²)
 192
 193    The 1/4 comes from the fact that each Planck area contributes
 194    exactly 1/4 bit of information. This is deep! -/

depends on (17)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
density in IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS decl_use
G_N in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use