Holography Clausius Selector Target Clausius Selector Holds

The Clausius selector

The Clausius relation, δQ = T·ΔS, is the classical statement that heat flowing into a system equals its temperature times its entropy change. In the Recognition Science framework, this relation becomes a test for what entropy really measures. The declaration target_clausius_selector_holds is a machine-checked theorem proving that, under the framework's posting rule, the entropy assigned to a horizon is determined entirely by its observable record of state changes, not by any hidden microscopic structure.

The proof constructs two different horizon maps on the same domain of sixteen faces. Both maps post the same two-state record, true or false, so they have the same record cost of one bit. But their internal structure differs sharply: one map has eight faces posting true and eight posting false, while the other has just one face posting true and fifteen posting false. The theorem shows that any entropy function obeying the Clausius relation must assign the same unit gap between the two record states for both maps. A function based on the hidden microstate counts, by contrast, assigns different gaps to the two maps and fails the Clausius test outright.

The key mechanism is that heat, defined as the sum of signed record changes along a path, factors through the record trace. Any motion that stays within the same record state posts zero heat, regardless of how many hidden configurations it passes through. Two horizons with identical record traces are therefore calorimetrically indistinguishable, no matter how much internal degeneracy each conceals. Clausius consistency then forces the entropy gap across the record to be exactly one unit, which yields the Bekenstein coefficient of one quarter when divided by the number of admissible sectors.

What the theorem does not claim is that the Clausius relation itself is derived from the framework. The relation δQ = T·ΔS is taken as input, a standard physics premise stated as the IsClausius predicate with temperature set to one in bit units. The framework's posting rule, that heat is the posted ledger flux with one bit per record flip, is likewise a definitional choice, not a theorem. What is proved is the conditional statement: if boundary heat is the posted flux and boundary entropy obeys Clausius, then horizon entropy must be the record cost, and the Bekenstein quarter follows.

/-- Clausius gap on map A (witnesses: config `1` is open, config `0` is closed). -/
theorem clausius_gap_A (E : Bool → ℤ) (hE : IsClausius mapA E) :
    E true - E false = 1 :=
  clausius_gap mapA E hE 1 0 (by decide) (by decide)

/-- Clausius gap on map B (same witnesses; its kernel is 1/15 instead of 8/8). -/
theorem clausius_gap_B (E : Bool → ℤ) (hE : IsClausius mapB E) :
    E true - E false = 1 :=
  clausius_gap mapB E hE 1 0 (by decide) (by decide)

/-- **δQ is a function of the boundary record trace alone.** The bulk-side heat sum equals
the trace-side heat of the projected record sequence, for every horizon map and every bulk
path. Everything the kernel does — its size, its structure, which fiber the path wanders
in — is calorimetrically invisible. -/
theorem pathHeat_factors {α : Type*} (f : α → Bool) (p : List α) :
    pathHeat f p = traceHeat (p.map f) := by
  induction p with
  | nil => rfl
  | cons c rest ih =>
    cases rest with
    | nil => rfl
    | cons c' rest' =>
      simp only [pathHeat, traceHeat, List.map_cons, stepHeat] at *
      omega

/-- **Kernel motion posts zero heat**, at any fiber size. A bulk path confined to a single
fiber (all points carry the same record) has zero total posted flux. -/
theorem pathHeat_kernel_zero {α : Type*} (f : α → Bool) (b : Bool) :
    ∀ p : List α, (∀ x ∈ p, f x = b) → pathHeat f p = 0 := by
  intro p
  induction p with
  | nil => intro _; rfl
  | cons c rest ih =>
    intro h
    cases rest with
    | nil => rfl
    | cons c' rest' =>
      have hc : f c = b := h c (by simp)
      have hc' : f c' = b := h c' (by simp)
      have hrest : ∀ x ∈ (c' :: rest'), f x = b := by
        intro x hx; exact h x (List.mem_cons_of_mem c hx)
      simp only [pathHeat]
      rw [stepHeat_eq_zero_of_kernel f (hc.trans hc'.symm), ih hrest]
      ring

/-- **The Bekenstein coefficient from Clausius.** Composing with the descent theorem: any
Clausius-consistent boundary entropy on the closure map forces the pixel-to-sector ratio
`1/4`. -/
theorem bekenstein_of_clausius (E : Bool → ℤ) (hE : IsClausius mapA E) :
    (((E true - E false).toNat : ℚ)) / (admissibleSectors.card : ℚ) = 1 / 4 :=
  bekenstein_coefficient_of_record_cost _ (clausius_implies_record_identification E hE)

/-- **The degeneracy reading fails Clausius on map A.** `microstateCost mapA` assigns `3`
to both records (both fibers have 8 microstates), so its record gap is `0`; but a record
flip posts `1` bit of heat. `δQ = 1 ≠ 0 = T·ΔS`. -/
theorem microstate_not_clausius_A :
    ¬ IsClausius mapA (fun b => (microstateCost mapA b : ℤ)) := by
  intro h
  have hgap := clausius_gap_A _ h
  have ht : microstateCost mapA true = 3 := by decide
  have hf : microstateCost mapA false = 3 := by decide
  rw [ht, hf] at hgap
  norm_num at hgap

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

What this page does not claim

The Clausius relation δQ = T·ΔS is derived from the framework; it is taken as a standard physics input. The posting rule that heat is the posted ledger flux is derived; it is a definitional choice within the framework. The theorem applies to horizons with more than two record states or to continuous state spaces.

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: