Holography Clausius Selector Microstate Not Clausius B

The microstate gap

The classical Clausius relation, δQ = T·ΔS, ties the heat a system exchanges to the change in its entropy. In the Recognition Science framework, this relation becomes a test for any proposed definition of entropy. The declaration microstate_not_clausius_B applies that test to one candidate: entropy defined by counting the hidden internal states, or microstates, behind a horizon. The framework proves that this candidate fails the test on a specific horizon map, meaning it cannot be the entropy that obeys the Clausius relation.

The framework sets up two horizon maps, mapA and mapB, on the same domain of sixteen faces. Both post the same record of true and false values, so they have the same record cost. But they differ in their kernel structure: mapA has eight faces posting true, while mapB has only one. The microstate cost, a count of these internal configurations, assigns a gap of three between the true and false records on mapA, and a gap of zero on mapB. The theorem microstate_not_clausius_B proves that this microstate-based entropy cannot satisfy the Clausius condition on mapB, because the required unit gap between true and false is not present.

The result is one half of a fork in the framework's development. The other theorem, microstate_not_clausius_A, proves the same failure on mapA. Together they show that microstate counting is not a viable entropy candidate under the Clausius test. The framework's preferred candidate, the record cost, passes the test: a theorem proves that any entropy obeying Clausius must assign a unit gap between the two records, and the record cost does exactly that. This leads to the Bekenstein one-quarter coefficient for horizon entropy.

What the declaration does not claim is broader. It does not prove that microstate counting is wrong in all contexts, only that it fails this specific Clausius test on these finite maps. It does not establish that the record cost is the only possible entropy, only that it is the unique one satisfying the Clausius condition as defined. And it does not make any physical claim about real black holes; the maps are finite combinatorial objects, and the bridge to physical horizons remains an open question in the framework.

/-- **The degeneracy reading fails Clausius on map B too**, by a different margin: its
record gap is `0 − 3 = −3` against a posted `+1`. -/
theorem microstate_not_clausius_B :
    ¬ IsClausius mapB (fun b => (microstateCost mapB b : ℤ)) := by
  intro h
  have hgap := clausius_gap_B _ h
  have ht : microstateCost mapB true = 0 := by decide
  have hf : microstateCost mapB false = 3 := by decide
  rw [ht, hf] at hgap
  norm_num at hgap

/-- The kernels differ: map A's `true`-fiber has 8 microstates, map B's has 1. -/
theorem different_kernels :
    (Finset.univ.filter (fun c => mapA c = true)).card = 8
    ∧ (Finset.univ.filter (fun c => mapB c = true)).card = 1 := by decide

/-- The microstate (degeneracy) functional distinguishes the two maps:
`microstateCost mapA true = 3` but `microstateCost mapB true = 0`. -/
theorem microstate_disagrees :
    microstateCost mapA true = 3 ∧ microstateCost mapB true = 0 := by decide

/-- **Clausius forces the unit record gap.** On any horizon that realizes both records,
every Clausius-consistent entropy has `E true − E false = 1`: exactly one bit across the
posted record — the record cost — regardless of the kernel. -/
theorem clausius_gap {α : Type*} (f : α → Bool) (E : Bool → ℤ)
    (hE : IsClausius f E) (c c' : α) (hc : f c = false) (hc' : f c' = true) :
    E true - E false = 1 := by
  have h := hE c c'
  rw [hc, hc'] at h
  simpa [stepHeat, hc, hc'] using h.symm

/-- The record potential (`1` on the posted record `true`, `0` on `false`) satisfies
Clausius for EVERY horizon map, of any kernel structure. -/
theorem record_potential_clausius {α : Type*} (f : α → Bool) :
    IsClausius f (fun b => if b then 1 else 0) := by
  intro c c'; simp [stepHeat]

What this page does not claim

This does not claim microstate counting is invalid in all physical contexts. This does not claim the record cost is the only possible entropy, only the unique one satisfying Clausius as defined. This does not claim any direct physical result about real black holes.

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