Holography Keystone Factor Three Violation Survives Unit Conversion

The unit-proof violation

The Bekenstein bound is a physical limit stating that the total entropy within a region cannot exceed a value proportional to the region's energy and size. In the Recognition Science framework, a ledger (a discrete record of events) can account for the entropy of a black hole horizon in two ways. One reading, the record reading, assigns an entropy equal to one quarter of the horizon's area. The other, the microstate reading, assigns exactly three times that amount. The theorem violation_survives_unit_conversion proves that this factor-of-three violation of the bound remains a violation whether entropy is measured in bits or in nats, the two standard units for information.

The proof is a simple inequality. If a number S strictly exceeds a bound bound, then multiplying both sides by the positive constant ln 2 preserves the strict inequality. Since converting from bits to nats multiplies both the entropy and the bound by this same factor, a strict violation in bits remains a strict violation in nats. The theorem is machine-checked in the framework's library of formal theorems, and it is a mathematical statement about real numbers, not a physical assumption.

This result matters because it closes a potential escape route. If the microstate reading only violated the bound in one unit system, a defender might argue the violation was an artifact of the units chosen. The theorem shows that no such rescue is possible. The exclusion of the microstate reading, conditional on other named premises, is therefore unaffected by this particular kind of objection.

In Recognition Science, this theorem is part of a larger conditional argument. The full argument assumes that the Bekenstein bound holds for total horizon entropy, that the horizon area saturates the bound, and that entropy is additive across pixels. Given those premises, the microstate reading is inconsistent. The unit-conversion theorem is a small but necessary piece of that structure, ensuring the inconsistency does not depend on a unit convention.

/-- **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))

/-- **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))

/-- **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

What this page does not claim

This theorem does not prove that the Bekenstein bound holds for total horizon entropy; that is an open hypothesis. This theorem does not establish that the microstate reading is physically incorrect, only that it is inconsistent with the named premises. This theorem does not derive the factor of three from physical principles; it is a machine-checked consequence of the ledger cost definitions.

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: