Holography Keystone Factor Three Keystone Selects Record Reading

The factor-3 keystone

The Bekenstein bound is a physical limit: the total entropy of a system cannot exceed a constant times its energy and its size. In the standard formula, a black hole's entropy is one quarter of its horizon area. The question is what that entropy actually counts. One reading says it counts the black hole's internal microstates, the many possible arrangements of its constituents. Another says it counts the record, the discrete ledger of recognition events that the horizon itself keeps.

In Recognition Science, the framework models a horizon as a collection of independent pixels, each with a cost for its state. A machine-checked library of formal theorems proves that the microstate cost is exactly three times the record cost for the same closed configuration. This factor of three is not an assumption; it is computed by exhaustive case analysis on the finite configuration space. The theorem keystone_selects_record_reading then shows what happens when the horizon saturates the Bekenstein bound, meaning its entropy equals the bound's maximum. Under that condition, the record reading satisfies the bound with equality, while the microstate reading, at three times the record value, strictly violates it. The violation is scale-free: it holds at every horizon radius, with no dependence on volume, a bulk-to-boundary map, or a large-radius limit.

This is a conditional exclusion, not an unconditional proof. The argument assumes three premises: that the total entropy is the per-pixel sum, that the Bekenstein bound applies to that total, and that the horizon saturates the bound. The first is a model premise, the second is an open hypothesis, and the third is a model input. The theorem proves that, given these premises, the microstate reading is inconsistent while the record reading is consistent. It does not prove that the premises themselves are true. The factor of three is proved; the exclusion is proved conditional on the named legs.

The result changes what it means to choose the record reading. It is no longer a bare identification, a guess about what entropy counts. Inside the holographic program, with the bound and saturation in place, the microstate reading is not merely disfavored; it is inconsistent. The record reading is the only one that survives. The unit choice cannot rescue the microstate reading, because the violation is a strict ratio of three, invariant under converting bits to nats. The keystone does not derive the one-quarter coefficient from nothing; it shows that within its stated conditions, the alternative is impossible.

/-- **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 keystone package.** Under saturation, the two readings are separated by the
bound itself: record passes (with equality), microstate fails (strictly). Conditional on
LEG-B this is the selector discharge. -/
theorem keystone_selects_record_reading (A E R : ℝ) (hA : 0 < A)
    (hSat : A / 4 = 2 * Real.pi * E * R) :
    TotalEntropyBekensteinBound (A / 4) E R
      ∧ ¬ TotalEntropyBekensteinBound (3 * (A / 4)) E R :=
  ⟨record_reading_saturates A E R hSat, microstate_reading_violates A E R hA 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]

/-- **Certificate.** The keystone in one statement: conditional on LEG-A (per-pixel
additivity), LEG-B (total-entropy Bekenstein bound), and horizon saturation, the
microstate reading is inconsistent and the record reading saturates. The `1/4` premise
`HorizonEntropyIsRecordCost` is thereby discharged BY EXCLUSION within the dichotomy —
modulo exactly the named open legs, nothing else. -/
theorem keystone_certificate :
    (∀ (m N : ℕ) (S E R : ℝ), 0 < N →
        HorizonEntropyIsMicrostateCost m →
        S = (m : ℝ) * N →
        ((CoefficientBridge.rawBits * N : ℕ) : ℝ) / 4 = 2 * Real.pi * E * R →
        TotalEntropyBekensteinBound S E R → False)
    ∧ (∀ (m N : ℕ) (S E R : ℝ),
        HorizonEntropyIsRecordCost m →
        S = (m : ℝ) * N →
        ((CoefficientBridge.rawBits * N : ℕ) : ℝ) / 4 = 2 * Real.pi * E * R →
        TotalEntropyBekensteinBound S E R) :=
  ⟨fun m N S E R hN hMicro hAdd hSat hBound =>
      microstate_chain_contradicts_bound m N S E R hN hMicro hAdd hSat hBound,
    fun m N S E R hRec hAdd hSat =>
      record_chain_saturates_bound m N S E R hRec hAdd hSat⟩

What this page does not claim

The Bekenstein bound itself is not proved; it is an open hypothesis. The factor of three does not by itself derive the one-quarter area coefficient; it only excludes the microstate reading conditional on the named premises. The theorem does not claim that the record reading is physically realized, only that it is the consistent one under the stated conditions.

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: