Holography Keystone Factor Three Violation Is Scale Free

The scale-free violation

The Bekenstein bound is a physical limit that connects a region's entropy to its energy and size. In its standard form, it says the total entropy S of a system cannot exceed 2π times its energy E times its radius R. The bound is famous because black holes appear to saturate it: their entropy, the Bekenstein-Hawking value A/4 (one quarter of the horizon area in Planck units), sits exactly on the limit. The question at stake is what kind of entropy that A/4 counts.

In the Recognition Science framework, a ledger (a discrete record of events) carries two possible costs for a horizon: a record cost, which counts the bits needed to describe the boundary itself, and a microstate cost, which counts the bits needed to describe everything inside. The framework's machine-checked library of formal theorems proves that the microstate cost is exactly three times the record cost for the same closure map: 3 = 3·1, both computed by direct evaluation. At the density level, this means the microstate reading assigns 3/4 of the raw bits, while the record reading assigns 1/4.

The theorem named violation_is_scale_free is a small algebraic consequence with a large meaning. It states that if the horizon saturates the bound, so A/4 = 2πER, then the microstate entropy 3·(A/4) equals 3·(2πER). The violation is the constant factor 3 at every horizon radius. No volume scaling, no large-radius limit, and no bulk-to-boundary map is needed to see the excess. The factor is fixed by the ledger structure itself, not by any approximation.

This scale-freeness distinguishes the argument from a correction that fades at large radii or a shell effect that matters only near the horizon. If the microstate reading were wrong only by a small amount, one might hope to fix it with a perturbative adjustment. The theorem shows the excess is a strict ratio, so no unit conversion from bits to nats can rescue it, and no asymptotic regime makes it small. The exclusion, conditional on the named premises, is structural.

What the theorem does not claim is just as important. It does not prove that the Bekenstein bound itself holds for total thermodynamic horizon entropy in this framework; that statement, LEG-B, remains an open hypothesis. It does not prove that the horizon saturates the bound; that saturation is a model input from Schwarzschild geometry. It does not prove that the record reading is correct. The theorem only establishes that, given saturation, the microstate reading violates the bound by exactly the factor 3 at every scale, while the record reading saturates it. The choice between the two readings is then decided by exclusion, conditional on the open legs, not by an unconditional derivation of the 1/4 coefficient.

/-- **The factor 3 is ledger-forced, not hand-typed.** The kernel-side (microstate) cost of
the one-face closure map is exactly three times its image-side (record) cost: `3 = 3 · 1`.
Both sides are computed by `decide` on the actual map; the `3` in "the microstate reading
assigns `3·(A/4)`" is THIS `3`. -/
theorem factor_three_is_ledger_forced :
    microstateCost (fun c : PixelLocal.FaceCfg => PixelLocal.closed c) true
      = 3 * recordCost (fun c : PixelLocal.FaceCfg => PixelLocal.closed c) := by
  decide

/-- The same factor at the density level: the nullity density `3/4` is three times the rank
density `1/4` (`CoefficientBridge.freeBits = 3 · closureRank`). -/
theorem density_ratio_is_three :
    (CoefficientBridge.freeBits : ℚ) / (CoefficientBridge.rawBits : ℚ)
      = 3 * ((CoefficientBridge.closureRank : ℚ) / (CoefficientBridge.rawBits : ℚ)) := by
  rw [CoefficientBridge.freeBits_eq_three, CoefficientBridge.closureRank_eq_one,
    CoefficientBridge.rawBits_eq_four]
  norm_num

/-- **Scale-freeness of the violation.** The excess is exactly the constant 3 at every
saturated horizon: `3·(A/4) = 3·(2πER)` whenever `A/4 = 2πER`. This is what distinguishes
the keystone from a `δ`-shell or large-`R` correction argument. -/
theorem violation_is_scale_free (A E R : ℝ)
    (hSat : A / 4 = 2 * Real.pi * E * R) :
    3 * (A / 4) = 3 * (2 * Real.pi * E * R) := by
  rw [hSat]

/-- **Microstate reading violates the saturated bound — at every radius.** Given the same
saturation and a nondegenerate horizon (`0 < A`), the microstate-reading entropy `3·(A/4)`
strictly exceeds the bound. The violation is the fixed factor 3: no volume scaling, no
bulk-to-boundary map, no asymptotics. -/
theorem microstate_reading_violates (A E R : ℝ) (hA : 0 < A)
    (hSat : A / 4 = 2 * Real.pi * E * R) :
    ¬ TotalEntropyBekensteinBound (3 * (A / 4)) E R := by
  unfold TotalEntropyBekensteinBound
  rw [← hSat]
  intro h
  linarith

/-- **The unit choice cannot rescue the microstate reading.** A strict violation in bits
stays a strict violation in nats (multiplying both sides by `ln 2 > 0`), so the exclusion
is invariant under the `EntropyCandidateAudit.bitsToNats` conversion. -/
theorem violation_survives_unit_conversion (S bound : ℝ) (h : bound < S) :
    bound * Real.log 2 < S * Real.log 2 :=
  mul_lt_mul_of_pos_right h (Real.log_pos (by norm_num))

What this page does not claim

The Bekenstein bound for total thermodynamic horizon entropy is proved; it is an open hypothesis. The horizon saturation A/4 = 2πER is derived; it is a model input. The record reading of horizon entropy is unconditionally established; it is selected only by exclusion under the named premises.

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/KeystoneFactorThree.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: