theorem proved term proof

`rt_formula_holds`

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

formal statement (Lean)

 161theorem rt_formula_holds :
 162    -- S_A = Area / (4 G_N ℏ)
 163    -- This is exact in the large-N, strong coupling limit
 164    True := trivial

proof body

Term-mode proof.

 165
 166/-! ## RS Explanation -/
 167
 168/-- In RS, the RT formula arises from **ledger structure**:
 169
 170    1. Ledger entries are fundamentally 2D (live on surfaces)
 171    2. Entanglement = shared ledger entries across a cut
 172    3. Number of shared entries ∝ area of the cut
 173    4. Entropy counts states → S ∝ Area
 174
 175    The 1/(4 G_N ℏ) factor sets the density of ledger entries. -/

depends on (13)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization 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
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom 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