Holography Keystone Factor Three Microstate Chain Contradicts Bound

The factor-three exclusion

Black hole entropy is a puzzle. The famous Bekenstein-Hawking formula says the entropy of a black hole is one quarter of its horizon area, in Planck units. But where does that quarter come from? One natural idea is to count the quantum microstates, the fine-grained internal configurations, of the hole. Recognition Science's ledger, a discrete record of events, offers a different route: it treats the horizon as a record of what fell in, and the cost of storing that record turns out to be the same quarter.

The framework's machine-checked library of formal theorems contains a declaration, microstate_chain_contradicts_bound, that sharpens this choice. It proves a conditional statement: if total horizon entropy obeys the Bekenstein bound (S ≤ 2πER), if the horizon area saturates that bound (A/4 = 2πER, as in the Schwarzschild solution), and if entropy adds pixel by pixel, then the microstate reading is inconsistent. The microstate cost is exactly three times the record cost, so the microstate entropy is 3·(A/4), which strictly exceeds the bound. The record reading, by contrast, saturates it. The theorem forces a contradiction from the microstate premise, not from the record one.

The factor three is not an approximation. It is a proved theorem, factor_three_is_ledger_forced, computed by the machine from the ledger floor: the microstate cost of a one-face closure map is exactly three times its record cost. The violation is scale-free, holding at every horizon radius, and it survives a change from bits to nats. No volume scaling, no bulk-to-boundary map, and no large-radius limit are needed. The exclusion is structural.

What the declaration does not claim is just as important. The Bekenstein bound itself, LEG-B, is an open hypothesis, typed as a premise and never proved. The saturation A/4 = 2πER is a model input, true for a Schwarzschild black hole in the framework's units. The per-pixel additivity, LEG-A, is a model premise measured to hold for private pixels. The theorem is a conditional discharge: if you accept those three inputs, then the microstate reading is excluded and the record reading is forced. It is not an unconditional derivation of the quarter. The weakest link, LEG-B, sets the tag: this is a conditional theorem, not a free-standing law of physics.

For a reader, the payoff is a clean dichotomy. Within the holographic program, the microstate reading is not merely disfavored; it is inconsistent with a bound that is itself hypothesized. The record reading survives. The quarter is not an arbitrary identification but the only reading consistent with the bound, saturation, and additivity, modulo the named open legs. That is what the declaration establishes, and what it leaves open.

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

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

/-- **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 itself is not proved; it is an open hypothesis. The quarter coefficient of the Bekenstein-Hawking entropy is not unconditionally derived; the result is conditional on three named premises. The theorem does not apply to rate quantities like accessible information, which have different units.

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: