Holography Kmsdetailed Balance Bekenstein Bound From Kms

The forced bound

The Bekenstein bound is a physical limit on how much entropy can fit inside a region of space with a given energy and size. In its standard form it says the entropy S of any system obeys S ≤ 2πER, where E is the total energy and R is the radius of the smallest sphere that contains the system. The bound is famous because it hints that the deepest laws of physics might be written on a boundary rather than in a volume, an idea called holography.

The Recognition Science framework reaches the same inequality through a different door. Its library of machine-checked formal theorems contains a declaration, bekenstein_bound_from_kms, that derives S(p) ≤ 2πER for every delivered record distribution p. The derivation starts from three named premises. The first, detailed balance, says a reference state is stationary edge-by-edge: for any two records i and j, the probability of being in i times the rate of moving from i to j equals the probability of being in j times the rate of moving from j to i. The second, the KMS rate ratio, says the rates themselves obey the Boltzmann ratio, so that the ratio of forward to backward transition rates equals exp(−β(En j − En i)). The third, positive rates, says every transition is dynamically allowed. From these alone, the theorem forces the reference state to take the exponential Gibbs form, and then the bound follows.

The significance is that the exponential form is no longer assumed. Earlier rungs of the framework's ladder posited the Gibbs form directly, or assumed the state minimizes free energy. Here both of those become theorems downstream of the dynamics. The bound is conditional on two further premises: the partition function Z ≤ 1, and the horizon rate κ = 1/R. The phrase 'for every delivered record distribution' means the inequality holds for all states p that arise in the framework, not just for equilibrium ones.

What the declaration does not claim is just as important. It does not prove the Bekenstein bound for all physical systems in the conventional sense; it proves it within the framework's model, given its premises. It does not derive the KMS rate ratio from first principles; that ratio is a named model, a definitional choice, and the framework's own notes flag the task of deriving it from the deficit-free Euclidean period as remaining physics work. And it does not establish the value of the constant 2π; that magnitude comes from a separate theorem about the deficit-free period. The theorem is a piece of conditional mathematics: if the three dynamical premises hold, then the bound holds.

/-- **CONDITIONAL Bekenstein bound for ALL states, from KMS + detailed balance.**
Identical conclusion to the Rung-1/Rung-2 assemblies (`S(p) ≤ 2πER` for every
delivered record distribution), with the reference-state premise now fully dynamical:
the seam rates satisfy the KMS ratio at the deficit-free period and the reference is
stationary under them. The chain: KMS + detailed balance force the Gibbs form
(THEOREM), the Gibbs inequality prices the delivered state against it (THEOREM),
`Z ≤ 1` converts the free-energy offset into slack (premise), and the deficit-free
period supplies `β = 2πR` (THEOREM given `HorizonRate`). -/
theorem bekenstein_bound_from_kms {n : ℕ}
    (p q En : Fin n → ℝ) (W : Fin n → Fin n → ℝ) (beta kappa E R : ℝ)
    (hp : ∀ i, 0 ≤ p i) (hp1 : ∑ i, p i = 1)
    (hkms : KMSRateRatio W beta En) (hdb : DetailedBalance q W)
    (hW : PositiveRates W) (hq1 : ∑ i, q i = 1)
    (hZ : partitionFunction beta En ≤ 1)
    (hR : DeficitFreePeriod.HorizonRate kappa R) (hkappa : 0 < kappa)
    (hbeta : beta = DeficitFreePeriod.euclideanPeriod kappa)
    (hE : ∑ i, p i * En i ≤ E) :
    KeystoneFactorThree.TotalEntropyBekensteinBound (shannonEntropy p) E R := by
  have hn : 0 < n := by
    rcases Nat.eq_zero_or_pos n with rfl | hn
    · exact absurd hq1 (by simp)
    · exact hn
  exact bekenstein_bound_from_equilibrium p q En beta kappa E R hp hp1
    (kms_implies_equilibrium hn hkms hdb hW hq1) hZ hR hkappa hbeta hE

/-- **The exponential form is forced by the dynamics.** A normalized state that is
stationary (detailed balance) under any positive rate matrix satisfying the KMS ratio
at inverse temperature β IS the normalized Gibbs state, record by record. -/
theorem kms_forces_gibbs_form {n : ℕ} (hn : 0 < n) {q : Fin n → ℝ}
    {W : Fin n → Fin n → ℝ} {beta : ℝ} {En : Fin n → ℝ}
    (hkms : KMSRateRatio W beta En) (hdb : DetailedBalance q W)
    (hW : PositiveRates W) (hq1 : ∑ i, q i = 1) :
    q = gibbsState beta En := by
  obtain ⟨i0⟩ := Fin.pos_iff_nonempty.mp hn
  -- The weighted occupation is the same constant on every record.
  have hconst : ∀ i, q i * Real.exp (beta * En i) = q i0 * Real.exp (beta * En i0) :=
    fun i => weighted_occupation_eq hkms hdb hW i i0
  -- Solve for q i: exponential form with an undetermined constant.
  have hqi : ∀ i, q i = (q i0 * Real.exp (beta * En i0)) * Real.exp (-(beta * En i)) := by
    intro i
    have h := hconst i
    have hexp : Real.exp (beta * En i) ≠ 0 := ne_of_gt (Real.exp_pos _)
    have hdiv : q i = (q i0 * Real.exp (beta * En i0)) / Real.exp (beta * En i) :=
      eq_div_of_mul_eq hexp h
    rw [hdiv, div_eq_mul_inv, ← Real.exp_neg]
  -- Normalization prices the constant: c · Z = 1.
  have hsum : (q i0 * Real.exp (beta * En i0)) * partitionFunction beta En = 1 := by
    rw [← hq1]
    unfold partitionFunction
    rw [Finset.mul_sum]
    exact (Finset.sum_congr rfl fun i _ => (hqi i).symm)
  have hZpos := partitionFunction_pos hn beta En
  have hcval : q i0 * Real.exp (beta * En i0) = 1 / partitionFunction beta En :=
    (eq_div_iff (ne_of_gt hZpos)).mpr hsum
  funext i
  rw [hqi i, hcval]
  unfold gibbsState
  ring

/-- Named MODEL premise (KMS rate ratio): the seam transition rates price every
forward/backward pair by the Boltzmann ratio,
`W(i→j)/W(j→i) = exp(−β(En j − En i))`, written multiplicatively so no positivity is
needed to state it. This is the rate-level shadow of correlator KMS periodicity at
inverse temperature β; at `β = 2π/κ` it is the B2/B3 lane's output shape. -/
def KMSRateRatio {n : ℕ} (W : Fin n → Fin n → ℝ) (beta : ℝ) (En : Fin n → ℝ) : Prop :=
  ∀ i j, W i j * Real.exp (beta * En j) = W j i * Real.exp (beta * En i)

What this page does not claim

The theorem does not prove the Bekenstein bound for all physical systems outside the framework's model. The theorem does not derive the KMS rate ratio from first principles; that ratio is a named model. The theorem does not establish the value of the constant 2π; that magnitude comes from a separate theorem.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Holography/KMSDetailedBalance.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: