def definition def or abbrev

`excessBandwidth`

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

formal statement (Lean)

 170noncomputable def excessBandwidth (M : ℝ) : ℝ :=

proof body

Definition body.

 171  horizonBandwidth M - horizonDemand M
 172
 173/-- The entropy of a BH is exactly its holographic bandwidth capacity,
 174    confirming that area = information = bandwidth. -/

depends on (18)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
entropy in IndisputableMonolith.Foundation.InitialCondition decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived 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
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
M in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use
entropy in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
entropy in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use
horizonBandwidth in IndisputableMonolith.Unification.BlackHoleBandwidth decl_use
horizonDemand in IndisputableMonolith.Unification.BlackHoleBandwidth decl_use
bandwidth in IndisputableMonolith.Unification.RecognitionBandwidth decl_use