Holography Keystone Factor Three Factor Three Is Ledger Forced

The factor-3 keystone

The Bekenstein-Hawking formula gives the entropy of a black hole as one quarter of its horizon area, in Planck units. The Recognition Science framework asks a pointed question about that 1/4: is it a count of the ledger's record entries, a discrete record of events on the horizon, or a count of the microstates, the fine-grained internal configurations that could underlie the same horizon? The framework's library of machine-checked theorems does not answer that question outright. Instead it proves a sharp structural fact: if you take the microstate reading, the entropy is not 1/4 of the area but exactly 3/4, a factor of three larger, at every horizon radius.

The proof of that factor of three is the declaration factor_three_is_ledger_forced. It is a theorem in the framework's machine-checked library of formal theorems, and it is axiom-clean: the statement is checked by the kernel with no framework-specific axioms. The theorem says that the kernel-side microstate cost of a one-face closure map is exactly three times its image-side record cost, written 3 = 3 · 1. Both sides are computed by a decision procedure on the actual map; the 3 in the microstate reading assigns 3·(A/4) is this very 3. The same ratio appears at the density level: the nullity density 3/4 is three times the rank density 1/4.

The factor is scale-free. If the horizon area A saturates the bound A/4 = 2πER, then the microstate reading gives 3·(A/4) = 3·(2πER), an excess of exactly 3 at every radius. This is what distinguishes the keystone from a δ-shell or large-radius correction argument: there is no volume scaling, no bulk-to-boundary map, no asymptotics involved. The violation is a strict ratio statement, so it survives a change of units from bits to nats; multiplying both sides by ln 2 > 0 cannot rescue the microstate reading.

What the factor does not do is prove that the record reading is the correct physical one. That conclusion is conditional. The framework states three named premises: per-pixel additivity of entropy, the total-entropy Bekenstein bound, and horizon saturation. The first two are hypotheses, not theorems; the saturation is a model input. Given those, the framework proves that the microstate reading contradicts the bound while the record reading saturates it, so the record reading is selected by exclusion within the proved dichotomy. The factor of three itself is unconditional, but the physical discharge is not.

The consequence is a precise division of labor. The framework has not derived the Bekenstein-Hawking 1/4 from nothing. It has shown that, inside the holographic program with bound, saturation, and additivity, the microstate reading is inconsistent, not merely disfavored. The selector premise is no longer a bare identification; it is a conditional exclusion. That is the keystone's value: it converts a question of taste into a question of consistency, modulo exactly the named open legs and nothing else.

/-- **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 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 microstate chain is inconsistent (the keystone, fully typed).** Assemble the
named premises: the horizon carries per-pixel multiplicity `m` under the MICROSTATE
reading (`HorizonEntropyIsMicrostateCost`, so `m = 3` by `decide`); total entropy is
per-pixel additive over `N ≥ 1` private pixels (LEG-A, `hAdd`); the horizon area in pixel
units is `rawBits · N = 4N` and saturates `A/4 = 2πER` (`hSat`); and the total-entropy
Bekenstein bound holds (LEG-B, `hBound`). CONTRADICTION: `S = 3N > N = 2πER`. So within
the dichotomy, conditional on LEG-A + LEG-B + saturation, the microstate reading is
excluded and `HorizonEntropyIsRecordCost` is forced. -/
theorem microstate_chain_contradicts_bound
    (m N : ℕ) (S E R : ℝ) (hN : 0 < N)
    (hMicro : HorizonEntropyIsMicrostateCost m)
    (hAdd : S = (m : ℝ) * N)
    (hSat : ((CoefficientBridge.rawBits * N : ℕ) : ℝ) / 4 = 2 * Real.pi * E * R)
    (hBound : TotalEntropyBekensteinBound S E R) :
    False := by
  have hm : m = 3 := by
    unfold HorizonEntropyIsMicrostateCost at hMicro
    rw [hMicro]; decide
  have hA : ((CoefficientBridge.rawBits * N : ℕ) : ℝ) = 4 * N := by
    rw [CoefficientBridge.rawBits_eq_four]; push_cast; ring
  rw [hA] at hSat
  unfold TotalEntropyBekensteinBound at hBound
  rw [hAdd, hm, ← hSat] at hBound
  have hNpos : (0 : ℝ) < N := by exact_mod_cast hN
  push_cast at hBound
  linarith

/-- **The record chain is consistent (saturation).** The same assembly under the RECORD
reading (`m = 1`) yields `S = N = 2πER`: the bound is saturated, not violated. Together
with `microstate_chain_contradicts_bound` this is the conditional discharge of
`HorizonEntropyIsRecordCost`: within the proved dichotomy, it is the unique reading
consistent with the (hypothesized) total-entropy Bekenstein bound at a saturated
horizon. -/
theorem record_chain_saturates_bound
    (m N : ℕ) (S E R : ℝ)
    (hRec : HorizonEntropyIsRecordCost m)
    (hAdd : S = (m : ℝ) * N)
    (hSat : ((CoefficientBridge.rawBits * N : ℕ) : ℝ) / 4 = 2 * Real.pi * E * R) :
    TotalEntropyBekensteinBound S E R := by
  have hm : m = 1 := by
    unfold HorizonEntropyIsRecordCost at hRec
    rw [hRec]; exact recordCost_closed
  have hA : ((CoefficientBridge.rawBits * N : ℕ) : ℝ) = 4 * N := by
    rw [CoefficientBridge.rawBits_eq_four]; push_cast; ring
  rw [hA] at hSat
  unfold TotalEntropyBekensteinBound
  rw [hAdd, hm]
  push_cast
  linarith [le_of_eq hSat]

What this page does not claim

The Bekenstein-Hawking 1/4 is not unconditionally derived; the discharge is conditional on the named open legs. The framework does not prove that the record reading is physically correct, only that it is consistent where the microstate reading is not. The factor of three is not a claim about any particular black hole spacetime; it is a statement about the framework's cost functions.

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: