Holography Clausius Selector Clausius Implies Record Identification

/-- **Clausius derives the record-cost identification.** For any Clausius-consistent
boundary entropy on the RS closure map, the entropy span across the posted record —
`E true − E false = 1` bit — is exactly `recordCost closed`. So the plaquette multiplicity
demanded by Clausius satisfies `HorizonEntropyIsRecordCost`: the identification the fork
paper states as a premise is here a consequence of `δQ = T·ΔS` plus the ledger posting
rule. -/
theorem clausius_implies_record_identification (E : Bool → ℤ)
    (hE : IsClausius mapA E) :
    HorizonEntropyIsRecordCost (E true - E false).toNat := by
  have h := clausius_gap_A E hE
  unfold HorizonEntropyIsRecordCost
  rw [h]
  decide

/-- **Signed ledger heat of one bulk step** `c → c'` under horizon map `f`, in units of one
posted bit at unit temperature: `+1` when the record flips up, `-1` when it flips down, `0`
when the record is unchanged. This is the MODEL input: `δQ` at a horizon is the posted
ledger flux (a step posts iff it performs a boundary distinction; double-entry gives the
sign). Kernel motion — a step inside one fiber — posts nothing, by construction of the
ledger, not by choice of entropy functional. -/
def stepHeat {α : Type*} (f : α → Bool) (c c' : α) : ℤ :=
  (if f c' then 1 else 0) - (if f c then 1 else 0)

/-- **δ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 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 is not even map-consistent.** The two horizons are
calorimetrically identical (`matched_trace_equal_heat`), yet the microstate functional
assigns them different record gaps (`0` vs `−3`). An entropy that Clausius-integrates
against the same δQ record cannot depend on the map's kernel; this one does. -/
theorem microstate_gap_map_dependent :
    (microstateCost mapA true : ℤ) - (microstateCost mapA false : ℤ)
      ≠ (microstateCost mapB true : ℤ) - (microstateCost mapB false : ℤ) := by
  decide

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