Holography Clausius Selector

/-- Verify-target certificate handle (`#print axioms`-gated). -/
theorem clausiusSelectorCert : target_clausius_selector :=
  target_clausius_selector_holds

/-- **Matched record traces ⇒ equal heat, across DIFFERENT horizons.** Two bulk paths, one
under map A (fibers 8/8) and one under map B (fibers 1/15), with the same boundary record
trace, post identical total heat. The two horizons hide different bulk degeneracy and are
calorimetrically indistinguishable. -/
theorem matched_trace_equal_heat (p q : List FaceCfg)
    (h : p.map mapA = q.map mapB) : pathHeat mapA p = pathHeat mapB q := by
  rw [pathHeat_factors, pathHeat_factors, h]

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

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

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

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

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